From 28869764c41725a0c98df4f1b8de5bfd618551c3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 26 Apr 2022 14:56:40 -0500 Subject: [PATCH] Refactor mkRep option for instantiation (#8657) This removes mkRep as an option for addInstantiation. It adds a new interface for making term vectors representative, which is required for FMF instantiation. --- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 1 - .../quantifiers/fmf/full_model_check.cpp | 12 ++-- src/theory/quantifiers/fmf/model_engine.cpp | 49 ++++++++-------- src/theory/quantifiers/instantiate.cpp | 58 +++++++++++++------ src/theory/quantifiers/instantiate.h | 9 +-- 5 files changed, 75 insertions(+), 54 deletions(-) diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 37aeaedcb..7760b9391 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -521,7 +521,6 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { subs, InferenceId::QUANTIFIERS_INST_CEGQI, Node::null(), - false, usedVts)) { return true; diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 3c5ec49ac..c21ed4393 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -745,11 +745,9 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i } // just add the instance d_triedLemmas++; - if (instq->addInstantiation(f, - inst, - InferenceId::QUANTIFIERS_INST_FMF_FMC, - Node::null(), - true)) + instq->processInstantiationRep(f, inst); + if (instq->addInstantiation( + f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC, Node::null())) { Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; d_addedLemmas++; @@ -898,11 +896,11 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc* fm, if (ev!=d_true) { Trace("fmc-exh-debug") << ", add!"; //add as instantiation + ie->processInstantiationRep(f, inst); if (ie->addInstantiation(f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH, - Node::null(), - true)) + Node::null())) { Trace("fmc-exh-debug") << " ...success."; addedLemmas++; diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 7cb2a348b..a295c3005 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -266,18 +266,17 @@ int ModelEngine::checkModel(){ return d_addedLemmas; } - - -void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ +void ModelEngine::exhaustiveInstantiate(Node q, int effort) +{ //first check if the builder can do the exhaustive instantiation unsigned prev_alem = d_builder->getNumAddedLemmas(); unsigned prev_tlem = d_builder->getNumTriedLemmas(); FirstOrderModel* fm = d_treg.getModel(); - int retEi = d_builder->doExhaustiveInstantiation(fm, f, effort); + int retEi = d_builder->doExhaustiveInstantiation(fm, q, effort); if( retEi!=0 ){ if( retEi<0 ){ Trace("fmf-exh-inst") << "-> Builder determined complete instantiation was impossible." << std::endl; - d_incompleteQuants.insert(f); + d_incompleteQuants.insert(q); }else{ Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl; } @@ -286,9 +285,10 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ }else{ if( TraceIsOn("fmf-exh-inst-debug") ){ Trace("fmf-exh-inst-debug") << " Instantiation Constants: "; - for( size_t i=0; igetRepSet(), &qrbe); - if( riter.setQuantifier( f ) ){ + if (riter.setQuantifier(q)) + { Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl; if( !riter.isIncomplete() ){ int triedLemmas = 0; @@ -306,20 +307,18 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ !riter.isFinished() && (addedLemmas == 0 || !options().quantifiers.fmfOneInstPerRound)) { - //instantiation was not shown to be true, construct the match - InstMatch m( f ); - for (unsigned i = 0; i < riter.getNumTerms(); i++) - { - m.set(d_qstate, i, riter.getCurrentTerm(i)); - } - Trace("fmf-model-eval") << "* Add instantiation " << m << std::endl; + // instantiation was not shown to be true, construct the term vector + std::vector terms; + riter.getCurrentTerms(terms); + Trace("fmf-model-eval") + << "* Add instantiation " << terms << std::endl; triedLemmas++; //add as instantiation - if (inst->addInstantiation(f, - m.d_vals, + inst->processInstantiationRep(q, terms); + if (inst->addInstantiation(q, + terms, InferenceId::QUANTIFIERS_INST_FMF_EXH, - Node::null(), - true)) + Node::null())) { addedLemmas++; if (d_qstate.isInConflict()) @@ -327,19 +326,23 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ break; } }else{ - Trace("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl; + Trace("fmf-model-eval") + << "* Failed Add instantiation " << terms << std::endl; } riter.increment(); } d_addedLemmas += addedLemmas; d_triedLemmas += triedLemmas; } - }else{ + } + else + { Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl; } //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round - if( riter.isIncomplete() ){ - d_incompleteQuants.insert(f); + if (riter.isIncomplete()) + { + d_incompleteQuants.insert(q); } } } diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 7fa845d35..23abba94a 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -101,19 +101,28 @@ bool Instantiate::addInstantiation(Node q, std::vector& terms, InferenceId id, Node pfArg, - bool mkRep, bool doVts) { // For resource-limiting (also does a time check). d_qim.safePoint(Resource::QuantifierStep); Assert(!d_qstate.isInConflict()); + Assert(q.getKind() == FORALL); Assert(terms.size() == q[0].getNumChildren()); - Trace("inst-add-debug") << "For quantified formula " << q - << ", add instantiation: " << std::endl; - for (unsigned i = 0, size = terms.size(); i < size; i++) + if (TraceIsOn("inst-add-debug")) + { + Trace("inst-add-debug") << "For quantified formula " << q + << ", add instantiation: " << std::endl; + for (size_t i = 0, size = terms.size(); i < size; i++) + { + Trace("inst-add-debug") << " " << q[0][i]; + Trace("inst-add-debug") << " -> " << terms[i]; + Trace("inst-add-debug") << std::endl; + } + Trace("inst-add-debug") << "id is " << id << std::endl; + } + // ensure the terms are non-null and well-typed + for (size_t i = 0, size = terms.size(); i < size; i++) { - Trace("inst-add-debug") << " " << q[0][i]; - Trace("inst-add-debug2") << " -> " << terms[i]; TypeNode tn = q[0][i].getType(); if (terms[i].isNull()) { @@ -123,13 +132,6 @@ bool Instantiate::addInstantiation(Node q, // are cast to integers for { x -> t } where x has type Int and t has // type Real. terms[i] = ensureType(terms[i], tn); - if (mkRep) - { - // pick the best possible representative for instantiation, based on past - // use and simplicity of term - terms[i] = d_treg.getModel()->getInternalRepresentative(terms[i], q, i); - } - Trace("inst-add-debug") << " -> " << terms[i] << std::endl; if (terms[i].isNull()) { Trace("inst-add-debug") @@ -137,7 +139,12 @@ bool Instantiate::addInstantiation(Node q, << std::endl; return false; } + } #ifdef CVC5_ASSERTIONS + for (size_t i = 0, size = terms.size(); i < size; i++) + { + TypeNode tn = q[0][i].getType(); + Assert(!terms[i].isNull()); bool bad_inst = false; if (TermUtil::containsUninterpretedConstant(terms[i])) { @@ -181,9 +188,8 @@ bool Instantiate::addInstantiation(Node q, } Assert(false); } -#endif } - Trace("inst-add-debug") << "id is " << id << std::endl; +#endif EntailmentCheck* ec = d_treg.getEntailmentCheck(); // Note we check for entailment before checking for term vector duplication. @@ -220,7 +226,7 @@ bool Instantiate::addInstantiation(Node q, if (options().quantifiers.instMaxLevel != -1) { TermDb* tdb = d_treg.getTermDatabase(); - for (Node& t : terms) + for (const Node& t : terms) { if (!tdb->isTermEligibleForInstantiation(t, q)) { @@ -349,7 +355,7 @@ bool Instantiate::addInstantiation(Node q, if (TraceIsOn("inst")) { Trace("inst") << "*** Instantiate " << q << " with " << std::endl; - for (unsigned i = 0, size = terms.size(); i < size; i++) + for (size_t i = 0, size = terms.size(); i < size; i++) { if (TraceIsOn("inst")) { @@ -395,16 +401,30 @@ bool Instantiate::addInstantiation(Node q, return true; } +void Instantiate::processInstantiationRep(Node q, std::vector& terms) +{ + Assert(q.getKind() == FORALL); + Assert(terms.size() == q[0].getNumChildren()); + for (size_t i = 0, size = terms.size(); i < size; i++) + { + Assert(!terms[i].isNull()); + // pick the best possible representative for instantiation, based on past + // use and simplicity of term + terms[i] = d_treg.getModel()->getInternalRepresentative(terms[i], q, i); + // Note it may be a null representative here, it is then replaced + // by an arbitrary term if necessary during addInstantiation. + } +} + bool Instantiate::addInstantiationExpFail(Node q, std::vector& terms, std::vector& failMask, InferenceId id, Node pfArg, - bool mkRep, bool doVts, bool expFull) { - if (addInstantiation(q, terms, id, pfArg, mkRep, doVts)) + if (addInstantiation(q, terms, id, pfArg, doVts)) { return true; } diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index e41740eda..81f0d8af5 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -141,8 +141,6 @@ class Instantiate : public QuantifiersUtil * manager * @param pfArg an additional node to add to the arguments of the INSTANTIATE * step - * @param mkRep whether to take the representatives of the terms in the - * range of the substitution m, * @param doVts whether we must apply virtual term substitution to the * instantiation lemma. * @@ -162,7 +160,6 @@ class Instantiate : public QuantifiersUtil std::vector& terms, InferenceId id, Node pfArg = Node::null(), - bool mkRep = false, bool doVts = false); /** * Same as above, but we also compute a vector failMask indicating which @@ -192,9 +189,13 @@ class Instantiate : public QuantifiersUtil std::vector& failMask, InferenceId id, Node pfArg = Node::null(), - bool mkRep = false, bool doVts = false, bool expFull = true); + /** + * Ensure each term in terms is the chosen representative for its + * corresponding variable in q. + */ + void processInstantiationRep(Node q, std::vector& terms); /** record instantiation * * Explicitly record that q has been instantiated with terms, with virtual -- 2.30.2