From aa1f4021b70a1016502ead46bf68907bf092d65c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 7 Apr 2021 14:45:45 -0500 Subject: [PATCH] (proof-new) Proper implementation of proof node cloning (#6285) Previously, we were traversing proof node as a tree, now we use a dag traversal. This also makes sure that proofs work when we have a external proof conversion and we are in incremental mode. In such cases, the final proof must be cloned to ensure that we do not overwrite proof nodes, which may be reused across multiple check-sat. --- src/expr/proof_node.cpp | 13 ------- src/expr/proof_node.h | 2 - src/expr/proof_node_manager.cpp | 49 +++++++++++++++++++++++++ src/expr/proof_node_manager.h | 8 ++++ src/smt/proof_manager.cpp | 8 ++++ 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::clone() const -{ - std::vector> cchildren; - for (const std::shared_ptr& cp : d_children) - { - cchildren.push_back(cp->clone()); - } - std::shared_ptr thisc = - std::make_shared(d_rule, cchildren, d_args); - thisc->d_proven = d_proven; - return thisc; -} - void ProofNode::setValue( PfRule id, const std::vector>& 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 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 ProofNodeManager::clone( + std::shared_ptr pn) +{ + const ProofNode* orig = pn.get(); + std::unordered_map> visited; + std::unordered_map>::iterator it; + std::vector visit; + std::shared_ptr 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>& children = + cur->getChildren(); + for (const std::shared_ptr& cp : children) + { + visit.push_back(cp.get()); + } + continue; + } + visit.pop_back(); + if (it->second.get() == nullptr) + { + std::vector> cchildren; + const std::vector>& children = + cur->getChildren(); + for (const std::shared_ptr& cp : children) + { + it = visited.find(cp.get()); + Assert(it != visited.end()); + Assert(it->second != nullptr); + cchildren.push_back(it->second); + } + cloned = std::make_shared( + 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 clone(std::shared_ptr 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 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 -- 2.30.2