From: Andrew Reynolds Date: Tue, 30 Mar 2021 15:05:29 +0000 (-0500) Subject: Implement simple tracking of instantiation lemmas (#6077) X-Git-Tag: cvc5-1.0.0~2009 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4948485775b04d95dbf69eee311bf452d0bfac3d;p=cvc5.git Implement simple tracking of instantiation lemmas (#6077) We require tracking of instantiation lemmas for quantifier elimination. Recently, this feature was removed in favor of reconstructing instantiations via substitutions. This does not quite work if instantiation lemmas have more complex post-processing, e.g. virtual term substitution. This PR reimplements a much simpler form of instantiation tracking that simply adds instantiation bodies to a vector, per quantified formula. It uses this vector for quantifier elimination. Fixes #5899. --- diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index 9a0178cfe..ba11319d3 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -99,21 +99,11 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, Assert(topq.getKind() == FORALL); Trace("smt-qe") << "Get qe based on preprocessed quantified formula " << topq << std::endl; - std::vector> insts; - qe->getInstantiationTermVectors(topq, insts); - std::vector vars(ne[0].begin(), ne[0].end()); - std::vector conjs; - // apply the instantiation on the original body - for (const std::vector& inst : insts) - { - // note we do not convert to witness form here, since we could be - // an internal subsolver - Subs s; - s.add(vars, inst); - Node c = s.apply(ne[1].negate()); - conjs.push_back(c); - } - ret = nm->mkAnd(conjs); + std::vector insts; + qe->getInstantiations(topq, insts); + // note we do not convert to witness form here, since we could be + // an internal subsolver (SmtEngine::isInternalSubsolver). + ret = nm->mkAnd(insts); Trace("smt-qe") << "QuantElimSolver returned : " << ret << std::endl; if (q.getKind() == EXISTS) { diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 3690cbcac..19821d347 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -473,23 +473,23 @@ Node InstStrategyCegqi::getCounterexampleLiteral(Node q) bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { Assert(!d_curr_quant.isNull()); + // check if we need virtual term substitution (if used delta or infinity) + bool usedVts = d_vtsCache->containsVtsTerm(subs, false); 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; - inst->recordInstantiation(d_curr_quant, subs, false, false); + inst->recordInstantiation(d_curr_quant, subs, usedVts); return true; } - // 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)) + else if (inst->addInstantiation(d_curr_quant, + subs, + InferenceId::QUANTIFIERS_INST_CEGQI, + false, + false, + usedVts)) { return true; } diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 61c7703ed..b74f4ae0f 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -51,7 +51,7 @@ Instantiate::Instantiate(QuantifiersState& qs, d_qreg(qr), d_treg(tr), d_pnm(pnm), - d_total_inst_debug(qs.getUserContext()), + d_insts(qs.getUserContext()), d_c_inst_match_trie_dom(qs.getUserContext()), d_pfInst(pnm ? new CDProof(pnm) : nullptr) { @@ -68,24 +68,16 @@ Instantiate::~Instantiate() bool Instantiate::reset(Theory::Effort e) { - if (!d_recorded_inst.empty()) - { - Trace("quant-engine-debug") << "Removing " << d_recorded_inst.size() - << " instantiations..." << std::endl; - // remove explicitly recorded instantiations - for (std::pair >& r : d_recorded_inst) - { - removeInstantiationInternal(r.first, r.second); - } - d_recorded_inst.clear(); - } + Trace("inst-debug") << "Reset, effort " << e << std::endl; + // clear explicitly recorded instantiations + d_recordedInst.clear(); return true; } void Instantiate::registerQuantifier(Node q) {} bool Instantiate::checkComplete() { - if (!d_recorded_inst.empty()) + if (!d_recordedInst.empty()) { Trace("quant-engine-debug") << "Set incomplete due to recorded instantiations." << std::endl; @@ -337,7 +329,10 @@ bool Instantiate::addInstantiation(Node q, return false; } - d_total_inst_debug[q] = d_total_inst_debug[q] + 1; + // add to list of instantiations + InstLemmaList* ill = getOrMkInstLemmaList(q); + ill->d_list.push_back(body); + // add to temporary debug statistics (# inst on this round) d_temp_inst_debug[q]++; if (Trace.isOn("inst")) { @@ -480,12 +475,16 @@ bool Instantiate::addInstantiationExpFail(Node q, return false; } -bool Instantiate::recordInstantiation(Node q, +void Instantiate::recordInstantiation(Node q, std::vector& terms, - bool modEq, - bool addedLem) + bool doVts) { - return recordInstantiationInternal(q, terms, modEq, addedLem); + Trace("inst-debug") << "Record instantiation for " << q << std::endl; + // get the instantiation list, which ensures that q is marked as a quantified + // formula we instantiated, despite only recording an instantiation here + getOrMkInstLemmaList(q); + Node inst = getInstantiation(q, terms, doVts); + d_recordedInst[q].push_back(inst); } bool Instantiate::existsInstantiation(Node q, @@ -562,14 +561,8 @@ Node Instantiate::getInstantiation(Node q, std::vector& terms, bool doVts) bool Instantiate::recordInstantiationInternal(Node q, std::vector& terms, - bool modEq, - bool addedLem) + bool modEq) { - if (!addedLem) - { - // record the instantiation for deletion later - d_recorded_inst.push_back(std::pair >(q, terms)); - } if (options::incrementalSolving()) { Trace("inst-add-debug") @@ -607,24 +600,13 @@ bool Instantiate::removeInstantiationInternal(Node q, std::vector& terms) return d_inst_match_trie[q].removeInstMatch(q, terms); } -void Instantiate::getInstantiatedQuantifiedFormulas(std::vector& qs) +void Instantiate::getInstantiatedQuantifiedFormulas(std::vector& qs) const { - if (options::incrementalSolving()) - { - for (context::CDHashSet::const_iterator it = - d_c_inst_match_trie_dom.begin(); - it != d_c_inst_match_trie_dom.end(); - ++it) - { - qs.push_back(*it); - } - } - else + for (NodeInstListMap::const_iterator it = d_insts.begin(); + it != d_insts.end(); + ++it) { - for (std::pair& t : d_inst_match_trie) - { - qs.push_back(t.first); - } + qs.push_back(it->first); } } @@ -671,6 +653,20 @@ void Instantiate::getInstantiationTermVectors( } } +void Instantiate::getInstantiations(Node q, std::vector& insts) +{ + Trace("inst-debug") << "get instantiations for " << q << std::endl; + InstLemmaList* ill = getOrMkInstLemmaList(q); + insts.insert(insts.end(), ill->d_list.begin(), ill->d_list.end()); + // also include recorded instantations (for qe-partial) + std::map >::const_iterator it = + d_recordedInst.find(q); + if (it != d_recordedInst.end()) + { + insts.insert(insts.end(), it->second.begin(), it->second.end()); + } +} + bool Instantiate::isProofEnabled() const { return d_pfInst != nullptr; } void Instantiate::debugPrint(std::ostream& out) @@ -705,12 +701,11 @@ void Instantiate::debugPrintModel() { if (Trace.isOn("inst-per-quant")) { - for (NodeUIntMap::iterator it = d_total_inst_debug.begin(); - it != d_total_inst_debug.end(); + for (NodeInstListMap::iterator it = d_insts.begin(); it != d_insts.end(); ++it) { - Trace("inst-per-quant") - << " * " << (*it).second << " for " << (*it).first << std::endl; + Trace("inst-per-quant") << " * " << (*it).second->d_list.size() << " for " + << (*it).first << std::endl; } } } @@ -731,6 +726,19 @@ Node Instantiate::ensureType(Node n, TypeNode tn) return Node::null(); } +InstLemmaList* Instantiate::getOrMkInstLemmaList(TNode q) +{ + NodeInstListMap::iterator it = d_insts.find(q); + if (it != d_insts.end()) + { + return it->second.get(); + } + std::shared_ptr ill = + std::make_shared(d_qstate.getUserContext()); + d_insts.insert(q, ill); + return ill.get(); +} + Instantiate::Statistics::Statistics() : d_instantiations("Instantiate::Instantiations_Total", 0), d_inst_duplicate("Instantiate::Duplicate_Inst", 0), diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index be410c2c8..94e16b526 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -69,6 +69,15 @@ class InstantiationRewriter bool doVts) = 0; }; +/** Context-dependent list of nodes */ +class InstLemmaList +{ + public: + InstLemmaList(context::Context* c) : d_list(c) {} + /** The list */ + context::CDList d_list; +}; + /** Instantiate * * This class is used for generating instantiation lemmas. It maintains an @@ -90,7 +99,8 @@ class InstantiationRewriter */ class Instantiate : public QuantifiersUtil { - typedef context::CDHashMap NodeUIntMap; + using NodeInstListMap = context:: + CDHashMap, NodeHashFunction>; public: Instantiate(QuantifiersState& qs, @@ -187,13 +197,13 @@ class Instantiate : public QuantifiersUtil bool expFull = true); /** record instantiation * - * Explicitly record that q has been instantiated with terms. This is the - * same as addInstantiation, but does not enqueue an instantiation lemma. + * Explicitly record that q has been instantiated with terms, with virtual + * term substitution if doVts is true. This is the same as addInstantiation, + * but does not enqueue an instantiation lemma. */ - bool recordInstantiation(Node q, + void recordInstantiation(Node q, std::vector& terms, - bool modEq = false, - bool addedLem = true); + bool doVts = false); /** exists instantiation * * Returns true if and only if the instantiation already was added or @@ -240,7 +250,7 @@ class Instantiate : public QuantifiersUtil * Get the list of quantified formulas that were instantiated in the current * user context, store them in qs. */ - void getInstantiatedQuantifiedFormulas(std::vector& qs); + void getInstantiatedQuantifiedFormulas(std::vector& qs) const; /** get instantiation term vectors * * Get term vectors corresponding to for all instantiations lemmas added in @@ -255,6 +265,11 @@ class Instantiate : public QuantifiersUtil */ void getInstantiationTermVectors( std::map > >& insts); + /** + * Get instantiations for quantified formula q. If q is (forall ((x T)) (P + * x)), this is a list of the form (P t1) ... (P tn) for ground terms ti. + */ + void getInstantiations(Node q, std::vector& insts); //--------------------------------------end user-level interface utilities /** Are proofs enabled for this object? */ @@ -281,15 +296,12 @@ class Instantiate : public QuantifiersUtil private: /** record instantiation, return true if it was not a duplicate * - * addedLem : whether an instantiation lemma was added for the vector we are - * recording. If this is false, we bookkeep the vector. * modEq : whether to check for duplication modulo equality in instantiation * tries (for performance), */ bool recordInstantiationInternal(Node q, std::vector& terms, - bool modEq = false, - bool addedLem = true); + bool modEq = false); /** remove instantiation from the cache */ bool removeInstantiationInternal(Node q, std::vector& terms); /** @@ -297,6 +309,8 @@ class Instantiate : public QuantifiersUtil * if possible. */ static Node ensureType(Node n, TypeNode tn); + /** Get or make the instantiation list for quantified formula q */ + InstLemmaList* getOrMkInstLemmaList(TNode q); /** Reference to the quantifiers state */ QuantifiersState& d_qstate; @@ -311,8 +325,19 @@ class Instantiate : public QuantifiersUtil /** instantiation rewriter classes */ std::vector d_instRewrite; - /** statistics for debugging total instantiations per quantifier */ - NodeUIntMap d_total_inst_debug; + /** + * The list of all instantiation lemma bodies per quantifier. This is used + * for debugging and for quantifier elimination. + */ + NodeInstListMap d_insts; + /** explicitly recorded instantiations + * + * Sometimes an instantiation is recorded internally but not sent out as a + * lemma, for instance, for partial quantifier elimination. This is a map + * of these instantiations, for each quantified formula. This map is cleared + * on presolve, e.g. it is local to a check-sat call. + */ + std::map > d_recordedInst; /** statistics for debugging total instantiations per quantifier per round */ std::map d_temp_inst_debug; @@ -328,14 +353,6 @@ class Instantiate : public QuantifiersUtil * is valid. */ context::CDHashSet d_c_inst_match_trie_dom; - - /** explicitly recorded instantiations - * - * Sometimes an instantiation is recorded internally but not sent out as a - * lemma, for instance, for partial quantifier elimination. This is a map - * of these instantiations, for each quantified formula. - */ - std::vector > > d_recorded_inst; /** * A CDProof storing instantiation steps. */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 8d8f54768..f1ca0dd9f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -630,6 +630,11 @@ void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector d_qim.getInstantiate()->getInstantiationTermVectors(insts); } +void QuantifiersEngine::getInstantiations(Node q, std::vector& insts) +{ + d_qim.getInstantiate()->getInstantiations(q, insts); +} + void QuantifiersEngine::printSynthSolution( std::ostream& out ) { if (d_qmodules->d_synth_e) { diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 28f162ddd..d05137e80 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -154,6 +154,11 @@ public: std::vector >& tvecs); void getInstantiationTermVectors( std::map > >& insts); + /** + * Get instantiations for quantified formula q. If q is (forall ((x T)) (P x)), + * this is a list of the form (P t1) ... (P tn) for ground terms ti. + */ + void getInstantiations(Node q, std::vector& insts); /** * Get skolemization vectors, where for each quantified formula that was * skolemized, this is the list of skolems that were used to witness the diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c7d97d0fd..1a773de0a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1776,6 +1776,7 @@ set(regress_1_tests regress1/quantifiers/issue5507-qe.smt2 regress1/quantifiers/issue5658-qe.smt2 regress1/quantifiers/issue5766-wrong-sel-trigger.smt2 + regress1/quantifiers/issue5899-qe.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lia-witness-div-pp.smt2 diff --git a/test/regress/regress1/quantifiers/issue5899-qe.smt2 b/test/regress/regress1/quantifiers/issue5899-qe.smt2 new file mode 100644 index 000000000..963eaabcd --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5899-qe.smt2 @@ -0,0 +1,402 @@ +; SCRUBBER: sed 's/(.*)/()/g' +; EXPECT: () +; EXIT: 0 + + +(set-logic LIRA) +(define-fun + __node_init_HH_4 + ((HH.usr.x@0 Bool) + (HH.usr.y@0 Bool) + (HH.res.init_flag@0 Bool)) + Bool + (and + (= HH.usr.y@0 HH.usr.x@0) + HH.res.init_flag@0)) +;; Success + +(define-fun + __node_trans_HH_4 + ((HH.usr.x@1 Bool) + (HH.usr.y@1 Bool) + (HH.res.init_flag@1 Bool) + (HH.usr.x@0 Bool) + (HH.usr.y@0 Bool) + (HH.res.init_flag@0 Bool)) + Bool + (and + (= HH.usr.y@1 (or HH.usr.x@1 HH.usr.y@0)) + (not HH.res.init_flag@1))) +;; Success + +(define-fun + __node_init_FTH_4 + ((FTH.usr.x@0 Bool) + (FTH.usr.r@0 Bool) + (FTH.res.init_flag@0 Bool) + (FTH.res.abs_0@0 Bool) + (FTH.res.inst_1@0 Bool)) + Bool + (and + (= FTH.usr.r@0 FTH.usr.x@0) + (__node_init_HH_4 + FTH.usr.x@0 + FTH.res.abs_0@0 + FTH.res.inst_1@0) + FTH.res.init_flag@0)) +;; Success + +(define-fun + __node_trans_FTH_4 + ((FTH.usr.x@1 Bool) + (FTH.usr.r@1 Bool) + (FTH.res.init_flag@1 Bool) + (FTH.res.abs_0@1 Bool) + (FTH.res.inst_1@1 Bool) + (FTH.usr.x@0 Bool) + (FTH.usr.r@0 Bool) + (FTH.res.init_flag@0 Bool) + (FTH.res.abs_0@0 Bool) + (FTH.res.inst_1@0 Bool)) + Bool + (and + (= + FTH.usr.r@1 + (and (not FTH.res.abs_0@0) FTH.usr.x@1)) + (__node_trans_HH_4 + FTH.usr.x@1 + FTH.res.abs_0@1 + FTH.res.inst_1@1 + FTH.usr.x@0 + FTH.res.abs_0@0 + FTH.res.inst_1@0) + (not FTH.res.init_flag@1))) +;; Success + +(declare-fun %f137@0 () Bool) +;; Success + +(declare-fun %f144@0 () Bool) +;; Success + +(declare-fun %f145@0 () Real) +;; Success + +(declare-fun %f146@0 () Real) +;; Success + +(declare-fun %f147@0 () Int) +;; Success + +(declare-fun %f148@0 () Real) +;; Success + +(declare-fun %f149@0 () Real) +;; Success + +(declare-fun %f136@0 () Bool) +;; Success + +(declare-fun %f150@0 () Bool) +;; Success + +(declare-fun %f151@0 () Bool) +;; Success + +(declare-fun %f152@0 () Bool) +;; Success + +(declare-fun %f154@0 () Bool) +;; Success + +(declare-fun %f155@0 () Bool) +;; Success + +(declare-fun %f156@0 () Bool) +;; Success + +(declare-fun %f157@0 () Bool) +;; Success + +(declare-fun %f158@0 () Bool) +;; Success + +(declare-fun %f275@0 () Bool) +;; Success + +(declare-fun %f274@0 () Bool) +;; Success + +(declare-fun %f273@0 () Bool) +;; Success + +(declare-fun %f272@0 () Bool) +;; Success + +(declare-fun %f271@0 () Bool) +;; Success + +(declare-fun %f137@1 () Bool) +;; Success + +(declare-fun %f144@1 () Bool) +;; Success + +(declare-fun %f145@1 () Real) +;; Success + +(declare-fun %f146@1 () Real) +;; Success + +(declare-fun %f147@1 () Int) +;; Success + +(declare-fun %f148@1 () Real) +;; Success + +(declare-fun %f149@1 () Real) +;; Success + +(declare-fun %f136@1 () Bool) +;; Success + +(declare-fun %f150@1 () Bool) +;; Success + +(declare-fun %f151@1 () Bool) +;; Success + +(declare-fun %f152@1 () Bool) +;; Success + +(declare-fun %f154@1 () Bool) +;; Success + +(declare-fun %f155@1 () Bool) +;; Success + +(declare-fun %f156@1 () Bool) +;; Success + +(declare-fun %f157@1 () Bool) +;; Success + +(declare-fun %f158@1 () Bool) +;; Success + +(declare-fun %f275@1 () Bool) +;; Success + +(declare-fun %f274@1 () Bool) +;; Success + +(declare-fun %f273@1 () Bool) +;; Success + +(declare-fun %f272@1 () Bool) +;; Success + +(declare-fun %f271@1 () Bool) +;; Success + +(get-qe + (exists + ((X1 Bool) + (X2 Bool) + (X3 Bool) + (X4 Bool) + (X5 Bool) + (X6 Bool) + (X7 Bool) + (X8 Bool) + (X9 Bool) + (X10 Bool) + (X11 Bool) + (X12 Bool) + (X13 Bool) + (X14 Bool) + (X15 Real) + (X16 Real) + (X17 Int) + (X18 Real) + (X19 Real) + (X20 Bool) + (X21 Bool)) + (not + (or + (and + (or X21 (not X20)) + (or + (and + (not %f150@0) + (or + (__node_trans_FTH_4 + false + false + false + true + false + false + %f154@0 + %f274@0 + %f273@0 + %f272@0) + (__node_trans_FTH_4 + false + false + false + false + false + false + %f154@0 + %f274@0 + %f273@0 + %f272@0)) + (or + (__node_trans_HH_4 false true false false %f151@0 %f275@0) + (__node_trans_HH_4 false false false false %f151@0 %f275@0)) + (or + (__node_trans_HH_4 false true false %f156@0 %f157@0 %f271@0) + (__node_trans_HH_4 + false + false + false + %f156@0 + %f157@0 + %f271@0))) + (and + %f150@0 + (__node_trans_HH_4 true true false %f156@0 %f157@0 %f271@0) + (or + (__node_trans_FTH_4 + false + false + false + true + false + true + %f154@0 + %f274@0 + %f273@0 + %f272@0) + (__node_trans_FTH_4 + false + false + false + false + false + true + %f154@0 + %f274@0 + %f273@0 + %f272@0)) + (or + (__node_trans_HH_4 false true false true %f151@0 %f275@0) + (__node_trans_HH_4 false false false true %f151@0 %f275@0))))) + (and + X20 + (not X21) + (or + (and + (not %f150@0) + (__node_trans_HH_4 true true false false %f151@0 %f275@0) + (or + (and + (__node_trans_HH_4 + false + true + false + %f156@0 + %f157@0 + %f271@0) + (or + (__node_trans_FTH_4 + true + false + false + true + false + false + %f154@0 + %f274@0 + %f273@0 + %f272@0) + (and + (= %f148@0 X19) + (= %f149@0 X18) + (__node_trans_FTH_4 + true + true + false + true + false + false + %f154@0 + %f274@0 + %f273@0 + %f272@0)))) + (and + (__node_trans_HH_4 + false + false + false + %f156@0 + %f157@0 + %f271@0) + (or + (__node_trans_FTH_4 + true + true + false + true + false + false + %f154@0 + %f274@0 + %f273@0 + %f272@0) + (__node_trans_FTH_4 + true + false + false + true + false + false + %f154@0 + %f274@0 + %f273@0 + %f272@0))))) + (and + %f150@0 + (__node_trans_HH_4 true true false %f156@0 %f157@0 %f271@0) + (__node_trans_HH_4 true true false true %f151@0 %f275@0) + (or + (__node_trans_FTH_4 + true + false + false + true + false + true + %f154@0 + %f274@0 + %f273@0 + %f272@0) + (and + (= %f148@0 X19) + (= %f149@0 X18) + (__node_trans_FTH_4 + true + true + false + true + false + true + %f154@0 + %f274@0 + %f273@0 + %f272@0)))))))))) + +(exit) +;; NoResponse +