diff options
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/proof_node_updater.cpp | 112 | ||||
| -rw-r--r-- | src/expr/proof_node_updater.h | 11 |
2 files changed, 91 insertions, 32 deletions
diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp index 1e8fe4e7d..55eebb0d1 100644 --- a/src/expr/proof_node_updater.cpp +++ b/src/expr/proof_node_updater.cpp @@ -15,12 +15,22 @@ #include "expr/proof_node_updater.h" #include "expr/lazy_proof.h" +#include "expr/proof_node_algorithm.h" namespace CVC4 { ProofNodeUpdaterCallback::ProofNodeUpdaterCallback() {} ProofNodeUpdaterCallback::~ProofNodeUpdaterCallback() {} +bool ProofNodeUpdaterCallback::update(Node res, + PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args, + CDProof* cdp) +{ + return false; +} + ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm, ProofNodeUpdaterCallback& cb) : d_pnm(pnm), d_cb(cb) @@ -30,53 +40,95 @@ ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm, void ProofNodeUpdater::process(std::shared_ptr<ProofNode> pf) { Trace("pf-process") << "ProofNodeUpdater::process" << std::endl; - std::unordered_set<ProofNode*> visited; - std::unordered_set<ProofNode*>::iterator it; + 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; + // 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; do { cur = visit.back(); visit.pop_back(); it = visited.find(cur); + res = cur->getResult(); if (it == visited.end()) { - visited.insert(cur); - // should it be updated? - if (d_cb.shouldUpdate(cur)) + itc = resCache.find(res); + if (itc != resCache.end()) { - PfRule id = cur->getRule(); - // use CDProof to open a scope for which the callback updates - CDProof cpf(d_pnm); - const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren(); - std::vector<Node> ccn; - for (const std::shared_ptr<ProofNode>& cp : cc) - { - Node cpres = cp->getResult(); - ccn.push_back(cpres); - // store in the proof - cpf.addProof(cp); - } - // only if the callback updated the node - if (d_cb.update(id, ccn, cur->getArguments(), &cpf)) - { - // build the proof, which should be closed - std::shared_ptr<ProofNode> npn = cpf.getProofFor(cur->getResult()); - Assert(npn->isClosed()); - // then, update the original proof node based on this one - d_pnm->updateNode(cur, npn.get()); - } + // already have a proof + visited[cur] = true; + d_pnm->updateNode(cur, itc->second); } - const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren(); - // now, process children - for (const std::shared_ptr<ProofNode>& cp : ccp) + else { - visit.push_back(cp.get()); + visited[cur] = false; + // run update first + runUpdate(cur); + visit.push_back(cur); + 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()); + } } } + else if (!it->second) + { + visited[cur] = true; + // cache result + resCache[res] = cur; + } } while (!visit.empty()); Trace("pf-process") << "ProofNodeUpdater::process: finished" << std::endl; } +void ProofNodeUpdater::runUpdate(ProofNode* cur) +{ + // should it be updated? + if (!d_cb.shouldUpdate(cur)) + { + return; + } + PfRule id = cur->getRule(); + // use CDProof to open a scope for which the callback updates + CDProof cpf(d_pnm); + const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren(); + std::vector<Node> ccn; + for (const std::shared_ptr<ProofNode>& cp : cc) + { + Node cpres = cp->getResult(); + ccn.push_back(cpres); + // store in the proof + cpf.addProof(cp); + } + Trace("pf-process-debug") + << "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)) + { + std::shared_ptr<ProofNode> npn = cpf.getProofFor(res); + // then, update the original proof node based on this one + Trace("pf-process-debug") << "Update node..." << std::endl; + d_pnm->updateNode(cur, npn.get()); + Trace("pf-process-debug") << "...update node finished." << std::endl; + } + Trace("pf-process-debug") << "..finished" << std::endl; +} + } // namespace CVC4 diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h index be7a120ee..061a12310 100644 --- a/src/expr/proof_node_updater.h +++ b/src/expr/proof_node_updater.h @@ -42,10 +42,11 @@ class ProofNodeUpdaterCallback * the proof changed. It can be assumed that cdp contains proofs of each * fact in children. */ - virtual bool update(PfRule id, + virtual bool update(Node res, + PfRule id, const std::vector<Node>& children, const std::vector<Node>& args, - CDProof* cdp) = 0; + CDProof* cdp); }; /** @@ -72,6 +73,12 @@ class ProofNodeUpdater ProofNodeManager* d_pnm; /** The callback */ ProofNodeUpdaterCallback& d_cb; + /** + * 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. + */ + void runUpdate(ProofNode* cur); }; } // namespace CVC4 |