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.

5 files changed, 23 insertions, 13 deletions

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index effb5938c..b2c7bf704 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -280,7 +280,8 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {
   }
 }
 
-FullModelChecker::FullModelChecker(QuantifiersEngine* qe) : QModelBuilder(qe)
+FullModelChecker::FullModelChecker(QuantifiersEngine* qe, QuantifiersState& qs)
+    : QModelBuilder(qe, qs)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
@@ -593,7 +594,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
   Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;
   // register the quantifier
   registerQuantifiedFormula(f);
-  Assert(!d_qe->inConflict());
+  Assert(!d_qstate.isInConflict());
   // we do not do model-based quantifier instantiation if the option
   // disables it, or if the quantified formula has an unhandled type.
   if (!optUseModel() || !isHandled(f))
@@ -708,7 +709,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
       {
         Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
         d_addedLemmas++;
-        if (d_qe->inConflict() || options::fmfOneInstPerRound())
+        if (d_qstate.isInConflict() || options::fmfOneInstPerRound())
         {
           break;
         }
@@ -850,7 +851,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
         {
           Trace("fmc-exh-debug")  << " ...success.";
           addedLemmas++;
-          if( d_qe->inConflict() || options::fmfOneInstPerRound() ){
+          if (d_qstate.isInConflict() || options::fmfOneInstPerRound())
+          {
             break;
           }
         }else{
diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h
index 89a472948..76c131369 100644
--- a/src/theory/quantifiers/fmf/full_model_check.h
+++ b/src/theory/quantifiers/fmf/full_model_check.h
@@ -149,7 +149,7 @@ private:
   Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
 
  public:
-  FullModelChecker(QuantifiersEngine* qe);
+  FullModelChecker(QuantifiersEngine* qe, QuantifiersState& qs);
 
   void debugPrintCond(const char * tr, Node n, bool dispStar = false);
   void debugPrint(const char * tr, Node n, bool dispStar = false);
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index 4f34c3baa..cdb65f2b2 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -29,11 +29,12 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-QModelBuilder::QModelBuilder(QuantifiersEngine* qe)
+QModelBuilder::QModelBuilder(QuantifiersEngine* qe, QuantifiersState& qs)
     : TheoryEngineModelBuilder(qe->getTheoryEngine()),
       d_qe(qe),
       d_addedLemmas(0),
-      d_triedLemmas(0)
+      d_triedLemmas(0),
+      d_qstate(qs)
 {
 }
 
diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index 16e6f2a0b..82f9fa6c3 100644
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -20,6 +20,7 @@
 #include "expr/node.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/inst_match.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/theory_model_builder.h"
 
 namespace CVC4 {
@@ -40,7 +41,7 @@ class QModelBuilder : public TheoryEngineModelBuilder
   unsigned d_triedLemmas;
 
  public:
-  QModelBuilder(QuantifiersEngine* qe);
+  QModelBuilder(QuantifiersEngine* qe, QuantifiersState& qs);
 
   //do exhaustive instantiation  
   // 0 :  failed, but resorting to true exhaustive instantiation may work
@@ -56,6 +57,10 @@ class QModelBuilder : public TheoryEngineModelBuilder
   //statistics 
   unsigned getNumAddedLemmas() { return d_addedLemmas; }
   unsigned getNumTriedLemmas() { return d_triedLemmas; }
+
+ protected:
+  /** The quantifiers state object */
+  QuantifiersState& d_qstate;
 };
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 3849dc2c6..4d74c1697 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -77,7 +77,7 @@ void ModelEngine::check(Theory::Effort e, QEffort quant_e)
     doCheck = quant_e == QEFFORT_MODEL;
   }
   if( doCheck ){
-    Assert(!d_quantEngine->inConflict());
+    Assert(!d_qstate.isInConflict());
     int addedLemmas = 0;
 
     //the following will test that the model satisfies all asserted universal quantifiers by
@@ -217,7 +217,7 @@ int ModelEngine::checkModel(){
       //determine if we should check this quantifier
       if( d_quantEngine->getModel()->isQuantifierActive( q ) && d_quantEngine->hasOwnership( q, this ) ){
         exhaustiveInstantiate( q, e );
-        if (d_quantEngine->inConflict())
+        if (d_qstate.isInConflict())
         {
           break;
         }
@@ -228,12 +228,13 @@ int ModelEngine::checkModel(){
     if( d_addedLemmas>0 ){
       break;
     }else{
-      Assert(!d_quantEngine->inConflict());
+      Assert(!d_qstate.isInConflict());
     }
   }
 
   //print debug information
-  if( d_quantEngine->inConflict() ){
+  if (d_qstate.isInConflict())
+  {
     Trace("model-engine") << "Conflict, added lemmas = ";
   }else{
     Trace("model-engine") << "Added Lemmas = ";
@@ -293,7 +294,8 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
           if (inst->addInstantiation(f, m, true))
           {
             addedLemmas++;
-            if( d_quantEngine->inConflict() ){
+            if (d_qstate.isInConflict())
+            {
               break;
             }
           }else{