Previously in the proof node updater only structural reasoning was done at post-visit time (merging subproofs, checking free assumptions). This commit adds a virtual method to allow updating the proof node at post-visit time.
In particular this commit is important to functionality in the alethe post processing that is deactivated in master.
CC @Lachnitt
return pn->getRule() != PfRule::ALETHE_RULE;
}
+bool AletheProofPostprocessCallback::shouldUpdatePost(
+ std::shared_ptr<ProofNode> pn, const std::vector<Node>& fa)
+{
+ Assert(!pn->getArguments().empty());
+ AletheRule rule = getAletheRule(pn->getArguments()[0]);
+ return rule == AletheRule::RESOLUTION || rule == AletheRule::REORDERING
+ || rule == AletheRule::CONTRACTION;
+}
+
bool AletheProofPostprocessCallback::update(Node res,
PfRule id,
const std::vector<Node>& children,
return success;
}
case PfRule::THEORY_REWRITE:
- {
- return addAletheStep(AletheRule::ALL_SIMPLIFY,
+ {
+ return addAletheStep(AletheRule::ALL_SIMPLIFY,
res,
nm->mkNode(kind::SEXPR, d_cl, res),
children,
}
// Adds an OR rule to the premises of a step if the premise is not a clause and
-// should not be a singleton. Since FACTORING and REORDERING always take
+// should not be a singleton. Since CONTRACTION and REORDERING always take
// non-singletons, this function adds an OR step to their premise if it was
// formerly printed as (cl (or F1 ... Fn)). For resolution, it is necessary to
// check all children to find out whether they're singleton before determining
// if they are already printed correctly.
-bool AletheProofPostprocessCallback::finalize(Node res,
- PfRule id,
- const std::vector<Node>& children,
- const std::vector<Node>& args,
- CDProof* cdp)
+bool AletheProofPostprocessCallback::updatePost(
+ Node res,
+ PfRule id,
+ const std::vector<Node>& children,
+ const std::vector<Node>& args,
+ CDProof* cdp)
{
NodeManager* nm = NodeManager::currentNM();
AletheRule rule = getAletheRule(args[0]);
}
return false;
}
- default: return false;
+ default:
+ {
+ Unreachable();
+ return false;
+ }
}
return false;
}
const std::vector<Node>& args,
CDProof* cdp,
bool& continueUpdate) override;
+ /** Should proof pn be updated at post-visit?
+ *
+ * Only if its top-level Alethe proof rule is RESOLUTION, REORDERING, or
+ * CONTRACTION.
+ */
+ bool shouldUpdatePost(std::shared_ptr<ProofNode> pn,
+ const std::vector<Node>& fa) override;
/**
* This method is used to add an additional application of the or-rule between
* a conclusion (cl (or F1 ... Fn)) and a rule that uses this conclusion as a
* premise and treats it as a clause, i.e. assumes that it has been printed
* as (cl F1 ... Fn).
*/
- bool finalize(Node res,
- PfRule id,
- const std::vector<Node>& children,
- const std::vector<Node>& args,
- CDProof* cdp);
+ bool updatePost(Node res,
+ PfRule id,
+ const std::vector<Node>& children,
+ const std::vector<Node>& args,
+ CDProof* cdp) override;
/**
* This method is used to add some last steps to a proof when this is
* necessary. The final step should always be printed as (cl). However:
return false;
}
+bool ProofNodeUpdaterCallback::shouldUpdatePost(std::shared_ptr<ProofNode> pn,
+ const std::vector<Node>& fa)
+{
+ return false;
+}
+
+bool ProofNodeUpdaterCallback::updatePost(Node res,
+ PfRule id,
+ const std::vector<Node>& children,
+ const std::vector<Node>& args,
+ CDProof* cdp)
+{
+ return false;
+}
+
ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm,
ProofNodeUpdaterCallback& cb,
bool mergeSubproofs,
Trace("pf-process") << "ProofNodeUpdater::process: finished" << std::endl;
}
-bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur,
- const std::vector<Node>& fa,
- bool& continueUpdate)
+bool ProofNodeUpdater::updateProofNode(std::shared_ptr<ProofNode> cur,
+ const std::vector<Node>& fa,
+ bool& continueUpdate,
+ bool preVisit)
{
- // should it be updated?
- if (!d_cb.shouldUpdate(cur, fa, continueUpdate))
- {
- return false;
- }
PfRule id = cur->getRule();
// use CDProof to open a scope for which the callback updates
CDProof cpf(d_pnm, nullptr, "ProofNodeUpdater::CDProof", d_autoSym);
Trace("pf-process-debug")
<< "Updating (" << cur->getRule() << "): " << res << std::endl;
// only if the callback updated the node
- if (d_cb.update(res, id, ccn, cur->getArguments(), &cpf, continueUpdate))
+ if (preVisit
+ ? d_cb.update(res, id, ccn, cur->getArguments(), &cpf, continueUpdate)
+ : d_cb.updatePost(res, id, ccn, cur->getArguments(), &cpf))
{
std::shared_ptr<ProofNode> npn = cpf.getProofFor(res);
std::vector<Node> fullFa;
// We have that npn is a node we occurring the final updated version of
// the proof. We can now debug based on the expected set of free
// assumptions.
- Trace("pfnu-debug") << "Ensure update closed..." << std::endl;
+ Trace("pfnu-debug") << "Ensure updated closed..." << std::endl;
pfnEnsureClosedWrt(
npn.get(), fullFa, "pfnu-debug", "ProofNodeUpdater:postupdate");
}
return false;
}
+bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur,
+ const std::vector<Node>& fa,
+ bool& continueUpdate,
+ bool preVisit)
+{
+ // should it be updated?
+ if (preVisit ? !d_cb.shouldUpdate(cur, fa, continueUpdate)
+ : !d_cb.shouldUpdatePost(cur, fa))
+ {
+ return false;
+ }
+ return updateProofNode(cur, fa, continueUpdate, preVisit);
+}
+
void ProofNodeUpdater::runFinalize(
std::shared_ptr<ProofNode> cur,
const std::vector<Node>& fa,
std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& resCacheNcWaiting,
std::unordered_map<const ProofNode*, bool>& cfaMap)
{
+ // run update (marked as post-visit) to a fixed point
+ bool dummyContinueUpdate;
+ while (runUpdate(cur, fa, dummyContinueUpdate, false))
+ {
+ Trace("pf-process-debug") << "...updated proof." << std::endl;
+ }
if (d_mergeSubproofs)
{
Node res = cur->getResult();
const std::vector<Node>& args,
CDProof* cdp,
bool& continueUpdate);
+
+ /** As above, but at post-visit.
+ *
+ * We do not pass a continueUpdate flag to this method, or the one below,
+ * since the children of this proof node have already been updated.
+ */
+ virtual bool shouldUpdatePost(std::shared_ptr<ProofNode> pn,
+ const std::vector<Node>& fa);
+
+ /** As above, but at post-visit. */
+ virtual bool updatePost(Node res,
+ PfRule id,
+ const std::vector<Node>& children,
+ const std::vector<Node>& args,
+ CDProof* cdp);
};
/**
*/
void processInternal(std::shared_ptr<ProofNode> pf, std::vector<Node>& fa);
/**
- * Update proof node cur based on the callback. This modifies curr using
- * ProofNodeManager::updateNode based on the proof node constructed to
- * replace it by the callback. Return true if cur was updated. If
- * continueUpdate is updated to false, then cur is not updated further
- * and its children are not traversed.
+ * Update proof node cur based on the callback and on whether we are updating
+ * at pre visit or post visit time. This modifies curr using
+ * ProofNodeManager::updateNode based on the proof node constructed to replace
+ * it by the callback. If we are debugging free assumptions, the set fa is
+ * used to check whether the updated proof node is closed with relation to
+ * them. Return true if cur was updated, and continueUpdate may be set to
+ * false by the callback.
+ */
+ bool updateProofNode(std::shared_ptr<ProofNode> cur,
+ const std::vector<Node>& fa,
+ bool& continueUpdate,
+ bool preVisit);
+ /**
+ * Update the node cur if it should be updated according to the callback. How
+ * the callback performs the update, if at all, depends if we are at pre- or
+ * post-visit time. If continueUpdate is updated to false, then cur is not
+ * updated further and its children are not traversed (when pre-visiting).
*/
bool runUpdate(std::shared_ptr<ProofNode> cur,
const std::vector<Node>& fa,
- bool& continueUpdate);
+ bool& continueUpdate,
+ bool preVisit = true);
/**
* Finalize the node cur. This is called at the moment that it is established
- * that cur will appear in the final proof. We do any final debug checking
- * and add it to resCache/resCacheNcWaiting if we are merging subproofs, where
- * these map result formulas to proof nodes with/without assumptions.
+ * that cur will appear in the final proof. We do any final debug checking and
+ * add it to resCache/resCacheNcWaiting if we are merging subproofs, where
+ * these map result formulas to proof nodes with/without assumptions. If we
+ * are updating nodes at post visit time, then we run updateProofNode on it.
+ *
*/
void runFinalize(std::shared_ptr<ProofNode> cur,
const std::vector<Node>& fa,
projects / cvc5.git / commitdiff