(proof-new) Fixes for theory preprocessing proofs (#5171)

This fixes several subtle issues with theory preprocessing.

The main fix is to ensure proofs are correct for cases where the theory preprocessor applies either with or without theory preprocessing (calling Theory::ppRewrite on subterms) enabled, see argument doTheoryPreprocess of preprocess. If disabled, it applies term formula removal and rewriting only. This is required for processing lemmas that are marked as "do not preprocess", which is an optimization, but is also necessary since theory combination may e.g. split on equality that was solved during ppRewrite. The solution is to use 2 separate term conversion sequences for these 2 cases.

It also fixes an issue where preprocessing is term-context-sensitive: terms underneath quantifiers are treated differently. This is now handled by a new TermContext callback "InQuantTermContext".

6 files changed, 160 insertions, 34 deletions

diff --git a/src/expr/term_context.cpp b/src/expr/term_context.cpp
index 6974e2114..67da6d842 100644
--- a/src/expr/term_context.cpp
+++ b/src/expr/term_context.cpp
@@ -69,6 +69,22 @@ bool RtfTermContext::hasNestedTermChildren(TNode t)
          && k != kind::BITVECTOR_EAGER_ATOM;
 }
 
+uint32_t InQuantTermContext::initialValue() const { return 0; }
+
+uint32_t InQuantTermContext::computeValue(TNode t,
+                                          uint32_t tval,
+                                          size_t index) const
+{
+  return t.isClosure() ? 1 : tval;
+}
+
+uint32_t InQuantTermContext::getValue(bool inQuant) { return inQuant ? 1 : 0; }
+
+bool InQuantTermContext::inQuant(uint32_t val, bool& inQuant)
+{
+  return val == 1;
+}
+
 uint32_t PolarityTermContext::initialValue() const
 {
   // by default, we have true polarity
diff --git a/src/expr/term_context.h b/src/expr/term_context.h
index ec7b488f9..b0ce03e48 100644
--- a/src/expr/term_context.h
+++ b/src/expr/term_context.h
@@ -93,6 +93,24 @@ class RtfTermContext : public TermContext
 };
 
 /**
+ * Simpler version of above that only computes whether we are inside a
+ * quantifier.
+ */
+class InQuantTermContext : public TermContext
+{
+ public:
+  InQuantTermContext() {}
+  /** The initial value: not beneath a quantifier. */
+  uint32_t initialValue() const override;
+  /** Compute the value of the index^th child of t whose hash is tval */
+  uint32_t computeValue(TNode t, uint32_t tval, size_t index) const override;
+  /** get hash value from the flags */
+  static uint32_t getValue(bool inQuant);
+  /** get flags from the hash value */
+  static bool inQuant(uint32_t val, bool& inQuant);
+};
+
+/**
  * Polarity term context.
  *
  * This class computes the polarity of a term-context-sensitive term, which is
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 5034119e8..cf7c00e2b 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -552,6 +552,11 @@ void RemoveTermFormulas::setProofNodeManager(ProofNodeManager* pnm)
   }
 }
 
+ProofGenerator* RemoveTermFormulas::getTConvProofGenerator()
+{
+  return d_tpg.get();
+}
+
 bool RemoveTermFormulas::isProofEnabled() const { return d_pnm != nullptr; }
 
 }/* CVC4 namespace */
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index 30972c1cc..25dcd0295 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -107,11 +107,19 @@ class RemoveTermFormulas {
 
   /**
    * Set proof node manager, which signals this class to enable proofs using the
-   * given checker.
+   * given proof node manager.
    */
   void setProofNodeManager(ProofNodeManager* pnm);
 
   /**
+   * Get proof generator that is responsible for all proofs for removing term
+   * formulas from nodes. When proofs are enabled, the returned trust node
+   * of the run method use this proof generator (the trust nodes in newAsserts
+   * do not use this generator).
+   */
+  ProofGenerator* getTConvProofGenerator();
+
+  /**
    * Get axiom for term n. This returns the axiom that this class uses to
    * eliminate the term n, which is determined by its top-most symbol. For
    * example, if n is (ite n1 n2 n3), this returns the formula:
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 049598dbb..80b824ca0 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -38,8 +38,17 @@ TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
                       &d_pfContext,
                       TConvPolicy::FIXPOINT,
                       TConvCachePolicy::NEVER,
-                      "TheoryPreprocessor::TConvProofGenerator")
+                      "TheoryPreprocessor::preprocess_rewrite",
+                      &d_iqtc)
                 : nullptr),
+      d_tspg(nullptr),
+      d_tpgRew(pnm ? new TConvProofGenerator(pnm,
+                                             &d_pfContext,
+                                             TConvPolicy::FIXPOINT,
+                                             TConvCachePolicy::NEVER,
+                                             "TheoryPreprocessor::rewrite")
+                   : nullptr),
+      d_tspgNoPp(nullptr),
       d_lp(pnm ? new LazyCDProof(pnm,
                                  nullptr,
                                  &d_pfContext,
@@ -53,6 +62,26 @@ TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
     // push the proof context, since proof steps may be cleared on calls to
     // clearCache() below.
     d_pfContext.push();
+    // Make the main term conversion sequence generator, which tracks up to
+    // three conversions made in succession:
+    // (1) theory preprocessing+rewriting
+    // (2) term formula removal
+    // (3) rewriting
+    // Steps (1) and (3) use a common term conversion generator.
+    std::vector<ProofGenerator*> ts;
+    ts.push_back(d_tpg.get());
+    ts.push_back(d_tfr.getTConvProofGenerator());
+    ts.push_back(d_tpg.get());
+    d_tspg.reset(new TConvSeqProofGenerator(
+        pnm, ts, &d_pfContext, "TheoryPreprocessor::sequence"));
+    // Make the "no preprocess" term conversion sequence generator, which
+    // applies only steps (2) and (3), where notice (3) must use the
+    // "pure rewrite" term conversion (d_tpgRew).
+    std::vector<ProofGenerator*> tsNoPp;
+    tsNoPp.push_back(d_tfr.getTConvProofGenerator());
+    tsNoPp.push_back(d_tpgRew.get());
+    d_tspgNoPp.reset(new TConvSeqProofGenerator(
+        pnm, tsNoPp, &d_pfContext, "TheoryPreprocessor::sequence_no_pp"));
   }
 }
 
@@ -60,8 +89,9 @@ TheoryPreprocessor::~TheoryPreprocessor() {}
 
 void TheoryPreprocessor::clearCache()
 {
+  Trace("tpp-proof-debug") << "TheoryPreprocessor::clearCache" << std::endl;
   d_ppCache.clear();
-  // clear proofs from d_tpg and d_lp using internal push/pop context
+  // clear proofs from d_tpg, d_tspg and d_lp using internal push/pop context
   if (isProofEnabled())
   {
     d_pfContext.pop();
@@ -77,6 +107,7 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
   // In this method, all rewriting steps of node are stored in d_tpg.
 
   Trace("tpp-proof-debug") << "TheoryPreprocessor::preprocess: start " << node
+                           << ", doTheoryPreprocess=" << doTheoryPreprocess
                            << std::endl;
   // Run theory preprocessing, maybe
   Node ppNode = node;
@@ -94,22 +125,10 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
   Trace("te-tform-rm") << "Remove term formulas from " << ppNode << std::endl;
   TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems, false);
   Trace("te-tform-rm") << "..done " << ttfr.getNode() << std::endl;
-  Node retNode = ttfr.getNode();
-  if (isProofEnabled())
-  {
-    // if we rewrote
-    if (retNode != ppNode)
-    {
-      // should always have provided a proof generator, or else term formula
-      // removal and this class do not agree on whether proofs are enabled.
-      Assert(ttfr.getGenerator() != nullptr);
-      Trace("tpp-proof-debug")
-          << "TheoryPreprocessor: addRewriteStep (term formula removal) "
-          << ppNode << " -> " << retNode << std::endl;
-      // store as a rewrite in d_tpg
-      d_tpg->addRewriteStep(ppNode, retNode, ttfr.getGenerator());
-    }
-  }
+  Node rtfNode = ttfr.getNode();
+  Trace("tpp-proof-debug")
+      << "TheoryPreprocessor::preprocess: rtf returned node " << rtfNode
+      << std::endl;
 
   if (Debug.isOn("lemma-ites"))
   {
@@ -125,13 +144,54 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
   }
   // Rewrite the main node, we rewrite and store the proof step, if necessary,
   // in d_tpg, which maintains the fact that d_tpg can prove the rewrite.
-  Trace("tpp-proof-debug")
-      << "TheoryPreprocessor::preprocess: rewrite returned node " << retNode
-      << std::endl;
-  retNode = rewriteWithProof(retNode);
+  Node retNode = rewriteWithProof(rtfNode);
   Trace("tpp-proof-debug")
       << "TheoryPreprocessor::preprocess: after rewriting is " << retNode
       << std::endl;
+  if (node == retNode)
+  {
+    // no change
+    Assert(newLemmas.empty());
+    return TrustNode::null();
+  }
+
+  // Now, sequence the conversion steps if proofs are enabled.
+  TrustNode tret;
+  if (isProofEnabled())
+  {
+    std::vector<Node> cterms;
+    cterms.push_back(node);
+    if (doTheoryPreprocess)
+    {
+      cterms.push_back(ppNode);
+    }
+    cterms.push_back(rtfNode);
+    cterms.push_back(retNode);
+    // We have that:
+    // node -> ppNode via preprocessing + rewriting (if doTheoryPreprocess)
+    // ppNode -> rtfNode via term formula removal
+    // rtfNode -> retNode via rewriting
+    if (!doTheoryPreprocess)
+    {
+      // If preprocessing is not performed, we cannot use the main sequence
+      // generator, instead we use d_tspgNoPp.
+      // We register the top-level rewrite in the pure rewrite term converter.
+      d_tpgRew->addRewriteStep(
+          rtfNode, retNode, PfRule::REWRITE, {}, {rtfNode});
+      // Now get the trust node from the sequence generator
+      tret = d_tspgNoPp->mkTrustRewriteSequence(cterms);
+    }
+    else
+    {
+      // we wil use the sequence generator
+      tret = d_tspg->mkTrustRewriteSequence(cterms);
+    }
+    tret.debugCheckClosed("tpp-proof-debug", "TheoryPreprocessor::lemma_ret");
+  }
+  else
+  {
+    tret = TrustNode::mkTrustRewrite(node, retNode, nullptr);
+  }
 
   // now, rewrite the lemmas
   Trace("tpp-proof-debug") << "TheoryPreprocessor::preprocess: process lemmas"
@@ -170,15 +230,8 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
     newLemmas[i].debugCheckClosed("tpp-proof-debug",
                                   "TheoryPreprocessor::lemma_new");
   }
-  if (node == retNode)
-  {
-    // no change
-    return TrustNode::null();
-  }
   Trace("tpp-proof-debug") << "Preprocessed: " << node << " " << retNode
                            << std::endl;
-  TrustNode tret = TrustNode::mkTrustRewrite(node, retNode, d_tpg.get());
-  tret.debugCheckClosed("tpp-proof-debug", "TheoryPreprocessor::lemma_ret");
   return tret;
 }
 
@@ -205,7 +258,7 @@ TrustNode TheoryPreprocessor::theoryPreprocess(TNode assertion)
     preprocess_stack_element& stackHead = toVisit.back();
     TNode current = stackHead.node;
 
-    Debug("theory::internal")
+    Trace("theory::preprocess-debug")
         << "TheoryPreprocessor::theoryPreprocess(" << assertion
         << "): processing " << current << endl;
 
@@ -258,7 +311,7 @@ TrustNode TheoryPreprocessor::theoryPreprocess(TNode assertion)
       {
         result = rewriteWithProof(result);
       }
-      Debug("theory::internal")
+      Trace("theory::preprocess-debug")
           << "TheoryPreprocessor::theoryPreprocess(" << assertion
           << "): setting " << current << " -> " << result << endl;
       d_ppCache[current] = result;
@@ -286,7 +339,7 @@ TrustNode TheoryPreprocessor::theoryPreprocess(TNode assertion)
       else
       {
         // No children, so we're done
-        Debug("substitution::internal")
+        Trace("theory::preprocess-debug")
             << "SubstitutionMap::internalSubstitute(" << assertion
             << "): setting " << current << " -> " << current << endl;
         d_ppCache[current] = current;
@@ -349,6 +402,7 @@ Node TheoryPreprocessor::rewriteWithProof(Node term)
       Trace("tpp-proof-debug")
           << "TheoryPreprocessor: addRewriteStep (rewriting) " << term << " -> "
           << termr << std::endl;
+      // always use term context hash 0 (default)
       d_tpg->addRewriteStep(term, termr, PfRule::REWRITE, {}, {term});
     }
   }
@@ -380,6 +434,7 @@ Node TheoryPreprocessor::preprocessWithProof(Node term)
           << termr << std::endl;
       trn.debugCheckClosed("tpp-proof-debug",
                            "TheoryPreprocessor::preprocessWithProof");
+      // always use term context hash 0 (default)
       d_tpg->addRewriteStep(term, termr, trn.getGenerator());
     }
     else
diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h
index db43b6828..769d548d9 100644
--- a/src/theory/theory_preprocessor.h
+++ b/src/theory/theory_preprocessor.h
@@ -21,6 +21,7 @@
 
 #include "expr/lazy_proof.h"
 #include "expr/node.h"
+#include "expr/tconv_seq_proof_generator.h"
 #include "expr/term_conversion_proof_generator.h"
 #include "theory/trust_node.h"
 
@@ -85,8 +86,31 @@ class TheoryPreprocessor
   RemoveTermFormulas& d_tfr;
   /** The context for the proof generator below */
   context::Context d_pfContext;
-  /** A term conversion proof generator */
+  /** The term context, which computes hash values for term contexts. */
+  InQuantTermContext d_iqtc;
+  /**
+   * A term conversion proof generator storing preprocessing and rewriting
+   * steps.
+   */
   std::unique_ptr<TConvProofGenerator> d_tpg;
+  /**
+   * A term conversion sequence generator, which applies theory preprocessing,
+   * term formula removal, and rewriting in sequence.
+   */
+  std::unique_ptr<TConvSeqProofGenerator> d_tspg;
+  /**
+   * A term conversion proof generator storing rewriting steps, which is used
+   * for calls to preprocess when doTheoryPreprocess is false. We store
+   * (top-level) rewrite steps only. Notice this is intentionally separate
+   * from d_tpg, which interleaves both preprocessing and rewriting.
+   */
+  std::unique_ptr<TConvProofGenerator> d_tpgRew;
+  /**
+   * A term conversion sequence generator, which applies term formula removal
+   * and rewriting in sequence. This is used for reconstruct proofs of
+   * calls to preprocess where doTheoryPreprocess is false.
+   */
+  std::unique_ptr<TConvSeqProofGenerator> d_tspgNoPp;
   /** A lazy proof, for additional lemmas. */
   std::unique_ptr<LazyCDProof> d_lp;
   /** Helper for theoryPreprocess */