(proof-new) Option to automatically add SYMM steps during proof node update. (#5939)

Required for work on external proof conversions.

diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp
index af32c223d7d39f755726b3da5654109a506447ab..16e339645a7dedecf9849e6ba07d80123c741e6e 100644 (file)
--- 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 82c2ee068fd1c06196db6fe117d164da4bcdc1eb..9814c81664ffbf9a72ab75c587ae54ce6c392e4a 100644 (file)
--- 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