From 72f70f1573651bcbf5f327c7a3411ece0e607e3f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 26 Mar 2021 11:47:22 -0500 Subject: [PATCH] Pass term registry to quantifiers modules (#6216) --- src/theory/datatypes/sygus_extension.cpp | 1 + .../quantifiers/cegqi/ceg_instantiator.cpp | 2 +- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 22 ++++++++++++------- .../quantifiers/cegqi/inst_strategy_cegqi.h | 3 ++- .../quantifiers/conjecture_generator.cpp | 14 ++++++------ src/theory/quantifiers/conjecture_generator.h | 3 ++- .../ematching/instantiation_engine.cpp | 2 +- .../quantifiers/fmf/bounded_integers.cpp | 10 ++++----- src/theory/quantifiers/fmf/bounded_integers.h | 2 ++ src/theory/quantifiers/fmf/model_engine.cpp | 5 +++-- src/theory/quantifiers/fmf/model_engine.h | 3 ++- .../quantifiers/inst_strategy_enumerative.cpp | 3 ++- .../quantifiers/inst_strategy_enumerative.h | 1 + .../quantifiers/quant_conflict_find.cpp | 5 +++-- src/theory/quantifiers/quant_conflict_find.h | 3 ++- src/theory/quantifiers/quant_module.cpp | 9 +++----- src/theory/quantifiers/quant_module.h | 10 ++++++--- src/theory/quantifiers/quant_split.cpp | 5 +++-- src/theory/quantifiers/quant_split.h | 3 ++- .../quantifiers/quantifiers_modules.cpp | 18 +++++++-------- src/theory/quantifiers/sygus/synth_engine.cpp | 8 +++---- src/theory/quantifiers/sygus/synth_engine.h | 3 ++- src/theory/quantifiers/sygus_inst.cpp | 13 ++++++----- src/theory/quantifiers/sygus_inst.h | 3 ++- 24 files changed, 87 insertions(+), 64 deletions(-) diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 9a952601d..f553e27f2 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -32,6 +32,7 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" #include "theory/theory_model.h" +#include "theory/theory_state.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index d3bc788cd..ca9599ba3 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -26,7 +26,7 @@ #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 2c0fba7a6..99df6cf13 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -24,6 +24,7 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/rewriter.h" @@ -52,8 +53,9 @@ TrustNode InstRewriterCegqi::rewriteInstantiation(Node q, InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr) - : QuantifiersModule(qs, qim, qr, qe), + QuantifiersRegistry& qr, + TermRegistry& tr) + : QuantifiersModule(qs, qim, qr, tr, qe), d_irew(new InstRewriterCegqi(this)), d_cbqi_set_quant_inactive(false), d_incomplete_check(false), @@ -84,10 +86,10 @@ bool InstStrategyCegqi::needsCheck(Theory::Effort e) QuantifiersModule::QEffort InstStrategyCegqi::needsModel(Theory::Effort e) { - size_t nquant = d_quantEngine->getModel()->getNumAssertedQuantifiers(); + size_t nquant = d_treg.getModel()->getNumAssertedQuantifiers(); for (size_t i = 0; i < nquant; i++) { - Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + Node q = d_treg.getModel()->getAssertedQuantifier(i); if (doCbqi(q)) { return QEFFORT_STANDARD; @@ -193,11 +195,15 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort) d_incomplete_check = false; d_active_quant.clear(); //check if any cbqi lemma has not been added yet - for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ - Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + FirstOrderModel* fm = d_treg.getModel(); + size_t nquant = fm->getNumAssertedQuantifiers(); + for (size_t i = 0; i < nquant; i++) + { + Node q = fm->getAssertedQuantifier(i); //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine if( doCbqi( q ) ){ - if( d_quantEngine->getModel()->isQuantifierActive( q ) ){ + if (fm->isQuantifierActive(q)) + { d_active_quant[q] = true; Debug("cegqi-debug") << "Check quantified formula " << q << "..." << std::endl; Node cel = getCounterexampleLiteral(q); @@ -211,7 +217,7 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort) Trace("cegqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl; }else{ Trace("cegqi") << "Inactive : " << q << std::endl; - d_quantEngine->getModel()->setQuantifierActive( q, false ); + fm->setQuantifierActive(q, false); d_cbqi_set_quant_inactive = true; d_active_quant.erase( q ); } diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index 92b9506e7..6db755246 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -71,7 +71,8 @@ class InstStrategyCegqi : public QuantifiersModule InstStrategyCegqi(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr); + QuantifiersRegistry& qr, + TermRegistry& tr); ~InstStrategyCegqi(); /** whether to do counterexample-guided instantiation for quantifier q */ diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 04ab464f8..d253fce23 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -21,7 +21,6 @@ #include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" -#include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/rewriter.h" @@ -89,8 +88,9 @@ void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& ConjectureGenerator::ConjectureGenerator(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr) - : QuantifiersModule(qs, qim, qr, qe), + QuantifiersRegistry& qr, + TermRegistry& tr) + : QuantifiersModule(qs, qim, qr, tr, qe), d_notify(*this), d_uequalityEngine( d_notify, qs.getSatContext(), "ConjectureGenerator::ee", false), @@ -318,7 +318,7 @@ Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) { } bool ConjectureGenerator::isHandledTerm( TNode n ){ - return d_quantEngine->getTermDatabase()->isTermActive(n) + return getTermDatabase()->isTermActive(n) && inst::TriggerTermInfo::isAtomicTrigger(n) && (n.getKind() != APPLY_UF || n.getOperator().getKind() != SKOLEM); } @@ -537,7 +537,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) d_ue_canon.clear(); d_thm_index.clear(); std::vector< Node > provenConj; - quantifiers::FirstOrderModel* m = d_quantEngine->getModel(); + quantifiers::FirstOrderModel* m = d_treg.getModel(); for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ Node q = m->getAssertedQuantifier( i ); Trace("thm-db-debug") << "Is " << q << " a relevant theorem?" << std::endl; @@ -570,7 +570,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) { isSubsume = true; //set inactive (will be ignored by other modules) - d_quantEngine->getModel()->setQuantifierActive( q, false ); + m->setQuantifierActive(q, false); } else { @@ -1103,7 +1103,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< if( n.getNumChildren()>0 ){ Trace("sg-gt-enum-debug") << "Get enumerate uf terms " << n << " (" << num << ")" << std::endl; - TermEnumeration* te = d_quantEngine->getTermRegistry().getTermEnumeration(); + TermEnumeration* te = d_treg.getTermEnumeration(); // below, we do a fair enumeration of vectors vec of indices whose sum is // 1,2,3, ... std::vector< int > vec; diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index eaf7ff172..6b4df3df8 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -439,7 +439,8 @@ private: //information about ground equivalence classes ConjectureGenerator(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr); + QuantifiersRegistry& qr, + TermRegistry& tr); ~ConjectureGenerator(); /* needs check */ diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index 9153d9280..2298eb253 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -37,7 +37,7 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, qe), + : QuantifiersModule(qs, qim, qr, tr, qe), d_instStrategies(), d_isup(), d_i_ag(), diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 0a035a691..3c871014a 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -26,7 +26,6 @@ #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" using namespace CVC4; @@ -90,8 +89,9 @@ BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, + TermRegistry& tr, DecisionManager* dm) - : QuantifiersModule(qs, qim, qr, qe), d_dm(dm) + : QuantifiersModule(qs, qim, qr, tr, qe), d_dm(dm) { } @@ -573,10 +573,10 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node getBounds( f, v, rsi, l, u ); Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl; if( !l.isNull() ){ - l = d_quantEngine->getModel()->getValue( l ); + l = d_treg.getModel()->getValue(l); } if( !u.isNull() ){ - u = d_quantEngine->getModel()->getValue( u ); + u = d_treg.getModel()->getValue(u); } Trace("bound-int-rsi") << "Value is " << l << " ... " << u << std::endl; return; @@ -631,7 +631,7 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) { Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl; Assert(!expr::hasFreeVar(sr)); Node sro = sr; - sr = d_quantEngine->getModel()->getValue(sr); + sr = d_treg.getModel()->getValue(sr); // if non-constant, then sr does not occur in the model, we fail if (!sr.isConst()) { diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index fd32b3555..cb64978bb 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -24,6 +24,7 @@ #include "context/context.h" #include "expr/attribute.h" #include "theory/decision_strategy.h" +#include "theory/quantifiers/quant_bound_inference.h" namespace CVC4 { namespace theory { @@ -167,6 +168,7 @@ private: QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, + TermRegistry& tr, DecisionManager* dm); virtual ~BoundedIntegers(); diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index b05f25b5e..85a2622b7 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -34,8 +34,9 @@ namespace quantifiers { ModelEngine::ModelEngine(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr) - : QuantifiersModule(qs, qim, qr, qe), + QuantifiersRegistry& qr, + TermRegistry& tr) + : QuantifiersModule(qs, qim, qr, tr, qe), d_incomplete_check(true), d_addedLemmas(0), d_triedLemmas(0), diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index d0c0da4dd..0188de06f 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -46,7 +46,8 @@ public: ModelEngine(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr); + QuantifiersRegistry& qr, + TermRegistry& tr); virtual ~ModelEngine(); public: diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index f2a41975f..007c37b20 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -33,8 +33,9 @@ InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, + TermRegistry& tr, RelevantDomain* rd) - : QuantifiersModule(qs, qim, qr, qe), d_rd(rd), d_fullSaturateLimit(-1) + : QuantifiersModule(qs, qim, qr, tr, qe), d_rd(rd), d_fullSaturateLimit(-1) { } void InstStrategyEnum::presolve() diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index 92e5ec71b..c97d8d1f4 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -65,6 +65,7 @@ class InstStrategyEnum : public QuantifiersModule QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, + TermRegistry& tr, RelevantDomain* rd); ~InstStrategyEnum() {} /** Presolve */ diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 52096a8ec..ba1c3ddab 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1857,8 +1857,9 @@ bool MatchGen::isHandled( TNode n ) { QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr) - : QuantifiersModule(qs, qim, qr, qe), + QuantifiersRegistry& qr, + TermRegistry& tr) + : QuantifiersModule(qs, qim, qr, tr, qe), d_conflict(qs.getSatContext(), false), d_true(NodeManager::currentNM()->mkConst(true)), d_false(NodeManager::currentNM()->mkConst(false)), diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 5b54f8055..818b99ea7 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -239,7 +239,8 @@ private: //for equivalence classes QuantConflictFind(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr); + QuantifiersRegistry& qr, + TermRegistry& tr); /** register quantifier */ void registerQuantifier(Node q) override; diff --git a/src/theory/quantifiers/quant_module.cpp b/src/theory/quantifiers/quant_module.cpp index c694d9c22..a3256ee31 100644 --- a/src/theory/quantifiers/quant_module.cpp +++ b/src/theory/quantifiers/quant_module.cpp @@ -13,10 +13,6 @@ **/ #include "theory/quantifiers/quant_module.h" -#include "theory/quantifiers/inst_match.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" using namespace CVC4::kind; @@ -27,8 +23,9 @@ QuantifiersModule::QuantifiersModule( quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, + quantifiers::TermRegistry& tr, QuantifiersEngine* qe) - : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr) + : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr) { } @@ -64,7 +61,7 @@ QuantifiersEngine* QuantifiersModule::getQuantifiersEngine() const quantifiers::TermDb* QuantifiersModule::getTermDatabase() const { - return d_quantEngine->getTermDatabase(); + return d_treg.getTermDatabase(); } quantifiers::QuantifiersState& QuantifiersModule::getState() diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h index 948f14407..d0c2d024e 100644 --- a/src/theory/quantifiers/quant_module.h +++ b/src/theory/quantifiers/quant_module.h @@ -24,6 +24,7 @@ #include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/quantifiers_state.h" +#include "theory/quantifiers/term_registry.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -63,6 +64,7 @@ class QuantifiersModule QuantifiersModule(quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, + quantifiers::TermRegistry& tr, QuantifiersEngine* qe); virtual ~QuantifiersModule() {} /** Presolve. @@ -169,12 +171,14 @@ class QuantifiersModule protected: /** pointer to the quantifiers engine that owns this module */ QuantifiersEngine* d_quantEngine; - /** The state of the quantifiers engine */ + /** Reference to the state of the quantifiers engine */ quantifiers::QuantifiersState& d_qstate; - /** The quantifiers inference manager */ + /** Reference to the quantifiers inference manager */ quantifiers::QuantifiersInferenceManager& d_qim; - /** The quantifiers registry */ + /** Reference to the quantifiers registry */ quantifiers::QuantifiersRegistry& d_qreg; + /** Reference to the term registry */ + quantifiers::TermRegistry& d_treg; }; /* class QuantifiersModule */ } // namespace theory diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 55f3469d2..23087286b 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -31,8 +31,9 @@ using namespace CVC4::theory::quantifiers; QuantDSplit::QuantDSplit(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr) - : QuantifiersModule(qs, qim, qr, qe), d_added_split(qs.getUserContext()) + QuantifiersRegistry& qr, + TermRegistry& tr) + : QuantifiersModule(qs, qim, qr, tr, qe), d_added_split(qs.getUserContext()) { } diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index d91b00146..13af881ee 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -52,7 +52,8 @@ class QuantDSplit : public QuantifiersModule { QuantDSplit(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr); + QuantifiersRegistry& qr, + TermRegistry& tr); /** determine whether this quantified formula will be reduced */ void checkOwnership(Node q) override; /* whether this module needs to check this round */ diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index 1a7697608..f9467f7d8 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -51,12 +51,12 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe, // add quantifiers modules if (options::quantConflictFind()) { - d_qcf.reset(new QuantConflictFind(qe, qs, qim, qr)); + d_qcf.reset(new QuantConflictFind(qe, qs, qim, qr, tr)); modules.push_back(d_qcf.get()); } if (options::conjectureGen()) { - d_sg_gen.reset(new ConjectureGenerator(qe, qs, qim, qr)); + d_sg_gen.reset(new ConjectureGenerator(qe, qs, qim, qr, tr)); modules.push_back(d_sg_gen.get()); } if (!options::finiteModelFind() || options::fmfInstEngine()) @@ -66,24 +66,24 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe, } if (options::cegqi()) { - d_i_cbqi.reset(new InstStrategyCegqi(qe, qs, qim, qr)); + d_i_cbqi.reset(new InstStrategyCegqi(qe, qs, qim, qr, tr)); modules.push_back(d_i_cbqi.get()); qim.getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter()); } if (options::sygus()) { - d_synth_e.reset(new SynthEngine(qe, qs, qim, qr)); + d_synth_e.reset(new SynthEngine(qe, qs, qim, qr, tr)); modules.push_back(d_synth_e.get()); } // finite model finding if (options::fmfBound()) { - d_bint.reset(new BoundedIntegers(qe, qs, qim, qr, dm)); + d_bint.reset(new BoundedIntegers(qe, qs, qim, qr, tr, dm)); modules.push_back(d_bint.get()); } if (options::finiteModelFind() || options::fmfBound()) { - d_model_engine.reset(new ModelEngine(qe, qs, qim, qr)); + d_model_engine.reset(new ModelEngine(qe, qs, qim, qr, tr)); modules.push_back(d_model_engine.get()); Trace("quant-init-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " @@ -102,7 +102,7 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe, } if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE) { - d_qsplit.reset(new QuantDSplit(qe, qs, qim, qr)); + d_qsplit.reset(new QuantDSplit(qe, qs, qim, qr, tr)); modules.push_back(d_qsplit.get()); } if (options::quantAlphaEquiv()) @@ -113,12 +113,12 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe, if (options::fullSaturateQuant() || options::fullSaturateInterleave()) { d_rel_dom.reset(new RelevantDomain(qe, qr)); - d_fs.reset(new InstStrategyEnum(qe, qs, qim, qr, d_rel_dom.get())); + d_fs.reset(new InstStrategyEnum(qe, qs, qim, qr, tr, d_rel_dom.get())); modules.push_back(d_fs.get()); } if (options::sygusInst()) { - d_sygus_inst.reset(new SygusInst(qe, qs, qim, qr)); + d_sygus_inst.reset(new SygusInst(qe, qs, qim, qr, tr)); modules.push_back(d_sygus_inst.get()); } } diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 98475911c..d77a42a14 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -20,7 +20,6 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" using namespace CVC4::kind; using namespace std; @@ -32,9 +31,10 @@ namespace quantifiers { SynthEngine::SynthEngine(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr) - : QuantifiersModule(qs, qim, qr, qe), - d_tds(qe->getTermDatabaseSygus()), + QuantifiersRegistry& qr, + TermRegistry& tr) + : QuantifiersModule(qs, qim, qr, tr, qe), + d_tds(tr.getTermDatabaseSygus()), d_conj(nullptr), d_sqp(qe) { diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index dcc5dd085..a4bed1737 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -36,7 +36,8 @@ class SynthEngine : public QuantifiersModule SynthEngine(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr); + QuantifiersRegistry& qr, + TermRegistry& tr); ~SynthEngine(); /** presolve * diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 52a2787f7..c5f9b44b0 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -186,8 +186,9 @@ void addSpecialValues( SygusInst::SygusInst(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr) - : QuantifiersModule(qs, qim, qr, qe), + QuantifiersRegistry& qr, + TermRegistry& tr) + : QuantifiersModule(qs, qim, qr, tr, qe), d_ce_lemma_added(qs.getUserContext()), d_global_terms(qs.getUserContext()), d_notified_assertions(qs.getUserContext()) @@ -209,7 +210,7 @@ void SygusInst::reset_round(Theory::Effort e) d_active_quant.clear(); d_inactive_quant.clear(); - FirstOrderModel* model = d_quantEngine->getModel(); + FirstOrderModel* model = d_treg.getModel(); uint32_t nasserted = model->getNumAssertedQuantifiers(); for (uint32_t i = 0; i < nasserted; ++i) @@ -245,9 +246,9 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e) if (quant_e != QEFFORT_STANDARD) return; - FirstOrderModel* model = d_quantEngine->getModel(); + FirstOrderModel* model = d_treg.getModel(); Instantiate* inst = d_qim.getInstantiate(); - TermDbSygus* db = d_quantEngine->getTermDatabaseSygus(); + TermDbSygus* db = d_treg.getTermDatabaseSygus(); SygusExplain syexplain(db); NodeManager* nm = NodeManager::currentNM(); options::SygusInstMode mode = options::sygusInstMode(); @@ -480,7 +481,7 @@ void SygusInst::registerCeLemma(Node q, std::vector& types) /* Generate counterexample lemma for 'q'. */ NodeManager* nm = NodeManager::currentNM(); - TermDbSygus* db = d_quantEngine->getTermDatabaseSygus(); + TermDbSygus* db = d_treg.getTermDatabaseSygus(); /* For each variable x_i of \forall x_i . P[x_i], create a fresh datatype * instantiation constant ic_i with type types[i] and wrap each ic_i in diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h index 413c9f3a7..dc8bc9c10 100644 --- a/src/theory/quantifiers/sygus_inst.h +++ b/src/theory/quantifiers/sygus_inst.h @@ -66,7 +66,8 @@ class SygusInst : public QuantifiersModule SygusInst(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, - QuantifiersRegistry& qr); + QuantifiersRegistry& qr, + TermRegistry& tr); ~SygusInst() = default; bool needsCheck(Theory::Effort e) override; -- 2.30.2