(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, 0 insertions, 54 deletions

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,