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.

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 980bc1d4b0b759988d8abc44fbcc3d16f93718e7..118e7023c12afb377ba81239a96c2adbdf820b8d 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -254,7 +254,7 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e)
 {
   if (quant_e == QEFFORT_STANDARD)
   {
-    Assert(!d_quantEngine->inConflict());
+    Assert(!d_qstate.isInConflict());
     double clSet = 0;
     if( Trace.isOn("cegqi-engine") ){
       clSet = double(clock())/double(CLOCKS_PER_SEC);
@@ -269,12 +269,14 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e)
         Node q = it->first;
         Trace("cegqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl;
         process(q, e, ee);
-        if (d_quantEngine->inConflict())
+        if (d_qstate.isInConflict())
         {
           break;
         }
       }
-      if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
+      if (d_qstate.isInConflict()
+          || d_quantEngine->getNumLemmasWaiting() > lastWaiting)
+      {
         break;
       }
     }

diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h
index 0a4c1b76fc09bb36b157faafb80afd3ec87e2411..916790d9c9209c41f64de8050efab5c7bf405cf8 100644 (file)
--- a/src/theory/quantifiers/ematching/inst_strategy.h
+++ b/src/theory/quantifiers/ematching/inst_strategy.h
@@ -28,6 +28,8 @@ class QuantifiersEngine;
 
 namespace quantifiers {
 
+class QuantifiersState;
+
 /** A status response to process */
 enum class InstStrategyStatus
 {
@@ -43,7 +45,10 @@ enum class InstStrategyStatus
 class InstStrategy
 {
  public:
-  InstStrategy(QuantifiersEngine* qe) : d_quantEngine(qe) {}
+  InstStrategy(QuantifiersEngine* qe, QuantifiersState& qs)
+      : d_quantEngine(qe), d_qstate(qs)
+  {
+  }
   virtual ~InstStrategy() {}
   /** presolve */
   virtual void presolve() {}
@@ -57,6 +62,8 @@ class InstStrategy
  protected:
   /** reference to the instantiation engine */
   QuantifiersEngine* d_quantEngine;
+  /** The quantifiers state object */
+  QuantifiersState& d_qstate;
 }; /* class InstStrategy */
 
 }  // namespace quantifiers

diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 8091eded55cdac0019a7a44a7b52bd511f247b76..36288855805fff70d17a6263def254a78a1f4b59 100644 (file)
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -58,8 +58,9 @@ struct sortTriggers {
 };
 
 InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(QuantifiersEngine* qe,
+                                                         QuantifiersState& qs,
                                                          QuantRelevance* qr)
-    : InstStrategy(qe), d_quant_rel(qr)
+    : InstStrategy(qe, qs), d_quant_rel(qr)
 {
   //how to select trigger terms
   d_tr_strategy = options::triggerSelMode();
@@ -202,13 +203,12 @@ InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f,
       {
         d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
       }
-      if (d_quantEngine->inConflict())
+      if (d_qstate.isInConflict())
       {
         break;
       }
     }
-    if (d_quantEngine->inConflict()
-        || (hasInst && options::multiTriggerPriority()))
+    if (d_qstate.isInConflict() || (hasInst && options::multiTriggerPriority()))
     {
       break;
     }

diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
index d3c7c2c67421584c0083f14d20829162de3cb60c..ac3c60ffe62ba2ce84e53bc7ef55b51235965a51 100644 (file)
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
@@ -85,7 +85,9 @@ class InstStrategyAutoGenTriggers : public InstStrategy
   std::map<Node, bool> d_hasUserPatterns;
 
  public:
-  InstStrategyAutoGenTriggers(QuantifiersEngine* qe, QuantRelevance* qr);
+  InstStrategyAutoGenTriggers(QuantifiersEngine* qe,
+                              QuantifiersState& qs,
+                              QuantRelevance* qr);
   ~InstStrategyAutoGenTriggers() {}
 
   /** get auto-generated trigger */

diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
index f7f2531bb6e59ae64bd05dffc10488112a1715a5..581a2969720ad5d639a022dcce41bf0e64c1f993 100644 (file)
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
@@ -23,8 +23,9 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-InstStrategyUserPatterns::InstStrategyUserPatterns(QuantifiersEngine* ie)
-    : InstStrategy(ie)
+InstStrategyUserPatterns::InstStrategyUserPatterns(QuantifiersEngine* ie,
+                                                   QuantifiersState& qs)
+    : InstStrategy(ie, qs)
 {
 }
 InstStrategyUserPatterns::~InstStrategyUserPatterns() {}
@@ -128,7 +129,7 @@ InstStrategyStatus InstStrategyUserPatterns::process(Node q,
     {
       d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
     }
-    if (d_quantEngine->inConflict())
+    if (d_qstate.isInConflict())
     {
       // we are already in conflict
       break;

diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
index ed0cd0ac6f0e9b9ddc5cc7d8ab7bccf07d2e1ff5..3d7ddd97ba0f77bcb286c5449e4d60a1dee93f74 100644 (file)
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
@@ -33,7 +33,7 @@ namespace quantifiers {
 class InstStrategyUserPatterns : public InstStrategy
 {
  public:
-  InstStrategyUserPatterns(QuantifiersEngine* qe);
+  InstStrategyUserPatterns(QuantifiersEngine* qe, QuantifiersState& qs);
   ~InstStrategyUserPatterns();
   /** add pattern */
   void addUserPattern(Node q, Node pat);

diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 382cb233f462f1eba75c7b809c1808d970764ab8..cd0ab7976265ab91aa73b0f542ced6b382709563 100644 (file)
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -53,13 +53,13 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe,
     // user-provided patterns
     if (options::userPatternsQuant() != options::UserPatMode::IGNORE)
     {
-      d_isup.reset(new InstStrategyUserPatterns(d_quantEngine));
+      d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs));
       d_instStrategies.push_back(d_isup.get());
     }
 
     // auto-generated patterns
     d_i_ag.reset(
-        new InstStrategyAutoGenTriggers(d_quantEngine, d_quant_rel.get()));
+        new InstStrategyAutoGenTriggers(d_quantEngine, qs, d_quant_rel.get()));
     d_instStrategies.push_back(d_i_ag.get());
   }
 }

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index effb5938c34c638497c9316457dfe53c652974c6..b2c7bf704cc55a87b4553ea29552d9b8058d19ee 100644 (file)
--- 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 89a4729485285800c19bb24c272f14f7cd23ed2e..76c13136913f2cfab0a11c5cc46b3920941bd593 100644 (file)
--- 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 4f34c3baa2b815fbc2c9b04fd9bb82a98be1d8da..cdb65f2b2f1ee4b58eda13ded414c22b2721d96f 100644 (file)
--- 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 16e6f2a0bfa0f197c668fa4f35be05611a8df5c5..82f9fa6c33f9a4074284b2c7bf04b52f1434f143 100644 (file)
--- 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 3849dc2c657a7f621e51528d5cba27f6fe516bdf..4d74c16974f7cd7a1d34e17a2aaa503f501399c5 100644 (file)
--- 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{

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index 1dff5e00029f4628cd8b89e3d6172ccf1f342002..d1c09a9e8b32ef7a00259272757419d035cb4139 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -80,7 +80,7 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e)
     }
     if (options::fullSaturateQuant() && !doCheck)
     {
-      if (!d_quantEngine->theoryEngineNeedsCheck())
+      if (!d_qstate.getValuation().needCheck())
       {
         doCheck = quant_e == QEFFORT_LAST_CALL;
         fullEffort = true;
@@ -91,7 +91,7 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e)
   {
     return;
   }
-  Assert(!d_quantEngine->inConflict());
+  Assert(!d_qstate.isInConflict());
   double clSet = 0;
   if (Trace.isOn("fs-engine"))
   {
@@ -145,13 +145,13 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e)
             // added lemma
             addedLemmas++;
           }
