From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 18 Aug 2020 19:11:23 +0000 (-0500)
Subject: (proof-new) Minor updates to trust node (#4900)
X-Git-Tag: cvc5-1.0.0~2986
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=41edd09dda3d18c98b6cafcf3a3c98d4155fbe19;p=cvc5.git

(proof-new) Minor updates to trust node (#4900)
---

diff --git a/src/theory/trust_node.cpp b/src/theory/trust_node.cpp
index 25aef5a72..041d04d75 100644
--- a/src/theory/trust_node.cpp
+++ b/src/theory/trust_node.cpp
@@ -121,6 +121,22 @@ Node TrustNode::getPropExpProven(TNode lit, Node exp)
 
 Node TrustNode::getRewriteProven(TNode n, Node nr) { return n.eqNode(nr); }
 
+void TrustNode::debugCheckClosed(const char* c,
+                                 const char* ctx,
+                                 bool reqNullGen)
+{
+  pfgEnsureClosed(d_proven, d_gen, c, ctx, reqNullGen);
+}
+
+std::string TrustNode::identifyGenerator() const
+{
+  if (d_gen == nullptr)
+  {
+    return "null";
+  }
+  return d_gen->identify();
+}
+
 std::ostream& operator<<(std::ostream& out, TrustNode n)
 {
   out << "(" << n.getKind() << " " << n.getProven() << ")";
diff --git a/src/theory/trust_node.h b/src/theory/trust_node.h
index ff174b63e..b7be0e4e5 100644
--- a/src/theory/trust_node.h
+++ b/src/theory/trust_node.h
@@ -142,6 +142,15 @@ class TrustNode
   static Node getPropExpProven(TNode lit, Node exp);
   /** Get the proven formula corresponding to a rewrite */
   static Node getRewriteProven(TNode n, Node nr);
+  /** For debugging */
+  std::string identifyGenerator() const;
+
+  /**
+   * debug check closed on Trace c, context ctx is string for debugging
+   *
+   * @param reqNullGen Whether we consider a null generator to be a failure.
+   */
+  void debugCheckClosed(const char* c, const char* ctx, bool reqNullGen = true);
 
  private:
   TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g = nullptr);