summaryrefslogtreecommitdiff
path: root/src/theory/trust_node.cpp
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-08-18 14:11:23 -0500
committerGitHub <noreply@github.com>2020-08-18 14:11:23 -0500
commit41edd09dda3d18c98b6cafcf3a3c98d4155fbe19 (patch)
tree00e50f0f88d9a61605f865def97e229c3e4866b6 /src/theory/trust_node.cpp
parent50b0f20be87cd82f464d3f8fc15a5fa2f0a47556 (diff)
(proof-new) Minor updates to trust node (#4900)
Diffstat (limited to 'src/theory/trust_node.cpp')
-rw-r--r--src/theory/trust_node.cpp16
1 files changed, 16 insertions, 0 deletions
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() << ")";
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback