Move decision manager into theory inference manager (#6231)

This makes it so that the decision manager is accessible from TheoryInferenceManager.

This is work towards breaking circular dependencies in quantifiers, and also helps simplify several other dependencies in e.g. UF and datatypes.

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 2335fb491606d3d75086bde25207a405d393390a..15ccd400d65290c0c2402928b1c64792b99aa30b 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1184,7 +1184,7 @@ void TheoryArrays::presolve()
   {
     d_dstratInit = true;
     // add the decision strategy, which is user-context-independent
-    getDecisionManager()->registerStrategy(
+    d_im.getDecisionManager()->registerStrategy(
         DecisionManager::STRAT_ARRAYS,
         d_dstrat.get(),
         DecisionManager::STRAT_SCOPE_CTX_INDEPENDENT);

diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index f553e27f27b39f75db4ee3166c13ec1685b80381..fa99ca659ab4916a3bd39fb0a4389e3a7fccfae0 100644 (file)
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -42,12 +42,10 @@ using namespace CVC4::theory::datatypes;
 
 SygusExtension::SygusExtension(TheoryState& s,
                                InferenceManager& im,
-                               quantifiers::TermDbSygus* tds,
-                               DecisionManager* dm)
+                               quantifiers::TermDbSygus* tds)
     : d_state(s),
       d_im(im),
       d_tds(tds),
-      d_dm(dm),
       d_ssb(tds),
       d_testers(s.getSatContext()),
       d_testers_exp(s.getSatContext()),
@@ -1332,8 +1330,9 @@ void SygusExtension::registerSizeTerm(Node e)
                                         d_state.getSatContext(),
                                         d_state.getValuation()));
     }
-    d_dm->registerStrategy(DecisionManager::STRAT_DT_SYGUS_ENUM_ACTIVE,
-                           d_anchor_to_ag_strategy[e].get());
+    d_im.getDecisionManager()->registerStrategy(
+        DecisionManager::STRAT_DT_SYGUS_ENUM_ACTIVE,
+        d_anchor_to_ag_strategy[e].get());
   }
   Node m;
   if (!ag.isNull())
@@ -1413,8 +1412,8 @@ void SygusExtension::registerMeasureTerm( Node m ) {
     Trace("sygus-sb") << "Sygus : register measure term : " << m << std::endl;
     d_szinfo[m].reset(new SygusSizeDecisionStrategy(d_im, m, d_state));
     // register this as a decision strategy
-    d_dm->registerStrategy(DecisionManager::STRAT_DT_SYGUS_ENUM_SIZE,
-                           d_szinfo[m].get());
+    d_im.getDecisionManager()->registerStrategy(
+        DecisionManager::STRAT_DT_SYGUS_ENUM_SIZE, d_szinfo[m].get());
   }
 }
 

diff --git a/src/theory/datatypes/sygus_extension.h b/src/theory/datatypes/sygus_extension.h
index 6cf96eefcd624f1919ad8b50cbc3ed7c2afdc3b0..86f15ba6d4f719db43dc4e0dd4c0398a7fde0cbd 100644 (file)
--- a/src/theory/datatypes/sygus_extension.h
+++ b/src/theory/datatypes/sygus_extension.h
@@ -71,8 +71,7 @@ class SygusExtension
  public:
   SygusExtension(TheoryState& s,
                  InferenceManager& im,
-                 quantifiers::TermDbSygus* tds,
-                 DecisionManager* dm);
+                 quantifiers::TermDbSygus* tds);
   ~SygusExtension();
   /**
    * Notify this class that tester for constructor tindex has been asserted for
@@ -113,8 +112,6 @@ class SygusExtension
   InferenceManager& d_im;
   /** Pointer to the sygus term database */
   quantifiers::TermDbSygus* d_tds;
