(proof-new) Option to not automatically consider symmetry in CDProof (#5895)

There are compelling use cases not to automatically introduce SYMM steps in CDProof, e.g. in CDProofs used within ProofNodeUpdater for external conversions.

diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp
index 94ca26dd6eabed2ac11b39b741a368e459230036..1c21a59e7681023000b908000d9107399b60dba4 100644 (file)
--- a/src/expr/proof.cpp
+++ b/src/expr/proof.cpp
@@ -18,8 +18,15 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 
-CDProof::CDProof(ProofNodeManager* pnm, context::Context* c, std::string name)
-    : d_manager(pnm), d_context(), d_nodes(c ? c : &d_context), d_name(name)
+CDProof::CDProof(ProofNodeManager* pnm,
+                 context::Context* c,
+                 std::string name,
+                 bool autoSymm)
+    : d_manager(pnm),
+      d_context(),
+      d_nodes(c ? c : &d_context),
+      d_name(name),
+      d_autoSymm(autoSymm)
 {
 }
 
@@ -60,6 +67,11 @@ std::shared_ptr<ProofNode> CDProof::getProofSymm(Node fact)
     Trace("cdproof") << "...existing non-assume " << pf->getRule() << std::endl;
     return pf;
   }
+  else if (!d_autoSymm)
+  {
+    Trace("cdproof") << "...not auto considering symmetry" << std::endl;
+    return pf;
+  }
   Node symFact = getSymmFact(fact);
   if (symFact.isNull())
   {
@@ -212,6 +224,10 @@ bool CDProof::addStep(Node expected,
 
 void CDProof::notifyNewProof(Node expected)
 {
+  if (!d_autoSymm)
+  {
+    return;
+  }
   // ensure SYMM proof is also linked to an existing proof, if it is an
   // assumption.
   Node symExpected = getSymmFact(expected);
@@ -353,6 +369,10 @@ bool CDProof::hasStep(Node fact)
   {
     return true;
   }
+  else if (!d_autoSymm)
+  {
+    return false;
+  }
   Node symFact = getSymmFact(fact);
   if (symFact.isNull())
   {

diff --git a/src/expr/proof.h b/src/expr/proof.h
index b5bcc7d5083b0339f6f650f0ed2d3aa8cb53f3a7..8350b49544bad53df83931d95f4aa34ec4de9525 100644 (file)
--- a/src/expr/proof.h
+++ b/src/expr/proof.h
@@ -134,9 +134,17 @@ namespace CVC4 {
 class CDProof : public ProofGenerator
 {
  public:
+  /**
+   * @param pnm The proof node manager responsible for constructor ProofNode
+   * @param c The context this proof depends on
+   * @param name The name of this proof (for debugging)
+   * @param autoSymm Whether this proof automatically adds symmetry steps based
+   * on policy documented above.
+   */
   CDProof(ProofNodeManager* pnm,
           context::Context* c = nullptr,
-          std::string name = "CDProof");
+          std::string name = "CDProof",
+          bool autoSymm = true);
   virtual ~CDProof();
   /**
    * Make proof for fact.
@@ -247,6 +255,8 @@ class CDProof : public ProofGenerator
   NodeProofNodeMap d_nodes;
   /** Name identifier */
   std::string d_name;
+  /** Whether we automatically add symmetry steps */
+  bool d_autoSymm;
   /** Ensure fact sym */
   std::shared_ptr<ProofNode> getProofSymm(Node fact);
   /**