(proof-new) Skeleton proof support in the Rewriter (#4730)

This adds support for skeleton proofs in the rewriter (REWRITE -> THEORY_REWRITE).

It adds "extended equality rewrite" as a new method of the rewriter/theory rewriters.

The unit test of this feature should be added on a followup PR.

Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>

10 files changed, 322 insertions, 20 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 930bf2370..278632a90 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -771,6 +771,7 @@ libcvc4_add_sources(
   theory/theory_preprocessor.h
   theory/theory_proof_step_buffer.cpp
   theory/theory_proof_step_buffer.h
+  theory/theory_rewriter.cpp
   theory/theory_rewriter.h
   theory/theory_registrar.h
   theory/theory_test_utils.h
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index 08998e66e..c9250f9ea 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -31,6 +31,7 @@ const char* toString(PfRule id)
     case PfRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO";
     case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM";
     case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM";
+    case PfRule::THEORY_REWRITE: return "THEORY_REWRITE";
     case PfRule::PREPROCESS: return "PREPROCESS";
     //================================================= Boolean rules
     case PfRule::SPLIT: return "SPLIT";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 87e8565ca..e7464dd24 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -163,6 +163,15 @@ enum class PfRule : uint32_t
   // Notice that we apply rewriting on the witness form of F and G, similar to
   // MACRO_SR_PRED_INTRO.
   MACRO_SR_PRED_TRANSFORM,
+  // ======== Theory Rewrite
+  // Children: none
+  // Arguments: (t, preRewrite?)
+  // ----------------------------------------
+  // Conclusion: (= t t')
+  // where
+  //  t' is the result of applying either a pre-rewrite or a post-rewrite step
+  //  to t (depending on the second argument).
+  THEORY_REWRITE,
 
   //================================================= Processing rules
   // ======== Preprocess
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index a8249ae7c..59f405337 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -59,9 +59,20 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(PfRule::MACRO_SR_PRED_INTRO, this);
   pc->registerChecker(PfRule::MACRO_SR_PRED_ELIM, this);
   pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this);
+  pc->registerChecker(PfRule::THEORY_REWRITE, this);
   pc->registerChecker(PfRule::PREPROCESS, this);
 }
 
