(proof-new) Distinguish pre vs post rewrites in term conversion proof generator (#5833)

This is work towards resolving two kinds of failures on proof-new:

(1) Functional issues with proofs from the rewriter, in particular when a term pre-rewrites and post-rewrites to different things,
(2) Conversion issues in theory-preprocessing, where all steps are assumed to be post-rewrites but some are in fact pre-rewrites. This leads to the term conversion proof generator proving something different than what is expected.

A followup PR will simplify and fix proofs for theory-preprocessing.

2 files changed, 60 insertions, 43 deletions

diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp
index d351d88b6..d37ccf914 100644
--- a/src/expr/term_conversion_proof_generator.cpp
+++ b/src/expr/term_conversion_proof_generator.cpp
@@ -51,7 +51,8 @@ TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm,
                                          TermContext* tccb,
                                          bool rewriteOps)
     : d_proof(pnm, nullptr, c, name + "::LazyCDProof"),
-      d_rewriteMap(c ? c : &d_context),
+      d_preRewriteMap(c ? c : &d_context),
+      d_postRewriteMap(c ? c : &d_context),
       d_policy(pol),
       d_cpolicy(cpol),
       d_name(name),
@@ -65,23 +66,22 @@ TConvProofGenerator::~TConvProofGenerator() {}
 void TConvProofGenerator::addRewriteStep(Node t,
                                          Node s,
                                          ProofGenerator* pg,
+                                         bool isPre,
                                          PfRule trustId,
                                          bool isClosed,
                                          uint32_t tctx)
 {
-  Node eq = registerRewriteStep(t, s, tctx);
+  Node eq = registerRewriteStep(t, s, tctx, isPre);
   if (!eq.isNull())
   {
     d_proof.addLazyStep(eq, pg, trustId, isClosed);
   }
 }
 
