diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/alpha_equivalence.cpp | 172 | ||||
-rw-r--r-- | src/theory/quantifiers/alpha_equivalence.h | 60 | ||||
-rw-r--r-- | src/theory/quantifiers/proof_checker.cpp | 36 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_modules.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_modules.h | 2 |
5 files changed, 236 insertions, 36 deletions
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<Node>& vars, + std::vector<Node>& subs) +{ + Trace("aeq") << "Alpha equivalence : register " << q << std::endl; + // construct canonical quantified formula with visited cache + std::map<TNode, Node> visited; + Node t = d_tc->getCanonicalTerm(q[1], visited, d_sortCommutativeOpChildren); + // only need to store BOUND_VARIABLE in substitution + std::map<Node, TNode>& bm = d_bvmap[q]; + for (const std::pair<const TNode, Node>& 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<Node, TNode>& bmr = d_bvmap[qret]; + std::map<Node, TNode>::iterator itb; + for (const std::pair<const Node, TNode>& 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<TypeNode, size_t> typCount; std::vector< TypeNode > typs; - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - TypeNode tn = q[0][i].getType(); + for (const Node& v : q[0]) + { + TypeNode tn = v.getType(); typCount[tn]++; if( std::find( typs.begin(), typs.end(), tn )==typs.end() ){ typs.push_back( tn ); @@ -81,33 +134,112 @@ Node AlphaEquivalenceDb::addTerm(Node q) return ret; } -AlphaEquivalence::AlphaEquivalence() : d_termCanon(), d_aedb(&d_termCanon) {} +AlphaEquivalence::AlphaEquivalence(Env& env) + : EnvObj(env), + d_termCanon(), + d_aedb(&d_termCanon, true), + d_pnm(env.getProofNodeManager()), + d_pfAlpha(d_pnm ? new EagerProofGenerator(d_pnm) : nullptr) +{ +} -Node AlphaEquivalence::reduceQuantifier(Node q) +TrustNode AlphaEquivalence::reduceQuantifier(Node q) { Assert(q.getKind() == FORALL); - Trace("aeq") << "Alpha equivalence : register " << q << std::endl; - Node ret = d_aedb.addTerm(q); + Node ret; + std::vector<Node> vars; + std::vector<Node> 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<Node> 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<Node> 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<bool>()) + { + // ---------- MACRO_SR_PRED_INTRO + // sret = q + std::vector<Node> 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<ProofNode> 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<Node>& vars, + std::vector<Node>& 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<Node, std::map<Node, TNode> > 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<EagerProofGenerator> 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<Node> allVars[2]; + std::vector<Node> vars; + std::vector<Node> 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; |