Add interface to TheoryState for sort inference and facts (#5967)

This eliminates the need for direct references to TheoryEngine from quantifiers and UF+cardinality.

This PR also eliminates an unnecessary reference to TheoryEngine in TheoryModelBuilder and breaks a few more dependencies in quantifiers modules.

15 files changed, 85 insertions, 57 deletions

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 8b60152a8..0d1a51a30 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -181,8 +181,11 @@ void SolvedForm::pop_back(Node pv, Node n, TermProperties& pv_prop)
   d_theta.pop_back();
 }
 
-CegInstantiator::CegInstantiator(Node q, InstStrategyCegqi* parent)
+CegInstantiator::CegInstantiator(Node q,
+                                 QuantifiersState& qs,
+                                 InstStrategyCegqi* parent)
     : d_quant(q),
+      d_qstate(qs),
       d_parent(parent),
       d_qe(parent->getQuantifiersEngine()),
       d_is_nested_quant(false),
@@ -1337,22 +1340,37 @@ void CegInstantiator::processAssertions() {
     }
   }
   //collect assertions for relevant theories
-  for( unsigned i=0; i<d_tids.size(); i++ ){
-    TheoryId tid = d_tids[i];
-    Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid );
-    if( theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid) ){
-      Trace("cegqi-proc") << "Collect assertions from theory " << tid << std::endl;
-      d_curr_asserts[tid].clear();
-      //collect all assertions from theory
-      for( context::CDList<Assertion>::const_iterator it = theory->facts_begin(); it != theory->facts_end(); ++ it) {
-        Node lit = (*it).d_assertion;
-        Node atom = lit.getKind()==NOT ? lit[0] : lit;
-        if( d_is_nested_quant || std::find( d_ce_atoms.begin(), d_ce_atoms.end(), atom )!=d_ce_atoms.end() ){
-          d_curr_asserts[tid].push_back( lit );
-          Trace("cegqi-proc-debug") << "...add : " << lit << std::endl;
-        }else{
-          Trace("cegqi-proc") << "...do not consider literal " << tid << " : " << lit << " since it is not part of CE body." << std::endl;
-        }
+  const LogicInfo& logicInfo = d_qstate.getLogicInfo();
+  for (TheoryId tid : d_tids)
+  {
+    if (!logicInfo.isTheoryEnabled(tid))
+    {
+      continue;
+    }
+    Trace("cegqi-proc") << "Collect assertions from theory " << tid
+                        << std::endl;
+    d_curr_asserts[tid].clear();
+    // collect all assertions from theory
+    for (context::CDList<Assertion>::const_iterator
+             it = d_qstate.factsBegin(tid),
+             itEnd = d_qstate.factsEnd(tid);
+         it != itEnd;
+         ++it)
+    {
+      Node lit = (*it).d_assertion;
+      Node atom = lit.getKind() == NOT ? lit[0] : lit;
+      if (d_is_nested_quant
+          || std::find(d_ce_atoms.begin(), d_ce_atoms.end(), atom)
+                 != d_ce_atoms.end())
+      {
+        d_curr_asserts[tid].push_back(lit);
+        Trace("cegqi-proc-debug") << "...add : " << lit << std::endl;
+      }
+      else
+      {
+        Trace("cegqi-proc")
+            << "...do not consider literal " << tid << " : " << lit
+            << " since it is not part of CE body." << std::endl;
       }
     }
   }
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h
index b8a337cdb..85e14d579 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h
@@ -33,6 +33,7 @@ namespace quantifiers {
 class Instantiator;
 class InstantiatorPreprocess;
 class InstStrategyCegqi;
+class QuantifiersState;
 
 /**
  * Descriptions of the types of constraints that a term was solved for in.
@@ -209,7 +210,7 @@ class CegInstantiator {
    * The instantiator will be constructing instantiations for quantified formula
    * q, parent is the owner of this object.
    */
-  CegInstantiator(Node q, InstStrategyCegqi* parent);
+  CegInstantiator(Node q, QuantifiersState& qs, InstStrategyCegqi* parent);
   virtual ~CegInstantiator();
   /** check
    * This adds instantiations based on the state of d_vars in current context
@@ -353,6 +354,8 @@ class CegInstantiator {
  private:
   /** The quantified formula of this instantiator */
   Node d_quant;
+  /** Reference to the quantifiers state */
+  QuantifiersState& d_qstate;
   /** The parent of this instantiator */
   InstStrategyCegqi* d_parent;
   /** quantified formula associated with this instantiator */
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index a79fbb9b6..dff10ddf1 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -503,7 +503,7 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
   std::map<Node, std::unique_ptr<CegInstantiator>>::iterator it =
       d_cinst.find(q);
   if( it==d_cinst.end() ){
-    d_cinst[q].reset(new CegInstantiator(q, this));
+    d_cinst[q].reset(new CegInstantiator(q, d_qstate, this));
     return d_cinst[q].get();
   }
   return it->second.get();
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index b9a3e1f34..700ae2c64 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -87,8 +87,9 @@ Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma()
 BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe,
                                  QuantifiersState& qs,
                                  QuantifiersInferenceManager& qim,
-                                 QuantifiersRegistry& qr)
-    : QuantifiersModule(qs, qim, qr, qe)
+                                 QuantifiersRegistry& qr,
+                                 DecisionManager* dm)
+    : QuantifiersModule(qs, qim, qr, qe), d_dm(dm)
 {
 }
 
@@ -500,9 +501,7 @@ void BoundedIntegers::checkOwnership(Node f)
                                               d_qstate.getUserContext(),
                                               d_qstate.getValuation(),
                                               isProxy));
