diff options
| -rw-r--r-- | src/expr/proof_node.cpp | 13 | ||||
| -rw-r--r-- | src/expr/proof_node.h | 2 | ||||
| -rw-r--r-- | src/expr/proof_node_manager.cpp | 49 | ||||
| -rw-r--r-- | src/expr/proof_node_manager.h | 8 | ||||
| -rw-r--r-- | src/smt/proof_manager.cpp | 8 | ||||
| -rw-r--r-- | src/theory/uf/proof_equality_engine.cpp | 2 |
6 files changed, 66 insertions, 16 deletions
diff --git a/src/expr/proof_node.cpp b/src/expr/proof_node.cpp index f7ad65844..9450ddc99 100644 --- a/src/expr/proof_node.cpp +++ b/src/expr/proof_node.cpp @@ -44,19 +44,6 @@ bool ProofNode::isClosed() return assumps.empty(); } -std::shared_ptr<ProofNode> ProofNode::clone() const -{ - std::vector<std::shared_ptr<ProofNode>> cchildren; - for (const std::shared_ptr<ProofNode>& cp : d_children) - { - cchildren.push_back(cp->clone()); - } - std::shared_ptr<ProofNode> thisc = - std::make_shared<ProofNode>(d_rule, cchildren, d_args); - thisc->d_proven = d_proven; - return thisc; -} - void ProofNode::setValue( PfRule id, const std::vector<std::shared_ptr<ProofNode>>& children, diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h index 13c7f2878..ddd8e1e27 100644 --- a/src/expr/proof_node.h +++ b/src/expr/proof_node.h @@ -105,8 +105,6 @@ class ProofNode bool isClosed(); /** Print debug on output strem os */ void printDebug(std::ostream& os) const; - /** Clone, create a deep copy of this */ - std::shared_ptr<ProofNode> clone() const; private: /** diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp index 036c50947..7ac228f80 100644 --- a/src/expr/proof_node_manager.cpp +++ b/src/expr/proof_node_manager.cpp @@ -299,6 +299,55 @@ Node ProofNodeManager::checkInternal( ProofChecker* ProofNodeManager::getChecker() const { return d_checker; } +std::shared_ptr<ProofNode> ProofNodeManager::clone( + std::shared_ptr<ProofNode> pn) +{ + const ProofNode* orig = pn.get(); + std::unordered_map<const ProofNode*, std::shared_ptr<ProofNode>> visited; + std::unordered_map<const ProofNode*, std::shared_ptr<ProofNode>>::iterator it; + std::vector<const ProofNode*> visit; + std::shared_ptr<ProofNode> cloned; + visit.push_back(orig); + const ProofNode* cur; + while (!visit.empty()) + { + cur = visit.back(); + it = visited.find(cur); + if (it == visited.end()) + { + visited[cur] = nullptr; + const std::vector<std::shared_ptr<ProofNode>>& children = + cur->getChildren(); + for (const std::shared_ptr<ProofNode>& cp : children) + { + visit.push_back(cp.get()); + } + continue; + } + visit.pop_back(); + if (it->second.get() == nullptr) + { + std::vector<std::shared_ptr<ProofNode>> cchildren; + const std::vector<std::shared_ptr<ProofNode>>& children = + cur->getChildren(); + for (const std::shared_ptr<ProofNode>& cp : children) + { + it = visited.find(cp.get()); + Assert(it != visited.end()); + Assert(it->second != nullptr); + cchildren.push_back(it->second); + } + cloned = std::make_shared<ProofNode>( + cur->getRule(), cchildren, cur->getArguments()); + visited[cur] = cloned; + // we trust the above cloning does not change what is proven + cloned->d_proven = cur->d_proven; + } + } + Assert(visited.find(orig) != visited.end()); + return visited[orig]; +} + bool ProofNodeManager::updateNodeInternal( ProofNode* pn, PfRule id, diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h index 54d398545..32513cd0d 100644 --- a/src/expr/proof_node_manager.h +++ b/src/expr/proof_node_manager.h @@ -158,6 +158,14 @@ class ProofNodeManager bool updateNode(ProofNode* pn, ProofNode* pnr); /** Get the underlying proof checker */ ProofChecker* getChecker() const; + /** + * Clone a proof node, which creates a deep copy of pn and returns it. The + * dag structure of pn is the same as that in the returned proof node. + * + * @param pn The proof node to clone + * @return the cloned proof node. + */ + std::shared_ptr<ProofNode> clone(std::shared_ptr<ProofNode> pn); private: /** The (optional) proof checker */ diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 5b938ab64..b651e390c 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -19,6 +19,7 @@ #include "expr/proof_node_manager.h" #include "options/base_options.h" #include "options/proof_options.h" +#include "options/smt_options.h" #include "proof/dot/dot_printer.h" #include "smt/assertions.h" #include "smt/defined_function.h" @@ -121,6 +122,13 @@ void PfManager::printProof(std::ostream& out, { Trace("smt-proof") << "PfManager::printProof: start" << std::endl; std::shared_ptr<ProofNode> fp = getFinalProof(pfn, as, df); + // if we are in incremental mode, we don't want to invalidate the proof + // nodes in fp, since these may be reused in further check-sat calls + if (options::incrementalSolving() + && options::proofFormatMode() != options::ProofFormatMode::NONE) + { + fp = d_pnm->clone(fp); + } // TODO (proj #37) according to the proof format, post process the proof node // TODO (proj #37) according to the proof format, print the proof node diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index 5292f754f..3d6176840 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -349,7 +349,7 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc, return TrustNode::null(); } // clone it so that we have a fresh copy - pfBody = pfBody->clone(); + pfBody = d_pnm->clone(pfBody); Trace("pfee-proof") << "pfee::ensureProofForFact: add scope" << std::endl; // The free assumptions must be closed by assumps, which should be passed // as arguments of SCOPE. However, some of the free assumptions may not |