Minor cleanup of quantifiers engine (#4994)

Eventually, QuanitifersEngine should not depend on TheoryEngine. This is a first step in this direction. It eliminates some uses of TheoryEngine and eliminates a unnecessary friend relationship between quantifiers::TermDb and TheoryEngine. Further refactoring will be done in future PRs.

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index a771309f0c424e3c8be6a8283b239c95ac7c97a6..ab1bb16b5dd7b5c47e6c740ccea1cec5becb01bc 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -205,7 +205,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
       dlds = itds->second.get();
     }
     // it is appended to the list of strategies
-    d_quantEngine->getTheoryEngine()->getDecisionManager()->registerStrategy(
+    d_quantEngine->getDecisionManager()->registerStrategy(
         DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE, dlds);
     return true;
   }else{

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index d0536a1eab759032edd76559b4e39b534aa41550..7cc087b667be9b5f29f0cf2f7d92dc2ae932b47e 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -557,7 +557,7 @@ void CegisUnifEnumDecisionStrategy::initialize(
   }
 
   // register this strategy
-  d_qe->getTheoryEngine()->getDecisionManager()->registerStrategy(
+  d_qe->getDecisionManager()->registerStrategy(
       DecisionManager::STRAT_QUANT_CEGIS_UNIF_NUM_ENUMS, this);
 
   // create single condition enumerator for each decision tree strategy

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 5b7ad2049e59fe3fa6cdc778de0ce0f8fc2b920d..52b24ac1a4f144f3a160a52404ce9e6b7d7738ac 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -235,7 +235,7 @@ void SynthConjecture::assign(Node q)
                                     d_feasible_guard,
                                     d_qe->getSatContext(),
                                     d_qe->getValuation()));
-  d_qe->getTheoryEngine()->getDecisionManager()->registerStrategy(
+  d_qe->getDecisionManager()->registerStrategy(
       DecisionManager::STRAT_QUANT_SYGUS_FEASIBLE, d_feasible_strategy.get());
   // this must be called, both to ensure that the feasible guard is
   // decided on with true polariy, but also to ensure that output channel
@@ -255,7 +255,7 @@ void SynthConjecture::assign(Node q)
   {
     d_stream_strategy.reset(new SygusStreamDecisionStrategy(
         d_qe->getSatContext(), d_qe->getValuation()));
-    d_qe->getTheoryEngine()->getDecisionManager()->registerStrategy(
+    d_qe->getDecisionManager()->registerStrategy(
         DecisionManager::STRAT_QUANT_SYGUS_STREAM_FEASIBLE,
         d_stream_strategy.get());
     d_current_stream_guard = d_stream_strategy->getLiteral(0);

diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 56fee3319a30dcd42ca154d53412b8e7c92cd430..ea5ff69e51ab5d5eb6efea06ccac1e22828a6f2b 100644 (file)
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -264,7 +264,7 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
                                     d_quantEngine->getValuation());
 
   d_dstrat[q].reset(ds);
-  d_quantEngine->getTheoryEngine()->getDecisionManager()->registerStrategy(
+  d_quantEngine->getDecisionManager()->registerStrategy(
       DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE, ds);
 
   /* Add counterexample lemma (lit => ~P[x_i/eval_i]) */

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 6e5dca4ef37880f989b143b84e02d64d883e2ac8..bac67c7b682d8d134f0ac06265f7ef3bb71b5c16 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1091,15 +1091,25 @@ bool TermDb::reset( Theory::Effort effort ){
       }
       ++eqcs_i;
     }
-    for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
-      Theory* theory = d_quantEngine->getTheoryEngine()->d_theoryTable[theoryId];
-      if (theory && d_quantEngine->getTheoryEngine()->d_logicInfo.isTheoryEnabled(theoryId)) {
-        context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
-        for (unsigned i = 0; it != it_end; ++ it, ++i) {
-          if ((*it).d_assertion.getKind() != INST_CLOSURE)
-          {
-            setHasTerm((*it).d_assertion);
-          }
+    TheoryEngine* te = d_quantEngine->getTheoryEngine();
+    const LogicInfo& logicInfo = te->getLogicInfo();
+    for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId)
+    {
+      if (!logicInfo.isTheoryEnabled(theoryId))
+      {
+        continue;
+      }
+      Theory* theory = te->theoryOf(theoryId);
+      Assert(theory != nullptr);
+      for (context::CDList<Assertion>::const_iterator
+               it = theory->facts_begin(),
+               it_end = theory->facts_end();
+           it != it_end;
+           ++it)
+      {
+        if ((*it).d_assertion.getKind() != INST_CLOSURE)
+        {
+          setHasTerm((*it).d_assertion);
         }
       }
     }

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index da60561ad6e20987e93bf1f3f7801b636a053d91..59082b55f8e475a1a46333aaac83aa9091d69817 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -172,39 +172,37 @@ class QuantifiersEnginePrivate
   }
 };
 
-QuantifiersEngine::QuantifiersEngine(context::Context* c,
-                                     context::UserContext* u,
-                                     TheoryEngine* te,
+QuantifiersEngine::QuantifiersEngine(TheoryEngine* te, DecisionManager& dm,
                                      ProofNodeManager* pnm)
     : d_te(te),
+      d_context(te->getSatContext()),
+      d_userContext(te->getUserContext()),
+      d_decManager(dm),
       d_masterEqualityEngine(nullptr),
-      d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)),
+      d_eq_query(
+          new quantifiers::EqualityQueryQuantifiersEngine(d_context, this)),
       d_tr_trie(new inst::TriggerTrie),
       d_model(nullptr),
       d_builder(nullptr),
       d_qepr(nullptr),
       d_term_util(new quantifiers::TermUtil(this)),
       d_term_canon(new expr::TermCanonize),