-          if (d_quantEngine->inConflict())
+          if (d_qstate.isInConflict())
           {
             break;
           }
         }
       }
-      if (d_quantEngine->inConflict()
+      if (d_qstate.isInConflict()
           || (addedLemmas > 0 && options::fullSaturateStratify()))
       {
         // we break if we are in conflict, or if we added any lemma at this
@@ -331,7 +331,7 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd)
           {
             index--;
           }
-          if (d_quantEngine->inConflict())
+          if (d_qstate.isInConflict())
           {
             // could be conflicting for an internal reason (such as term
             // indices computed in above calls)

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index b123c3e15930bc1ec3fb3ab4f1669a0006d06e19..ed02c6b3294dee6b360350e1eebde694672ad541 100644 (file)
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -105,7 +105,7 @@ bool Instantiate::addInstantiation(
 {
   // For resource-limiting (also does a time check).
   d_qe->getOutputChannel().safePoint(ResourceManager::Resource::QuantifierStep);
-  Assert(!d_qe->inConflict());
+  Assert(!d_qstate.isInConflict());
   Assert(terms.size() == q[0].getNumChildren());
   Assert(d_term_db != nullptr);
   Assert(d_term_util != nullptr);

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 822c9b3233b3d71864d583323d57aaa969c3a3c2..b214f907ae9cc242de209b95f3d44cdeb6f8956e 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -637,7 +637,7 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p,
     }
   }
   // spurious if quantifiers engine is in conflict
-  return p->d_quantEngine->inConflict();
+  return p->d_qstate.isInConflict();
 }
 
 bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) {
@@ -1203,27 +1203,27 @@ bool MatchGen::reset_round(QuantConflictFind* p)
     //}
     // modified
     TermDb* tdb = p->getTermDatabase();
-    QuantifiersEngine* qe = p->getQuantifiersEngine();
+    QuantifiersState& qs = p->getState();
     for (unsigned i = 0; i < 2; i++)
     {
       if (tdb->isEntailed(d_n, i == 0))
       {
         d_ground_eval[0] = i==0 ? p->d_true : p->d_false;
       }
-      if (qe->inConflict())
+      if (qs.isInConflict())
       {
         return false;
       }
     }
   }else if( d_type==typ_eq ){
     TermDb* tdb = p->getTermDatabase();
-    QuantifiersEngine* qe = p->getQuantifiersEngine();
+    QuantifiersState& qs = p->getState();
     for (unsigned i = 0, size = d_n.getNumChildren(); i < size; i++)
     {
       if (!expr::hasBoundVar(d_n[i]))
       {
         TNode t = tdb->getEntailedTerm(d_n[i]);
-        if (qe->inConflict())
+        if (qs.isInConflict())
         {
           return false;
         }
@@ -2027,7 +2027,7 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
       {
         // check this quantified formula
         checkQuantifiedFormula(q, isConflict, addedLemmas);
-        if (d_conflict || d_quantEngine->inConflict())
+        if (d_conflict || d_qstate.isInConflict())
         {
           break;
         }
@@ -2036,7 +2036,7 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
     // We are done if we added a lemma, or discovered a conflict in another
     // way. An example of the latter case is when two disequal congruent terms
     // are discovered during term indexing.
-    if (addedLemmas > 0 || d_quantEngine->inConflict())
+    if (addedLemmas > 0 || d_qstate.isInConflict())
     {
       break;
     }
@@ -2100,7 +2100,7 @@ void QuantConflictFind::checkQuantifiedFormula(Node q,
   Instantiate* qinst = d_quantEngine->getInstantiate();
   while (qi->getNextMatch(this))
   {
-    if (d_quantEngine->inConflict())
+    if (d_qstate.isInConflict())
     {
       Trace("qcf-check") << "   ... Quantifiers engine discovered conflict, ";
       Trace("qcf-check") << "probably related to disequal congruent terms in "

diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index dcf38eccb1da177c49496635208718273b591ffb..b561b589bd7aa8f12e271eb4469f14b822bed845 100644 (file)
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -71,6 +71,17 @@ quantifiers::TermUtil* QuantifiersModule::getTermUtil() const
   return d_quantEngine->getTermUtil();
 }
 
+quantifiers::QuantifiersState& QuantifiersModule::getState()
+{
+  return d_qstate;
+}
+
+quantifiers::QuantifiersInferenceManager&
+QuantifiersModule::getInferenceManager()
+{
+  return d_qim;
+}
+
 QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){
   initialize( n, computeEq );
 }

diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 5040bd2323184b085ac7b9b45bef16e919859623..16791b130ef8aa7a05c11e5f68d5dab935c8c24d 100644 (file)
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -156,6 +156,10 @@ class QuantifiersModule {
   quantifiers::TermDb* getTermDatabase() const;
   /** get currently used term utility object */
   quantifiers::TermUtil* getTermUtil() const;
+  /** get the quantifiers state */
+  quantifiers::QuantifiersState& getState();
+  /** get the quantifiers inference manager */
+  quantifiers::QuantifiersInferenceManager& getInferenceManager();
   //----------------------------end general queries
  protected:
   /** pointer to the quantifiers engine that owns this module */

diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index fc1bda5794ac341583a606e9889c6952f4a46906..43051eb99c3deb25755cde1b754e9400c47348fd 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -136,8 +136,7 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e)
     activeCheckConj.clear();
     activeCheckConj = acnext;
     acnext.clear();
-  } while (!activeCheckConj.empty()
-           && !d_quantEngine->theoryEngineNeedsCheck());
+  } while (!activeCheckConj.empty() && !d_qstate.getValuation().needCheck());
   Trace("sygus-engine")
       << "Finished Counterexample Guided Instantiation engine." << std::endl;
 }

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 12cdb1b8c8193ba2282c467f03a8f77e0e1c8c61..075ec6ceb1ae2936e39c31044d67dc4f34f0150a 100644 (file)
--- 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;
         }

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index fa7e50e1cecfd25e80f518ca720310754ded2a83..83aafe33a778014a62c285334aaea2a5774f6883 100644 (file)
--- 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)
   {

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 5a371ff09e0c61db58c1d2954027dd54c4b03633..2790ad11a7e9390766da14e8adbee754e01b4467 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -234,17 +234,8 @@ public:
  void markRelevant(Node q);
  /** has added lemma */
  bool hasAddedLemma() const;
- /** theory engine needs check
-  *
-  * This is true if the theory engine has more constraints to process. When
-  * it is false, we are tentatively going to terminate solving with
-  * sat/unknown. For details, see TheoryEngine::needCheck.
-  */
- bool theoryEngineNeedsCheck() const;
  /** is in conflict */
- bool inConflict() { return d_conflict; }
- /** set conflict */
- void setConflict();
+ bool inConflict() const;
  /** get current q effort */
  QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; }
  /** get number of waiting lemmas */
