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.

1 files changed, 3 insertions, 3 deletions

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;
         }