-      d_term_db(new quantifiers::TermDb(c, u, this)),
+      d_term_db(new quantifiers::TermDb(d_context, d_userContext, this)),
       d_sygus_tdb(nullptr),
       d_quant_attr(new quantifiers::QuantAttributes(this)),
-      d_instantiate(new quantifiers::Instantiate(this, u, pnm)),
-      d_skolemize(new quantifiers::Skolemize(this, u)),
+      d_instantiate(new quantifiers::Instantiate(this, d_userContext, pnm)),
+      d_skolemize(new quantifiers::Skolemize(this, d_userContext)),
       d_term_enum(new quantifiers::TermEnumeration),
-      d_conflict_c(c, false),
-      // d_quants(u),
-      d_quants_prereg(u),
-      d_quants_red(u),
-      d_lemmas_produced_c(u),
-      d_ierCounter_c(c),
-      // d_ierCounter(c),
-      // d_ierCounter_lc(c),
-      // d_ierCounterLastLc(c),
-      d_presolve(u, true),
-      d_presolve_in(u),
-      d_presolve_cache(u),
-      d_presolve_cache_wq(u),
-      d_presolve_cache_wic(u)
+      d_conflict_c(d_context, false),
+      d_quants_prereg(d_userContext),
+      d_quants_red(d_userContext),
+      d_lemmas_produced_c(d_userContext),
+      d_ierCounter_c(d_context),
+      d_presolve(d_userContext, true),
+      d_presolve_in(d_userContext),
+      d_presolve_cache(d_userContext),
+      d_presolve_cache_wq(d_userContext),
+      d_presolve_cache_wic(d_userContext)
 {
   // initialize the private utility
   d_private.reset(new QuantifiersEnginePrivate);
@@ -217,7 +215,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
 
   if (options::sygus() || options::sygusInst())
   {
-    d_sygus_tdb.reset(new quantifiers::TermDbSygus(c, this));
+    d_sygus_tdb.reset(new quantifiers::TermDbSygus(d_context, this));
   }
 
   d_util.push_back(d_instantiate.get());
@@ -245,7 +243,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
 
   bool needsBuilder = false;
-  d_private->initialize(this, c, d_modules, needsBuilder);
+  d_private->initialize(this, d_context, d_modules, needsBuilder);
 
   if (d_private->d_rel_dom.get())
   {
@@ -261,16 +259,18 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
     {
       Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
       d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
-          this, c, "FirstOrderModelFmc"));
-      d_builder.reset(new quantifiers::fmcheck::FullModelChecker(c, this));
+          this, d_context, "FirstOrderModelFmc"));
+      d_builder.reset(
+          new quantifiers::fmcheck::FullModelChecker(d_context, this));
     }else{
       Trace("quant-engine-debug") << "...make default model builder." << std::endl;
       d_model.reset(
-          new quantifiers::FirstOrderModel(this, c, "FirstOrderModel"));
-      d_builder.reset(new quantifiers::QModelBuilder(c, this));
+          new quantifiers::FirstOrderModel(this, d_context, "FirstOrderModel"));
+      d_builder.reset(new quantifiers::QModelBuilder(d_context, this));
     }
   }else{
-    d_model.reset(new quantifiers::FirstOrderModel(this, c, "FirstOrderModel"));
+    d_model.reset(
+        new quantifiers::FirstOrderModel(this, d_context, "FirstOrderModel"));
   }
 }
 
