(proof-new) Fixes for proofs in rewriter (#5307)

This PR fixes proofs in the rewriter so that we use attributes for marking whether a node has been rewritten with proofs instead of consulting the provided TConvProofGenerator for hasRewriteStep. This additionally marks TRUST_REWRITE steps if a rewriter happens to be nondeterministic (e.g. quantifiers). It furthermore decouples rewriteWithProof from reconstruction for theory rewrite steps.

The proof postprocessor is additionally updated so that extended equality REWRITE steps are converted to THEORY_REWRITE steps with identifier RW_REWRITE_EQ_EXT for consistency, since eliminating REWRITE should result in THEORY_REWRITE only. This required generalizing the argument to THEORY_REWRITE to be a MethodId instead of a Boolean.

6 files changed, 111 insertions, 32 deletions

diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index e24d5c522..2b5565318 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -201,16 +201,17 @@ enum class PfRule : uint32_t
   THEORY_LEMMA,
   // ======== Theory Rewrite
   // Children: none
-  // Arguments: (F, tid, preRewrite?)
+  // Arguments: (F, tid, rid)
   // ----------------------------------------
   // Conclusion: F
   // where F is an equality of the form (= t t') where t' is obtained by
-  // applying the theory rewriter with identifier tid in either its prewrite
-  // (when preRewrite is true) or postrewrite method. Notice that the checker
-  // for this rule does not replay the rewrite to ensure correctness, since
-  // theory rewriter methods are not static. For example, the quantifiers
-  // rewriter involves constructing new bound variables that are not guaranteed
-  // to be consistent on each call.
+  // applying the kind of rewriting given by the method identifier rid, which
+  // is one of:
+  //  { RW_REWRITE_THEORY_PRE, RW_REWRITE_THEORY_POST, RW_REWRITE_EQ_EXT }
+  // Notice that the checker for this rule does not replay the rewrite to ensure
+  // correctness, since theory rewriter methods are not static. For example,
+  // the quantifiers rewriter involves constructing new bound variables that are
+  // not guaranteed to be consistent on each call.
   THEORY_REWRITE,
   // The rules in this section have the signature of a "trusted rule":
   //
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index a7723d265..40e61964c 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -21,6 +21,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/builtin/proof_checker.h"
 #include "theory/rewriter.h"
+#include "theory/theory.h"
 
 using namespace CVC4::kind;
 using namespace CVC4::theory;
@@ -543,14 +544,11 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
     Node eq = args[0].eqNode(ret);
     if (idr == MethodId::RW_REWRITE || idr == MethodId::RW_REWRITE_EQ_EXT)
     {
-      // automatically expand THEORY_REWRITE as well here if set
-      bool elimTR =
-          (d_elimRules.find(PfRule::THEORY_REWRITE) != d_elimRules.end());
       // rewrites from theory::Rewriter
       bool isExtEq = (idr == MethodId::RW_REWRITE_EQ_EXT);
       // use rewrite with proof interface
       Rewriter* rr = d_smte->getRewriter();
-      TrustNode trn = rr->rewriteWithProof(args[0], elimTR, isExtEq);
+      TrustNode trn = rr->rewriteWithProof(args[0], isExtEq);
       std::shared_ptr<ProofNode> pfn = trn.toProofNode();
       if (pfn == nullptr)
       {
@@ -559,10 +557,17 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
         // did not have a proof of rewriting, probably isExtEq is true
         if (isExtEq)
         {
-          // don't update
-          return Node::null();
+          // update to THEORY_REWRITE with idr
+          Assert(args.size() >= 1);
+          TheoryId theoryId = Theory::theoryOf(args[0].getType());
+          Node tid = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId);
+          cdp->addStep(eq, PfRule::THEORY_REWRITE, {}, {eq, tid, args[1]});
+        }
+        else
+        {
+          // this should never be applied
+          cdp->addStep(eq, PfRule::TRUST_REWRITE, {}, {eq});
         }
-        cdp->addStep(eq, PfRule::TRUST_REWRITE, {}, {eq});
       }
       else
       {
@@ -590,6 +595,24 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
     }
     return eq;
   }
+  else if (id == PfRule::THEORY_REWRITE)
+  {
+    Assert(!args.empty());
+    Node eq = args[0];
+    Assert(eq.getKind() == EQUAL);
+    // try to replay theory rewrite
+    // first, check that maybe its just an evaluation step
+    ProofChecker* pc = d_pnm->getChecker();
+    Node ceval =
+        pc->checkDebug(PfRule::EVALUATE, {}, {eq[0]}, eq, "smt-proof-pp-debug");
+    if (!ceval.isNull() && ceval == eq)
+    {
+      cdp->addStep(eq, PfRule::EVALUATE, {}, {eq[0]});
+      return eq;
+    }
+    // otherwise no update
+    Trace("final-pf-hole") << "hole: " << id << " : " << eq << std::endl;
+  }
 
   // TRUST, PREPROCESS, THEORY_LEMMA, THEORY_PREPROCESS?
 