-            d_quantEngine->getTheoryEngine()
-                ->getDecisionManager()
-                ->registerStrategy(DecisionManager::STRAT_QUANT_BOUND_INT_SIZE,
+            d_dm->registerStrategy(DecisionManager::STRAT_QUANT_BOUND_INT_SIZE,
                                    d_rms[r].get());
           }
         }
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index dce515d0d..9d4a414e9 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -28,6 +28,7 @@ namespace CVC4 {
 namespace theory {
 
 class RepSetIterator;
+class DecisionManager;
 
 /**
  * Attribute set to 1 for literals that comprise the bounds of a quantified
@@ -164,7 +165,8 @@ private:
   BoundedIntegers(QuantifiersEngine* qe,
                   QuantifiersState& qs,
                   QuantifiersInferenceManager& qim,
-                  QuantifiersRegistry& qr);
+                  QuantifiersRegistry& qr,
+                  DecisionManager* dm);
   virtual ~BoundedIntegers();
 
   void presolve() override;
@@ -231,6 +233,8 @@ private:
   Node matchBoundVar( Node v, Node t, Node e );
   
   bool getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi );
+  /** Pointer to the decision manager */
+  DecisionManager* d_dm;
 };
 
 }
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index cdb65f2b2..13bdcf963 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -30,7 +30,7 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
 QModelBuilder::QModelBuilder(QuantifiersEngine* qe, QuantifiersState& qs)
-    : TheoryEngineModelBuilder(qe->getTheoryEngine()),
+    : TheoryEngineModelBuilder(),
       d_qe(qe),
       d_addedLemmas(0),
       d_triedLemmas(0),
diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index 74f553800..8142165aa 100644
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -41,6 +41,7 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe,
                                     QuantifiersState& qs,
                                     QuantifiersInferenceManager& qim,
                                     QuantifiersRegistry& qr,
