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 | |
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')
-rw-r--r-- | src/theory/trust_node.cpp | 21 | ||||
-rw-r--r-- | src/theory/trust_node.h | 17 |
2 files changed, 33 insertions, 5 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() << ")"; diff --git a/src/theory/trust_node.h b/src/theory/trust_node.h index d8d4f579b..a3c0fbec5 100644 --- a/src/theory/trust_node.h +++ b/src/theory/trust_node.h @@ -31,6 +31,7 @@ enum class TrustNodeKind : uint32_t CONFLICT, LEMMA, PROP_EXP, + REWRITE, INVALID }; /** @@ -87,6 +88,10 @@ class TrustNode static TrustNode mkTrustPropExp(TNode lit, Node exp, ProofGenerator* g = nullptr); + /** Make a proven node for rewrite */ + static TrustNode mkTrustRewrite(TNode n, + Node nr, + ProofGenerator* g = nullptr); /** The null proven node */ static TrustNode null(); ~TrustNode() {} @@ -96,8 +101,9 @@ class TrustNode * * This is the node that is used in a common interface, either: * (1) A T-unsat conjunction conf to pass to OutputChannel::conflict, - * (2) A valid T-formula lem to pass to OutputChannel::lemma, or - * (3) A conjunction of literals exp to return in Theory::explain(lit). + * (2) A valid T-formula lem to pass to OutputChannel::lemma, + * (3) A conjunction of literals exp to return in Theory::explain(lit), or + * (4) A result of rewriting a term n into an equivalent one nr. * * Notice that this node does not necessarily correspond to a valid formula. * The call getProven() below retrieves a valid formula corresponding to @@ -110,7 +116,8 @@ class TrustNode * for the above cases: * (1) (not conf), for conflicts, * (2) lem, for lemmas, - * (3) (=> exp lit), for propagations from explanations. + * (3) (=> exp lit), for propagations from explanations, + * (4) (= n nr), for results of rewriting. * * When constructing this trust node, the proof generator should be able to * provide a proof for this fact. @@ -125,8 +132,10 @@ class TrustNode static Node getConflictProven(Node conf); /** Get the proven formula corresponding to a lemma call */ static Node getLemmaProven(Node lem); - /** Get the proven formula corresponding to explanations for propagation*/ + /** Get the proven formula corresponding to explanations for propagation */ static Node getPropExpProven(TNode lit, Node exp); + /** Get the proven formula corresponding to a rewrite */ + static Node getRewriteProven(TNode n, Node nr); private: TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g = nullptr); |