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.
return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited);
}
+Node TermCanonize::getCanonicalTerm(TNode n,
+ std::map<TNode, Node>& visited,
+ bool apply_torder,
+ bool doHoVar)
+{
+ std::map<std::pair<TypeNode, uint32_t>, unsigned> var_count;
+ return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited);
+}
+
} // namespace expr
} // namespace cvc5
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<TNode, Node>& visited,
+ bool apply_torder = false,
+ bool doHoVar = true);
private:
/** The (optional) type class callback */
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";
// 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)
// Conclusion: F
// where F is an equality of the form t = QuantifiersPreprocess::preprocess(t)
QUANTIFIERS_PREPROCESS,
-
//================================================= String rules
//======================== Core solver
// ======== Concat eq
#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 {
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 );
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
#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 {
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
* 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;
};
}
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);
}
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());
}
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())
namespace cvc5 {
namespace theory {
-
+
class QuantifiersEngine;
class DecisionManager;
// 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)
NodeSet d_quants_prereg;
/** quantifiers reduced */
BoolMap d_quants_red;
- std::map<Node, Node> d_quants_red_lem;
/** Number of rounds we have instantiated */
uint32_t d_numInstRoundsLemma;
}; /* class QuantifiersEngine */
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
--- /dev/null
+(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)
projects / cvc5.git / commitdiff