diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-22 18:22:11 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-22 18:22:11 -0500 |
commit | bea30aa5dd6b36fc5a206c4742abadf8c3fab5c1 (patch) | |
tree | 8cf0f2f5b56f2c9994d8ab9d59f73c66f91b2498 /src/theory/trust_node.cpp | |
parent | 1a6ef9fe8da8770e05fb9bd05a83d386aba8c1e9 (diff) |
(proof-new) Add REWRITE trust node kind. (#4624)
This will be used for a number of purposes, including tracking proofs for rewriting and preprocessing.
Diffstat (limited to 'src/theory/trust_node.cpp')
-rw-r--r-- | src/theory/trust_node.cpp | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/src/theory/trust_node.cpp b/src/theory/trust_node.cpp index 5ded29fcd..af2d60241 100644 --- a/src/theory/trust_node.cpp +++ b/src/theory/trust_node.cpp @@ -26,6 +26,7 @@ const char* toString(TrustNodeKind tnk) case TrustNodeKind::CONFLICT: return "CONFLICT"; case TrustNodeKind::LEMMA: return "LEMMA"; case TrustNodeKind::PROP_EXP: return "PROP_EXP"; + case TrustNodeKind::REWRITE: return "REWRITE"; default: return "?"; } } @@ -59,6 +60,13 @@ TrustNode TrustNode::mkTrustPropExp(TNode lit, Node exp, ProofGenerator* g) return TrustNode(TrustNodeKind::PROP_EXP, pekey, g); } +TrustNode TrustNode::mkTrustRewrite(TNode n, Node nr, ProofGenerator* g) +{ + Node rkey = getRewriteProven(n, nr); + Assert(g == nullptr || g->hasProofFor(rkey)); + return TrustNode(TrustNodeKind::REWRITE, rkey, g); +} + TrustNode TrustNode::null() { return TrustNode(TrustNodeKind::INVALID, Node::null()); @@ -75,7 +83,16 @@ TrustNodeKind TrustNode::getKind() const { return d_tnk; } Node TrustNode::getNode() const { - return d_tnk == TrustNodeKind::LEMMA ? d_proven : d_proven[0]; + switch (d_tnk) + { + // the node of lemma is the node itself + case TrustNodeKind::LEMMA: return d_proven; + // the node of the rewrite is the right hand side of EQUAL + case TrustNodeKind::REWRITE: return d_proven[1]; + // the node of an explained propagation is the antecendant of an IMPLIES + // the node of a conflict is underneath a NOT + default: return d_proven[0]; + } } Node TrustNode::getProven() const { return d_proven; } @@ -92,6 +109,8 @@ Node TrustNode::getPropExpProven(TNode lit, Node exp) return NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, lit); } +Node TrustNode::getRewriteProven(TNode n, Node nr) { return n.eqNode(nr); } + std::ostream& operator<<(std::ostream& out, TrustNode n) { out << "(trust " << n.getNode() << ")"; |