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.

diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp
index 7bea8f3f2f17cf1b65d648998012925634f30d02..36944cdd1dea5a0c4f996d888606d5931e63fd9f 100644 (file)
--- 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 0eba3619bb94c847e00da73c3f9ab3f9ca6ae4f6..6beb2e9ba3049fce8bab8079f1d0fc3ea48bbe58 100644 (file)
--- 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 40c0cb0a220a2a4175925b75948397612c5c7148..de88c037ec32919517f585cf564d495743d31e0f 100644 (file)
--- 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))