[proof-new] Have mkScope agnostic to True assumptions (#5086)

diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index 54315ee058f5c5974da051b099b9d8d8a218a820..66a8197d8491f2f45abf418ea27960e1bb72d2b3 100644 (file)
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -22,7 +22,11 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 
-ProofNodeManager::ProofNodeManager(ProofChecker* pc) : d_checker(pc) {}
+ProofNodeManager::ProofNodeManager(ProofChecker* pc)
+    : d_checker(pc)
+{
+  d_true = NodeManager::currentNM()->mkConst(true);
+}
 
 std::shared_ptr<ProofNode> ProofNodeManager::mkNode(
     PfRule id,
@@ -88,6 +92,19 @@ 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);

diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h
index 774177d668ff7b552cebb2914c724e05a3e997d0..799a50f2e41b89dc9d762ccfe8ec79fcbe69aaa7 100644 (file)
--- a/src/expr/proof_node_manager.h
+++ b/src/expr/proof_node_manager.h
@@ -118,7 +118,6 @@ class ProofNodeManager
                                      bool ensureClosed = true,
                                      bool doMinimize = false,
                                      Node expected = Node::null());
-
   /**
    * This method updates pn to be a proof of the form <id>( children, args ),
    * while maintaining its d_proven field. This method returns false if this
@@ -150,6 +149,8 @@ class ProofNodeManager
  private:
   /** The (optional) proof checker */
   ProofChecker* d_checker;
+  /** the true node */
+  Node d_true;
   /** Check internal
    *
    * This returns the result of proof checking a ProofNode with the provided