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.

6 files changed, 22 insertions, 12 deletions

diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h
index 0a4c1b76f..916790d9c 100644
--- 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 8091eded5..362888558 100644
--- 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 d3c7c2c67..ac3c60ffe 100644
--- 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 f7f2531bb..581a29697 100644
--- 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 ed0cd0ac6..3d7ddd97b 100644
--- 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 382cb233f..cd0ab7976 100644
--- 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());
   }
 }