@@ -384,9 +375,6 @@ public:
   //------------- temporary information during check
   /** current effort level */
   QuantifiersModule::QEffort d_curr_effort_level;
-  /** are we in conflict */
-  bool d_conflict;
-  context::CDO<bool> d_conflict_c;
   /** has added lemma this round */
   bool d_hasAddedLemma;
   //------------- end temporary information during check

diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp
index 95a96808e5c8121d4bb333060bf2ca7f10a6361b..47528e1a6c7810b779efb80ee5b928d14cbcee9d 100644 (file)
--- a/src/theory/theory_state.cpp
+++ b/src/theory/theory_state.cpp
@@ -137,5 +137,7 @@ bool TheoryState::hasSatValue(TNode n, bool& value) const
   return d_valuation.hasSatValue(n, value);
 }
 
+Valuation& TheoryState::getValuation() { return d_valuation; }
+
 }  // namespace theory
 }  // namespace CVC4

diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h
index 187d586a1d2d7b49790ffa6ff81d35e5afc4cc19..7c2a044bf8a2017e4f8dd3ec3412680499711da5 100644 (file)
--- a/src/theory/theory_state.h
+++ b/src/theory/theory_state.h
@@ -83,6 +83,9 @@ class TheoryState
   /** Returns true if n has a current SAT assignment and stores it in value. */
   virtual bool hasSatValue(TNode n, bool& value) const;
 
+  /** Get the underlying valuation class */
+  Valuation& getValuation();
+
  protected:
   /** Pointer to the SAT context object used by the theory. */
   context::Context* d_context;