@@ -712,14 +735,6 @@ bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
                                                  bool& continueUpdate)
 {
   PfRule r = pn->getRule();
-  if (Trace.isOn("final-pf-hole"))
-  {
-    if (r == PfRule::THEORY_REWRITE)
-    {
-      Trace("final-pf-hole") << "hole: " << r << " : " << pn->getResult()
-                            << std::endl;
-    }
-  }
   // if not doing eager pedantic checking, fail if below threshold
   if (!options::proofNewPedanticEager())
   {
@@ -758,7 +773,8 @@ ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm,
                                      ProofGenerator* pppg)
     : d_pnm(pnm),
       d_cb(pnm, smte, pppg),
-      d_updater(d_pnm, d_cb),
+      // the update merges subproofs
+      d_updater(d_pnm, d_cb, true),
       d_finalCb(pnm),
       d_finalizer(d_pnm, d_finalCb)
 {
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 73d39f417..4e2e78bae 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -34,6 +34,8 @@ const char* toString(MethodId id)
     case MethodId::RW_REWRITE_EQ_EXT: return "RW_REWRITE_EQ_EXT";
     case MethodId::RW_EVALUATE: return "RW_EVALUATE";
     case MethodId::RW_IDENTITY: return "RW_IDENTITY";
+    case MethodId::RW_REWRITE_THEORY_PRE: return "RW_REWRITE_THEORY_PRE";
+    case MethodId::RW_REWRITE_THEORY_POST: return "RW_REWRITE_THEORY_POST";
     case MethodId::SB_DEFAULT: return "SB_DEFAULT";
     case MethodId::SB_LITERAL: return "SB_LITERAL";
     case MethodId::SB_FORMULA: return "SB_FORMULA";
@@ -76,7 +78,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 3);
   pc->registerTrustedChecker(PfRule::TRUST_REWRITE, this, 1);
   pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1);
-  pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 1);
+  pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 3);
 }
 
 Node BuiltinProofRuleChecker::applySubstitutionRewrite(
@@ -282,6 +284,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
       exp.push_back(children[i]);
     }
     Node res = applySubstitution(args[0], exp, ids);
+    if (res.isNull())
+    {
+      return Node::null();
+    }
     return args[0].eqNode(res);
   }
   else if (id == PfRule::REWRITE)
@@ -294,6 +300,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
       return Node::null();
     }
     Node res = applyRewrite(args[0], idr);
+    if (res.isNull())
+    {
+      return Node::null();
+    }
     return args[0].eqNode(res);
   }
   else if (id == PfRule::EVALUATE)
@@ -301,6 +311,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     Assert(children.empty());
     Assert(args.size() == 1);
     Node res = applyRewrite(args[0], MethodId::RW_EVALUATE);
+    if (res.isNull())
+    {
+      return Node::null();
+    }
     return args[0].eqNode(res);
   }
   else if (id == PfRule::MACRO_SR_EQ_INTRO)
@@ -312,6 +326,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
       return Node::null();
     }
     Node res = applySubstitutionRewrite(args[0], children, ids, idr);
+    if (res.isNull())
+    {
+      return Node::null();
+    }
     return args[0].eqNode(res);
   }
   else if (id == PfRule::MACRO_SR_PRED_INTRO)
diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h
index 66b04de45..fc26beaa1 100644
--- a/src/theory/builtin/proof_checker.h
+++ b/src/theory/builtin/proof_checker.h
@@ -50,6 +50,12 @@ enum class MethodId : uint32_t
   RW_EVALUATE,
   // identity
   RW_IDENTITY,
