From 77b75a69e51b742e1448d754b6886c10ef76e79f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 24 Mar 2021 17:44:52 -0500 Subject: [PATCH] Use inference manager to access intantiate utility instead of quantifiers engine (#6198) Towards breaking dependencies on quantifers engine. --- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 35 +++++++++---------- .../quantifiers/conjecture_generator.cpp | 5 +-- .../quantifiers/ematching/ho_trigger.cpp | 14 ++++---- .../quantifiers/ematching/im_generator.h | 32 ++++++++--------- .../ematching/inst_match_generator_simple.h | 16 ++++----- src/theory/quantifiers/ematching/trigger.cpp | 2 +- .../quantifiers/fmf/full_model_check.cpp | 10 +++--- src/theory/quantifiers/fmf/full_model_check.h | 4 ++- src/theory/quantifiers/fmf/model_builder.cpp | 11 +++--- src/theory/quantifiers/fmf/model_builder.h | 9 +++-- src/theory/quantifiers/fmf/model_engine.cpp | 2 +- .../quantifiers/inst_strategy_enumerative.cpp | 2 +- .../quantifiers/quant_conflict_find.cpp | 15 ++++++-- src/theory/quantifiers/quant_conflict_find.h | 4 +++ .../quantifiers/quantifiers_modules.cpp | 8 ++--- .../sygus/ce_guided_single_inv.cpp | 3 +- .../quantifiers/sygus/synth_conjecture.cpp | 2 +- src/theory/quantifiers/sygus_inst.cpp | 2 +- src/theory/quantifiers_engine.cpp | 22 +++++------- src/theory/quantifiers_engine.h | 12 +++---- 20 files changed, 108 insertions(+), 102 deletions(-) diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index dcc0e885b..2c0fba7a6 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -471,32 +471,29 @@ Node InstStrategyCegqi::getCounterexampleLiteral(Node q) bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { Assert(!d_curr_quant.isNull()); + Instantiate* inst = d_qim.getInstantiate(); //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma if (d_qreg.getQuantAttributes().isQuantElimPartial(d_curr_quant)) { d_cbqi_set_quant_inactive = true; d_incomplete_check = true; - d_quantEngine->getInstantiate()->recordInstantiation( - d_curr_quant, subs, false, false); + inst->recordInstantiation(d_curr_quant, subs, false, false); return true; - }else{ - //check if we need virtual term substitution (if used delta or infinity) - bool used_vts = d_vtsCache->containsVtsTerm(subs, false); - if (d_quantEngine->getInstantiate()->addInstantiation( - d_curr_quant, - subs, - InferenceId::QUANTIFIERS_INST_CEGQI, - false, - false, - used_vts)) - { - return true; - }else{ - //this should never happen for monotonic selection strategies - Trace("cegqi-warn") << "WARNING: Existing instantiation" << std::endl; - return false; - } } + // check if we need virtual term substitution (if used delta or infinity) + bool used_vts = d_vtsCache->containsVtsTerm(subs, false); + if (inst->addInstantiation(d_curr_quant, + subs, + InferenceId::QUANTIFIERS_INST_CEGQI, + false, + false, + used_vts)) + { + return true; + } + // this should never happen for monotonic selection strategies + Trace("cegqi-warn") << "WARNING: Existing instantiation" << std::endl; + return false; } bool InstStrategyCegqi::addPendingLemma(Node lem) const diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index f1ed9fe00..04ab464f8 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -21,6 +21,7 @@ #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" @@ -602,7 +603,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) //check each skolem variable bool disproven = true; std::vector skolems; - d_quantEngine->getSkolemize()->getSkolemConstants(q, skolems); + d_qim.getSkolemize()->getSkolemConstants(q, skolems); Trace("sg-conjecture") << " CONJECTURE : "; std::vector< Node > ce; for (unsigned j = 0; j < skolems.size(); j++) @@ -1102,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->getTermEnumeration(); + TermEnumeration* te = d_quantEngine->getTermRegistry().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/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 6206b24a7..4cdce940e 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -20,6 +20,7 @@ #include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/quantifiers_state.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/uf/theory_uf_rewriter.h" @@ -236,7 +237,6 @@ bool HigherOrderTrigger::sendInstantiation(std::vector& m, InferenceId id) d_lchildren.clear(); d_arg_to_arg_rep.clear(); d_arg_vector.clear(); - QuantifiersState& qs = d_quantEngine->getState(); for (std::pair >& ha : ho_var_apps_subs) { TNode var = ha.first; @@ -288,9 +288,9 @@ bool HigherOrderTrigger::sendInstantiation(std::vector& m, InferenceId id) } else if (!itf->second.isNull()) { - if (!qs.areEqual(itf->second, args[k])) + if (!d_qstate.areEqual(itf->second, args[k])) { - if (!d_quantEngine->getTermDatabase()->isEntailed( + if (!d_treg.getTermDatabase()->isEntailed( itf->second.eqNode(args[k]), true)) { fixed_vals[k] = Node::null(); @@ -323,7 +323,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector& m, InferenceId id) { if (!itf->second.isNull()) { - Node r = qs.getRepresentative(itf->second); + Node r = d_qstate.getRepresentative(itf->second); std::map::iterator itfr = arg_to_rep.find(r); if (itfr != arg_to_rep.end()) { @@ -375,7 +375,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector& m, InferenceId id) else { // do not run higher-order matching - return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m, id); + return d_qim.getInstantiate()->addInstantiation(d_quant, m, id); } } @@ -389,7 +389,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector& m, if (var_index == d_ho_var_list.size()) { // we now have an instantiation to try - return d_quantEngine->getInstantiate()->addInstantiation( + return d_qim.getInstantiate()->addInstantiation( d_quant, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_HO); } else @@ -476,7 +476,7 @@ uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas() Trace("ho-quant-trigger") << "addHoTypeMatchPredicateLemmas..." << std::endl; uint64_t numLemmas = 0; // this forces expansion of APPLY_UF terms to curried HO_APPLY chains - TermDb* tdb = d_quantEngine->getTermDatabase(); + TermDb* tdb = d_treg.getTermDatabase(); unsigned size = tdb->getNumOperators(); NodeManager* nm = NodeManager::currentNM(); for (unsigned j = 0; j < size; j++) diff --git a/src/theory/quantifiers/ematching/im_generator.h b/src/theory/quantifiers/ematching/im_generator.h index 0d0f9498d..efc65cdef 100644 --- a/src/theory/quantifiers/ematching/im_generator.h +++ b/src/theory/quantifiers/ematching/im_generator.h @@ -36,22 +36,22 @@ namespace inst { class Trigger; /** IMGenerator class -* -* Virtual base class for generating InstMatch objects, which correspond to -* quantifier instantiations. The main use of this class is as a backend utility -* to Trigger (see theory/quantifiers/ematching/trigger.h). -* -* Some functions below take as argument a pointer to the current quantifiers -* engine, which is used for making various queries about what terms and -* equalities exist in the current context. -* -* Some functions below take a pointer to a parent Trigger object, which is used -* to post-process and finalize the instantiations through -* sendInstantiation(...), where the parent trigger will make calls to -* qe->getInstantiate()->addInstantiation(...). The latter function is the entry -* point in which instantiate lemmas are enqueued to be sent on the output -* channel. -*/ + * + * Virtual base class for generating InstMatch objects, which correspond to + * quantifier instantiations. The main use of this class is as a backend utility + * to Trigger (see theory/quantifiers/ematching/trigger.h). + * + * Some functions below take as argument a pointer to the current quantifiers + * engine, which is used for making various queries about what terms and + * equalities exist in the current context. + * + * Some functions below take a pointer to a parent Trigger object, which is used + * to post-process and finalize the instantiations through + * sendInstantiation(...), where the parent trigger will make calls to + * Instantiate::addInstantiation(...). The latter function is the entry + * point in which instantiate lemmas are enqueued to be sent on the output + * channel. + */ class IMGenerator { public: IMGenerator(Trigger* tparent); diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h index ad48d9c91..6ae2f915b 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h @@ -41,10 +41,6 @@ namespace inst { * The implementation traverses the term indices in TermDatabase for adding * instantiations, which is more efficient than the techniques required for * handling non-simple single triggers. - * - * In contrast to other instantiation generators, it does not call - * IMGenerator::sendInstantiation and for performance reasons instead calls - * qe->getInstantiate()->addInstantiation(...) directly. */ class InstMatchGeneratorSimple : public IMGenerator { @@ -88,12 +84,12 @@ class InstMatchGeneratorSimple : public IMGenerator std::map d_var_num; /** add instantiations, helper function. * - * m is the current match we are building, - * addedLemmas is the number of lemmas we have added via calls to - * qe->getInstantiate()->aaddInstantiation(...), - * argIndex is the argument index in d_match_pattern we are currently - * matching, - * tat is the term index we are currently traversing. + * @param m the current match we are building, + * @param addedLemmas the number of lemmas we have added via calls to + * Instantiate::addInstantiation(...), + * @param argIndex the argument index in d_match_pattern we are currently + * matching, + * @param tat the term index we are currently traversing. */ void addInstantiations(InstMatch& m, uint64_t& addedLemmas, diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index af0a0bfbc..c93e1a99b 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -154,7 +154,7 @@ uint64_t Trigger::addInstantiations() bool Trigger::sendInstantiation(std::vector& m, InferenceId id) { - return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m, id); + return d_qim.getInstantiate()->addInstantiation(d_quant, m, id); } bool Trigger::sendInstantiation(InstMatch& m, InferenceId id) diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 2245e16dd..dd28af380 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -284,8 +284,9 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) { } FullModelChecker::FullModelChecker(QuantifiersState& qs, - QuantifiersRegistry& qr) - : QModelBuilder(qs, qr) + QuantifiersRegistry& qr, + QuantifiersInferenceManager& qim) + : QModelBuilder(qs, qr, qim) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -628,7 +629,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i Trace("fmc") << std::endl; // consider all entries going to non-true - Instantiate* instq = d_qe->getInstantiate(); + Instantiate* instq = d_qim.getInstantiate(); for (unsigned i = 0, msize = mcond.size(); i < msize; i++) { if (d_quant_models[f].d_value[i] == d_true) @@ -833,6 +834,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc* fm, Trace("fmc-exh-debug") << "Set element domains..." << std::endl; int addedLemmas = 0; //now do full iteration + Instantiate* ie = d_qim.getInstantiate(); while( !riter.isFinished() ){ d_triedLemmas++; Trace("fmc-exh-debug") << "Inst : "; @@ -858,7 +860,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc* fm, if (ev!=d_true) { Trace("fmc-exh-debug") << ", add!"; //add as instantiation - if (d_qe->getInstantiate()->addInstantiation( + if (ie->addInstantiation( f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH, true)) { Trace("fmc-exh-debug") << " ...success."; diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index 904a1b9a0..972c977e8 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -154,7 +154,9 @@ protected: Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ); public: - FullModelChecker(QuantifiersState& qs, QuantifiersRegistry& qr); + FullModelChecker(QuantifiersState& qs, + QuantifiersRegistry& qr, + QuantifiersInferenceManager& qim); void debugPrintCond(const char * tr, Node n, bool dispStar = false); void debugPrint(const char * tr, Node n, bool dispStar = false); diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index 9aa687fbd..a24f72e32 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -30,13 +30,15 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -QModelBuilder::QModelBuilder(QuantifiersState& qs, QuantifiersRegistry& qr) +QModelBuilder::QModelBuilder(QuantifiersState& qs, + QuantifiersRegistry& qr, + QuantifiersInferenceManager& qim) : TheoryEngineModelBuilder(), d_addedLemmas(0), d_triedLemmas(0), - d_qe(nullptr), d_qstate(qs), - d_qreg(qr) + d_qreg(qr), + d_qim(qim) { } @@ -96,6 +98,7 @@ void QModelBuilder::debugModel( TheoryModel* m ){ int tests = 0; int bad = 0; QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference(); + Instantiate* inst = d_qim.getInstantiate(); for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); std::vector< Node > vars; @@ -112,7 +115,7 @@ void QModelBuilder::debugModel( TheoryModel* m ){ { terms.push_back( riter.getCurrentTerm( k ) ); } - Node n = d_qe->getInstantiate()->getInstantiation(f, vars, terms); + Node n = inst->getInstantiation(f, vars, terms); Node val = fm->getValue( n ); if (!val.isConst() || !val.getConst()) { diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index 7ba7a66e2..af5dee3cf 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -28,6 +28,7 @@ namespace quantifiers { class FirstOrderModel; class QuantifiersState; class QuantifiersRegistry; +class QuantifiersInferenceManager; class QModelBuilder : public TheoryEngineModelBuilder { @@ -40,9 +41,9 @@ class QModelBuilder : public TheoryEngineModelBuilder unsigned d_triedLemmas; public: - QModelBuilder(QuantifiersState& qs, QuantifiersRegistry& qr); - //!!!!!!!!!!!!!!!!!!!!! temporary (project #15) - void finishInit(QuantifiersEngine* qe) { d_qe = qe; } + QModelBuilder(QuantifiersState& qs, + QuantifiersRegistry& qr, + QuantifiersInferenceManager& qim); //do exhaustive instantiation // 0 : failed, but resorting to true exhaustive instantiation may work @@ -66,6 +67,8 @@ class QModelBuilder : public TheoryEngineModelBuilder QuantifiersState& d_qstate; /** Reference to the quantifiers registry */ QuantifiersRegistry& d_qreg; + /** The quantifiers inference manager */ + quantifiers::QuantifiersInferenceManager& d_qim; }; }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index eb7398f92..b05f25b5e 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -279,7 +279,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ if( !riter.isIncomplete() ){ int triedLemmas = 0; int addedLemmas = 0; - Instantiate* inst = d_quantEngine->getInstantiate(); + Instantiate* inst = d_qim.getInstantiate(); while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ //instantiation was not shown to be true, construct the match InstMatch m( f ); diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index c14ce4ad3..c58bcc863 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -194,7 +194,7 @@ bool InstStrategyEnum::process(Node quantifier, bool fullEffort, bool isRd) mkTermTupleEnumerator(quantifier, &ttec)); std::vector terms; std::vector failMask; - Instantiate* ie = d_quantEngine->getInstantiate(); + Instantiate* ie = d_qim.getInstantiate(); for (enumerator->init(); enumerator->hasNext();) { if (d_qstate.isInConflict()) diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 7bf7cc09b..62f15a6a6 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -37,7 +37,10 @@ namespace CVC4 { namespace theory { namespace quantifiers { -QuantInfo::QuantInfo() : d_unassigned_nvar(0), d_una_index(0), d_mg(nullptr) {} +QuantInfo::QuantInfo() + : d_unassigned_nvar(0), d_una_index(0), d_parent(nullptr), d_mg(nullptr) +{ +} QuantInfo::~QuantInfo() { delete d_mg; @@ -49,8 +52,14 @@ QuantInfo::~QuantInfo() { d_var_mg.clear(); } +QuantifiersInferenceManager& QuantInfo::getInferenceManager() +{ + Assert(d_parent != nullptr); + return d_parent->getInferenceManager(); +} void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) { + d_parent = p; d_q = q; d_extra_var.clear(); for( unsigned i=0; id_quantEngine->getInstantiate()->getInstantiation(d_q, terms); + getInferenceManager().getInstantiate()->getInstantiation(d_q, terms); inst = Rewriter::rewrite(inst); Node inst_eval = p->getTermDatabase()->evaluateTerm( inst, options::qcfTConstraint(), true); @@ -2107,7 +2116,7 @@ void QuantConflictFind::checkQuantifiedFormula(Node q, } // try to make a matches making the body false or propagating Trace("qcf-check-debug") << "Get next match..." << std::endl; - Instantiate* qinst = d_quantEngine->getInstantiate(); + Instantiate* qinst = d_qim.getInstantiate(); while (qi->getNextMatch(this)) { if (d_qstate.isInConflict()) diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index fe9aa411b..5b54f8055 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -131,6 +131,8 @@ public: public: QuantInfo(); ~QuantInfo(); + /** Get quantifiers inference manager */ + QuantifiersInferenceManager& getInferenceManager(); std::vector< TNode > d_vars; std::vector< TypeNode > d_var_types; std::map< TNode, int > d_var_num; @@ -143,6 +145,8 @@ public: typedef std::map< int, MatchGen * > VarMgMap; private: + /** The parent who owns this class */ + QuantConflictFind* d_parent; MatchGen * d_mg; VarMgMap d_var_mg; public: diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index bb35d6d26..1a7697608 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -68,7 +68,7 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe, { d_i_cbqi.reset(new InstStrategyCegqi(qe, qs, qim, qr)); modules.push_back(d_i_cbqi.get()); - qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter()); + qim.getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter()); } if (options::sygus()) { @@ -91,16 +91,14 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe, if (tr.useFmcModel()) { Trace("quant-init-debug") << "...make fmc builder." << std::endl; - d_builder.reset(new fmcheck::FullModelChecker(qs, qr)); + d_builder.reset(new fmcheck::FullModelChecker(qs, qr, qim)); } else { Trace("quant-init-debug") << "...make default model builder." << std::endl; - d_builder.reset(new QModelBuilder(qs, qr)); + d_builder.reset(new QModelBuilder(qs, qr, qim)); } - // !!!!!!!!!!!!! temporary (project #15) - d_builder->finishInit(qe); } if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE) { diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index f93260f0c..066bcd769 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -27,6 +27,7 @@ #include "theory/quantifiers/sygus/sygus_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.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" @@ -348,7 +349,7 @@ Node CegSingleInv::getSolutionFromInst(size_t index) ptn = ptn.getRangeType(); } Trace("csi-sol") << "Get solution for (unconstrained) " << prog << std::endl; - s = d_qe->getTermEnumeration()->getEnumerateTerm(ptn, 0); + s = d_qe->getTermRegistry().getTermEnumeration()->getEnumerateTerm(ptn, 0); } else { diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 831216445..a0058f2d8 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -178,7 +178,7 @@ void SynthConjecture::assign(Node q) Trace("cegqi") << "Base quantified formula is : " << d_embed_quant << std::endl; // construct base instantiation - d_base_inst = Rewriter::rewrite(d_qe->getInstantiate()->getInstantiation( + d_base_inst = Rewriter::rewrite(d_qim.getInstantiate()->getInstantiation( d_embed_quant, vars, d_candidates)); if (!d_embedSideCondition.isNull()) { diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index bbc13b463..52a2787f7 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -246,7 +246,7 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e) if (quant_e != QEFFORT_STANDARD) return; FirstOrderModel* model = d_quantEngine->getModel(); - Instantiate* inst = d_quantEngine->getInstantiate(); + Instantiate* inst = d_qim.getInstantiate(); TermDbSygus* db = d_quantEngine->getTermDatabaseSygus(); SygusExplain syexplain(db); NodeManager* nm = NodeManager::currentNM(); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 2cface166..0155eb05a 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -112,6 +112,10 @@ quantifiers::QuantifiersRegistry& QuantifiersEngine::getQuantifiersRegistry() { return d_qreg; } +quantifiers::TermRegistry& QuantifiersEngine::getTermRegistry() +{ + return d_treg; +} quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const { @@ -124,26 +128,16 @@ quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const /// !!!!!!!!!!!!!! temporary (project #15) -quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const -{ - return d_treg.getTermDatabase(); -} quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() const { return d_treg.getTermDatabaseSygus(); } -quantifiers::TermEnumeration* QuantifiersEngine::getTermEnumeration() const -{ - return d_treg.getTermEnumeration(); -} -quantifiers::Instantiate* QuantifiersEngine::getInstantiate() const -{ - return d_qim.getInstantiate(); -} -quantifiers::Skolemize* QuantifiersEngine::getSkolemize() const + +quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const { - return d_qim.getSkolemize(); + return d_treg.getTermDatabase(); } + quantifiers::inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const { return d_tr_trie.get(); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 1f1dcc950..cb60c8e88 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -80,22 +80,18 @@ class QuantifiersEngine { quantifiers::QuantifiersInferenceManager& getInferenceManager(); /** The quantifiers registry */ quantifiers::QuantifiersRegistry& getQuantifiersRegistry(); + /** The term registry */ + quantifiers::TermRegistry& getTermRegistry(); //---------------------- end external interface //---------------------- utilities /** get the model builder */ quantifiers::QModelBuilder* getModelBuilder() const; - /** get model */ - quantifiers::FirstOrderModel* getModel() const; /** get term database */ quantifiers::TermDb* getTermDatabase() const; + /** get model */ + quantifiers::FirstOrderModel* getModel() const; /** get term database sygus */ quantifiers::TermDbSygus* getTermDatabaseSygus() const; - /** get term enumeration utility */ - quantifiers::TermEnumeration* getTermEnumeration() const; - /** get instantiate utility */ - quantifiers::Instantiate* getInstantiate() const; - /** get skolemize utility */ - quantifiers::Skolemize* getSkolemize() const; /** get trigger database */ quantifiers::inst::TriggerTrie* getTriggerDatabase() const; //---------------------- end utilities -- 2.30.2