-  /** Pointer to the decision manager */
-  DecisionManager* d_dm;
   /** the simple symmetry breaking utility */
   SygusSimpleSymBreak d_ssb;
   /**

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 7f57d5942e4cbae438a9cea6a7dcaa2d78fb45a5..7af0686f86715014af49faf5d761a1a65f43c4b7 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -116,8 +116,7 @@ void TheoryDatatypes::finishInit()
   {
     quantifiers::TermDbSygus* tds =
         getQuantifiersEngine()->getTermDatabaseSygus();
-    d_sygusExtension.reset(
-        new SygusExtension(d_state, d_im, tds, getDecisionManager()));
+    d_sygusExtension.reset(new SygusExtension(d_state, d_im, tds));
     // do congruence on evaluation functions
     d_equalityEngine->addFunctionKind(kind::DT_SYGUS_EVAL);
   }

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

diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 3c871014a8e0fd39f75f18817c3dd2f0c0874cf8..8fcbeca4f99a1a4fb8b06ff6c4f076595499f96e 100644 (file)
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -89,9 +89,8 @@ BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe,
                                  QuantifiersState& qs,
                                  QuantifiersInferenceManager& qim,
                                  QuantifiersRegistry& qr,
-                                 TermRegistry& tr,
-                                 DecisionManager* dm)
-    : QuantifiersModule(qs, qim, qr, tr, qe), d_dm(dm)
+                                 TermRegistry& tr)
+    : QuantifiersModule(qs, qim, qr, tr, qe)
 {
 }
 
@@ -475,6 +474,7 @@ void BoundedIntegers::checkOwnership(Node f)
   
   if( bound_success ){
     d_bound_quants.push_back( f );
+    DecisionManager* dm = d_qim.getDecisionManager();
     for( unsigned i=0; i<d_set[f].size(); i++) {
       Node v = d_set[f][i];
       std::map< Node, Node >::iterator itr = d_range[f].find( v );
@@ -503,8 +503,8 @@ void BoundedIntegers::checkOwnership(Node f)
                                               d_qstate.getUserContext(),
                                               d_qstate.getValuation(),
                                               isProxy));
-            d_dm->registerStrategy(DecisionManager::STRAT_QUANT_BOUND_INT_SIZE,
-                                   d_rms[r].get());
+            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 cb64978bbe89256240d8198f5616935fe60e16b7..f3684ab888eea919a629456ac444e36396e191b2 100644 (file)
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -168,8 +168,7 @@ private:
                   QuantifiersState& qs,
                   QuantifiersInferenceManager& qim,
                   QuantifiersRegistry& qr,
-                  TermRegistry& tr,
-                  DecisionManager* dm);
+                  TermRegistry& tr);
   virtual ~BoundedIntegers();
 
   void presolve() override;
@@ -236,8 +235,6 @@ 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/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index f9467f7d897e5cc67dfd12962d3f07ac5b58d00a..0c8c9399b1d0881844fa2b318153e9c9cc977e95 100644 (file)
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -45,7 +45,6 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe,
                                     QuantifiersInferenceManager& qim,
                                     QuantifiersRegistry& qr,
                                     TermRegistry& tr,
-                                    DecisionManager* dm,
                                     std::vector<QuantifiersModule*>& modules)
 {
   // add quantifiers modules
@@ -78,7 +77,7 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe,
   // finite model finding
   if (options::fmfBound())
   {
-    d_bint.reset(new BoundedIntegers(qe, qs, qim, qr, tr, dm));
+    d_bint.reset(new BoundedIntegers(qe, qs, qim, qr, tr));
     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 4ecbf7af493af3a2749e75a8b5eef2a705dd91ad..8d4cd46c3e4b51c7cc058212c62c86e8c0b81898 100644 (file)
--- a/src/theory/quantifiers/quantifiers_modules.h
+++ b/src/theory/quantifiers/quantifiers_modules.h
@@ -59,7 +59,6 @@ class QuantifiersModules
                   QuantifiersInferenceManager& qim,
                   QuantifiersRegistry& qr,
                   TermRegistry& tr,
-                  DecisionManager* dm,
                   std::vector<QuantifiersModule*>& modules);
 
  private:

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index fec15fdc65ee84c4d488f7db4477359cef1f0758..ce7d058c38e7eaff17acf74fda776c71780034ce 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -564,7 +564,7 @@ void CegisUnifEnumDecisionStrategy::initialize(
   }
 
   // register this strategy
-  d_qe->getDecisionManager()->registerStrategy(
+  d_qim.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 a0058f2d888da6c9bf1c499e97bb562d3372d724..d6afd2f66e704f84e0ed88b9a9268bb1a4c48383 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -246,7 +246,7 @@ void SynthConjecture::assign(Node q)
                                     d_feasible_guard,
                                     d_qstate.getSatContext(),
                                     d_qstate.getValuation()));
-  d_qe->getDecisionManager()->registerStrategy(
+  d_qim.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

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

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 17a76468c6a016d2ae4ee848117bde92d2971789..8d8f547681a4a55ca4c54e48a8fcdfabc9848178 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -51,7 +51,6 @@ QuantifiersEngine::QuantifiersEngine(
     : d_qstate(qstate),
       d_qim(qim),
       d_te(nullptr),
-      d_decManager(nullptr),
       d_pnm(pnm),
       d_qreg(qr),
       d_treg(tr),
@@ -69,13 +68,12 @@ QuantifiersEngine::QuantifiersEngine(
 
 QuantifiersEngine::~QuantifiersEngine() {}
 
-void QuantifiersEngine::finishInit(TheoryEngine* te, DecisionManager* dm)
+void QuantifiersEngine::finishInit(TheoryEngine* te)
 {
   d_te = te;
-  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_treg, dm, d_modules);
+  d_qmodules->initialize(this, d_qstate, d_qim, d_qreg, d_treg, d_modules);
   if (d_qmodules->d_rel_dom.get())
   {
     d_util.push_back(d_qmodules->d_rel_dom.get());
@@ -88,11 +86,6 @@ void QuantifiersEngine::finishInit(TheoryEngine* te, DecisionManager* dm)
   d_qreg.getQuantifiersBoundInference().finishInit(d_qmodules->d_bint.get());
 }
 
-DecisionManager* QuantifiersEngine::getDecisionManager()
-{
-  return d_decManager;
-}
-
 quantifiers::QuantifiersState& QuantifiersEngine::getState()
 {
   return d_qstate;

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 15ea004e2d5266600af71f21b121e038cd02345f..28f162ddd681609cf4669075205fb7bd1f8d1a16 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -31,7 +31,6 @@ class TheoryEngine;
 
 namespace theory {
 
-class DecisionManager;
 class QuantifiersModule;
 class RepSetIterator;
 
@@ -65,8 +64,6 @@ class QuantifiersEngine {
                     ProofNodeManager* pnm);
   ~QuantifiersEngine();
   //---------------------- external interface
-  /** Get the decision manager */
-  DecisionManager* getDecisionManager();
   /** The quantifiers state object */
   quantifiers::QuantifiersState& getState();
   /** The quantifiers inference manager */
