From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Thu, 17 Sep 2020 21:22:21 +0000 (-0300)
Subject: [proof-new] Have mkScope agnostic to True assumptions (#5086)
X-Git-Tag: cvc5-1.0.0~2843
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d256af7a024fa09c6352fb0e7881ae39d17ae611;p=cvc5.git

[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 54315ee05..66a8197d8 100644
--- 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 774177d66..799a50f2e 100644
--- 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