(proof-new) Handle mismatched assumptions in proof equality engine during mkScope (#5012)

This modifies the fix for Boolean equalities with constants so that is addressed lazily during ProofNodeManager mkScope instead of when asserting assumptions to the proof equality engine. This ensures that the default method for asserting facts to the equality engine for external assertions does not have any special cases.

A previously abandoned solution to this issue had made this a part of CDProof. Instead, this PR modifies the mkScope method only. The fix makes mkScope robust to any assumption mismatches in mkScope that can be fixed by rewriting, not just Boolean equality with constants. It is intended to be used infrequently as a last resort when mkScope has mismatched assumptions. The handling of mismatches due to symmetry remains in this method.

1 files changed, 57 insertions, 18 deletions

diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index 4875b7c46..0d13531a5 100644
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/proof.h"
 #include "expr/proof_node_algorithm.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 
@@ -65,6 +66,13 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
   Trace("pnm-scope") << "ProofNodeManager::mkScope " << assumps << std::endl;
   // we first ensure the assumptions are flattened
   std::unordered_set<Node, NodeHashFunction> ac{assumps.begin(), assumps.end()};
+  // map from the rewritten form of assumptions to the original. This is only
+  // computed in the rare case when we need rewriting to match the
+  // assumptions. An example of this is for Boolean constant equalities in
+  // scoped proofs from the proof equality engine.
+  std::unordered_map<Node, Node, NodeHashFunction> acr;
+  // whether we have compute the map above
+  bool computedAcr = false;
 
   // The free assumptions of the proof
   std::map<Node, std::vector<ProofNode*>> famap;
@@ -83,30 +91,61 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
     // otherwise it may be due to symmetry?
     Node aeqSym = CDProof::getSymmFact(a);
     Trace("pnm-scope") << "  - try sym " << aeqSym << "\n";
-    if (!aeqSym.isNull())
+    Node aMatch;
+    if (!aeqSym.isNull() && ac.count(aeqSym))
     {
-      if (ac.count(aeqSym))
+      Trace("pnm-scope") << "- reorient assumption " << aeqSym << " via " << a
+                         << " for " << fa.second.size() << " proof nodes"
+                         << std::endl;
+      aMatch = aeqSym;
+    }
+    else
+    {
+      // Otherwise, may be derivable by rewriting. Note this is used in
+      // ensuring that proofs from the proof equality engine that involve
+      // equality with Boolean constants are closed.
+      if (!computedAcr)
       {
-        Trace("pnm-scope") << "- reorient assumption " << aeqSym << " via " << a
-                           << " for " << fa.second.size() << " proof nodes"
-                           << std::endl;
-        std::shared_ptr<ProofNode> pfaa = mkAssume(aeqSym);
-        for (ProofNode* pfs : fa.second)
+        computedAcr = true;
+        for (const Node& acc : ac)
         {
-          Assert(pfs->getResult() == a);
-          // must correct the orientation on this leaf
-          std::vector<std::shared_ptr<ProofNode>> children;
-          children.push_back(pfaa);
-          std::vector<Node> args;
-          args.push_back(a);
-          updateNode(pfs, PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
+          Node accr = theory::Rewriter::rewrite(acc);
+          if (accr != acc)
+          {
+            acr[accr] = acc;
+          }
         }
-        Trace("pnm-scope") << "...finished" << std::endl;
-        acu.insert(aeqSym);
-        continue;
       }
+      Node ar = theory::Rewriter::rewrite(a);
+      std::unordered_map<Node, Node, NodeHashFunction>::iterator itr =
+          acr.find(ar);
+      if (itr != acr.end())
+      {
+        aMatch = itr->second;
+      }
+    }
+
+    // if we found a match either by symmetry or rewriting, then we connect
+    // the assumption here.
+    if (!aMatch.isNull())
+    {
+      std::shared_ptr<ProofNode> pfaa = mkAssume(aMatch);
+      // must correct the orientation on this leaf
+      std::vector<std::shared_ptr<ProofNode>> children;
+      children.push_back(pfaa);
+      std::vector<Node> args;
+      args.push_back(a);
+      for (ProofNode* pfs : fa.second)
+      {
+        Assert(pfs->getResult() == a);
+        updateNode(pfs, PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
+      }
+      Trace("pnm-scope") << "...finished" << std::endl;
+      acu.insert(aMatch);
+      continue;
     }
-    // All free assumptions should be arguments to SCOPE.
+    // If we did not find a match, it is an error, since all free assumptions
+    // should be arguments to SCOPE.
     std::stringstream ss;
 
     bool dumpProofTraceOn = Trace.isOn("dump-proof-error");