+                                    DecisionManager* dm,
                                     std::vector<QuantifiersModule*>& modules)
 {
   // add quantifiers modules
@@ -73,7 +74,7 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe,
   // finite model finding
   if (options::fmfBound())
   {
-    d_bint.reset(new BoundedIntegers(qe, qs, qim, qr));
+    d_bint.reset(new BoundedIntegers(qe, qs, qim, qr, dm));
     modules.push_back(d_bint.get());
   }
   if (options::finiteModelFind() || options::fmfBound())
diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h
index 08266c8fe..c9960a1bc 100644
--- a/src/theory/quantifiers/quantifiers_modules.h
+++ b/src/theory/quantifiers/quantifiers_modules.h
@@ -32,6 +32,7 @@ namespace CVC4 {
 namespace theory {
   
 class QuantifiersEngine;
+class DecisionManager;
 
 namespace quantifiers {
 
@@ -55,6 +56,7 @@ class QuantifiersModules
                   QuantifiersState& qs,
                   QuantifiersInferenceManager& qim,
                   QuantifiersRegistry& qr,
+                  DecisionManager* dm,
                   std::vector<QuantifiersModule*>& modules);
 
  private:
diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp
index 07bd97918..0bcca266e 100644
--- a/src/theory/quantifiers/quantifiers_state.cpp
+++ b/src/theory/quantifiers/quantifiers_state.cpp
@@ -22,8 +22,9 @@ namespace quantifiers {
 
 QuantifiersState::QuantifiersState(context::Context* c,
                                    context::UserContext* u,
-                                   Valuation val)
-    : TheoryState(c, u, val), d_ierCounterc(c)
+                                   Valuation val,
+                                   const LogicInfo& logicInfo)
+    : TheoryState(c, u, val), d_ierCounterc(c), d_logicInfo(logicInfo)
 {
   // allow theory combination to go first, once initially
   d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
@@ -152,6 +153,8 @@ void QuantifiersState::debugPrintEqualityEngine(const char* c) const
   }
 }
 
+const LogicInfo& QuantifiersState::getLogicInfo() const { return d_logicInfo; }
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/quantifiers_state.h b/src/theory/quantifiers/quantifiers_state.h
index d45938f98..edebec156 100644
--- a/src/theory/quantifiers/quantifiers_state.h
+++ b/src/theory/quantifiers/quantifiers_state.h
@@ -30,7 +30,10 @@ namespace quantifiers {
 class QuantifiersState : public TheoryState
 {
  public:
-  QuantifiersState(context::Context* c, context::UserContext* u, Valuation val);
+  QuantifiersState(context::Context* c,
+                   context::UserContext* u,
+                   Valuation val,
+                   const LogicInfo& logicInfo);
   ~QuantifiersState() {}
   /**
    * Increment the instantiation counters, called once at the beginning of when
@@ -51,6 +54,8 @@ class QuantifiersState : public TheoryState
   uint64_t getInstRounds() const;
   /** debug print equality engine on trace c */
   void debugPrintEqualityEngine(const char* c) const;
+  /** get the logic info */
+  const LogicInfo& getLogicInfo() const;
 
  private:
   /** The number of instantiation rounds in this SAT context */
@@ -70,6 +75,8 @@ class QuantifiersState : public TheoryState
    * combination.
    */
   uint64_t d_instWhenPhase;
+  /** Information about the logic we're operating within. */
+  const LogicInfo& d_logicInfo;
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index 4f9a0ee91..2e9093b82 100644
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -14,12 +14,13 @@
 
 #include "theory/quantifiers/skolemize.h"
 
+#include "expr/dtype.h"
 #include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 #include "theory/sort_inference.h"
 #include "theory/theory_engine.h"
 
@@ -29,10 +30,8 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-Skolemize::Skolemize(QuantifiersEngine* qe,
-                     QuantifiersState& qs,
-                     ProofNodeManager* pnm)
-    : d_quantEngine(qe),
+Skolemize::Skolemize(QuantifiersState& qs, ProofNodeManager* pnm)
+    : d_qstate(qs),
       d_skolemized(qs.getUserContext()),
       d_pnm(pnm),
       d_epg(pnm == nullptr ? nullptr
@@ -350,13 +349,13 @@ Node Skolemize::getSkolemizedBody(Node f)
       }
     }
     Assert(d_skolem_constants[f].size() == f[0].getNumChildren());
-    if (options::sortInference())
+    SortInference* si = d_qstate.getSortInference();
+    if (si != nullptr)
     {
       for (unsigned i = 0; i < d_skolem_constants[f].size(); i++)
       {
         // carry information for sort inference
-        d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar(
-            f, f[0][i], d_skolem_constants[f][i]);
+        si->setSkolemVar(f, f[0][i], d_skolem_constants[f][i]);
       }
     }
     return ret;
diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h
index c959758a0..4f92b2eda 100644
--- a/src/theory/quantifiers/skolemize.h
+++ b/src/theory/quantifiers/skolemize.h
@@ -32,7 +32,7 @@ class DTypeConstructor;
 
 namespace theory {
 
-class QuantifiersEngine;
+class SortInference;
 
 namespace quantifiers {
 
@@ -69,7 +69,7 @@ class Skolemize
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
 
  public:
-  Skolemize(QuantifiersEngine* qe, QuantifiersState& qs, ProofNodeManager* pnm);
+  Skolemize(QuantifiersState& qs, ProofNodeManager* pnm);
   ~Skolemize() {}
   /** skolemize quantified formula q
    * If the return value ret of this function is non-null, then ret is a trust
@@ -140,8 +140,8 @@ class Skolemize
                          Node n,
                          TypeNode ntn,
                          std::vector<Node>& selfSel);
-  /** quantifiers engine that owns this module */
-  QuantifiersEngine* d_quantEngine;
+  /** Reference to the quantifiers state */
+  QuantifiersState& d_qstate;
   /** quantified formulas that have been skolemized */
   NodeNodeMap d_skolemized;
   /** map from quantified formulas to the list of skolem constants */
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index f111b23ce..cb5c7dfec 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -36,10 +36,8 @@ namespace quantifiers {
 
 TermDb::TermDb(QuantifiersState& qs,
                QuantifiersInferenceManager& qim,
-               QuantifiersRegistry& qr,
-               QuantifiersEngine* qe)
-    : d_quantEngine(qe),
-      d_qstate(qs),
+               QuantifiersRegistry& qr)
+    : d_qstate(qs),
       d_qim(qim),
       d_qreg(qr),
       d_termsContext(),
@@ -1083,19 +1081,16 @@ bool TermDb::reset( Theory::Effort effort ){
       }
       ++eqcs_i;
     }
-    TheoryEngine* te = d_quantEngine->getTheoryEngine();
-    const LogicInfo& logicInfo = te->getLogicInfo();
+    const LogicInfo& logicInfo = d_qstate.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 = d_qstate.factsBegin(theoryId),
+               it_end = d_qstate.factsEnd(theoryId);
            it != it_end;
            ++it)
       {
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 89d77e169..9a031f99c 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -77,8 +77,7 @@ class TermDb : public QuantifiersUtil {
  public:
   TermDb(QuantifiersState& qs,
          QuantifiersInferenceManager& qim,
-         QuantifiersRegistry& qr,
-         QuantifiersEngine* qe);
+         QuantifiersRegistry& qr);
   ~TermDb();
   /** presolve (called once per user check-sat) */
   void presolve();
@@ -291,8 +290,6 @@ class TermDb : public QuantifiersUtil {
   Node getHoTypeMatchPredicate(TypeNode tn);
 
  private:
-  /** reference to the quantifiers engine */
-  QuantifiersEngine* d_quantEngine;
   /** The quantifiers state object */
   QuantifiersState& d_qstate;
   /** The quantifiers inference manager */
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 7c2bbb019..0f1f5f7de 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -43,7 +43,7 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
                                      const LogicInfo& logicInfo,
                                      ProofNodeManager* pnm)
     : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm),
-      d_qstate(c, u, valuation),
+      d_qstate(c, u, valuation, logicInfo),
       d_qim(*this, d_qstate, pnm),
       d_qengine(d_qstate, d_qim, pnm)
 {