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

3 files changed, 57 insertions, 82 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");
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 323f8c6a2..00e4662f9 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -40,60 +40,6 @@ ProofEqEngine::ProofEqEngine(context::Context* c,
   d_false = nm->mkConst(false);
 }
 
-bool ProofEqEngine::assertAssume(TNode lit)
-{
-  Trace("pfee") << "pfee::assertAssume " << lit << std::endl;
-  // don't need to explicitly add anything to the proof here, since ASSUME
-  // nodes are constructed lazily
-  TNode atom = lit.getKind() == NOT ? lit[0] : lit;
-  bool polarity = lit.getKind() != NOT;
-
-  // Second, assert it directly to the equality engine, where it is its own
-  // explanation. Notice we do not reference count atom/lit.
-  if (atom.getKind() == EQUAL)
-  {
-    if (d_pfEnabled)
-    {
-      // If proofs are enabled, we check if lit is an assertion of the form
-      //   (= P true), (= P false), (= false P) or (= true P).
-      // Such literals must be handled as a special case here, since equality
-      // with Boolean constants have a special status internally within equality
-      // engine. In particular, the proofs constructed by EqProof conversion
-      // always produce proofs involving equalities with Boolean constants, and
-      // whose assumptions are only of the form P or (not P). However, in the
-      // case that (= P true) (resp (= P false)) is itself an input to the
-      // equality engine, we will explain in terms of P (resp. (not P)), which
-      // leads to a bogus proof, typically encountered in
-      // ProofNodeManager::mkScope.
-      //
-      // To correct this, we add an explicit *fact* that P holds by (= P true)
-      // here. This means that EqProof conversion may generate a proof where
-      // the internal equality (= P true) is justified by assumption P, and that
-      // afterwards, P is explained in terms of the original (external) equality
-      // (= P true) by the step provided here. This means that the proof may end
-      // up using (= P true) in a roundabout way (through two redundant steps),
-      // but regardless this allows the core proof utilities (EqProof
-      // conversion, proof equality engine, lazy proof, etc.) to be unconcerned
-      // with this case. Multiple users of the proof equality engine
-      // (SharedTermDatabase and TheoryArrays) require this special case.
-      if (atom[0].getKind() == kind::CONST_BOOLEAN
-          || atom[1].getKind() == kind::CONST_BOOLEAN)
-      {
-        Node nlit = Rewriter::rewrite(lit);
-        if (!CDProof::isSame(lit, nlit))
-        {
-          // use a rewrite step as a fact
-          std::vector<Node> pfChildren;
-          pfChildren.push_back(lit);
-          return assertFact(nlit, PfRule::MACRO_SR_PRED_ELIM, pfChildren, {});
-        }
-      }
-    }
-    return d_ee.assertEquality(atom, polarity, lit);
-  }
-  return d_ee.assertPredicate(atom, polarity, lit);
-}
-
 bool ProofEqEngine::assertFact(Node lit,
                                PfRule id,
                                const std::vector<Node>& exp,
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index e1105623a..d80c1e7bc 100644
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -87,16 +87,6 @@ class ProofEqEngine : public EagerProofGenerator
                 EqualityEngine& ee,
                 ProofNodeManager* pnm);
   ~ProofEqEngine() {}
-  //-------------------------- assert assumption
-  /**
-   * Assert literal lit by assumption to the underlying equality engine. It is
-   * its own explanation.
-   *
-   * @param lit The literal to assert to the equality engine
-   * @return true if this fact was processed by this method. If lit already
-   * holds in the equality engine, this method returns false.
-   */
-  bool assertAssume(TNode lit);
   //-------------------------- assert fact
   /**
    * Assert the literal lit by proof step id, given explanation exp and