+  // theory preRewrite, note this is only intended to be used as an argument
+  // to THEORY_REWRITE in the final proof. It is not implemented in
+  // applyRewrite below, see documentation in proof_rule.h for THEORY_REWRITE.
+  RW_REWRITE_THEORY_PRE,
+  // same as above, for theory postRewrite
+  RW_REWRITE_THEORY_POST,
   //---------------------------- Substitutions
   // (= x y) is interpreted as x -> y, using Node::substitute
   SB_DEFAULT,
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 9e5708d4d..7ebacee92 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -31,6 +31,13 @@ using namespace std;
 namespace CVC4 {
 namespace theory {
 
+/** Attribute true for nodes that have been rewritten with proofs enabled */
+struct RewriteWithProofsAttributeId
+{
+};
+typedef expr::Attribute<RewriteWithProofsAttributeId, bool>
+    RewriteWithProofsAttribute;
+
 // Note that this function is a simplified version of Theory::theoryOf for
 // (type-based) theoryOfMode. We expand and simplify it here for the sake of
 // efficiency.
@@ -100,7 +107,6 @@ Node Rewriter::rewrite(TNode node) {
 }
 
 TrustNode Rewriter::rewriteWithProof(TNode node,
-                                     bool elimTheoryRewrite,
                                      bool isExtEq)
 {
   // must set the proof checker before calling this
@@ -121,6 +127,7 @@ void Rewriter::setProofNodeManager(ProofNodeManager* pnm)
   // if not already initialized with proof support
   if (d_tpg == nullptr)
   {
+    Trace("rewriter") << "Rewriter::setProofNodeManager" << std::endl;
     // the rewriter is staticly determinstic, thus use static cache policy
     // for the term conversion proof generator
     d_tpg.reset(new TConvProofGenerator(pnm,
@@ -182,6 +189,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
                          Node node,
                          TConvProofGenerator* tcpg)
 {
+  RewriteWithProofsAttribute rpfa;
 #ifdef CVC4_ASSERTIONS
   bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean());
 
@@ -195,7 +203,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
 
   // Check if it's been cached already
   Node cached = getPostRewriteCache(theoryId, node);
-  if (!cached.isNull() && (tcpg == nullptr || tcpg->hasRewriteStep(node)))
+  if (!cached.isNull() && (tcpg == nullptr || node.getAttribute(rpfa)))
   {
     return cached;
   }
@@ -232,7 +240,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
       cached = getPreRewriteCache(rewriteStackTop.getTheoryId(),
                                   rewriteStackTop.d_node);
       if (cached.isNull()
-          || (tcpg != nullptr && !tcpg->hasRewriteStep(rewriteStackTop.d_node)))
+          || (tcpg != nullptr && !rewriteStackTop.d_node.getAttribute(rpfa)))
       {
         // Rewrite until fix-point is reached
         for(;;) {
@@ -271,7 +279,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
                                  rewriteStackTop.d_node);
     // If not, go through the children
     if (cached.isNull()
-        || (tcpg != nullptr && !tcpg->hasRewriteStep(rewriteStackTop.d_node)))
+        || (tcpg != nullptr && !rewriteStackTop.d_node.getAttribute(rpfa)))
     {
       // The child we need to rewrite
       unsigned child = rewriteStackTop.d_nextChild++;
@@ -355,6 +363,37 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
       }
 
       // We're done with the post rewrite, so we add to the cache
+      if (tcpg != nullptr)
+      {
+        // if proofs are enabled, mark that we've rewritten with proofs
+        rewriteStackTop.d_original.setAttribute(rpfa, true);
+        if (!cached.isNull())
+        {
+          // We may have gotten a different node, due to non-determinism in
+          // theory rewriters (e.g. quantifiers rewriter which introduces
+          // fresh BOUND_VARIABLE). This can happen if we wrote once without
+          // proofs and then rewrote again with proofs.
+          if (rewriteStackTop.d_node != cached)
+          {
+            Trace("rewriter-proof") << "WARNING: Rewritten forms with and "
+                                       "without proofs were not equivalent"
+                                    << std::endl;
+            Trace("rewriter-proof")
+                << "   original: " << rewriteStackTop.d_original << std::endl;
+            Trace("rewriter-proof")
+                << "with proofs: " << rewriteStackTop.d_node << std::endl;
+            Trace("rewriter-proof") << " w/o proofs: " << cached << std::endl;
+            Node eq = rewriteStackTop.d_node.eqNode(cached);
+            tcpg->addRewriteStep(rewriteStackTop.d_node,
+                                 cached,
+                                 PfRule::TRUST_REWRITE,
+                                 {},
+                                 {eq});
+            // don't overwrite the cache, should be the same
+            rewriteStackTop.d_node = cached;
+          }
+        }
+      }
       setPostRewriteCache(rewriteStackTop.getOriginalTheoryId(),
                           rewriteStackTop.d_original,
                           rewriteStackTop.d_node);
@@ -443,11 +482,13 @@ RewriteResponse Rewriter::processTrustRewriteResponse(
       Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId);
       // add small step trusted rewrite
       NodeManager* nm = NodeManager::currentNM();
+      Node rid = mkMethodId(isPre ? MethodId::RW_REWRITE_THEORY_PRE
+                                  : MethodId::RW_REWRITE_THEORY_POST);
       tcpg->addRewriteStep(proven[0],
                            proven[1],
                            PfRule::THEORY_REWRITE,
                            {},
-                           {proven, tidn, nm->mkConst(isPre)});
+                           {proven, tidn, rid});
     }
     else
     {
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index f38f3b174..e36426a81 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -83,15 +83,12 @@ class Rewriter {
    * to setProofNodeManager 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 node manager */