This formalizes the proofs of existentials that justify purification variables, e.g. those with witness form witness x. x = t for the term t they purify.
This PR generalizes EXISTS_INTRO to do this, and makes some simplifications to SkolemManager.
WITNESS_INTRO,
// ======== Exists intro
// Children: (P:F[t])
- // Arguments: (t)
+ // Arguments: ((exists ((x T)) F[x]))
// ----------------------------------------
// Conclusion: (exists ((x T)) F[x])
- // where x is a BOUND_VARIABLE unique to the pair F,t.
+ // This rule verifies that F[x] indeed matches F[t] with a substitution
+ // over x.
EXISTS_INTRO,
// ======== Skolemize
// Children: (P:(exists ((x1 T1) ... (xn Tn)) F))
};
typedef expr::Attribute<SkolemFormAttributeId, Node> SkolemFormAttribute;
+// Maps terms to their purify skolem variables
struct PurifySkolemAttributeId
{
};
// method deterministic ensures that the proof checker (e.g. for
// quantifiers) is capable of proving the expected value for conclusions
// of proof rules, instead of an alpha-equivalent variant of a conclusion.
- Node avp = getOrMakeBoundVariable(av, av);
+ Node avp = getOrMakeBoundVariable(av);
ovarsW.push_back(avp);
ovars.push_back(av);
}
return mkPurifySkolem(t, "", "", NodeManager::SKOLEM_BOOL_TERM_VAR);
}
-Node SkolemManager::mkExistential(Node t, Node p)
+ProofGenerator* SkolemManager::getProofGenerator(Node t) const
{
- Assert(p.getType().isBoolean());
- NodeManager* nm = NodeManager::currentNM();
- Node v = getOrMakeBoundVariable(t, p);
- Node bvl = nm->mkNode(BOUND_VAR_LIST, v);
- Node psubs = p.substitute(TNode(t), TNode(v));
- return nm->mkNode(EXISTS, bvl, psubs);
-}
-
-ProofGenerator* SkolemManager::getProofGenerator(Node t)
-{
- std::map<Node, ProofGenerator*>::iterator it = d_gens.find(t);
+ std::map<Node, ProofGenerator*>::const_iterator it = d_gens.find(t);
if (it != d_gens.end())
{
return it->second;
return k;
}
-Node SkolemManager::getOrMakeBoundVariable(Node t, Node s)
+Node SkolemManager::getOrMakeBoundVariable(Node t)
{
- std::pair<Node, Node> key(t, s);
- std::map<std::pair<Node, Node>, Node>::iterator it =
- d_witnessBoundVar.find(key);
+ std::map<Node, Node>::iterator it = d_witnessBoundVar.find(t);
if (it != d_witnessBoundVar.end())
{
return it->second;
}
TypeNode tt = t.getType();
Node v = NodeManager::currentNM()->mkBoundVar(tt);
- d_witnessBoundVar[key] = v;
+ d_witnessBoundVar[t] = v;
return v;
}
* Get proof generator for existentially quantified formula q. This returns
* the proof generator that was provided in a call to mkSkolem above.
*/
- ProofGenerator* getProofGenerator(Node q);
- /**
- * Make existential. Given t and p[t] where p is a formula, this returns
- * (exists ((x T)) p[x])
- * where T is the type of t, and x is a variable unique to t,p.
- */
- Node mkExistential(Node t, Node p);
+ ProofGenerator* getProofGenerator(Node q) const;
/**
* Convert to witness form, where notice this recursively replaces *all*
* skolems in n by their corresponding witness term. This is intended to be
* Map to canonical bound variables. This is used for example by the method
* mkExistential.
*/
- std::map<std::pair<Node, Node>, Node> d_witnessBoundVar;
+ std::map<Node, Node> d_witnessBoundVar;
/** Convert to witness or skolem form */
static Node convertInternal(Node n, bool toWitness);
/** Get or make skolem attribute for witness term w */
const std::string& comment = "",
int flags = NodeManager::SKOLEM_DEFAULT);
/**
- * Get or make bound variable unique to (s,t), for d_witnessBoundVar, where
- * t and s are terms.
+ * Get or make bound variable unique to t whose type is the same as t. This
+ * is used to construct canonical bound variables e.g. for constructing
+ * bound variables for witness terms in the skolemize method above.
*/
- Node getOrMakeBoundVariable(Node t, Node s);
+ Node getOrMakeBoundVariable(Node t);
};
} // namespace CVC4
"WfGenerator::TConvProofGenerator",
nullptr,
true),
- d_wintroPf(pnm, nullptr, nullptr, "WfGenerator::LazyCDProof")
+ d_wintroPf(pnm, nullptr, nullptr, "WfGenerator::LazyCDProof"),
+ d_pskPf(pnm, nullptr, "WfGenerator::PurifySkolemProof")
{
}
Node skBody = SkolemManager::getSkolemForm(curw[1]);
Node exists = nm->mkNode(kind::EXISTS, curw[0], skBody);
ProofGenerator* pg = skm->getProofGenerator(exists);
+ if (pg == nullptr)
+ {
+ // it may be a purification skolem
+ pg = convertExistsInternal(exists);
+ if (pg == nullptr)
+ {
+ // if no proof generator is provided, we justify the existential
+ // using the WITNESS_AXIOM trusted rule by providing it to the
+ // call to addLazyStep below.
+ Trace("witness-form")
+ << "WitnessFormGenerator: No proof generator for " << exists
+ << std::endl;
+ }
+ }
// --------------------------- from pg
// (exists ((x T)) (P x))
// --------------------------- WITNESS_INTRO
return d_eqs;
}
+ProofGenerator* WitnessFormGenerator::convertExistsInternal(Node exists)
+{
+ Assert(exists.getKind() == kind::EXISTS);
+ if (exists[0].getNumChildren() == 1 && exists[1].getKind() == kind::EQUAL
+ && exists[1][0] == exists[0][0])
+ {
+ Node tpurified = exists[1][1];
+ Trace("witness-form") << "convertExistsInternal: infer purification "
+ << exists << " for " << tpurified << std::endl;
+ // ------ REFL
+ // t = t
+ // ---------------- EXISTS_INTRO
+ // exists x. x = t
+ // The concluded existential is then used to construct the witness term
+ // via witness intro.
+ Node teq = tpurified.eqNode(tpurified);
+ d_pskPf.addStep(teq, PfRule::REFL, {}, {tpurified});
+ d_pskPf.addStep(exists, PfRule::EXISTS_INTRO, {teq}, {exists});
+ return &d_pskPf;
+ }
+ return nullptr;
+}
+
} // namespace smt
} // namespace CVC4
* of this class (d_tcpg).
*/
Node convertToWitnessForm(Node t);
+ /**
+ * Return a proof generator that can prove the given axiom exists.
+ */
+ ProofGenerator* convertExistsInternal(Node exists);
/** The term conversion proof generator */
TConvProofGenerator d_tcpg;
/** The nodes we have already added rewrite steps for in d_tcpg */
std::unordered_set<Node, NodeHashFunction> d_eqs;
/** Lazy proof storing witness intro steps */
LazyCDProof d_wintroPf;
+ /** CDProof for justifying purification existentials */
+ CDProof d_pskPf;
};
} // namespace smt
#include "theory/quantifiers/proof_checker.h"
+#include "expr/node_algorithm.h"
#include "expr/skolem_manager.h"
#include "theory/builtin/proof_checker.h"
Assert(children.size() == 1);
Assert(args.size() == 1);
Node p = children[0];
- Node t = args[0];
- return sm->mkExistential(t, p);
+ Node exists = args[0];
+ if (exists.getKind() != kind::EXISTS || exists[0].getNumChildren() != 1)
+ {
+ return Node::null();
+ }
+ std::unordered_map<Node, Node, NodeHashFunction> subs;
+ if (!expr::match(exists[1], p, subs))
+ {
+ return Node::null();
+ }
+ // substitution must contain only the variable of the existential
+ for (const std::pair<const Node, Node>& s : subs)
+ {
+ if (s.first != exists[0][0])
+ {
+ return Node::null();
+ }
+ }
+ return exists;
}
else if (id == PfRule::WITNESS_INTRO)
{
projects / cvc5.git / commitdiff