From 55d3b25f8d18495f92c0058df73f6ed80a369186 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 22 Sep 2021 22:03:29 -0500 Subject: [PATCH] Implement alpha equivalence proofs (#7066) This is a modified version of #6137 which accounts for extended rewriting between quantified formulas that are considered alpha equivalent. It also generalizes the proof rule ALPHA_EQUIV. Notice that if we were to make this rule more pedantic, we would check for variable shadowing during substitution, although this is not currently done. --- src/expr/term_canonize.cpp | 9 + src/expr/term_canonize.h | 8 + src/proof/proof_rule.cpp | 1 + src/proof/proof_rule.h | 12 +- src/theory/quantifiers/alpha_equivalence.cpp | 172 ++++++++++++++++-- src/theory/quantifiers/alpha_equivalence.h | 60 ++++-- src/theory/quantifiers/proof_checker.cpp | 36 ++++ .../quantifiers/quantifiers_modules.cpp | 2 +- src/theory/quantifiers/quantifiers_modules.h | 2 +- src/theory/quantifiers_engine.cpp | 50 ++--- src/theory/quantifiers_engine.h | 1 - test/regress/CMakeLists.txt | 1 + .../regress1/proofs/quant-alpha-eq.smt2 | 8 + 13 files changed, 299 insertions(+), 63 deletions(-) create mode 100644 test/regress/regress1/proofs/quant-alpha-eq.smt2 diff --git a/src/expr/term_canonize.cpp b/src/expr/term_canonize.cpp index 0e05a52ea..5ab5a4b1b 100644 --- a/src/expr/term_canonize.cpp +++ b/src/expr/term_canonize.cpp @@ -222,5 +222,14 @@ Node TermCanonize::getCanonicalTerm(TNode n, bool apply_torder, bool doHoVar) return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited); } +Node TermCanonize::getCanonicalTerm(TNode n, + std::map& visited, + bool apply_torder, + bool doHoVar) +{ + std::map, unsigned> var_count; + return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited); +} + } // namespace expr } // namespace cvc5 diff --git a/src/expr/term_canonize.h b/src/expr/term_canonize.h index e1524cbf6..74eefdd2d 100644 --- a/src/expr/term_canonize.h +++ b/src/expr/term_canonize.h @@ -87,6 +87,14 @@ class TermCanonize Node getCanonicalTerm(TNode n, bool apply_torder = false, bool doHoVar = true); + /** + * Same as above but tracks visited map, mapping subterms of n to their + * canonical forms. + */ + Node getCanonicalTerm(TNode n, + std::map& visited, + bool apply_torder = false, + bool doHoVar = true); private: /** The (optional) type class callback */ diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp index acb49843f..5cf5dc0f8 100644 --- a/src/proof/proof_rule.cpp +++ b/src/proof/proof_rule.cpp @@ -135,6 +135,7 @@ const char* toString(PfRule id) case PfRule::EXISTS_INTRO: return "EXISTS_INTRO"; case PfRule::SKOLEMIZE: return "SKOLEMIZE"; case PfRule::INSTANTIATE: return "INSTANTIATE"; + case PfRule::ALPHA_EQUIV: return "ALPHA_EQUIV"; case PfRule::QUANTIFIERS_PREPROCESS: return "QUANTIFIERS_PREPROCESS"; //================================================= String rules case PfRule::CONCAT_EQ: return "CONCAT_EQ"; diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index 7b93e3a55..bb677bdb9 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -835,6 +835,17 @@ enum class PfRule : uint32_t // has prefix "QUANTIFIERS_INST_E_MATCHING", then t is the trigger that // generated the instantiation. INSTANTIATE, + // ======== Alpha equivalence + // Children: none + // Arguments: (F, (y1 = z1), ..., (yn = zn) ) + // ---------------------------------------- + // Conclusion: (= F F*sigma) + // sigma maps y1 ... yn to z1 ... zn, where y1 ... yn are unique bound + // variables, and z1 ... zn are unique bound variables. Notice that this + // rule is correct only when z1, ..., zn are not contained in + // FV(F) \ { y1 ... yn }. The internal quantifiers proof checker does not + // currently check that this is the case. + ALPHA_EQUIV, // ======== (Trusted) quantifiers preprocess // Children: ? // Arguments: (F) @@ -842,7 +853,6 @@ enum class PfRule : uint32_t // Conclusion: F // where F is an equality of the form t = QuantifiersPreprocess::preprocess(t) QUANTIFIERS_PREPROCESS, - //================================================= String rules //======================== Core solver // ======== Concat eq diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index 50b444b36..f4370c017 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -15,6 +15,10 @@ #include "theory/quantifiers/alpha_equivalence.h" +#include "proof/method_id.h" +#include "proof/proof.h" +#include "proof/proof_node.h" + using namespace cvc5::kind; namespace cvc5 { @@ -60,13 +64,62 @@ Node AlphaEquivalenceDb::addTerm(Node q) Assert(q.getKind() == FORALL); Trace("aeq") << "Alpha equivalence : register " << q << std::endl; //construct canonical quantified formula - Node t = d_tc->getCanonicalTerm(q[1], true); + Node t = d_tc->getCanonicalTerm(q[1], d_sortCommutativeOpChildren); Trace("aeq") << " canonical form: " << t << std::endl; + return addTermToTypeTrie(t, q); +} + +Node AlphaEquivalenceDb::addTermWithSubstitution(Node q, + std::vector& vars, + std::vector& subs) +{ + Trace("aeq") << "Alpha equivalence : register " << q << std::endl; + // construct canonical quantified formula with visited cache + std::map visited; + Node t = d_tc->getCanonicalTerm(q[1], visited, d_sortCommutativeOpChildren); + // only need to store BOUND_VARIABLE in substitution + std::map& bm = d_bvmap[q]; + for (const std::pair& b : visited) + { + if (b.first.getKind() == BOUND_VARIABLE) + { + Assert(b.second.getKind() == BOUND_VARIABLE); + bm[b.second] = b.first; + } + } + Node qret = addTermToTypeTrie(t, q); + if (qret != q) + { + Assert(d_bvmap.find(qret) != d_bvmap.end()); + std::map& bmr = d_bvmap[qret]; + std::map::iterator itb; + for (const std::pair& b : bmr) + { + itb = bm.find(b.first); + if (itb == bm.end()) + { + // didn't use the same variables, fail + vars.clear(); + subs.clear(); + break; + } + // otherwise, we map the variable in the returned quantified formula + // to the variable that used the same canonical variable + vars.push_back(b.second); + subs.push_back(itb->second); + } + } + return qret; +} + +Node AlphaEquivalenceDb::addTermToTypeTrie(Node t, Node q) +{ //compute variable type counts std::map typCount; std::vector< TypeNode > typs; - for( unsigned i=0; i vars; + std::vector subs; + if (isProofEnabled()) + { + ret = d_aedb.addTermWithSubstitution(q, vars, subs); + } + else + { + ret = d_aedb.addTerm(q); + } + if (ret == q) + { + return TrustNode::null(); + } Node lem; - if (ret != q) + ProofGenerator* pg = nullptr; + // lemma ( q <=> d_quant ) + // Notice that we infer this equivalence regardless of whether q or ret + // have annotations (e.g. user patterns, names, etc.). + Trace("alpha-eq") << "Alpha equivalent : " << std::endl; + Trace("alpha-eq") << " " << q << std::endl; + Trace("alpha-eq") << " " << ret << std::endl; + lem = ret.eqNode(q); + if (q.getNumChildren() == 3) { - // lemma ( q <=> d_quant ) - // Notice that we infer this equivalence regardless of whether q or ret - // have annotations (e.g. user patterns, names, etc.). - Trace("alpha-eq") << "Alpha equivalent : " << std::endl; - Trace("alpha-eq") << " " << q << std::endl; - Trace("alpha-eq") << " " << ret << std::endl; - lem = q.eqNode(ret); - if (q.getNumChildren() == 3) + Notice() << "Ignoring annotated quantified formula based on alpha " + "equivalence: " + << q << std::endl; + } + // if successfully computed the substitution above + if (isProofEnabled() && !vars.empty()) + { + std::vector pfArgs; + pfArgs.push_back(ret); + for (size_t i = 0, nvars = vars.size(); i < nvars; i++) + { + pfArgs.push_back(vars[i].eqNode(subs[i])); + Trace("alpha-eq") << "subs: " << vars[i] << " -> " << subs[i] + << std::endl; + } + CDProof cdp(d_pnm); + Node sret = + ret.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); + std::vector transEq; + Node eq = ret.eqNode(sret); + transEq.push_back(eq); + // ---------- ALPHA_EQUIV + // ret = sret + cdp.addStep(eq, PfRule::ALPHA_EQUIV, {}, pfArgs); + // if not syntactically equal, maybe it can be transformed + bool success = false; + if (sret == q) + { + success = true; + } + else + { + Node eq2 = sret.eqNode(q); + transEq.push_back(eq2); + Node eq2r = extendedRewrite(eq2); + if (eq2r.isConst() && eq2r.getConst()) + { + // ---------- MACRO_SR_PRED_INTRO + // sret = q + std::vector pfArgs2; + pfArgs2.push_back(eq2); + addMethodIds(pfArgs2, + MethodId::SB_DEFAULT, + MethodId::SBA_SEQUENTIAL, + MethodId::RW_EXT_REWRITE); + cdp.addStep(eq2, PfRule::MACRO_SR_PRED_INTRO, {}, pfArgs2); + success = true; + } + } + // if successful, store the proof and remember the proof generator + if (success) { - Notice() << "Ignoring annotated quantified formula based on alpha " - "equivalence: " - << q << std::endl; + if (transEq.size() > 1) + { + // TRANS of ALPHA_EQ and MACRO_SR_PRED_INTRO steps from above + cdp.addStep(lem, PfRule::TRANS, transEq, {}); + } + std::shared_ptr pn = cdp.getProofFor(lem); + Trace("alpha-eq") << "Proof is " << *pn.get() << std::endl; + d_pfAlpha->setProofFor(lem, pn); + pg = d_pfAlpha.get(); } } - return lem; + return TrustNode::mkTrustLemma(lem, pg); } +bool AlphaEquivalence::isProofEnabled() const { return d_pfAlpha != nullptr; } + } // namespace quantifiers } // namespace theory } // namespace cvc5 diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h index 886830229..d1a05e486 100644 --- a/src/theory/quantifiers/alpha_equivalence.h +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -18,19 +18,20 @@ #ifndef CVC5__ALPHA_EQUIVALENCE_H #define CVC5__ALPHA_EQUIVALENCE_H -#include "theory/quantifiers/quant_util.h" - #include "expr/term_canonize.h" +#include "proof/eager_proof_generator.h" +#include "smt/env_obj.h" +#include "theory/quantifiers/quant_util.h" namespace cvc5 { namespace theory { namespace quantifiers { /** - * This trie stores a trie of the above form for each multi-set of types. For - * each term t registered to this node, we store t in the appropriate - * AlphaEquivalenceNode trie. For example, if t contains 2 free variables - * of type T1 and 3 free variables of type T2, then it is stored at + * This trie stores a trie for each multi-set of types. For each term t + * registered to this node, we store t in the appropriate + * AlphaEquivalenceTypeNode trie. For example, if t contains 2 free variables of + * type T1 and 3 free variables of type T2, then it is stored at * d_children[T1][2].d_children[T2][3]. */ class AlphaEquivalenceTypeNode { @@ -59,7 +60,10 @@ public: class AlphaEquivalenceDb { public: - AlphaEquivalenceDb(expr::TermCanonize* tc) : d_tc(tc) {} + AlphaEquivalenceDb(expr::TermCanonize* tc, bool sortCommChildren) + : d_tc(tc), d_sortCommutativeOpChildren(sortCommChildren) + { + } /** adds quantified formula q to this database * * This function returns a quantified formula q' that is alpha-equivalent to @@ -67,37 +71,65 @@ class AlphaEquivalenceDb * to addTerm. */ Node addTerm(Node q); + /** + * Add term with substitution, which additionally finds a set of terms such + * that q' * subs is alpha-equivalent (possibly modulo rewriting) to q, where + * q' is the return quantified formula. + */ + Node addTermWithSubstitution(Node q, + std::vector& vars, + std::vector& subs); private: + /** + * Add term to the trie, where t is the canonized form of the body of + * quantified formula q. Returns the quantified formula, if any, that already + * had been added to this class, or q otherwise. + */ + Node addTermToTypeTrie(Node t, Node q); /** a trie per # of variables per type */ AlphaEquivalenceTypeNode d_ae_typ_trie; /** pointer to the term canonize utility */ expr::TermCanonize* d_tc; + /** whether to sort children of commutative operators during canonization. */ + bool d_sortCommutativeOpChildren; + /** + * Maps quantified formulas to variables map, used for tracking substitutions + * in addTermWithSubstitution. The range in d_bvmap[q] contains the mapping + * from canonical free variables to variables in q. + */ + std::map > d_bvmap; }; /** * A quantifiers module that computes reductions based on alpha-equivalence, * using the above utilities. */ -class AlphaEquivalence +class AlphaEquivalence : protected EnvObj { public: - AlphaEquivalence(); + AlphaEquivalence(Env& env); ~AlphaEquivalence(){} /** reduce quantifier * - * If non-null, its return value is lemma justifying why q is reducible. - * This is of the form ( q = q' ) where q' is a quantified formula that - * was previously registered to this class via a call to reduceQuantifier, - * and q and q' are alpha-equivalent. + * If non-null, its return value is a trust node containing the lemma + * justifying why q is reducible. This lemma is of the form ( q = q' ) where + * q' is a quantified formula that was previously registered to this class via + * a call to reduceQuantifier, and q and q' are alpha-equivalent. */ - Node reduceQuantifier( Node q ); + TrustNode reduceQuantifier(Node q); private: /** a term canonizer */ expr::TermCanonize d_termCanon; /** the database of quantified formulas registered to this class */ AlphaEquivalenceDb d_aedb; + /** Pointer to the proof node manager */ + ProofNodeManager* d_pnm; + /** An eager proof generator storing alpha equivalence proofs.*/ + std::unique_ptr d_pfAlpha; + /** Are proofs enabled for this object? */ + bool isProofEnabled() const; }; } diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp index 5e02e16a5..c8ff49e11 100644 --- a/src/theory/quantifiers/proof_checker.cpp +++ b/src/theory/quantifiers/proof_checker.cpp @@ -32,6 +32,7 @@ void QuantifiersProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::EXISTS_INTRO, this); pc->registerChecker(PfRule::SKOLEMIZE, this); pc->registerChecker(PfRule::INSTANTIATE, this); + pc->registerChecker(PfRule::ALPHA_EQUIV, this); // trusted rules pc->registerTrustedChecker(PfRule::QUANTIFIERS_PREPROCESS, this, 3); } @@ -120,6 +121,41 @@ Node QuantifiersProofRuleChecker::checkInternal( body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); return inst; } + else if (id == PfRule::ALPHA_EQUIV) + { + Assert(children.empty()); + if (args[0].getKind() != kind::FORALL) + { + return Node::null(); + } + // arguments must be equalities that are bound variables that are + // pairwise unique + std::unordered_set allVars[2]; + std::vector vars; + std::vector newVars; + for (size_t i = 1, nargs = args.size(); i < nargs; i++) + { + if (args[i].getKind() != kind::EQUAL) + { + return Node::null(); + } + for (size_t j = 0; j < 2; j++) + { + Node v = args[i][j]; + if (v.getKind() != kind::BOUND_VARIABLE + || allVars[j].find(v) != allVars[j].end()) + { + return Node::null(); + } + allVars[j].insert(v); + } + vars.push_back(args[i][0]); + newVars.push_back(args[i][1]); + } + Node renamedBody = args[0].substitute( + vars.begin(), vars.end(), newVars.begin(), newVars.end()); + return args[0].eqNode(renamedBody); + } else if (id == PfRule::QUANTIFIERS_PREPROCESS) { Assert(!args.empty()); diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index 563951189..f882daaba 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -96,7 +96,7 @@ void QuantifiersModules::initialize(Env& env, } if (options::quantAlphaEquiv()) { - d_alpha_equiv.reset(new AlphaEquivalence()); + d_alpha_equiv.reset(new AlphaEquivalence(env)); } // full saturation : instantiate from relevant domain, then arbitrary terms if (options::fullSaturateQuant() || options::fullSaturateInterleave()) diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h index 9878e79ae..a7c8fc576 100644 --- a/src/theory/quantifiers/quantifiers_modules.h +++ b/src/theory/quantifiers/quantifiers_modules.h @@ -34,7 +34,7 @@ namespace cvc5 { namespace theory { - + class QuantifiersEngine; class DecisionManager; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index b713dbec1..dfce485f2 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -507,37 +507,37 @@ void QuantifiersEngine::notifyCombineTheories() { // in quantifiers state. } -bool QuantifiersEngine::reduceQuantifier( Node q ) { - //TODO: this can be unified with preregistration: AlphaEquivalence takes ownership of reducable quants - BoolMap::const_iterator it = d_quants_red.find( q ); - if( it==d_quants_red.end() ){ - Node lem; +bool QuantifiersEngine::reduceQuantifier(Node q) +{ + // TODO: this can be unified with preregistration: AlphaEquivalence takes + // ownership of reducable quants + BoolMap::const_iterator it = d_quants_red.find(q); + if (it == d_quants_red.end()) + { + TrustNode tlem; InferenceId id = InferenceId::UNKNOWN; - std::map< Node, Node >::iterator itr = d_quants_red_lem.find( q ); - if( itr==d_quants_red_lem.end() ){ - if (d_qmodules->d_alpha_equiv) + if (d_qmodules->d_alpha_equiv) + { + Trace("quant-engine-red") + << "Alpha equivalence " << q << "?" << std::endl; + // add equivalence with another quantified formula + tlem = d_qmodules->d_alpha_equiv->reduceQuantifier(q); + id = InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ; + if (!tlem.isNull()) { - Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl; - //add equivalence with another quantified formula - lem = d_qmodules->d_alpha_equiv->reduceQuantifier(q); - id = InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ; - if( !lem.isNull() ){ - Trace("quant-engine-red") << "...alpha equivalence success." << std::endl; - ++(d_qstate.getStats().d_red_alpha_equiv); - } + Trace("quant-engine-red") + << "...alpha equivalence success." << std::endl; + ++(d_qstate.getStats().d_red_alpha_equiv); } - d_quants_red_lem[q] = lem; - }else{ - lem = itr->second; } - if( !lem.isNull() ){ - d_qim.lemma(lem, id); + if (!tlem.isNull()) + { + d_qim.trustedLemma(tlem, id); } - d_quants_red[q] = !lem.isNull(); - return !lem.isNull(); - }else{ - return (*it).second; + d_quants_red[q] = !tlem.isNull(); + return !tlem.isNull(); } + return (*it).second; } void QuantifiersEngine::registerQuantifierInternal(Node f) diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index e8c385fcd..547c30797 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -210,7 +210,6 @@ public: NodeSet d_quants_prereg; /** quantifiers reduced */ BoolMap d_quants_red; - std::map d_quants_red_lem; /** Number of rounds we have instantiated */ uint32_t d_numInstRoundsLemma; }; /* class QuantifiersEngine */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 176dadb40..55b932f81 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1750,6 +1750,7 @@ set(regress_1_tests regress1/proofs/issue6625-unsat-core-proofs.smt2 regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2 regress1/proofs/macro-res-exp-singleton-after-elimCrowd.smt2 + regress1/proofs/quant-alpha-eq.smt2 regress1/proofs/sat-trivial-cycle.smt2 regress1/proofs/unsat-cores-proofs.smt2 regress1/push-pop/arith_lra_01.smt2 diff --git a/test/regress/regress1/proofs/quant-alpha-eq.smt2 b/test/regress/regress1/proofs/quant-alpha-eq.smt2 new file mode 100644 index 000000000..f804df43f --- /dev/null +++ b/test/regress/regress1/proofs/quant-alpha-eq.smt2 @@ -0,0 +1,8 @@ +(set-logic AUFLIA) +(set-info :status unsat) +(declare-sort A$ 0) +(declare-fun p$ (A$) Bool) +(assert (exists ((?v0 A$)) (p$ ?v0))) +(assert (forall ((?v0 A$)) (not (p$ ?v0)))) +(assert (not false)) +(check-sat) -- 2.30.2