diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-29 09:31:20 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-29 14:31:20 +0000 |
commit | 0e08fa4ff925b201d42544dd4b28c74d1b245bd7 (patch) | |
tree | 60e6e3acb961cda82540903b834e27358f20bd99 /src/theory/quantifiers | |
parent | ba91b0ea10021ad299f30d23de4864940bb78100 (diff) |
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.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.h | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_modules.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_modules.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus_inst.cpp | 2 |
8 files changed, 11 insertions, 16 deletions
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]) */ |