From 0e7128b8effd4cc0002641ba545075a1ac346370 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 29 Mar 2022 13:17:29 -0500
Subject: [PATCH] Make ProofNodeManager mkScope more robust (#8435)

This make mkScope more robust in two ways:

- Literals rewritten to true can be justified by MACRO_SR_PRED_INTRO.
- Literals that are rewritten to other non-rewritable free assumptions can also be linked.

This is enough to ensure that current issues with (= t false) vs (not f) are fixed for Boolean arrays.
---
 src/proof/proof_node_manager.cpp              | 34 +++++++++----------
 .../cli/regress0/arrays/issue5925-2.smt2      |  1 -
 .../cli/regress0/arrays/issue5925.smt2        |  1 -
 3 files changed, 16 insertions(+), 20 deletions(-)

diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp
index 7bea8f3f2..36944cdd1 100644
--- a/src/proof/proof_node_manager.cpp
+++ b/src/proof/proof_node_manager.cpp
@@ -128,19 +128,6 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
       acu.insert(a);
       continue;
     }
-    // trivial assumption
-    if (a == d_true)
-    {
-      Trace("pnm-scope") << "- justify trivial True assumption\n";
-      for (std::shared_ptr<ProofNode> pfs : fa.second)
-      {
-        Assert(pfs->getResult() == a);
-        updateNode(pfs.get(), PfRule::MACRO_SR_PRED_INTRO, {}, {a});
-      }
-      Trace("pnm-scope") << "...finished" << std::endl;
-      acu.insert(a);
-      continue;
-    }
     Trace("pnm-scope") << "- try matching free assumption " << a << "\n";
     // otherwise it may be due to symmetry?
     Node aeqSym = CDProof::getSymmFact(a);
@@ -155,6 +142,20 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
     }
     else
     {
+      // trivial assumption (by rewriting)
+      Node ar = d_rewriter->rewrite(a);
+      if (ar == d_true)
+      {
+        Trace("pnm-scope") << "- justify trivial True assumption\n";
+        for (std::shared_ptr<ProofNode> pfs : fa.second)
+        {
+          Assert(pfs->getResult() == a);
+          updateNode(pfs.get(), PfRule::MACRO_SR_PRED_INTRO, {}, {a});
+        }
+        Trace("pnm-scope") << "...finished" << std::endl;
+        acu.insert(a);
+        continue;
+      }
       // 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.
@@ -164,13 +165,10 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
         for (const Node& acc : ac)
         {
           Node accr = d_rewriter->rewrite(acc);
-          if (accr != acc)
-          {
-            acr[accr] = acc;
-          }
+          acr[accr] = acc;
         }
       }
-      Node ar = d_rewriter->rewrite(a);
+      Trace("pnm-scope") << "- rewritten: " << ar << std::endl;
       std::unordered_map<Node, Node>::iterator itr = acr.find(ar);
       if (itr != acr.end())
       {
diff --git a/test/regress/cli/regress0/arrays/issue5925-2.smt2 b/test/regress/cli/regress0/arrays/issue5925-2.smt2
index 0eba3619b..6beb2e9ba 100644
--- a/test/regress/cli/regress0/arrays/issue5925-2.smt2
+++ b/test/regress/cli/regress0/arrays/issue5925-2.smt2
@@ -1,4 +1,3 @@
-; DISABLE-TESTER: proof
 (set-logic QF_A)
 (set-info :status unsat)
 (declare-const a (Array Bool Bool))
diff --git a/test/regress/cli/regress0/arrays/issue5925.smt2 b/test/regress/cli/regress0/arrays/issue5925.smt2
index 40c0cb0a2..de88c037e 100644
--- a/test/regress/cli/regress0/arrays/issue5925.smt2
+++ b/test/regress/cli/regress0/arrays/issue5925.smt2
@@ -1,4 +1,3 @@
-; DISABLE-TESTER: proof
 (set-logic QF_ABV)
 (set-info :status unsat)
 (declare-const a (Array Bool Bool))
-- 
2.30.2