From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 24 Feb 2021 01:12:32 +0000 (-0600)
Subject: Add interface to TheoryState for sort inference and facts (#5967)
X-Git-Tag: cvc5-1.0.0~2230
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=854ab7e1adce90ebd822cc29ffabf5546d13f5cc;p=cvc5.git

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.
---

diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp
index 79f387aa6..918b13140 100644
--- a/src/preprocessing/passes/sort_infer.cpp
+++ b/src/preprocessing/passes/sort_infer.cpp
@@ -34,7 +34,8 @@ SortInferencePass::SortInferencePass(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult SortInferencePass::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  SortInference* si = d_preprocContext->getTheoryEngine()->getSortInference();
+  theory::SortInference* si =
+      d_preprocContext->getTheoryEngine()->getSortInference();
 
   if (options::sortInference())
   {
diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp
index 295b7309e..bb2bf937a 100644
--- a/src/theory/model_manager.cpp
+++ b/src/theory/model_manager.cpp
@@ -62,7 +62,7 @@ void ModelManager::finishInit(eq::EqualityEngineNotify* notify)
   // not have a model builder
   if (d_modelBuilder == nullptr)
   {
-    d_alocModelBuilder.reset(new TheoryEngineModelBuilder(&d_te));
+    d_alocModelBuilder.reset(new TheoryEngineModelBuilder);
     d_modelBuilder = d_alocModelBuilder.get();
   }
   // notice that the equality engine of the model has yet to be assigned.
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)
 {
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index ec4cb7905..7046a8ef0 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -41,16 +41,17 @@ QuantifiersEngine::QuantifiersEngine(
       d_qim(qim),
       d_te(nullptr),
       d_decManager(nullptr),
+      d_pnm(pnm),
       d_qreg(),
       d_tr_trie(new inst::TriggerTrie),
       d_model(nullptr),
       d_builder(nullptr),
-      d_term_db(new quantifiers::TermDb(qstate, qim, d_qreg, this)),
+      d_term_db(new quantifiers::TermDb(qstate, qim, d_qreg)),
       d_eq_query(nullptr),
       d_sygus_tdb(nullptr),
       d_instantiate(
           new quantifiers::Instantiate(this, qstate, qim, d_qreg, pnm)),
-      d_skolemize(new quantifiers::Skolemize(this, qstate, pnm)),
+      d_skolemize(new quantifiers::Skolemize(d_qstate, d_pnm)),
       d_term_enum(new quantifiers::TermEnumeration),
       d_quants_prereg(qstate.getUserContext()),
       d_quants_red(qstate.getUserContext()),
@@ -113,15 +114,13 @@ void QuantifiersEngine::finishInit(TheoryEngine* te, DecisionManager* dm)
   d_decManager = dm;
   // Initialize the modules and the utilities here.
   d_qmodules.reset(new quantifiers::QuantifiersModules);
-  d_qmodules->initialize(this, d_qstate, d_qim, d_qreg, d_modules);
+  d_qmodules->initialize(this, d_qstate, d_qim, d_qreg, dm, d_modules);
   if (d_qmodules->d_rel_dom.get())
   {
     d_util.push_back(d_qmodules->d_rel_dom.get());
   }
 }
 
-TheoryEngine* QuantifiersEngine::getTheoryEngine() const { return d_te; }
-
 DecisionManager* QuantifiersEngine::getDecisionManager()
 {
   return d_decManager;
@@ -387,7 +386,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }
     if( Trace.isOn("quant-engine-assert") ){
       Trace("quant-engine-assert") << "Assertions : " << std::endl;
-      getTheoryEngine()->printAssertions("quant-engine-assert");
+      d_te->printAssertions("quant-engine-assert");
     }
 
     //reset utilities
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index c8f9cd6ad..f464b24d4 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -65,8 +65,6 @@ class QuantifiersEngine {
                     ProofNodeManager* pnm);
   ~QuantifiersEngine();
   //---------------------- external interface
-  /** get theory engine */
-  TheoryEngine* getTheoryEngine() const;
   /** Get the decision manager */
   DecisionManager* getDecisionManager();
   /** The quantifiers state object */
@@ -272,6 +270,8 @@ public:
   TheoryEngine* d_te;
   /** Reference to the decision manager of the theory engine */
   DecisionManager* d_decManager;
+  /** Pointer to the proof node manager */
+  ProofNodeManager* d_pnm;
   /** vector of utilities for quantifiers */
   std::vector<QuantifiersUtil*> d_util;
   /** vector of modules for quantifiers */
diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp
index 9fa216e67..63e3359ab 100644
--- a/src/theory/sort_inference.cpp
+++ b/src/theory/sort_inference.cpp
@@ -32,6 +32,7 @@ using namespace CVC4::kind;
 using namespace std;
 
 namespace CVC4 {
+namespace theory {
 
 void SortInference::UnionFind::print(const char * c){
   for( std::map< int, int >::iterator it = d_eqc.begin(); it != d_eqc.end(); ++it ){
@@ -864,4 +865,5 @@ bool SortInference::isHandledApplyUf(Kind k) const
   return k == APPLY_UF && !options::ufHo();
 }
 
-}/* CVC4 namespace */
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/sort_inference.h b/src/theory/sort_inference.h
index 059dc5582..46497c494 100644
--- a/src/theory/sort_inference.h
+++ b/src/theory/sort_inference.h
@@ -25,6 +25,7 @@
 #include "expr/type_node.h"
 
 namespace CVC4 {
+namespace theory {
 
 /** sort inference
  *
@@ -165,6 +166,7 @@ private:
  bool isHandledApplyUf(Kind k) const;
 };
 
+}  // namespace theory
 }
 
 #endif
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index a2e608b9f..e49ca8b05 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -250,6 +250,11 @@ TheoryEngine::TheoryEngine(context::Context* context,
     d_theoryOut[theoryId] = NULL;
   }
 
+  if (options::sortInference())
+  {
+    d_sortInfer.reset(new SortInference);
+  }
+
   smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime);
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 224d84664..d10e498a8 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -274,7 +274,7 @@ class TheoryEngine {
   void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
 
   /** sort inference module */
-  SortInference d_sortInfer;
+  std::unique_ptr<theory::SortInference> d_sortInfer;
 
   /** Time spent in theory combination */
   TimerStat d_combineTheoriesTime;
@@ -634,11 +634,10 @@ class TheoryEngine {
 
   /** For preprocessing pass lifting bit-vectors of size 1 to booleans */
 public:
+ theory::SortInference* getSortInference() { return d_sortInfer.get(); }
 
-  SortInference* getSortInference() { return &d_sortInfer; }
-
-  /** Prints the assertions to the debug stream */
-  void printAssertions(const char* tag);
+ /** Prints the assertions to the debug stream */
+ void printAssertions(const char* tag);
 
 private:
 
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 53b8f25a4..9604dc72b 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -16,8 +16,8 @@
 #include "expr/dtype.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
+#include "options/theory_options.h"
 #include "options/uf_options.h"
-#include "theory/theory_engine.h"
 #include "theory/uf/theory_uf_model.h"
 
 using namespace std;
@@ -60,9 +60,7 @@ Node TheoryEngineModelBuilder::Assigner::getNextAssignment()
   return n;
 }
 
-TheoryEngineModelBuilder::TheoryEngineModelBuilder(TheoryEngine* te) : d_te(te)
-{
-}
+TheoryEngineModelBuilder::TheoryEngineModelBuilder() {}
 
 Node TheoryEngineModelBuilder::evaluateEqc(TheoryModel* m, TNode r)
 {
diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h
index 4ffcbeee7..fde74a05f 100644
--- a/src/theory/theory_model_builder.h
+++ b/src/theory/theory_model_builder.h
@@ -47,7 +47,7 @@ class TheoryEngineModelBuilder
   typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
 
  public:
-  TheoryEngineModelBuilder(TheoryEngine* te);
+  TheoryEngineModelBuilder();
   virtual ~TheoryEngineModelBuilder() {}
   /**
    * Should be called only on models m after they have been prepared
@@ -84,8 +84,6 @@ class TheoryEngineModelBuilder
   void postProcessModel(bool incomplete, TheoryModel* m);
 
  protected:
-  /** pointer to theory engine */
-  TheoryEngine* d_te;
 
   //-----------------------------------virtual functions
   /** pre-process build model
diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp
index e145baa6a..2d6c713de 100644
--- a/src/theory/theory_state.cpp
+++ b/src/theory/theory_state.cpp
@@ -152,11 +152,25 @@ bool TheoryState::isSatLiteral(TNode lit) const
 
 TheoryModel* TheoryState::getModel() { return d_valuation.getModel(); }
 
+SortInference* TheoryState::getSortInference()
+{
+  return d_valuation.getSortInference();
+}
+
 bool TheoryState::hasSatValue(TNode n, bool& value) const
 {
   return d_valuation.hasSatValue(n, value);
 }
 
+context::CDList<Assertion>::const_iterator TheoryState::factsBegin(TheoryId tid)
+{
+  return d_valuation.factsBegin(tid);
+}
+context::CDList<Assertion>::const_iterator TheoryState::factsEnd(TheoryId tid)
+{
+  return d_valuation.factsEnd(tid);
+}
+
 Valuation& TheoryState::getValuation() { return d_valuation; }
 
 }  // namespace theory
diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h
index 891016f0a..60b45878f 100644
--- a/src/theory/theory_state.h
+++ b/src/theory/theory_state.h
@@ -81,10 +81,26 @@ class TheoryState
    * check.
    */
   TheoryModel* getModel();
+  /**
+   * Returns a pointer to the sort inference module, which lives in TheoryEngine
+   * and is non-null when options::sortInference is true.
+   */
+  SortInference* getSortInference();
 
   /** Returns true if n has a current SAT assignment and stores it in value. */
   virtual bool hasSatValue(TNode n, bool& value) const;
 
+  //------------------------------------------- access methods for assertions
+  /**
+   * The following methods are intended only to be used in limited use cases,
+   * for cases where a theory (e.g. quantifiers) requires knowing about the
+   * assertions from other theories.
+   */
+  /** The beginning iterator of facts for theory tid.*/
+  context::CDList<Assertion>::const_iterator factsBegin(TheoryId tid);
+  /** The beginning iterator of facts for theory tid.*/
+  context::CDList<Assertion>::const_iterator factsEnd(TheoryId tid);
+
   /** Get the underlying valuation class */
   Valuation& getValuation();
 
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index aa73e3419..94402e2d9 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -740,7 +740,7 @@ void SortModel::check(Theory::Effort level)
   Trace("uf-ss-debug") << "No splits added. " << d_cardinality << std::endl;
   Trace("uf-ss-si") << "Must combine region" << std::endl;
   bool recheck = false;
-  SortInference* si = d_thss->getSortInference();
+  SortInference* si = d_state.getSortInference();
   if (si != nullptr)
   {
     // If sort inference is enabled, search for regions with same sort.
@@ -1021,14 +1021,18 @@ int SortModel::addSplit(Region* r)
         AlwaysAssert(false);
       }
     }
-    SortInference* si = d_thss->getSortInference();
-    if (si != nullptr)
+    if (Trace.isOn("uf-ss-split-si"))
     {
-      for( int i=0; i<2; i++ ){
-        int sid = si->getSortId(ss[i]);
-        Trace("uf-ss-split-si") << sid << " ";
+      SortInference* si = d_state.getSortInference();
+      if (si != nullptr)
+      {
+        for (size_t i = 0; i < 2; i++)
+        {
+          int sid = si->getSortId(ss[i]);
+          Trace("uf-ss-split-si") << sid << " ";
+        }
+        Trace("uf-ss-split-si") << std::endl;
       }
-      Trace("uf-ss-split-si")  << std::endl;
     }
     //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " ";
     //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl;
@@ -1247,20 +1251,6 @@ CardinalityExtension::~CardinalityExtension()
   }
 }
 
-SortInference* CardinalityExtension::getSortInference()
-{
-  if (!options::sortInference())
-  {
-    return nullptr;
-  }
-  QuantifiersEngine* qe = d_th->getQuantifiersEngine();
-  if (qe != nullptr)
-  {
-    return qe->getTheoryEngine()->getSortInference();
-  }
-  return nullptr;
-}
-
 /** ensure eqc */
 void CardinalityExtension::ensureEqc(SortModel* c, Node a)
 {
@@ -1351,12 +1341,12 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
       Trace("uf-ss-debug") << "...check cardinality terms : " << lit[0] << " " << ct << std::endl;
       if( lit[0]==ct ){
         if( options::ufssFairnessMonotone() ){
+          SortInference* si = d_state.getSortInference();
           Trace("uf-ss-com-card-debug") << "...set master/slave" << std::endl;
           if( tn!=d_tn_mono_master ){
             std::map< TypeNode, bool >::iterator it = d_tn_mono_slave.find( tn );
             if( it==d_tn_mono_slave.end() ){
               bool isMonotonic;
-              SortInference* si = getSortInference();
               if (si != nullptr)
               {
                 isMonotonic = si->isMonotonic(tn);
diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h
index 6b5349ce7..4f1566424 100644
--- a/src/theory/uf/cardinality_extension.h
+++ b/src/theory/uf/cardinality_extension.h
@@ -25,9 +25,6 @@
 #include "theory/decision_manager.h"
 
 namespace CVC4 {
-
-class SortInference;
-
 namespace theory {
 namespace uf {
 
@@ -366,8 +363,6 @@ class CardinalityExtension
   ~CardinalityExtension();
   /** get theory */
   TheoryUF* getTheory() { return d_th; }
-  /** get sort inference module */
-  SortInference* getSortInference();
   /** new node */
   void newEqClass( Node n );
   /** merge */
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 1926c836e..0dd576a04 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -124,6 +124,15 @@ TheoryModel* Valuation::getModel() {
   }
   return d_engine->getModel();
 }
+SortInference* Valuation::getSortInference()
+{
+  if (d_engine == nullptr)
+  {
+    // no theory engine, thus we don't have a sort inference object
+    return nullptr;
+  }
+  return d_engine->getSortInference();
+}
 
 void Valuation::setUnevaluatedKind(Kind k)
 {
@@ -198,5 +207,18 @@ bool Valuation::needCheck() const{
 
 bool Valuation::isRelevant(Node lit) const { return d_engine->isRelevant(lit); }
 
+context::CDList<Assertion>::const_iterator Valuation::factsBegin(TheoryId tid)
+{
+  Theory* theory = d_engine->theoryOf(tid);
+  Assert(theory != nullptr);
+  return theory->facts_begin();
+}
+context::CDList<Assertion>::const_iterator Valuation::factsEnd(TheoryId tid)
+{
+  Theory* theory = d_engine->theoryOf(tid);
+  Assert(theory != nullptr);
+  return theory->facts_end();
+}
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 9759309fa..305795881 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -21,8 +21,10 @@
 #ifndef CVC4__THEORY__VALUATION_H
 #define CVC4__THEORY__VALUATION_H
 
+#include "context/cdlist.h"
 #include "expr/node.h"
 #include "options/theory_options.h"
+#include "theory/assertion.h"
 
 namespace CVC4 {
 
@@ -31,6 +33,7 @@ class TheoryEngine;
 namespace theory {
 
 class TheoryModel;
+class SortInference;
 
 /**
  * The status of an equality in the current context.
@@ -111,6 +114,11 @@ public:
    * check.
    */
   TheoryModel* getModel();
+  /**
+   * Returns a pointer to the sort inference module, which lives in TheoryEngine
+   * and is non-null when options::sortInference is true.
+   */
+  SortInference* getSortInference();
 
   //-------------------------------------- static configuration of the model
   /**
@@ -195,6 +203,17 @@ public:
    * or during LAST_CALL effort.
    */
   bool isRelevant(Node lit) const;
+
+  //------------------------------------------- access methods for assertions
+  /**
+   * The following methods are intended only to be used in limited use cases,
+   * for cases where a theory (e.g. quantifiers) requires knowing about the
+   * assertions from other theories.
+   */
+  /** The beginning iterator of facts for theory tid.*/
+  context::CDList<Assertion>::const_iterator factsBegin(TheoryId tid);
+  /** The beginning iterator of facts for theory tid.*/
+  context::CDList<Assertion>::const_iterator factsEnd(TheoryId tid);
 };/* class Valuation */
 
 }/* CVC4::theory namespace */