}
else if (id == PfRule::SUBS)
{
+ NodeManager* nm = NodeManager::currentNM();
// Notice that a naive way to reconstruct SUBS is to do a term conversion
// proof for each substitution.
// The proof of f(a) * { a -> g(b) } * { b -> c } = f(g(c)) is:
builtin::BuiltinProofRuleChecker::getMethodId(args[1], ids);
}
std::vector<std::shared_ptr<CDProof>> pfs;
- std::vector<Node> vvec;
- std::vector<Node> svec;
+ std::vector<TNode> vsList;
+ std::vector<TNode> ssList;
+ std::vector<TNode> fromList;
std::vector<ProofGenerator*> pgs;
+ // first, compute the entire substitution
for (size_t i = 0, nchild = children.size(); i < nchild; i++)
+ {
+ // get the substitution
+ builtin::BuiltinProofRuleChecker::getSubstitutionFor(
+ children[i], vsList, ssList, fromList, ids);
+ // ensure proofs for each formula in fromList
+ if (children[i].getKind() == AND && ids == MethodId::SB_DEFAULT)
+ {
+ for (size_t j = 0, nchildi = children[i].getNumChildren(); j < nchildi;
+ j++)
+ {
+ Node nodej = nm->mkConst(Rational(j));
+ cdp->addStep(
+ children[i][j], PfRule::AND_ELIM, {children[i]}, {nodej});
+ }
+ }
+ }
+ std::vector<Node> vvec;
+ std::vector<Node> svec;
+ for (size_t i = 0, nvs = vsList.size(); i < nvs; i++)
{
// Note we process in forward order, since later substitution should be
// applied to earlier ones, and the last child of a SUBS is processed
// first.
- // get the substitution
- TNode var, subs;
- builtin::BuiltinProofRuleChecker::getSubstitution(
- children[i], var, subs, ids);
+ TNode var = vsList[i];
+ TNode subs = ssList[i];
+ TNode childFrom = fromList[i];
Trace("smt-proof-pp-debug")
- << "...process " << var << " -> " << subs << " (" << children[i]
- << ", " << ids << ")" << std::endl;
+ << "...process " << var << " -> " << subs << " (" << childFrom << ", "
+ << ids << ")" << std::endl;
// apply the current substitution to the range
if (!vvec.empty())
{
std::shared_ptr<CDProof> pf = std::make_shared<CDProof>(d_pnm);
pfs.push_back(pf);
// prove the updated substitution
- TConvProofGenerator tcg(d_pnm, nullptr, TConvPolicy::ONCE);
+ TConvProofGenerator tcg(d_pnm,
+ nullptr,
+ TConvPolicy::ONCE,
+ TConvCachePolicy::NEVER,
+ "nested_SUBS_TConvProofGenerator",
+ nullptr,
+ true);
// add previous rewrite steps
for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++)
{
Assert(pfn != nullptr);
// add the proof
pf->addProof(pfn);
- // get proof for children[i] from cdp
- pfn = cdp->getProofFor(children[i]);
+ // get proof for childFrom from cdp
+ pfn = cdp->getProofFor(childFrom);
pf->addProof(pfn);
// ensure we have a proof of var = subs
- Node veqs = addProofForSubsStep(var, subs, children[i], pf.get());
+ Node veqs = addProofForSubsStep(var, subs, childFrom, pf.get());
// transitivity
pf->addStep(var.eqNode(ss), PfRule::TRANS, {veqs, seqss}, {});
// add to the substitution
}
// Just use equality from CDProof, but ensure we have a proof in cdp.
// This may involve a TRUE_INTRO/FALSE_INTRO if the substitution step
- // uses the assumption children[i] as a Boolean assignment (e.g.
- // children[i] = true if we are using MethodId::SB_LITERAL).
- addProofForSubsStep(var, subs, children[i], cdp);
+ // uses the assumption childFrom as a Boolean assignment (e.g.
+ // childFrom = true if we are using MethodId::SB_LITERAL).
+ addProofForSubsStep(var, subs, childFrom, cdp);
vvec.push_back(var);
svec.push_back(subs);
pgs.push_back(cdp);
if (ts != t)
{
// should be implied by the substitution now
- TConvProofGenerator tcpg(d_pnm, nullptr, TConvPolicy::ONCE);
+ TConvProofGenerator tcpg(d_pnm,
+ nullptr,
+ TConvPolicy::ONCE,
+ TConvCachePolicy::NEVER,
+ "SUBS_TConvProofGenerator",
+ nullptr,
+ true);
for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++)
{
// not necessarily closed, so we pass false to addRewriteStep.
std::shared_ptr<ProofNode> pfn = trn.toProofNode();
if (pfn == nullptr)
{
+ Trace("smt-proof-pp-debug")
+ << "Use TRUST_REWRITE for " << eq << std::endl;
// did not have a proof of rewriting, probably isExtEq is true
+ if (isExtEq)
+ {
+ // don't update
+ return Node::null();
+ }
cdp->addStep(eq, PfRule::TRUST_REWRITE, {}, {eq});
}
else
ProofNodeManager* pnm)
: d_ruleCount("finalProof::ruleCount"),
d_totalRuleCount("finalProof::totalRuleCount", 0),
+ d_minPedanticLevel("finalProof::minPedanticLevel", 10),
+ d_numFinalProofs("finalProofs::numFinalProofs", 0),
d_pnm(pnm),
d_pedanticFailure(false)
{
smtStatisticsRegistry()->registerStat(&d_ruleCount);
smtStatisticsRegistry()->registerStat(&d_totalRuleCount);
+ smtStatisticsRegistry()->registerStat(&d_minPedanticLevel);
+ smtStatisticsRegistry()->registerStat(&d_numFinalProofs);
}
ProofPostprocessFinalCallback::~ProofPostprocessFinalCallback()
{
smtStatisticsRegistry()->unregisterStat(&d_ruleCount);
smtStatisticsRegistry()->unregisterStat(&d_totalRuleCount);
+ smtStatisticsRegistry()->unregisterStat(&d_minPedanticLevel);
+ smtStatisticsRegistry()->unregisterStat(&d_numFinalProofs);
}
void ProofPostprocessFinalCallback::initializeUpdate()
{
d_pedanticFailure = false;
d_pedanticFailureOut.str("");
+ ++d_numFinalProofs;
}
bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
}
}
}
+ uint32_t plevel = d_pnm->getChecker()->getPedanticLevel(r);
+ if (plevel != 0)
+ {
+ d_minPedanticLevel.minAssign(plevel);
+ }
// record stats for the rule
d_ruleCount << r;
++d_totalRuleCount;
pc->registerChecker(PfRule::REMOVE_TERM_FORMULA_AXIOM, this);
// trusted rules
pc->registerTrustedChecker(PfRule::THEORY_LEMMA, this, 1);
- pc->registerTrustedChecker(PfRule::PREPROCESS, this, 2);
- pc->registerTrustedChecker(PfRule::PREPROCESS_LEMMA, this, 2);
- pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS, this, 2);
- pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS_LEMMA, this, 2);
- pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 2);
+ pc->registerTrustedChecker(PfRule::PREPROCESS, this, 3);
+ pc->registerTrustedChecker(PfRule::PREPROCESS_LEMMA, this, 3);
+ pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS, this, 3);
+ pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS_LEMMA, this, 3);
+ pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 3);
pc->registerTrustedChecker(PfRule::TRUST_REWRITE, this, 1);
pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1);
}
return n;
}
-bool BuiltinProofRuleChecker::getSubstitution(Node exp,
- TNode& var,
- TNode& subs,
- MethodId ids)
+bool BuiltinProofRuleChecker::getSubstitutionForLit(Node exp,
+ TNode& var,
+ TNode& subs,
+ MethodId ids)
{
if (ids == MethodId::SB_DEFAULT)
{
return true;
}
+bool BuiltinProofRuleChecker::getSubstitutionFor(Node exp,
+ std::vector<TNode>& vars,
+ std::vector<TNode>& subs,
+ std::vector<TNode>& from,
+ MethodId ids)
+{
+ TNode v;
+ TNode s;
+ if (exp.getKind() == AND && ids == MethodId::SB_DEFAULT)
+ {
+ for (const Node& ec : exp)
+ {
+ // non-recursive, do not use nested AND
+ if (!getSubstitutionForLit(ec, v, s, ids))
+ {
+ return false;
+ }
+ vars.push_back(v);
+ subs.push_back(s);
+ from.push_back(ec);
+ }
+ return true;
+ }
+ bool ret = getSubstitutionForLit(exp, v, s, ids);
+ vars.push_back(v);
+ subs.push_back(s);
+ from.push_back(exp);
+ return ret;
+}
+
Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids)
{
- TNode var, subs;
- if (!getSubstitution(exp, var, subs, ids))
+ std::vector<TNode> vars;
+ std::vector<TNode> subs;
+ std::vector<TNode> from;
+ if (!getSubstitutionFor(exp, vars, subs, from, ids))
{
return Node::null();
}
- Trace("builtin-pfcheck-debug")
- << "applySubstitution (" << ids << "): " << var << " -> " << subs
- << " (from " << exp << ")" << std::endl;
- return n.substitute(var, subs);
+ Node ns = n;
+ // apply substitution one at a time, in reverse order
+ for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
+ {
+ TNode v = vars[nvars - 1 - i];
+ TNode s = subs[nvars - 1 - i];
+ Trace("builtin-pfcheck-debug")
+ << "applySubstitution (" << ids << "): " << v << " -> " << s
+ << " (from " << exp << ")" << std::endl;
+ ns = ns.substitute(v, s);
+ }
+ return ns;
}
Node BuiltinProofRuleChecker::applySubstitution(Node n,
}
else if (id == PfRule::SCOPE)
{
+ NodeManager * nm = NodeManager::currentNM();
Assert(children.size() == 1);
if (args.empty())
{
{
return ant.notNode();
}
- return NodeManager::currentNM()->mkNode(IMPLIES, ant, children[0]);
+ return nm->mkNode(IMPLIES, ant, children[0]);
}
else if (id == PfRule::SUBS)
{
{
return Node::null();
}
- Node res = applySubstitutionRewrite(args[0], children, idr);
+ Node res = applySubstitutionRewrite(args[0], children, ids, idr);
return args[0].eqNode(res);
}
else if (id == PfRule::MACRO_SR_PRED_INTRO)
*/
Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE);
/**
- * Get substitution. Updates vars/subs to the substitution specified by
- * exp for the substitution method ids.
+ * Get substitution for literal exp. Updates vars/subs to the substitution
+ * specified by exp for the substitution method ids.
*/
- static bool getSubstitution(Node exp,
- TNode& var,
- TNode& subs,
- MethodId ids = MethodId::SB_DEFAULT);
+ static bool getSubstitutionForLit(Node exp,
+ TNode& var,
+ TNode& subs,
+ MethodId ids = MethodId::SB_DEFAULT);
+ /**
+ * Get substitution for formula exp. Adds to vars/subs to the substitution
+ * specified by exp for the substitution method ids, which may be multiple
+ * substitutions if exp is of kind AND and ids is SB_DEFAULT (note the other
+ * substitution types always interpret applications of AND as a formula).
+ * The vector "from" are the literals from exp that each substitution in
+ * vars/subs are based on. For example, if exp is (and (= x t) (= y s)), then
+ * vars = { x, y }, subs = { t, s }, from = { (= x y), (= y s) }.
+ */
+ static bool getSubstitutionFor(Node exp,
+ std::vector<TNode>& vars,
+ std::vector<TNode>& subs,
+ std::vector<TNode>& from,
+ MethodId ids = MethodId::SB_DEFAULT);
/**
* Apply substitution on n in skolem form. This encapsulates the exact
projects / cvc5.git / commitdiff