(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.

diff --git a/src/expr/proof_node.cpp b/src/expr/proof_node.cpp
index f7ad658445a57605c713b9d1ec978ecc9b58fb40..9450ddc999145ed443fcfe66616709f031a15808 100644 (file)
--- 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 13c7f2878182bfd1c46d0cf4d58c27d90962d715..ddd8e1e270163bfcb55f654a8cd443e9f56fba85 100644 (file)
--- 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 036c50947d8af68f1a12ea8373f34f2c4d26834a..7ac228f80b2d7f6b4a49b5162b3e89cae676202a 100644 (file)
--- 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 54d398545d83135405cd9af73c2520bb6f38a945..32513cd0d17a954247e980514039135440d98ace 100644 (file)
--- 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 5b938ab6480da6d5c3471de0b6549e8df8d99e76..b651e390c411e30a5765121f77da41f3451adccf 100644 (file)
--- 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 5292f754fe600c765a0fd3353e2f4365734b4d99..3d6176840b8845c5bdff8d2b6f402642281271ff 100644 (file)
--- 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