diff options
22 files changed, 56 insertions, 60 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 2335fb491..15ccd400d 100644 --- 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 f553e27f2..fa99ca659 100644 --- 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 6cf96eefc..86f15ba6d 100644 --- 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 7f57d5942..7af0686f8 100644 --- 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 99df6cf13..4f66e1034 100644 --- 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 3c871014a..8fcbeca4f 100644 --- 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 cb64978bb..f3684ab88 100644 --- 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 f9467f7d8..0c8c9399b 100644 --- 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 4ecbf7af4..8d4cd46c3 100644 --- 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 fec15fdc6..ce7d058c3 100644 --- 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 a0058f2d8..d6afd2f66 100644 --- 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 c5f9b44b0..1baf50045 100644 --- 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 17a76468c..8d8f54768 100644 --- 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 15ea004e2..28f162ddd 100644 --- 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 52e89159b..00e3e8251 100644 --- 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 204b938fa..7a8b44625 100644 --- 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 d95b67aaf..b697b004c 100644 --- 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 3a90a8ace..1261f2ce8 100644 --- 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 efa3f9163..cabd57240 100644 --- 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 68f70b740..db917daea 100644 --- 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 549d81c16..dca11524b 100644 --- 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 d61f2d15b..b36c6eb96 100644 --- 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()); } } |