summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/alpha_equivalence.cpp172
-rw-r--r--src/theory/quantifiers/alpha_equivalence.h60
-rw-r--r--src/theory/quantifiers/proof_checker.cpp36
-rw-r--r--src/theory/quantifiers/quantifiers_modules.cpp2
-rw-r--r--src/theory/quantifiers/quantifiers_modules.h2
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback