1 files changed, 19 insertions, 29 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index fa7e50e1c..83aafe33a 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -51,7 +51,6 @@ QuantifiersEngine::QuantifiersEngine(
       d_instantiate(new quantifiers::Instantiate(this, qstate, pnm)),
       d_skolemize(new quantifiers::Skolemize(this, qstate, pnm)),
       d_term_enum(new quantifiers::TermEnumeration),
-      d_conflict_c(qstate.getSatContext(), false),
       d_quants_prereg(qstate.getUserContext()),
       d_quants_red(qstate.getUserContext()),
       d_lemmas_produced_c(qstate.getUserContext()),
@@ -77,7 +76,6 @@ QuantifiersEngine::QuantifiersEngine(
   d_util.push_back(d_instantiate.get());
 
   d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
-  d_conflict = false;
   d_hasAddedLemma = false;
   //don't add true lemma
   d_lemmas_produced_c[d_term_util->d_true] = true;
@@ -107,12 +105,12 @@ QuantifiersEngine::QuantifiersEngine(
       Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
       d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
           this, qstate, "FirstOrderModelFmc"));
-      d_builder.reset(new quantifiers::fmcheck::FullModelChecker(this));
+      d_builder.reset(new quantifiers::fmcheck::FullModelChecker(this, qstate));
     }else{
       Trace("quant-engine-debug") << "...make default model builder." << std::endl;
       d_model.reset(
           new quantifiers::FirstOrderModel(this, qstate, "FirstOrderModel"));
-      d_builder.reset(new quantifiers::QModelBuilder(this));
+      d_builder.reset(new quantifiers::QModelBuilder(this, qstate));
     }
   }else{
     d_model.reset(
@@ -150,10 +148,7 @@ OutputChannel& QuantifiersEngine::getOutputChannel()
   return d_te->theoryOf(THEORY_QUANTIFIERS)->getOutputChannel();
 }
 /** get default valuation for the quantifiers engine */
-Valuation& QuantifiersEngine::getValuation()
-{
-  return d_te->theoryOf(THEORY_QUANTIFIERS)->getValuation();
-}
+Valuation& QuantifiersEngine::getValuation() { return d_qstate.getValuation(); }
 
 const LogicInfo& QuantifiersEngine::getLogicInfo() const
 {
@@ -372,7 +367,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
     Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl;
     return;
   }
-  if (d_conflict_c.get())
+  if (d_qstate.isInConflict())
   {
     if (e < Theory::EFFORT_LAST_CALL)
     {
@@ -417,7 +412,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }
   }
 
-  d_conflict = false;
   d_hasAddedLemma = false;
   bool setIncomplete = false;
 
@@ -448,11 +442,11 @@ void QuantifiersEngine::check( Theory::Effort e ){
         Trace("quant-engine-debug") << "  lemmas waiting = " << d_lemmas_waiting.size() << std::endl;
       }
       Trace("quant-engine-debug")
-          << "  Theory engine finished : " << !theoryEngineNeedsCheck()
-          << std::endl;
+          << "  Theory engine finished : "
+          << !d_qstate.getValuation().needCheck() << std::endl;
       Trace("quant-engine-debug") << "  Needs model effort : " << needsModelE << std::endl;
       Trace("quant-engine-debug")
-          << "  In conflict : " << d_conflict << std::endl;
+          << "  In conflict : " << d_qstate.isInConflict() << std::endl;
     }
     if( Trace.isOn("quant-engine-ee-pre") ){
       Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl;
@@ -538,7 +532,8 @@ void QuantifiersEngine::check( Theory::Effort e ){
                                       << " at effort " << quant_e << "..."
                                       << std::endl;
           mdl->check(e, quant_e);
-          if( d_conflict ){
+          if (d_qstate.isInConflict())
+          {
             Trace("quant-engine-debug") << "...conflict!" << std::endl;
             break;
           }
@@ -550,7 +545,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
       if( d_hasAddedLemma ){
         break;
       }else{
-        Assert(!d_conflict);
+        Assert(!d_qstate.isInConflict());
         if (quant_e == QuantifiersModule::QEFFORT_CONFLICT)
         {
           if( e==Theory::EFFORT_FULL ){
@@ -578,7 +573,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
                 setIncomplete = true;
               }
             }
-            if (d_conflict_c.get())
+            if (d_qstate.isInConflict())
             {
               // we reported a conflicting lemma, should return
               setIncomplete = true;
@@ -900,20 +895,13 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
 void QuantifiersEngine::markRelevant( Node q ) {
   d_model->markRelevant( q );
 }
+
 bool QuantifiersEngine::hasAddedLemma() const
 {
   return !d_lemmas_waiting.empty() || d_hasAddedLemma;
 }
-bool QuantifiersEngine::theoryEngineNeedsCheck() const
-{
-  return d_te->needCheck();
-}
 
-void QuantifiersEngine::setConflict()
-{
-  d_conflict = true;
-  d_conflict_c = true;
-}
+bool QuantifiersEngine::inConflict() const { return d_qstate.isInConflict(); }
 
 bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
   Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl;
@@ -925,7 +913,8 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
   }
   else if (options::instWhenMode() == options::InstWhenMode::FULL_DELAY)
   {
-    performCheck = (e >= Theory::EFFORT_FULL) && !theoryEngineNeedsCheck();
+    performCheck =
+        (e >= Theory::EFFORT_FULL) && !d_qstate.getValuation().needCheck();
   }
   else if (options::instWhenMode() == options::InstWhenMode::FULL_LAST_CALL)
   {
@@ -934,9 +923,10 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
   else if (options::instWhenMode()
            == options::InstWhenMode::FULL_DELAY_LAST_CALL)
   {
-    performCheck = ((e == Theory::EFFORT_FULL && !theoryEngineNeedsCheck()
-                     && d_ierCounter % d_inst_when_phase != 0)
-                    || e == Theory::EFFORT_LAST_CALL);
+    performCheck =
+        ((e == Theory::EFFORT_FULL && !d_qstate.getValuation().needCheck()
+          && d_ierCounter % d_inst_when_phase != 0)
+         || e == Theory::EFFORT_LAST_CALL);
   }
   else if (options::instWhenMode() == options::InstWhenMode::LAST_CALL)
   {