-void TConvProofGenerator::addRewriteStep(Node t,
-                                         Node s,
-                                         ProofStep ps,
-                                         uint32_t tctx)
+void TConvProofGenerator::addRewriteStep(
+    Node t, Node s, ProofStep ps, bool isPre, uint32_t tctx)
 {
-  Node eq = registerRewriteStep(t, s, tctx);
+  Node eq = registerRewriteStep(t, s, tctx, isPre);
   if (!eq.isNull())
   {
     d_proof.addStep(eq, ps);
@@ -93,31 +93,39 @@ void TConvProofGenerator::addRewriteStep(Node t,
                                          PfRule id,
                                          const std::vector<Node>& children,
                                          const std::vector<Node>& args,
+                                         bool isPre,
                                          uint32_t tctx)
 {
-  Node eq = registerRewriteStep(t, s, tctx);
+  Node eq = registerRewriteStep(t, s, tctx, isPre);
   if (!eq.isNull())
   {
     d_proof.addStep(eq, id, children, args);
   }
 }
 
-bool TConvProofGenerator::hasRewriteStep(Node t, uint32_t tctx) const
+bool TConvProofGenerator::hasRewriteStep(Node t,
+                                         uint32_t tctx,
+                                         bool isPre) const
 {
-  return !getRewriteStep(t, tctx).isNull();
+  return !getRewriteStep(t, tctx, isPre).isNull();
 }
 
-Node TConvProofGenerator::getRewriteStep(Node t, uint32_t tctx) const
+Node TConvProofGenerator::getRewriteStep(Node t,
+                                         uint32_t tctx,
+                                         bool isPre) const
 {
   Node thash = t;
   if (d_tcontext != nullptr)
   {
     thash = TCtxNode::computeNodeHash(t, tctx);
   }
-  return getRewriteStepInternal(thash);
+  return getRewriteStepInternal(thash, isPre);
 }
 
-Node TConvProofGenerator::registerRewriteStep(Node t, Node s, uint32_t tctx)
+Node TConvProofGenerator::registerRewriteStep(Node t,
+                                              Node s,
+                                              uint32_t tctx,
+                                              bool isPre)
 {
   if (t == s)
   {
@@ -134,14 +142,15 @@ Node TConvProofGenerator::registerRewriteStep(Node t, Node s, uint32_t tctx)
     Assert(tctx == 0);
   }
   // should not rewrite term to two different things
-  if (!getRewriteStepInternal(thash).isNull())
+  if (!getRewriteStepInternal(thash, isPre).isNull())
   {
-    Assert(getRewriteStepInternal(thash) == s)
+    Assert(getRewriteStepInternal(thash, isPre) == s)
         << identify() << " rewriting " << t << " to both " << s << " and "
-        << getRewriteStepInternal(thash);
+        << getRewriteStepInternal(thash, isPre);
     return Node::null();
   }
-  d_rewriteMap[thash] = s;
+  NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap;
+  rm[thash] = s;
   if (d_cpolicy == TConvCachePolicy::DYNAMIC)
   {
     // clear the cache
@@ -188,19 +197,23 @@ std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f)
         serr << " (see -t tconv-pf-gen-debug for details)";
       }
       serr << std::endl;
-      serr << "                  source: " << f[0] << std::endl;
-      serr << "expected after rewriting: " << f[1] << std::endl;
-      serr << "  actual after rewriting: " << conc[1] << std::endl;
+      serr << "                   source: " << f[0] << std::endl;
+      serr << "     requested conclusion: " << f[1] << std::endl;
+      serr << "conclusion from generator: " << conc[1] << std::endl;
 
       if (debugTraceEnabled)
       {
         Trace("tconv-pf-gen-debug") << "Printing rewrite steps..." << std::endl;
-        serr << "Rewrite steps: " << std::endl;
-        for (NodeNodeMap::const_iterator it = d_rewriteMap.begin();
-             it != d_rewriteMap.end();
-             ++it)
+        for (size_t r = 0; r < 2; r++)
         {
-          serr << (*it).first << " -> " << (*it).second << std::endl;
+          const NodeNodeMap& rm = r == 0 ? d_preRewriteMap : d_postRewriteMap;
+          serr << "Rewrite steps (" << (r == 0 ? "pre" : "post")
+               << "):" << std::endl;
+          for (NodeNodeMap::const_iterator it = rm.begin(); it != rm.end();
+               ++it)
+          {
+            serr << (*it).first << " -> " << (*it).second << std::endl;
+          }
         }
       }
       Unhandled() << serr.str();
@@ -288,8 +301,8 @@ Node TConvProofGenerator::getProofForRewriting(Node t,
     {
       Trace("tconv-pf-gen-rewrite") << "- previsit" << std::endl;
       visited[curHash] = Node::null();
-      // did we rewrite the current node (possibly at pre-rewrite)?
-      Node rcur = getRewriteStepInternal(curHash);
+      // did we rewrite the current node (at pre-rewrite)?
+      Node rcur = getRewriteStepInternal(curHash, true);
       if (!rcur.isNull())
       {
         Trace("tconv-pf-gen-rewrite")
@@ -484,13 +497,8 @@ Node TConvProofGenerator::getProofForRewriting(Node t,
           retHash = TCtxNode::computeNodeHash(cur, curCVal);
         }
         // did we rewrite ret (at post-rewrite)?
-        Node rret;
-        // only if not ONCE policy, which only does pre-rewrite
-        if (d_policy != TConvPolicy::ONCE)
-        {
-          rret = getRewriteStepInternal(retHash);
-        }
-        if (!rret.isNull())
+        Node rret = getRewriteStepInternal(retHash, false);
+        if (!rret.isNull() && d_policy == TConvPolicy::FIXPOINT)
         {
           Trace("tconv-pf-gen-rewrite")
               << "*** " << retHash << " postrewrites to " << rret << std::endl;
@@ -519,6 +527,8 @@ Node TConvProofGenerator::getProofForRewriting(Node t,
         }
         else
         {
+          // take its rewrite if it rewrote and we have ONCE rewriting policy
+          ret = rret.isNull() ? ret : rret;
           Trace("tconv-pf-gen-rewrite")
               << "-> (postrewrite) " << curHash << " = " << ret << std::endl;
           // it is final
@@ -553,10 +563,11 @@ void TConvProofGenerator::doCache(Node curHash,
   }
 }
 
-Node TConvProofGenerator::getRewriteStepInternal(Node t) const
+Node TConvProofGenerator::getRewriteStepInternal(Node t, bool isPre) const
 {
-  NodeNodeMap::const_iterator it = d_rewriteMap.find(t);
-  if (it == d_rewriteMap.end())
+  const NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap;
+  NodeNodeMap::const_iterator it = rm.find(t);
+  if (it == rm.end())
   {
     return Node::null();
   }
diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h
index 0a1f4e70a..dcf8b3fa4 100644
--- a/src/expr/term_conversion_proof_generator.h
+++ b/src/expr/term_conversion_proof_generator.h
@@ -144,6 +144,8 @@ class TConvProofGenerator : public ProofGenerator
   /**
    * Add rewrite step t --> s based on proof generator.
    *
+   * @param isPre Whether the rewrite is applied at prerewrite (pre-order
+   * traversal).
    * @param trustId If a null proof generator is provided, we add a step to
    * the proof that has trustId as the rule and expected as the sole argument.
    * @param isClosed whether to expect that pg can provide a closed proof for
@@ -156,25 +158,28 @@ class TConvProofGenerator : public ProofGenerator
   void addRewriteStep(Node t,
                       Node s,
                       ProofGenerator* pg,
+                      bool isPre = false,
                       PfRule trustId = PfRule::ASSUME,
                       bool isClosed = false,
                       uint32_t tctx = 0);
   /** Same as above, for a single step */
-  void addRewriteStep(Node t, Node s, ProofStep ps, uint32_t tctx = 0);
+  void addRewriteStep(
+      Node t, Node s, ProofStep ps, bool isPre = false, uint32_t tctx = 0);
   /** Same as above, with explicit arguments */
   void addRewriteStep(Node t,
                       Node s,
                       PfRule id,
                       const std::vector<Node>& children,
                       const std::vector<Node>& args,
+                      bool isPre = false,
                       uint32_t tctx = 0);
   /** Has rewrite step for term t */
-  bool hasRewriteStep(Node t, uint32_t tctx = 0) const;
+  bool hasRewriteStep(Node t, uint32_t tctx = 0, bool isPre = false) const;
   /** 
    * Get rewrite step for term t, returns the s provided in a call to
    * addRewriteStep if one exists, or null otherwise.
    */
-  Node getRewriteStep(Node t, uint32_t tctx = 0) const;
+  Node getRewriteStep(Node t, uint32_t tctx = 0, bool isPre = false) const;
   /**
    * Get the proof for formula f. It should be the case that f is of the form
    * t = t', where t' is the result of rewriting t based on the rewrite steps
@@ -194,7 +199,8 @@ class TConvProofGenerator : public ProofGenerator
   /** The (lazy) context dependent proof object. */
   LazyCDProof d_proof;
   /** map to rewritten forms */
-  NodeNodeMap d_rewriteMap;
+  NodeNodeMap d_preRewriteMap;
+  NodeNodeMap d_postRewriteMap;
   /**
    * Policy for how rewrites are applied to terms. As a simple example, say we
    * have registered the rewrite steps:
@@ -220,7 +226,7 @@ class TConvProofGenerator : public ProofGenerator
    */
   bool d_rewriteOps;
   /** Get rewrite step for (hash value of) term. */
-  Node getRewriteStepInternal(Node thash) const;
+  Node getRewriteStepInternal(Node thash, bool isPre) const;
   /**
    * Adds a proof of t = t' to the proof pf where t' is the result of rewriting
    * t based on the rewrite steps registered to this class. This method then
@@ -231,7 +237,7 @@ class TConvProofGenerator : public ProofGenerator
    * Register rewrite step, returns the equality t=s if t is distinct from s
    * and a rewrite step has not already been registered for t.
    */
-  Node registerRewriteStep(Node t, Node s, uint32_t tctx);
+  Node registerRewriteStep(Node t, Node s, uint32_t tctx, bool isPre);
   /** cache that r is the rewritten form of cur, pf can provide a proof */
   void doCache(Node curHash, Node cur, Node r, LazyCDProof& pf);
   /** get debug information on this generator */