From 85d96c3668495fb087f059e5662072ae66d69e22 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 22 Feb 2021 13:38:15 -0600
Subject: [PATCH] (proof-new) Option to automatically add SYMM steps during
 proof node update. (#5939)

Required for work on external proof conversions.
---
 src/expr/proof_node_updater.cpp |  8 +++++---
 src/expr/proof_node_updater.h   | 10 +++++++++-
 2 files changed, 14 insertions(+), 4 deletions(-)

diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp
index af32c223d..16e339645 100644
--- a/src/expr/proof_node_updater.cpp
+++ b/src/expr/proof_node_updater.cpp
@@ -35,11 +35,13 @@ bool ProofNodeUpdaterCallback::update(Node res,
 
 ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm,
                                    ProofNodeUpdaterCallback& cb,
-                                   bool mergeSubproofs)
+                                   bool mergeSubproofs,
+                                   bool autoSym)
     : d_pnm(pnm),
       d_cb(cb),
       d_debugFreeAssumps(false),
-      d_mergeSubproofs(mergeSubproofs)
+      d_mergeSubproofs(mergeSubproofs),
+      d_autoSym(autoSym)
 {
 }
 
@@ -183,7 +185,7 @@ bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur,
   }
   PfRule id = cur->getRule();
   // use CDProof to open a scope for which the callback updates
-  CDProof cpf(d_pnm);
+  CDProof cpf(d_pnm, nullptr, "ProofNodeUpdater::CDProof", d_autoSym);
   const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren();
   std::vector<Node> ccn;
   for (const std::shared_ptr<ProofNode>& cp : cc)
diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h
index 82c2ee068..9814c8166 100644
--- a/src/expr/proof_node_updater.h
+++ b/src/expr/proof_node_updater.h
@@ -80,10 +80,13 @@ class ProofNodeUpdater
    * @param cb The callback to apply to each node
    * @param mergeSubproofs Whether to automatically merge subproofs within
    * the same SCOPE that prove the same fact.
+   * @param autoSym Whether intermediate CDProof objects passed to updater
+   * callbacks automatically introduce SYMM steps.
    */
   ProofNodeUpdater(ProofNodeManager* pnm,
                    ProofNodeUpdaterCallback& cb,
-                   bool mergeSubproofs = false);
+                   bool mergeSubproofs = false,
+                   bool autoSym = true);
   /**
    * Post-process, which performs the main post-processing technique described
    * above.
@@ -142,6 +145,11 @@ class ProofNodeUpdater
   std::vector<Node> d_freeAssumps;
   /** Whether we are merging subproofs */
   bool d_mergeSubproofs;
+  /**
+   * Whether intermediate CDProof objects passed to updater callbacks
+   * automatically introduce SYMM steps.
+   */
+  bool d_autoSym;
 };
 
 }  // namespace CVC4
-- 
2.30.2