@@ -97,7 +94,7 @@ class QuantifiersEngine {
    * @param te The theory engine
    * @param dm The decision manager of the theory engine
    */
-  void finishInit(TheoryEngine* te, DecisionManager* dm);
+  void finishInit(TheoryEngine* te);
   //---------------------- end private initialization
 
  public:
@@ -189,8 +186,6 @@ public:
   quantifiers::QuantifiersInferenceManager& d_qim;
   /** Pointer to theory engine object */
   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 */

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 52e89159b896f4cdf94847601e3bfc8293ac5a37..00e3e82518b9cfc9b44afdf5066a4b9a367faf29 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -468,8 +468,8 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact)
     d_neg_guard_strategy[g].reset(new DecisionStrategySingleton(
         "sep_neg_guard", g, getSatContext(), getValuation()));
     DecisionStrategySingleton* ds = d_neg_guard_strategy[g].get();
-    getDecisionManager()->registerStrategy(DecisionManager::STRAT_SEP_NEG_GUARD,
-                                           ds);
+    d_im.getDecisionManager()->registerStrategy(
+        DecisionManager::STRAT_SEP_NEG_GUARD, ds);
     Node lit = ds->getLiteral(0);
     d_neg_guard[slbl][satom] = lit;
     Trace("sep-lemma-debug")

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 204b938fa7a2b310be875f2fe83dddaffc7b025e..7a8b446258ddac018ced80ec5f7bbb22c7cde8de 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -187,7 +187,7 @@ void TheoryStrings::presolve() {
     d_stringsFmf.presolve();
     // This strategy is local to a check-sat call, since we refresh the strategy
     // on every call to presolve.
-    getDecisionManager()->registerStrategy(
+    d_im.getDecisionManager()->registerStrategy(
         DecisionManager::STRAT_STRINGS_SUM_LENGTHS,
         d_stringsFmf.getDecisionStrategy(),
         DecisionManager::STRAT_SCOPE_LOCAL_SOLVE);

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index d95b67aaf2019349743a133fa1b8d886a3786a79..b697b004c2d23bf5161383099ad49945218c1fe2 100644 (file)
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -75,7 +75,6 @@ Theory::Theory(TheoryId id,
       d_factsHead(satContext, 0),
       d_sharedTermsIndex(satContext, 0),
       d_careGraph(nullptr),
-      d_decManager(nullptr),
       d_instanceName(name),
       d_checkTime(getStatsPrefix(id) + name + "::checkTime"),
       d_computeCareGraphTime(getStatsPrefix(id) + name
@@ -127,9 +126,11 @@ void Theory::setQuantifiersEngine(QuantifiersEngine* qe)
 
 void Theory::setDecisionManager(DecisionManager* dm)
 {
-  Assert(d_decManager == nullptr);
   Assert(dm != nullptr);
-  d_decManager = dm;
+  if (d_inferManager != nullptr)
+  {
+    d_inferManager->setDecisionManager(dm);
+  }
 }
 
 void Theory::finishInitStandalone()

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 3a90a8ace71df87015030d00691f0232057f9586..1261f2ce863f7b15ed5ca52b6ddfbc4af7f37615 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -481,9 +481,6 @@ class Theory {
     return d_quantEngine;
   }
 
-  /** Get the decision manager associated to this theory. */
-  DecisionManager* getDecisionManager() { return d_decManager; }
-
   /**
    * @return The theory state associated with this theory.
    */

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index efa3f916384a4fa36ee6a5efd4925a28698bc6bc..cabd572400646db19cef2026ad68b5db1cc3e0a8 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -172,7 +172,7 @@ void TheoryEngine::finishInit()
   // special model builder object
   if (d_logicInfo.isQuantified())
   {
-    d_quantEngine->finishInit(this, d_decManager.get());
+    d_quantEngine->finishInit(this);
   }
   // initialize the theory combination manager, which decides and allocates the
   // equality engines to use for all theories.

diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 68f70b740f6ebf70fcca0210a078a40eb7a037d3..db917daea7d7c412f2cfc90e1d919de529fa30d6 100644 (file)
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -36,6 +36,7 @@ TheoryInferenceManager::TheoryInferenceManager(Theory& t,
       d_theoryState(state),
       d_out(t.getOutputChannel()),
       d_ee(nullptr),
+      d_decManager(nullptr),
       d_pnm(pnm),
       d_cacheLemmas(cacheLemmas),
       d_keep(t.getSatContext()),
@@ -76,6 +77,11 @@ void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)
   }
 }
 
+void TheoryInferenceManager::setDecisionManager(DecisionManager* dm)
+{
+  d_decManager = dm;
+}
+
 bool TheoryInferenceManager::isProofEnabled() const { return d_pnm != nullptr; }
 
 void TheoryInferenceManager::reset()
@@ -488,6 +494,11 @@ bool TheoryInferenceManager::cacheLemma(TNode lem, LemmaProperty p)
   return true;
 }
 
+DecisionManager* TheoryInferenceManager::getDecisionManager()
+{
+  return d_decManager;
+}
+
 void TheoryInferenceManager::requirePhase(TNode n, bool pol)
 {
   return d_out.requirePhase(n, pol);

diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index 549d81c167f02e4f7b68f4eb9b6406adab3f41cf..dca11524b31bcfcd21d1816ee5e276cc97c175cd 100644 (file)
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -36,6 +36,7 @@ namespace theory {
 
 class Theory;
 class TheoryState;
+class DecisionManager;
 namespace eq {
 class EqualityEngine;
 class ProofEqEngine;
@@ -90,16 +91,22 @@ class TheoryInferenceManager
                          const std::string& name,
                          bool cacheLemmas = true);
   virtual ~TheoryInferenceManager();
+  //--------------------------------------- initialization
   /**
    * Set equality engine, ee is a pointer to the official equality engine
    * of theory.
    */
   void setEqualityEngine(eq::EqualityEngine* ee);
+  /** Set the decision manager */
+  void setDecisionManager(DecisionManager* dm);
+  //--------------------------------------- end initialization
   /**
    * Are proofs enabled in this inference manager? Returns true if the proof
    * node manager pnm provided to the constructor of this class was non-null.
    */
   bool isProofEnabled() const;
+  /** Get the underlying proof equality engine */
+  eq::ProofEqEngine* getProofEqEngine();
   /**
    * Reset, which resets counters regarding the number of added lemmas and
    * internal facts. This method should be manually called by the theory at
@@ -116,8 +123,6 @@ class TheoryInferenceManager
    * since the last call to reset.
    */
   bool hasSent() const;
-  /** Get the underlying proof equality engine */
-  eq::ProofEqEngine* getProofEqEngine();
   //--------------------------------------- propagations
   /**
    * T-propagate literal lit, possibly encountered by equality engine,
@@ -344,6 +349,8 @@ class TheoryInferenceManager
   /** Have we added a internal fact since the last call to reset? */
   bool hasSentFact() const;
   //--------------------------------------- phase requirements
+  /** Get the decision manager, which manages decision strategies. */
+  DecisionManager* getDecisionManager();
   /**
    * Set that literal n has SAT phase requirement pol, that is, it should be
    * decided with polarity pol, for details see OutputChannel::requirePhase.
@@ -418,6 +425,8 @@ class TheoryInferenceManager
   OutputChannel& d_out;
   /** Pointer to equality engine of the theory. */
   eq::EqualityEngine* d_ee;
+  /** Pointer to the decision manager */
+  DecisionManager* d_decManager;
   /** A proof equality engine */
   std::unique_ptr<eq::ProofEqEngine> d_pfee;
   /** The proof node manager of the theory */

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index d61f2d15be1c9d8c378aef2dc5b287f17da62571..b36c6eb9692061746535a4cf7df8db49d57a6c18 100644 (file)
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -507,8 +507,8 @@ void SortModel::initialize()
     d_initialized = true;
     // Strategy is user-context-dependent, since it is in sync with
     // user-context-dependent flag d_initialized.
-    d_thss->getTheory()->getDecisionManager()->registerStrategy(
-        DecisionManager::STRAT_UF_CARD, d_c_dec_strat.get());
+    d_im.getDecisionManager()->registerStrategy(DecisionManager::STRAT_UF_CARD,
+                                                d_c_dec_strat.get());
   }
 }
 
@@ -1656,7 +1656,7 @@ void CardinalityExtension::initializeCombinedCardinality()
       && !d_initializedCombinedCardinality.get())
   {
     d_initializedCombinedCardinality = true;
-    d_th->getDecisionManager()->registerStrategy(
+    d_im.getDecisionManager()->registerStrategy(
         DecisionManager::STRAT_UF_COMBINED_CARD, d_cc_dec_strat.get());
   }
 }