PfRule id,
const std::vector<Node>& children,
const std::vector<Node>& args,
- CDProof* cdp)
+ CDProof* cdp,
+ bool& continueUpdate)
{
return false;
}
ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm,
ProofNodeUpdaterCallback& cb)
- : d_pnm(pnm), d_cb(cb)
+ : d_pnm(pnm), d_cb(cb), d_debugFreeAssumps(false)
{
}
void ProofNodeUpdater::process(std::shared_ptr<ProofNode> pf)
+{
+ if (d_debugFreeAssumps)
+ {
+ if (Trace.isOn("pfnu-debug"))
+ {
+ Trace("pfnu-debug2") << "Initial proof: " << *pf.get() << std::endl;
+ Trace("pfnu-debug") << "ProofNodeUpdater::process" << std::endl;
+ Trace("pfnu-debug") << "Expected free assumptions: " << std::endl;
+ for (const Node& fa : d_freeAssumps)
+ {
+ Trace("pfnu-debug") << "- " << fa << std::endl;
+ }
+ std::vector<Node> assump;
+ expr::getFreeAssumptions(pf.get(), assump);
+ Trace("pfnu-debug") << "Current free assumptions: " << std::endl;
+ for (const Node& fa : assump)
+ {
+ Trace("pfnu-debug") << "- " << fa << std::endl;
+ }
+ }
+ }
+ processInternal(pf, d_freeAssumps);
+}
+
+void ProofNodeUpdater::processInternal(std::shared_ptr<ProofNode> pf,
+ const std::vector<Node>& fa)
{
Trace("pf-process") << "ProofNodeUpdater::process" << std::endl;
- std::unordered_map<ProofNode*, bool> visited;
- std::unordered_map<ProofNode*, bool>::iterator it;
- std::vector<ProofNode*> visit;
- ProofNode* cur;
- visit.push_back(pf.get());
- std::map<Node, ProofNode*>::iterator itc;
+ std::unordered_map<std::shared_ptr<ProofNode>, bool> visited;
+ std::unordered_map<std::shared_ptr<ProofNode>, bool>::iterator it;
+ std::vector<std::shared_ptr<ProofNode>> visit;
+ std::shared_ptr<ProofNode> cur;
+ visit.push_back(pf);
+ std::map<Node, std::shared_ptr<ProofNode>>::iterator itc;
// A cache from formulas to proof nodes that are in the current scope.
// Notice that we make a fresh recursive call to process if the current
// rule is SCOPE below.
- std::map<Node, ProofNode*> resCache;
- TNode res;
+ std::map<Node, std::shared_ptr<ProofNode>> resCache;
+ Node res;
do
{
cur = visit.back();
{
// already have a proof
visited[cur] = true;
- d_pnm->updateNode(cur, itc->second);
+ d_pnm->updateNode(cur.get(), itc->second.get());
}
else
{
visited[cur] = false;
- // run update first
- runUpdate(cur);
+ // run update to a fixed point
+ bool continueUpdate = true;
+ while (runUpdate(cur, fa, continueUpdate) && continueUpdate)
+ {
+ Trace("pf-process-debug") << "...updated proof." << std::endl;
+ }
+ if (!continueUpdate)
+ {
+ // no further changes should be made to cur according to the callback
+ Trace("pf-process-debug")
+ << "...marked to not continue update." << std::endl;
+ continue;
+ }
visit.push_back(cur);
+ // If we are not the top-level proof, we were a scope, or became a
+ // scope after updating, we need to make a separate recursive call to
+ // this method.
+ if (cur->getRule() == PfRule::SCOPE && cur != pf)
+ {
+ std::vector<Node> nfa;
+ // if we are debugging free assumptions, update the set
+ if (d_debugFreeAssumps)
+ {
+ nfa.insert(nfa.end(), fa.begin(), fa.end());
+ const std::vector<Node>& args = cur->getArguments();
+ nfa.insert(nfa.end(), args.begin(), args.end());
+ Trace("pfnu-debug2")
+ << "Process new scope with " << args << std::endl;
+ }
+ // Process in new call separately, since we should not cache
+ // the results of proofs that have a different scope.
+ processInternal(cur, nfa);
+ continue;
+ }
const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren();
// now, process children
for (const std::shared_ptr<ProofNode>& cp : ccp)
{
- if (cp->getRule() == PfRule::SCOPE)
- {
- // Process in new call separately, since we should not cache
- // the results of proofs that have a different scope.
- process(cp);
- continue;
- }
- visit.push_back(cp.get());
+ visit.push_back(cp);
}
}
}
visited[cur] = true;
// cache result
resCache[res] = cur;
+ if (d_debugFreeAssumps)
+ {
+ // 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;
+ pfnEnsureClosedWrt(
+ cur.get(), fa, "pfnu-debug", "ProofNodeUpdater:finalize");
+ }
}
} while (!visit.empty());
Trace("pf-process") << "ProofNodeUpdater::process: finished" << std::endl;
}
-void ProofNodeUpdater::runUpdate(ProofNode* cur)
+bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur,
+ const std::vector<Node>& fa,
+ bool& continueUpdate)
{
// should it be updated?
- if (!d_cb.shouldUpdate(cur))
+ if (!d_cb.shouldUpdate(cur.get()))
{
- return;
+ return false;
}
PfRule id = cur->getRule();
// use CDProof to open a scope for which the callback updates
<< "Updating (" << cur->getRule() << ")..." << std::endl;
Node res = cur->getResult();
// only if the callback updated the node
- if (d_cb.update(res, id, ccn, cur->getArguments(), &cpf))
+ if (d_cb.update(res, id, ccn, cur->getArguments(), &cpf, continueUpdate))
{
std::shared_ptr<ProofNode> npn = cpf.getProofFor(res);
+ std::vector<Node> fullFa;
+ if (d_debugFreeAssumps)
+ {
+ expr::getFreeAssumptions(cur.get(), fullFa);
+ Trace("pfnu-debug") << "Original proof : " << *cur << std::endl;
+ }
// then, update the original proof node based on this one
Trace("pf-process-debug") << "Update node..." << std::endl;
- d_pnm->updateNode(cur, npn.get());
+ d_pnm->updateNode(cur.get(), npn.get());
Trace("pf-process-debug") << "...update node finished." << std::endl;
+ if (d_debugFreeAssumps)
+ {
+ fullFa.insert(fullFa.end(), fa.begin(), fa.end());
+ // 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;
+ pfnEnsureClosedWrt(
+ npn.get(), fullFa, "pfnu-debug", "ProofNodeUpdater:postupdate");
+ }
+ Trace("pf-process-debug") << "..finished" << std::endl;
+ return true;
}
Trace("pf-process-debug") << "..finished" << std::endl;
+ return false;
+}
+
+void ProofNodeUpdater::setDebugFreeAssumptions(
+ const std::vector<Node>& freeAssumps)
+{
+ d_freeAssumps.clear();
+ d_freeAssumps.insert(
+ d_freeAssumps.end(), freeAssumps.begin(), freeAssumps.end());
+ d_debugFreeAssumps = true;
}
} // namespace CVC4
* Update the proof rule application, store steps in cdp. Return true if
* the proof changed. It can be assumed that cdp contains proofs of each
* fact in children.
+ *
+ * If continueUpdate is set to false in this method, then the resulting
+ * proof (the proof of res in cdp) is *not* called back to update by the
+ * proof node updater, nor are its children recursed. Otherwise, by default,
+ * the proof node updater will continue updating the resulting proof and will
+ * recursively update its children. This is analogous to marking REWRITE_DONE
+ * in a rewrite response.
*/
virtual bool update(Node res,
PfRule id,
const std::vector<Node>& children,
const std::vector<Node>& args,
- CDProof* cdp);
+ CDProof* cdp,
+ bool& continueUpdate);
};
/**
*/
void process(std::shared_ptr<ProofNode> pf);
+ /**
+ * Set free assumptions to freeAssumps. This indicates that we expect
+ * the proof we are processing to have free assumptions that are in
+ * freeAssumps. This enables checking when this is violated, which is
+ * expensive in general. It is not recommended that this method is called
+ * by default.
+ */
+ void setDebugFreeAssumptions(const std::vector<Node>& freeAssumps);
+
private:
/** The proof node manager */
ProofNodeManager* d_pnm;
/** The callback */
ProofNodeUpdaterCallback& d_cb;
+ /**
+ * Post-process, which performs the main post-processing technique described
+ * above.
+ */
+ void processInternal(std::shared_ptr<ProofNode> pf,
+ const 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.
+ * 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.
*/
- void runUpdate(ProofNode* cur);
+ bool runUpdate(std::shared_ptr<ProofNode> cur,
+ const std::vector<Node>& fa,
+ bool& continueUpdate);
+ /** Are we debugging free assumptions? */
+ bool d_debugFreeAssumps;
+ /** The initial free assumptions */
+ std::vector<Node> d_freeAssumps;
};
} // namespace CVC4
PfRule id,
const std::vector<Node>& children,
const std::vector<Node>& args,
- CDProof* cdp)
+ CDProof* cdp,
+ bool& continueUpdate)
{
Trace("smt-proof-pp-debug") << "- Post process " << id << " " << children
<< " / " << args << std::endl;
return !ret.isNull();
}
+bool ProofPostprocessCallback::updateInternal(Node res,
+ PfRule id,
+ const std::vector<Node>& children,
+ const std::vector<Node>& args,
+ CDProof* cdp)
+{
+ bool continueUpdate = true;
+ return update(res, id, children, args, cdp, continueUpdate);
+}
+
Node ProofPostprocessCallback::expandMacros(PfRule id,
const std::vector<Node>& children,
const std::vector<Node>& args,
{
Node eq = t.eqNode(ts);
// apply SUBS proof rule if necessary
- if (!update(eq, PfRule::SUBS, children, sargs, cdp))
+ if (!updateInternal(eq, PfRule::SUBS, children, sargs, cdp))
{
// if not elimianted, add as step
cdp->addStep(eq, PfRule::SUBS, children, sargs);
{
Node eq = ts.eqNode(tr);
// apply REWRITE proof rule
- if (!update(eq, PfRule::REWRITE, {}, rargs, cdp))
+ if (!updateInternal(eq, PfRule::REWRITE, {}, rargs, cdp))
{
// if not elimianted, add as step
cdp->addStep(eq, PfRule::REWRITE, {}, rargs);
projects / cvc5.git / commitdiff