From 524c2d9f44a7c4297422dd1356fe3dc377166180 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 26 Jan 2021 19:24:58 -0600 Subject: Use standard conflict mechanism in quantifiers state (#5822) Work towards eliminating dependencies on quantifiers engine, this updates quantifiers module to use the standard SAT-context dependent flag in quantifiers state instead of the one in QuantifiersEngine. It also eliminates the use of a custom call to theoryEngineNeedsCheck. --- src/theory/quantifiers/term_database.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/theory/quantifiers/term_database.cpp') diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 12cdb1b8c..075ec6ceb 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -410,7 +410,7 @@ void TermDb::computeUfTerms( TNode f ) { { Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " << n << "!!!!" << std::endl; - if (!d_quantEngine->theoryEngineNeedsCheck()) + if (!d_qstate.getValuation().needCheck()) { Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl; @@ -419,7 +419,7 @@ void TermDb::computeUfTerms( TNode f ) { Trace("term-db-lemma") << " add lemma : " << lem << std::endl; } d_quantEngine->addLemma(lem); - d_quantEngine->setConflict(); + d_qstate.notifyInConflict(); d_consistent_ee = false; return; } @@ -1062,7 +1062,7 @@ bool TermDb::reset( Theory::Effort effort ){ Trace("term-db-lemma") << "Purify equality lemma: " << eq << std::endl; d_quantEngine->addLemma(eq); - d_quantEngine->setConflict(); + d_qstate.notifyInConflict(); d_consistent_ee = false; return false; } -- cgit v1.2.3