From 3a180a2f8ffe8ad5756119ce0cbe61ab4ab28127 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 27 Jul 2021 12:24:17 -0500 Subject: [PATCH] Track instantiation reasons in proofs (#6935) This adds optional arguments to INSTANTIATE steps in proofs to track fine-grained reasons for relevant instantiations. Also simplifies an old argument modEq which was unused. FYI @MikolasJanota --- src/proof/proof_rule.h | 10 +++- src/smt/unsat_core_manager.cpp | 5 +- src/theory/inference_id.cpp | 6 +++ src/theory/inference_id.h | 5 ++ .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 2 +- src/theory/quantifiers/ematching/trigger.cpp | 3 +- src/theory/quantifiers/ematching/trigger.h | 2 + .../quantifiers/fmf/full_model_check.cpp | 14 ++++-- src/theory/quantifiers/fmf/model_builder.h | 2 - src/theory/quantifiers/fmf/model_engine.cpp | 7 ++- src/theory/quantifiers/instantiate.cpp | 47 ++++++++++++------- src/theory/quantifiers/instantiate.h | 20 ++++---- src/theory/quantifiers/proof_checker.cpp | 5 +- 13 files changed, 85 insertions(+), 43 deletions(-) diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index 4b95b47da..173e4df9a 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -827,10 +827,16 @@ enum class PfRule : uint32_t SKOLEMIZE, // ======== Instantiate // Children: (P:(forall ((x1 T1) ... (xn Tn)) F)) - // Arguments: (t1 ... tn) + // Arguments: (t1 ... tn, (id (t)?)? ) // ---------------------------------------- // Conclusion: F*sigma - // sigma maps x1 ... xn to t1 ... tn. + // where sigma maps x1 ... xn to t1 ... tn. + // + // The optional argument id indicates the inference id that caused the + // instantiation. The term t indicates an additional term (e.g. the trigger) + // associated with the instantiation, which depends on the id. If the id + // has prefix "QUANTIFIERS_INST_E_MATCHING", then t is the trigger that + // generated the instantiation. INSTANTIATE, // ======== (Trusted) quantifiers preprocess // Children: ? diff --git a/src/smt/unsat_core_manager.cpp b/src/smt/unsat_core_manager.cpp index ba2c07326..22304f9e8 100644 --- a/src/smt/unsat_core_manager.cpp +++ b/src/smt/unsat_core_manager.cpp @@ -80,7 +80,10 @@ void UnsatCoreManager::getRelevantInstantiations( const std::vector& instTerms = cur->getArguments(); Assert(cs.size() == 1); Node q = cs[0]->getResult(); - insts[q].push_back({instTerms.begin(), instTerms.end()}); + // the instantiation is a prefix of the arguments up to the number of + // variables + insts[q].push_back( + {instTerms.begin(), instTerms.begin() + q[0].getNumChildren()}); } for (const std::shared_ptr& cp : cs) { diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 9fbe37254..c0700c06e 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -16,6 +16,7 @@ #include "theory/inference_id.h" #include +#include "util/rational.h" namespace cvc5 { namespace theory { @@ -395,5 +396,10 @@ std::ostream& operator<<(std::ostream& out, InferenceId i) return out; } +Node mkInferenceIdNode(InferenceId i) +{ + return NodeManager::currentNM()->mkConst(Rational(static_cast(i))); +} + } // namespace theory } // namespace cvc5 diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 9ba324675..b3be59c5c 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -20,6 +20,8 @@ #include +#include "expr/node.h" + namespace cvc5 { namespace theory { @@ -786,6 +788,9 @@ const char* toString(InferenceId i); */ std::ostream& operator<<(std::ostream& out, InferenceId i); +/** Make node from inference id */ +Node mkInferenceIdNode(InferenceId i); + } // namespace theory } // namespace cvc5 diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index f059767a6..f65828d2f 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -491,7 +491,7 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { else if (inst->addInstantiation(d_curr_quant, subs, InferenceId::QUANTIFIERS_INST_CEGQI, - false, + Node::null(), false, usedVts)) { diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 62558e2c6..529125978 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -59,6 +59,7 @@ Trigger::Trigger(QuantifiersState& qs, Node np = ensureGroundTermPreprocessed(val, n, d_groundTerms); d_nodes.push_back(np); } + d_trNode = NodeManager::currentNM()->mkNode(SEXPR, d_nodes); if (Trace.isOn("trigger")) { QuantAttributes& qa = d_qreg.getQuantAttributes(); @@ -163,7 +164,7 @@ uint64_t Trigger::addInstantiations() bool Trigger::sendInstantiation(std::vector& m, InferenceId id) { - return d_qim.getInstantiate()->addInstantiation(d_quant, m, id); + return d_qim.getInstantiate()->addInstantiation(d_quant, m, id, d_trNode); } bool Trigger::sendInstantiation(InstMatch& m, InferenceId id) diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index 172e93c12..944a082c0 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -181,6 +181,8 @@ class Trigger { std::vector& gts); /** The nodes comprising this trigger. */ std::vector d_nodes; + /** The nodes as a single s-expression */ + Node d_trNode; /** * The preprocessed ground terms in the nodes of the trigger, which as an * optimization omits variables and constant subterms. These terms are diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index c3fa664d9..c4f83191b 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -725,8 +725,11 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i } // just add the instance d_triedLemmas++; - if (instq->addInstantiation( - f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC, true)) + if (instq->addInstantiation(f, + inst, + InferenceId::QUANTIFIERS_INST_FMF_FMC, + Node::null(), + true)) { Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; d_addedLemmas++; @@ -875,8 +878,11 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc* fm, if (ev!=d_true) { Trace("fmc-exh-debug") << ", add!"; //add as instantiation - if (ie->addInstantiation( - f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH, true)) + if (ie->addInstantiation(f, + inst, + InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH, + Node::null(), + true)) { Trace("fmc-exh-debug") << " ...success."; addedLemmas++; diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index cfccd4d93..a767af47a 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -56,8 +56,6 @@ class QModelBuilder : public TheoryEngineModelBuilder virtual int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; } //whether to construct model virtual bool optUseModel(); - /** exist instantiation ? */ - virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; } //debug model void debugModel(TheoryModel* m) override; //statistics diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 747b0621f..e58f66d0b 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -301,8 +301,11 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; triedLemmas++; //add as instantiation - if (inst->addInstantiation( - f, m.d_vals, InferenceId::QUANTIFIERS_INST_FMF_EXH, true)) + if (inst->addInstantiation(f, + m.d_vals, + InferenceId::QUANTIFIERS_INST_FMF_EXH, + Node::null(), + true)) { addedLemmas++; if (d_qstate.isInConflict()) diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 268d1371f..05361eaa1 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -101,8 +101,8 @@ void Instantiate::addRewriter(InstantiationRewriter* ir) bool Instantiate::addInstantiation(Node q, std::vector& terms, InferenceId id, + Node pfArg, bool mkRep, - bool modEq, bool doVts) { // For resource-limiting (also does a time check). @@ -229,7 +229,7 @@ bool Instantiate::addInstantiation(Node q, } // record the instantiation - bool recorded = recordInstantiationInternal(q, terms, modEq); + bool recorded = recordInstantiationInternal(q, terms); if (!recorded) { Trace("inst-add-debug") << " --> Already exists (no record)." << std::endl; @@ -250,7 +250,8 @@ bool Instantiate::addInstantiation(Node q, Trace("inst-add-debug") << "Constructing instantiation..." << std::endl; Assert(d_qreg.d_vars[q].size() == terms.size()); // get the instantiation - Node body = getInstantiation(q, d_qreg.d_vars[q], terms, doVts, pfTmp.get()); + Node body = getInstantiation( + q, d_qreg.d_vars[q], terms, id, pfArg, doVts, pfTmp.get()); Node orig_body = body; // now preprocess, storing the trust node for the rewrite TrustNode tpBody = QuantifiersRewriter::preprocess(body, true); @@ -394,12 +395,12 @@ bool Instantiate::addInstantiationExpFail(Node q, std::vector& terms, std::vector& failMask, InferenceId id, + Node pfArg, bool mkRep, - bool modEq, bool doVts, bool expFull) { - if (addInstantiation(q, terms, id, mkRep, modEq, doVts)) + if (addInstantiation(q, terms, id, pfArg, mkRep, doVts)) { return true; } @@ -421,7 +422,9 @@ bool Instantiate::addInstantiationExpFail(Node q, subs[vars[i]] = terms[i]; } // get the instantiation body - Node ibody = getInstantiation(q, vars, terms, doVts); + InferenceId idNone = InferenceId::UNKNOWN; + Node nulln; + Node ibody = getInstantiation(q, vars, terms, idNone, nulln, doVts); ibody = Rewriter::rewrite(ibody); for (size_t i = 0; i < tsize; i++) { @@ -450,7 +453,7 @@ bool Instantiate::addInstantiationExpFail(Node q, // check whether the instantiation rewrites to the same thing if (!success) { - Node ibodyc = getInstantiation(q, vars, terms, doVts); + Node ibodyc = getInstantiation(q, vars, terms, idNone, nulln, doVts); ibodyc = Rewriter::rewrite(ibodyc); success = (ibodyc == ibody); Trace("inst-exp-fail") << " rewrite invariant: " << success << std::endl; @@ -521,6 +524,8 @@ bool Instantiate::existsInstantiation(Node q, Node Instantiate::getInstantiation(Node q, std::vector& vars, std::vector& terms, + InferenceId id, + Node pfArg, bool doVts, LazyCDProof* pf) { @@ -534,7 +539,19 @@ Node Instantiate::getInstantiation(Node q, // store the proof of the instantiated body, with (open) assumption q if (pf != nullptr) { - pf->addStep(body, PfRule::INSTANTIATE, {q}, terms); + // additional arguments: if the inference id is not unknown, include it, + // followed by the proof argument if non-null. The latter is used e.g. + // to track which trigger caused an instantiation. + std::vector pfTerms = terms; + if (id != InferenceId::UNKNOWN) + { + pfTerms.push_back(mkInferenceIdNode(id)); + if (!pfArg.isNull()) + { + pfTerms.push_back(pfArg); + } + } + pf->addStep(body, PfRule::INSTANTIATE, {q}, pfTerms); } // run rewriters to rewrite the instantiation in sequence. @@ -564,18 +581,16 @@ Node Instantiate::getInstantiation(Node q, Node Instantiate::getInstantiation(Node q, std::vector& terms, bool doVts) { Assert(d_qreg.d_vars.find(q) != d_qreg.d_vars.end()); - return getInstantiation(q, d_qreg.d_vars[q], terms, doVts); + return getInstantiation( + q, d_qreg.d_vars[q], terms, InferenceId::UNKNOWN, Node::null(), doVts); } -bool Instantiate::recordInstantiationInternal(Node q, - std::vector& terms, - bool modEq) +bool Instantiate::recordInstantiationInternal(Node q, std::vector& terms) { if (options::incrementalSolving()) { Trace("inst-add-debug") - << "Adding into context-dependent inst trie, modEq = " << modEq - << std::endl; + << "Adding into context-dependent inst trie" << std::endl; CDInstMatchTrie* imt; std::map::iterator it = d_c_inst_match_trie.find(q); if (it != d_c_inst_match_trie.end()) @@ -588,10 +603,10 @@ bool Instantiate::recordInstantiationInternal(Node q, d_c_inst_match_trie[q] = imt; } d_c_inst_match_trie_dom.insert(q); - return imt->addInstMatch(d_qstate, q, terms, modEq); + return imt->addInstMatch(d_qstate, q, terms); } Trace("inst-add-debug") << "Adding into inst trie" << std::endl; - return d_inst_match_trie[q].addInstMatch(d_qstate, q, terms, modEq); + return d_inst_match_trie[q].addInstMatch(d_qstate, q, terms); } bool Instantiate::removeInstantiationInternal(Node q, std::vector& terms) diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index eddc7470b..1f380350f 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -139,10 +139,10 @@ class Instantiate : public QuantifiersUtil * @param terms the terms to instantiate with * @param id the identifier of the instantiation lemma sent via the inference * 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 modEq whether to check for duplication modulo equality in - * instantiation tries (for performance), * @param doVts whether we must apply virtual term substitution to the * instantiation lemma. * @@ -161,8 +161,8 @@ class Instantiate : public QuantifiersUtil bool addInstantiation(Node q, std::vector& terms, InferenceId id, + Node pfArg = Node::null(), bool mkRep = false, - bool modEq = false, bool doVts = false); /** * Same as above, but we also compute a vector failMask indicating which @@ -191,8 +191,8 @@ class Instantiate : public QuantifiersUtil std::vector& terms, std::vector& failMask, InferenceId id, + Node pfArg = Node::null(), bool mkRep = false, - bool modEq = false, bool doVts = false, bool expFull = true); /** record instantiation @@ -226,6 +226,8 @@ class Instantiate : public QuantifiersUtil Node getInstantiation(Node q, std::vector& vars, std::vector& terms, + InferenceId id = InferenceId::UNKNOWN, + Node pfArg = Node::null(), bool doVts = false, LazyCDProof* pf = nullptr); /** get instantiation @@ -293,14 +295,8 @@ class Instantiate : public QuantifiersUtil Statistics d_statistics; private: - /** record instantiation, return true if it was not a duplicate - * - * modEq : whether to check for duplication modulo equality in instantiation - * tries (for performance), - */ - bool recordInstantiationInternal(Node q, - std::vector& terms, - bool modEq = false); + /** record instantiation, return true if it was not a duplicate */ + bool recordInstantiationInternal(Node q, std::vector& terms); /** remove instantiation from the cache */ bool removeInstantiationInternal(Node q, std::vector& terms); /** diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp index f44f2f291..5e02e16a5 100644 --- a/src/theory/quantifiers/proof_checker.cpp +++ b/src/theory/quantifiers/proof_checker.cpp @@ -102,15 +102,16 @@ Node QuantifiersProofRuleChecker::checkInternal( else if (id == PfRule::INSTANTIATE) { Assert(children.size() == 1); + // note we may have more arguments than just the term vector if (children[0].getKind() != FORALL - || args.size() != children[0][0].getNumChildren()) + || args.size() < children[0][0].getNumChildren()) { return Node::null(); } Node body = children[0][1]; std::vector vars; std::vector subs; - for (unsigned i = 0, nargs = args.size(); i < nargs; i++) + for (size_t i = 0, nc = children[0][0].getNumChildren(); i < nc; i++) { vars.push_back(children[0][0][i]); subs.push_back(args[i]); -- 2.30.2