From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 22 Jun 2020 23:22:11 +0000 (-0500)
Subject: (proof-new) Add REWRITE trust node kind. (#4624)
X-Git-Tag: cvc5-1.0.0~3181
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bea30aa5dd6b36fc5a206c4742abadf8c3fab5c1;p=cvc5.git

(proof-new) Add REWRITE trust node kind. (#4624)

This will be used for a number of purposes, including tracking proofs for rewriting and preprocessing.
---

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);