diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-18 14:11:23 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-18 14:11:23 -0500 |
commit | 41edd09dda3d18c98b6cafcf3a3c98d4155fbe19 (patch) | |
tree | 00e50f0f88d9a61605f865def97e229c3e4866b6 /src/theory | |
parent | 50b0f20be87cd82f464d3f8fc15a5fa2f0a47556 (diff) |
(proof-new) Minor updates to trust node (#4900)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/trust_node.cpp | 16 | ||||
-rw-r--r-- | src/theory/trust_node.h | 9 |
2 files changed, 25 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() << ")"; 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); |