@@ -281,14 +281,18 @@ void QuantifiersEngine::setMasterEqualityEngine(eq::EqualityEngine* mee)
   d_masterEqualityEngine = mee;
 }
 
-context::Context* QuantifiersEngine::getSatContext()
+TheoryEngine* QuantifiersEngine::getTheoryEngine() const { return d_te; }
+
+DecisionManager* QuantifiersEngine::getDecisionManager()
 {
-  return d_te->theoryOf(THEORY_QUANTIFIERS)->getSatContext();
+  return &d_decManager;
 }
 
+context::Context* QuantifiersEngine::getSatContext() { return d_context; }
+
 context::UserContext* QuantifiersEngine::getUserContext()
 {
-  return d_te->theoryOf(THEORY_QUANTIFIERS)->getUserContext();
+  return d_userContext;
 }
 
 OutputChannel& QuantifiersEngine::getOutputChannel()

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index bd88034cbc228d2845405b4b236f12dbbeb922bb..72c0efce1f7fed584b02c9e749998dca6d536290 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -45,6 +45,7 @@ class TheoryEngine;
 
 namespace theory {
 
+class DecisionManager;
 class QuantifiersEnginePrivate;
 
 // TODO: organize this more/review this, github issue #1163
@@ -56,14 +57,14 @@ class QuantifiersEngine {
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 
  public:
-  QuantifiersEngine(context::Context* c,
-                    context::UserContext* u,
-                    TheoryEngine* te,
+  QuantifiersEngine(TheoryEngine* te, DecisionManager& dm,
                     ProofNodeManager* pnm);
   ~QuantifiersEngine();
   //---------------------- external interface
   /** get theory engine */
-  TheoryEngine* getTheoryEngine() const { return d_te; }
+  TheoryEngine* getTheoryEngine() const;
+  /** Get the decision manager */
+  DecisionManager* getDecisionManager();
   /** get default sat context for quantifiers engine */
   context::Context* getSatContext();
   /** get default sat context for quantifiers engine */
@@ -121,7 +122,7 @@ class QuantifiersEngine {
    * precendence.
    */
   std::map< Node, int > d_owner_priority;
-public:
+ public:
   /** get owner */
   QuantifiersModule * getOwner( Node q );
   /**
@@ -337,8 +338,14 @@ public:
   Statistics d_statistics;
 
  private:
-  /** reference to theory engine object */
+  /** Pointer to theory engine object */
   TheoryEngine* d_te;
+  /** The SAT context */
+  context::Context* d_context;
+  /** The user context */
+  context::UserContext* d_userContext;
+  /** Reference to the decision manager of the theory engine */
+  DecisionManager& d_decManager;
   /** Pointer to the master equality engine */
   eq::EqualityEngine* d_masterEqualityEngine;
   /** vector of utilities for quantifiers */

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 6a548e5b6607c20655e34ba8710a6f8e6f983eeb..ac06d266d67437ccd294d6626951e0760db1118c 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -165,8 +165,7 @@ void TheoryEngine::finishInit() {
   if (d_logicInfo.isQuantified())
   {
     // initialize the quantifiers engine
-    d_quantEngine =
-        new QuantifiersEngine(d_context, d_userContext, this, d_pnm);
+    d_quantEngine = new QuantifiersEngine(this, *d_decManager.get(), d_pnm);
   }
   // initialize the theory combination manager, which decides and allocates the
   // equality engines to use for all theories.

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 167bd6d75ed115be4dbda97f85eaca313b24324c..30b5d9fbbfc2a58b27fa0745a1dc13d90bca9181 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -94,10 +94,6 @@ namespace eq {
 class EqualityEngine;
 }  // namespace eq
 
-namespace quantifiers {
-class TermDb;
-}
-
 class EntailmentCheckParameters;
 class EntailmentCheckSideEffects;
 }/* CVC4::theory namespace */
@@ -115,7 +111,6 @@ class TheoryEngine {
   /** Shared terms database can use the internals notify the theories */
   friend class SharedTermsDatabase;
   friend class theory::CombinationEngine;
-  friend class theory::quantifiers::TermDb;
   friend class theory::EngineOutputChannel;
   friend class theory::CombinationEngine;
 
@@ -373,16 +368,12 @@ class TheoryEngine {
   /**
    * Get a pointer to the underlying sat context.
    */
-  inline context::Context* getSatContext() const {
-    return d_context;
-  }
+  context::Context* getSatContext() const { return d_context; }
 
   /**
    * Get a pointer to the underlying user context.
    */
-  inline context::Context* getUserContext() const {
-    return d_userContext;
-  }
+  context::UserContext* getUserContext() const { return d_userContext; }
 
   /**
    * Get a pointer to the underlying quantifiers engine.