+Node BuiltinProofRuleChecker::applyTheoryRewrite(Node n, bool preRewrite)
+{
+  TheoryId tid = Theory::theoryOf(n);
+  Rewriter* rewriter = Rewriter::getInstance();
+  Node nkr = preRewrite ? rewriter->preRewrite(tid, n).d_node
+                        : rewriter->postRewrite(tid, n).d_node;
+  return nkr;
+}
+
+
 Node BuiltinProofRuleChecker::applySubstitutionRewrite(
     Node n, const std::vector<Node>& exp, MethodId ids, MethodId idr)
 {
diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h
index 6dc7023d5..7e46587b7 100644
--- a/src/theory/builtin/proof_checker.h
+++ b/src/theory/builtin/proof_checker.h
@@ -77,6 +77,17 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
    */
   static Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE);
   /**
+   * Apply small-step rewrite on n in skolem form (either pre- or
+   * post-rewrite). This encapsulates the exact behavior of a THEORY_REWRITE
+   * step in a proof.
+   *
+   * @param n The node to rewrite
+   * @param preRewrite If true, performs a pre-rewrite or a post-rewrite
+   * otherwise
+   * @return The rewritten form of n
+   */
+  static Node applyTheoryRewrite(Node n, bool preRewrite);
+  /**
    * Get substitution. Updates vars/subs to the substitution specified by
    * exp (e.g. as an equality) for the substitution method ids.
    */
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 0247a7277..d77f6fe83 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -70,7 +70,8 @@ struct RewriteStackElement {
 
   /** The node we're currently rewriting */
   Node d_node;
-  /** Original node */
+  /** Original node (either the unrewritten node or the node after prerewriting)
+   */
   Node d_original;
   /** Id of the theory that's currently rewriting this node */
   unsigned d_theoryId : 8;
@@ -97,6 +98,41 @@ Node Rewriter::rewrite(TNode node) {
   return getInstance()->rewriteTo(theoryOf(node), node);
 }
 
+TrustNode Rewriter::rewriteWithProof(TNode node,
+                                     bool elimTheoryRewrite,
+                                     bool isExtEq)
+{
+  // must set the proof checker before calling this
+  Assert(d_tpg != nullptr);
+  if (isExtEq)
+  {
+    // theory rewriter is responsible for rewriting the equality
+    TheoryRewriter* tr = getInstance()->d_theoryRewriters[theoryOf(node)];
+    Assert(tr != nullptr);
+    return tr->rewriteEqualityExtWithProof(node);
+  }
+  Node ret = getInstance()->rewriteTo(theoryOf(node), node, d_tpg.get());
+  return TrustNode::mkTrustRewrite(node, ret, d_tpg.get());
+}
+
+void Rewriter::setProofChecker(ProofChecker* pc)
+{
+  // if not already initialized with proof support
+  if (d_tpg == nullptr)
+  {
+    d_pnm.reset(new ProofNodeManager(pc));
+    d_tpg.reset(new TConvProofGenerator(d_pnm.get()));
+  }
+}
+
+Node Rewriter::rewriteEqualityExt(TNode node)
+{
+  Assert(node.getKind() == kind::EQUAL);
+  // note we don't force caching of this method currently
+  return getInstance()->d_theoryRewriters[theoryOf(node)]->rewriteEqualityExt(
+      node);
+}
+
 void Rewriter::registerTheoryRewriter(theory::TheoryId tid,
                                       TheoryRewriter* trew)
 {
@@ -136,8 +172,10 @@ Rewriter* Rewriter::getInstance()
   return smt::currentSmtEngine()->getRewriter();
 }
 
-Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
-
+Node Rewriter::rewriteTo(theory::TheoryId theoryId,
+                         Node node,
+                         TConvProofGenerator* tcpg)
+{
 #ifdef CVC4_ASSERTIONS
   bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean());
 
@@ -151,7 +189,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
 
   // Check if it's been cached already
   Node cached = getPostRewriteCache(theoryId, node);
-  if (!cached.isNull()) {
+  if (!cached.isNull() && (tcpg == nullptr || tcpg->hasRewriteStep(node)))
+  {
     return cached;
   }
 
@@ -186,12 +225,15 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
       // Check if the pre-rewrite has already been done (it's in the cache)
       cached = getPreRewriteCache(rewriteStackTop.getTheoryId(),
                                   rewriteStackTop.d_node);
-      if (cached.isNull()) {
+      if (cached.isNull()
+          || (tcpg != nullptr && !tcpg->hasRewriteStep(rewriteStackTop.d_node)))
+      {
         // Rewrite until fix-point is reached
         for(;;) {
           // Perform the pre-rewrite
-          RewriteResponse response =
-              preRewrite(rewriteStackTop.getTheoryId(), rewriteStackTop.d_node);
+          RewriteResponse response = preRewrite(
+              rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg);
+
           // Put the rewritten node to the top of the stack
           rewriteStackTop.d_node = response.d_node;
           TheoryId newTheory = theoryOf(rewriteStackTop.d_node);
@@ -203,6 +245,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
           }
           rewriteStackTop.d_theoryId = newTheory;
         }
+
         // Cache the rewrite
         setPreRewriteCache(rewriteStackTop.getOriginalTheoryId(),
                            rewriteStackTop.d_original,
@@ -221,8 +264,9 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
     cached = getPostRewriteCache(rewriteStackTop.getTheoryId(),
                                  rewriteStackTop.d_node);
     // If not, go through the children
-    if(cached.isNull()) {
-
+    if (cached.isNull()
+        || (tcpg != nullptr && !tcpg->hasRewriteStep(rewriteStackTop.d_node)))
+    {
       // The child we need to rewrite
       unsigned child = rewriteStackTop.d_nextChild++;
 
@@ -261,8 +305,9 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
       // Done with all pre-rewriting, so let's do the post rewrite
       for(;;) {
         // Do the post-rewrite
-        RewriteResponse response =
-            postRewrite(rewriteStackTop.getTheoryId(), rewriteStackTop.d_node);
+        RewriteResponse response = postRewrite(
+            rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg);
+
         // We continue with the response we got
         TheoryId newTheoryId = theoryOf(response.d_node);
         if (newTheoryId != rewriteStackTop.getTheoryId()
@@ -276,7 +321,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
                  == d_rewriteStack->end());
           d_rewriteStack->insert(response.d_node);
 #endif
-          Node rewritten = rewriteTo(newTheoryId, response.d_node);
+          Node rewritten = rewriteTo(newTheoryId, response.d_node, tcpg);
           rewriteStackTop.d_node = rewritten;
 #ifdef CVC4_ASSERTIONS
           d_rewriteStack->erase(response.d_node);
@@ -301,11 +346,14 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
                != rewriteStackTop.d_node);
         rewriteStackTop.d_node = response.d_node;
       }
+
       // We're done with the post rewrite, so we add to the cache
       setPostRewriteCache(rewriteStackTop.getOriginalTheoryId(),
                           rewriteStackTop.d_original,
                           rewriteStackTop.d_node);
-    } else {
+    }
+    else
+    {
       // We were already in cache, so just remember it
       rewriteStackTop.d_node = cached;
       rewriteStackTop.d_theoryId = theoryOf(cached);
@@ -324,32 +372,83 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
   }
 
   Unreachable();
-}/* Rewriter::rewriteTo() */
+} /* Rewriter::rewriteTo() */
 
-RewriteResponse Rewriter::preRewrite(theory::TheoryId theoryId, TNode n)
+RewriteResponse Rewriter::preRewrite(theory::TheoryId theoryId,
+                                     TNode n,
+                                     TConvProofGenerator* tcpg)
 {
   Kind k = n.getKind();
   std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn =
       (k == kind::EQUAL) ? d_preRewritersEqual[theoryId] : d_preRewriters[k];
   if (fn == nullptr)
   {
+    if (tcpg != nullptr)
+    {
+      // call the trust rewrite response interface
+      TrustRewriteResponse tresponse =
+          d_theoryRewriters[theoryId]->preRewriteWithProof(n);
+      // process the trust rewrite response: store the proof step into
+      // tcpg if necessary and then convert to rewrite response.
+      return processTrustRewriteResponse(tresponse, true, tcpg);
+    }
     return d_theoryRewriters[theoryId]->preRewrite(n);
   }
   return fn(&d_re, n);
 }
 
-RewriteResponse Rewriter::postRewrite(theory::TheoryId theoryId, TNode n)
+RewriteResponse Rewriter::postRewrite(theory::TheoryId theoryId,
+                                      TNode n,
+                                      TConvProofGenerator* tcpg)
 {
   Kind k = n.getKind();
   std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn =
       (k == kind::EQUAL) ? d_postRewritersEqual[theoryId] : d_postRewriters[k];
   if (fn == nullptr)
   {
+    if (tcpg != nullptr)
+    {
+      // same as above, for post-rewrite
+      TrustRewriteResponse tresponse =
+          d_theoryRewriters[theoryId]->postRewriteWithProof(n);
+      return processTrustRewriteResponse(tresponse, false, tcpg);
+    }
     return d_theoryRewriters[theoryId]->postRewrite(n);
   }
   return fn(&d_re, n);
 }
 
+RewriteResponse Rewriter::processTrustRewriteResponse(
+    const TrustRewriteResponse& tresponse,
+    bool isPre,
+    TConvProofGenerator* tcpg)
+{
+  Assert(tcpg != nullptr);
+  TrustNode trn = tresponse.d_node;
+  Assert(trn.getKind() == TrustNodeKind::REWRITE);
+  Node proven = trn.getProven();
+  if (proven[0] != proven[1])
+  {
+    ProofGenerator* pg = trn.getGenerator();
+    if (pg == nullptr)
+    {
+      // add small step trusted rewrite
+      NodeManager* nm = NodeManager::currentNM();
+      tcpg->addRewriteStep(proven[0],
+                           proven[1],
+                           PfRule::THEORY_REWRITE,
+                           {},
+                           {proven[0], nm->mkConst(isPre)});
+    }
+    else
+    {
+      // store proven rewrite step
+      tcpg->addRewriteStep(proven[0], proven[1], pg);
+    }
+  }
+  return RewriteResponse(tresponse.d_status, trn.getNode());
+}
+
 void Rewriter::clearCaches() {
   Rewriter* rewriter = getInstance();
 
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index e021ac9e7..c57844f23 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -19,12 +19,18 @@
 #pragma once
 
 #include "expr/node.h"
+#include "expr/term_conversion_proof_generator.h"
 #include "theory/theory_rewriter.h"
+#include "theory/trust_node.h"
 #include "util/unsafe_interrupt_exception.h"
 
 namespace CVC4 {
 namespace theory {
 
+namespace builtin {
+class BuiltinProofRuleChecker;
+}
+
 class RewriterInitializer;
 
 /**
@@ -48,6 +54,8 @@ RewriteResponse identityRewrite(RewriteEnvironment* re, TNode n);
  * The main rewriter class.
  */
 class Rewriter {
+  friend builtin::BuiltinProofRuleChecker;
+
  public:
   Rewriter();
 
@@ -58,6 +66,38 @@ class Rewriter {
   static Node rewrite(TNode node);
 
   /**
+   * Rewrites the equality node using theoryOf() to determine which rewriter to
+   * use on the node corresponding to an equality s = t.
+   *
+   * Specifically, this method performs rewrites whose conclusion is not
+   * necessarily one of { s = t, t = s, true, false }, which is an invariant
+   * guaranted by the above method. This invariant is motivated by theory
+   * combination, which needs to guarantee that equalities between terms
+   * can be communicated for all pairs of terms.
+   */
+  static Node rewriteEqualityExt(TNode node);
+
+  /**
+   * Rewrite with proof production, which is managed by the term conversion
+   * proof generator managed by this class (d_tpg). This method requires a call
+   * to setProofChecker prior to this call.
+   *
+   * @param node The node to rewrite.
+   * @param elimTheoryRewrite Whether we also want fine-grained proofs for
+   * THEORY_REWRITE steps.
+   * @param isExtEq Whether node is an equality which we are applying
+   * rewriteEqualityExt on.
+   * @return The trust node of kind TrustNodeKind::REWRITE that contains the
+   * rewritten form of node.
+   */
+  TrustNode rewriteWithProof(TNode node,
+                             bool elimTheoryRewrite = false,
+                             bool isExtEq = false);
+
+  /** Set proof checker */
+  void setProofChecker(ProofChecker* pc);
+
+  /**
    * Garbage collects the rewrite caches.
    */
   static void clearCaches();
@@ -134,13 +174,24 @@ class Rewriter {
   /**
    * Rewrites the node using the given theory rewriter.
    */
-  Node rewriteTo(theory::TheoryId theoryId, Node node);
+  Node rewriteTo(theory::TheoryId theoryId,
+                 Node node,
+                 TConvProofGenerator* tcpg = nullptr);
 
   /** Calls the pre-rewriter for the given theory */
-  RewriteResponse preRewrite(theory::TheoryId theoryId, TNode n);
+  RewriteResponse preRewrite(theory::TheoryId theoryId,
+                             TNode n,
+                             TConvProofGenerator* tcpg = nullptr);
 
   /** Calls the post-rewriter for the given theory */
-  RewriteResponse postRewrite(theory::TheoryId theoryId, TNode n);
+  RewriteResponse postRewrite(theory::TheoryId theoryId,
+                              TNode n,
+                              TConvProofGenerator* tcpg = nullptr);
+  /** processes a trust rewrite response */
+  RewriteResponse processTrustRewriteResponse(
+      const TrustRewriteResponse& tresponse,
+      bool isPre,
+      TConvProofGenerator* tcpg);
 
   /**
    * Calls the equality-rewriter for the given theory.
@@ -175,6 +226,10 @@ class Rewriter {
 
   RewriteEnvironment d_re;
 
+  /** The proof node manager */
+  std::unique_ptr<ProofNodeManager> d_pnm;
+  /** The proof generator */
+  std::unique_ptr<TConvProofGenerator> d_tpg;
 #ifdef CVC4_ASSERTIONS
   std::unique_ptr<std::unordered_set<Node, NodeHashFunction>> d_rewriteStack =
       nullptr;
diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h
index 3251579ff..47a20a7ca 100644
--- a/src/theory/strings/sequences_rewriter.h
+++ b/src/theory/strings/sequences_rewriter.h
@@ -145,7 +145,7 @@ class SequencesRewriter : public TheoryRewriter
    * Specifically, this function performs rewrites whose conclusion is not
    * necessarily one of { s = t, t = s, true, false }.
    */
-  Node rewriteEqualityExt(Node node);
+  Node rewriteEqualityExt(Node node) override;
   /** rewrite string length
    * This is the entry point for post-rewriting terms node of the form
    *   str.len( t )
diff --git a/src/theory/theory_rewriter.cpp b/src/theory/theory_rewriter.cpp
new file mode 100644
index 000000000..a8dfbb2bb
--- /dev/null
+++ b/src/theory/theory_rewriter.cpp
@@ -0,0 +1,63 @@
+/*********************                                                        */
+/*! \file theory_rewriter.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The TheoryRewriter class
+ **
+ ** The TheoryRewriter class is the interface that theory rewriters implement.
+ **/
+
+#include "theory/theory_rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+
+TrustRewriteResponse::TrustRewriteResponse(RewriteStatus status,
+                                           Node n,
+                                           Node nr,
+                                           ProofGenerator* pg)
+    : d_status(status)
+{
+  // we always make non-null, regardless of whether n = nr
+  d_node = TrustNode::mkTrustRewrite(n, nr, pg);
+}
+
+TrustRewriteResponse TheoryRewriter::postRewriteWithProof(TNode node)
+{
+  RewriteResponse response = postRewrite(node);
+  // by default, we return a trust rewrite response with no proof generator
+  return TrustRewriteResponse(
+      response.d_status, node, response.d_node, nullptr);
+}
+
+TrustRewriteResponse TheoryRewriter::preRewriteWithProof(TNode node)
+{
+  RewriteResponse response = preRewrite(node);
+  // by default, we return a trust rewrite response with no proof generator
+  return TrustRewriteResponse(
+      response.d_status, node, response.d_node, nullptr);
+}
+
+Node TheoryRewriter::rewriteEqualityExt(Node node) { return node; }
+
+TrustNode TheoryRewriter::rewriteEqualityExtWithProof(Node node)
+{
+  Node nodeRew = rewriteEqualityExt(node);
+  if (nodeRew != node)
+  {
+    // by default, we return a trust rewrite response with no proof generator
+    return TrustNode::mkTrustRewrite(node, nodeRew, nullptr);
+  }
+  // no rewrite
+  return TrustNode::null();
+}
+
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/theory_rewriter.h b/src/theory/theory_rewriter.h
index 4a9c8d14f..cabfad2fc 100644
--- a/src/theory/theory_rewriter.h
+++ b/src/theory/theory_rewriter.h
@@ -20,6 +20,7 @@
 #define CVC4__THEORY__THEORY_REWRITER_H
 
 #include "expr/node.h"
+#include "theory/trust_node.h"
 
 namespace CVC4 {
 namespace theory {
@@ -53,6 +54,21 @@ struct RewriteResponse
   RewriteResponse(RewriteStatus status, Node n) : d_status(status), d_node(n) {}
 }; /* struct RewriteResponse */
 
+/** Same as above, with trust node instead of node. */
+struct TrustRewriteResponse
+{
+  TrustRewriteResponse(RewriteStatus status,
+                       Node n,
+                       Node nr,
+                       ProofGenerator* pg);
+  /** The status of the rewrite */
+  const RewriteStatus d_status;
+  /**
+   * The trust node corresponding to the rewrite.
+   */
+  TrustNode d_node;
+};
+
 /**
  * The interface that a theory rewriter has to implement.
  *
@@ -80,11 +96,47 @@ class TheoryRewriter
   virtual RewriteResponse postRewrite(TNode node) = 0;
 
   /**
+   * Performs a pre-rewrite step, with proofs.
+   *
+   * @param node The node to rewrite
+   */
+  virtual TrustRewriteResponse postRewriteWithProof(TNode node);
+
+  /**
    * Performs a post-rewrite step.
    *
    * @param node The node to rewrite
    */
   virtual RewriteResponse preRewrite(TNode node) = 0;
+
+  /**
+   * Performs a pre-rewrite step, with proofs.
+   *
+   * @param node The node to rewrite
+   */
+  virtual TrustRewriteResponse preRewriteWithProof(TNode node);
+
+  /** rewrite equality extended
+   *
+   * This method returns a formula that is equivalent to the equality between
+   * two terms s = t, given by node.
+   *
+   * Specifically, this method performs rewrites whose conclusion is not
+   * necessarily one of { s = t, t = s, true, false }. This is in constrast
+   * to postRewrite and preRewrite above, where the rewritten form of an
+   * equality must be one of these.
+   *
+   * @param node The node to rewrite
+   */
+  virtual Node rewriteEqualityExt(Node node);
+
+  /** rewrite equality extended, with proofs
+   *
+   * @param node The node to rewrite
+   * @return A trust node of kind TrustNodeKind::REWRITE, or the null trust
+   * node if no rewrites are applied.
+   */
+  virtual TrustNode rewriteEqualityExtWithProof(Node node);
 };
 
 }  // namespace theory