diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-17 11:57:07 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-17 11:57:07 -0500 |
commit | c431160c5c9d706cd6424dc6c4b9b316ff8a5941 (patch) | |
tree | 8e4c55f5ffcda6ab373d4c3a0ffb5e296e9f93a1 /src/expr/proof.cpp | |
parent | b4eeffd63cc00369ec6b47ed4289577af3dec4eb (diff) |
Add (context-dependent) Proof (#4323)
A (context-dependent) collection of proof steps that are linked to together to form a ProofNode dag.
Note that the name "Proof" is currently taken. I am calling this class "CDProof", although it is optionally context dependent.
Diffstat (limited to 'src/expr/proof.cpp')
-rw-r--r-- | src/expr/proof.cpp | 162 |
1 files changed, 162 insertions, 0 deletions
diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp new file mode 100644 index 000000000..6d2d70543 --- /dev/null +++ b/src/expr/proof.cpp @@ -0,0 +1,162 @@ +/********************* */ +/*! \file proof.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of proof + **/ + +#include "expr/proof.h" + +using namespace CVC4::kind; + +namespace CVC4 { + +CDProof::CDProof(ProofNodeManager* pnm, context::Context* c) + : d_manager(pnm), d_context(), d_nodes(c ? c : &d_context) +{ +} + +CDProof::~CDProof() {} + +std::shared_ptr<ProofNode> CDProof::getProof(Node fact) const +{ + NodeProofNodeMap::iterator it = d_nodes.find(fact); + if (it != d_nodes.end()) + { + return (*it).second; + } + return nullptr; +} + +bool CDProof::addStep(Node expected, + PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args, + bool ensureChildren, + bool forceOverwrite) +{ + // we must provide expected + Assert(!expected.isNull()); + + NodeProofNodeMap::iterator it = d_nodes.find(expected); + if (it != d_nodes.end()) + { + if (!forceOverwrite + && ((*it).second->getId() != PfRule::ASSUME || id == PfRule::ASSUME)) + { + // we do not overwrite if forceOverwrite is false and the previously + // provided step was not an assumption, or if the currently provided step + // is a (duplicate) assumption + return true; + } + // we will overwrite the existing proof node by updating its contents below + } + + // collect the child proofs, for each premise + std::vector<std::shared_ptr<ProofNode>> pchildren; + for (const Node& c : children) + { + std::shared_ptr<ProofNode> pc = getProof(c); + if (pc == nullptr) + { + if (ensureChildren) + { + // failed to get a proof for a child, fail + return false; + } + // otherwise, we initialize it as an assumption + std::vector<Node> pcargs = {c}; + std::vector<std::shared_ptr<ProofNode>> pcassume; + pc = d_manager->mkNode(PfRule::ASSUME, pcassume, pcargs, c); + // assumptions never fail to check + Assert(pc != nullptr); + d_nodes.insert(c, pc); + } + pchildren.push_back(pc); + } + + // create or update it + std::shared_ptr<ProofNode> pthis; + if (it == d_nodes.end()) + { + pthis = d_manager->mkNode(id, pchildren, args, expected); + if (pthis == nullptr) + { + // failed to construct the node, perhaps due to a proof checking failure + return false; + } + d_nodes.insert(expected, pthis); + } + else + { + // update its value + pthis = (*it).second; + d_manager->updateNode(pthis.get(), id, pchildren, args); + } + // the result of the proof node should be expected + Assert(pthis->getResult() == expected); + return true; +} + +bool CDProof::addProof(ProofNode* pn, bool forceOverwrite) +{ + std::unordered_map<ProofNode*, bool> visited; + std::unordered_map<ProofNode*, bool>::iterator it; + std::vector<ProofNode*> visit; + ProofNode* cur; + Node curFact; + visit.push_back(pn); + bool retValue = true; + do + { + cur = visit.back(); + curFact = cur->getResult(); + visit.pop_back(); + it = visited.find(cur); + if (it == visited.end()) + { + // visit the children + visited[cur] = false; + visit.push_back(cur); + const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren(); + for (const std::shared_ptr<ProofNode>& c : cs) + { + visit.push_back(c.get()); + } + } + else if (!it->second) + { + // we always call addStep, which may or may not overwrite the + // current step + std::vector<Node> pexp; + const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren(); + for (const std::shared_ptr<ProofNode>& c : cs) + { + Assert(!c->getResult().isNull()); + pexp.push_back(c->getResult()); + } + // can ensure children at this point + bool res = addStep(curFact, + cur->getId(), + pexp, + cur->getArguments(), + true, + forceOverwrite); + // should always succeed + Assert(res); + retValue = retValue && res; + visited[cur] = true; + } + } while (!visit.empty()); + + return retValue; +} + +} // namespace CVC4 |