(proof-new) Fix true explanations of propagations in pf equality engine (#5338)

This ensures we construct proper proofs for propagations whose conclusions are of the form (=> true lit). Literals may be propagated with "true" as an explanation in datatypes, e.g. discriminators for datatypes with 1 constructor.

diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index c238f9e350c2540cbbef3a2a149197959d4f2518..4682bbebb55c18bfbf9d81305d8678ba6752d57b 100644 (file)
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -164,12 +164,18 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
       // 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 (std::shared_ptr<ProofNode> pfs : fa.second)
       {
         Assert(pfs->getResult() == a);
-        updateNode(pfs.get(), PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
+        // use SYMM if possible
+        if (aMatch == aeqSym)
+        {
+          updateNode(pfs.get(), PfRule::SYMM, children, {});
+        }
+        else
+        {
+          updateNode(pfs.get(), PfRule::MACRO_SR_PRED_TRANSFORM, children, {a});
+        }
       }
       Trace("pnm-scope") << "...finished" << std::endl;
       acu.insert(aMatch);
@@ -223,23 +229,20 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
   Node minExpected;
   NodeManager* nm = NodeManager::currentNM();
   Node exp;
-  Node conc = pf->getResult();
   if (assumps.empty())
   {
-    Assert(!conc.isConst());
-    minExpected = conc;
+    // SCOPE with no arguments is a no-op, just return original
+    return pf;
+  }
+  Node conc = pf->getResult();
+  exp = assumps.size() == 1 ? assumps[0] : nm->mkNode(AND, assumps);
+  if (conc.isConst() && !conc.getConst<bool>())
+  {
+    minExpected = exp.notNode();
   }
   else
   {
-    exp = assumps.size() == 1 ? assumps[0] : nm->mkNode(AND, assumps);
-    if (conc.isConst() && !conc.getConst<bool>())
-    {
-      minExpected = exp.notNode();
-    }
-    else
-    {
-      minExpected = nm->mkNode(IMPLIES, exp, conc);
-    }
+    minExpected = nm->mkNode(IMPLIES, exp, conc);
   }
   return mkNode(PfRule::SCOPE, {pf}, assumps, minExpected);
 }

diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h
index 7d799314614be333282d8604d6a163950c77588e..dae0266bb59946b03514c197cbbf4ed28d08fbb3 100644 (file)
--- a/src/expr/proof_node_manager.h
+++ b/src/expr/proof_node_manager.h
@@ -111,7 +111,8 @@ class ProofNodeManager
    *
    * Additionally, if both ensureClosed and doMinimize are true, assumps is
    * updated to contain exactly the free asumptions of pf. This also includes
-   * having no duplicates.
+   * having no duplicates. Furthermore, if assumps is empty after minimization,
+   * this method is a no-op.
    *
    * In each case, the update vector assumps is passed as arguments to SCOPE.
    *

diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 184584aa9c657e72bafd0f0f292409a72a83bd19..18cdcf9026aa47ab5cea8d3ad452f696930d8282 100644 (file)
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -408,9 +408,20 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc,
       scopeAssumps.push_back(a);
     }
   }
-  // scope the proof constructed above, and connect the formula with the proof
-  // minimize the assumptions
+  // Scope the proof constructed above, and connect the formula with the proof
+  // minimize the assumptions.
   pf = d_pnm->mkScope(pfBody, scopeAssumps, true, true);
+  // If we have no assumptions, and are proving an explanation for propagation
+  if (scopeAssumps.empty() && tnk == TrustNodeKind::PROP_EXP)
+  {
+    // Must add "true" as an explicit argument. This is to ensure that the
+    // propagation F from true proves (=> true F) instead of F, since this is
+    // the form required by TrustNodeKind::PROP_EXP. We do not ensure closed or
+    // minimize here, since we already ensured the proof was closed above, and
+    // we do not want to minimize, or else "true" would be omitted.
+    scopeAssumps.push_back(nm->mkConst(true));
+    pf = d_pnm->mkScope(pf, scopeAssumps, false);
+  }
   exp = nm->mkAnd(scopeAssumps);
   // Make the lemma or conflict node. This must exactly match the conclusion
   // of SCOPE below.