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

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