Always theory-preprocess lemmas (#5817)

This PR makes it so that theory-preprocessing is always called on lemmas. It simplifies the proof production in the theory preprocessor accordingly.

Additionally, it ensures that our theory-preprocessor is run on lemmas that are generated from term formula removal. Previously, this was not the case and in fact certain lemmas (e.g. literals within witness terms that are not in preprocessed form) would escape and be asserted to TheoryEngine. This was uncovered by a unit test failure, the corresponding regression is added in this PR.

It adds a new interface removeItes to PropEngine which is required for the (deprecated) preprocessing pass removeItes.

This PR now makes the lemma propery PREPROCESS obsolete. Further simplification is possible after this PR in non-linear arithmetic and quantifiers, where it is not necessary to distinguish 2 caches for preprocessed vs. non-preprocessed lemmas.

10 files changed, 125 insertions, 138 deletions

diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index 91af2a5b8..66a32472b 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -44,16 +44,11 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
     Node assertion = (*assertions)[i];
     std::vector<theory::TrustNode> newAsserts;
     std::vector<Node> newSkolems;
-    TrustNode trn = pe->preprocess(assertion, newAsserts, newSkolems, false);
+    TrustNode trn = pe->removeItes(assertion, newAsserts, newSkolems);
     if (!trn.isNull())
     {
       // process
       assertions->replaceTrusted(i, trn);
-      // rewritten assertion has a dependence on the node (old pf architecture)
-      if (options::unsatCores() && !options::proofNew())
-      {
-        ProofManager::currentPM()->addDependence(trn.getNode(), assertion);
-      }
     }
     Assert(newSkolems.size() == newAsserts.size());
     for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++)
diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index 6c751f864..4552d13fc 100644
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -41,17 +41,11 @@ PreprocessingPassResult TheoryPreprocess::applyInternal(
     Node assertion = (*assertions)[i];
     std::vector<theory::TrustNode> newAsserts;
     std::vector<Node> newSkolems;
-    TrustNode trn =
-        propEngine->preprocess(assertion, newAsserts, newSkolems, true);
+    TrustNode trn = propEngine->preprocess(assertion, newAsserts, newSkolems);
     if (!trn.isNull())
     {
       // process
       assertions->replaceTrusted(i, trn);
-      // rewritten assertion has a dependence on the node (old pf architecture)
-      if (options::unsatCores())
-      {
-        ProofManager::currentPM()->addDependence(trn.getNode(), assertion);
-      }
     }
     Assert(newSkolems.size() == newAsserts.size());
     for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++)
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 2fa62d9f6..fb43ebe73 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -156,11 +156,17 @@ PropEngine::~PropEngine() {
 theory::TrustNode PropEngine::preprocess(
     TNode node,
     std::vector<theory::TrustNode>& newLemmas,
-    std::vector<Node>& newSkolems,
-    bool doTheoryPreprocess)
+    std::vector<Node>& newSkolems)
 {
-  return d_theoryProxy->preprocess(
-      node, newLemmas, newSkolems, doTheoryPreprocess);
+  return d_theoryProxy->preprocess(node, newLemmas, newSkolems);
+}
+
+theory::TrustNode PropEngine::removeItes(
+    TNode node,
+    std::vector<theory::TrustNode>& newLemmas,
+    std::vector<Node>& newSkolems)
+{
+  return d_theoryProxy->removeItes(node, newLemmas, newSkolems);
 }
 
 void PropEngine::notifyPreprocessedAssertions(
@@ -203,13 +209,12 @@ void PropEngine::assertFormula(TNode node) {
 Node PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
 {
   bool removable = isLemmaPropertyRemovable(p);
-  bool preprocess = isLemmaPropertyPreprocess(p);
 
   // call preprocessor
   std::vector<theory::TrustNode> ppLemmas;
   std::vector<Node> ppSkolems;
   theory::TrustNode tplemma =
-      d_theoryProxy->preprocessLemma(tlemma, ppLemmas, ppSkolems, preprocess);
+      d_theoryProxy->preprocessLemma(tlemma, ppLemmas, ppSkolems);
 
   Assert(ppSkolems.size() == ppLemmas.size());
 
@@ -439,8 +444,7 @@ Node PropEngine::getPreprocessedTerm(TNode n)
   // must preprocess
   std::vector<theory::TrustNode> newLemmas;
   std::vector<Node> newSkolems;
-  theory::TrustNode tpn =
-      d_theoryProxy->preprocess(n, newLemmas, newSkolems, true);
+  theory::TrustNode tpn = d_theoryProxy->preprocess(n, newLemmas, newSkolems);
   // send lemmas corresponding to the skolems introduced by preprocessing n
   for (const theory::TrustNode& tnl : newLemmas)
   {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 8086a427e..493dbfe01 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -102,15 +102,28 @@ class PropEngine
    * @param node The assertion to preprocess,
    * @param ppLemmas The lemmas to add to the set of assertions,
    * @param ppSkolems The skolems that newLemmas correspond to,
-   * @param doTheoryPreprocess whether to run theory-specific preprocessing.
    * @return The (REWRITE) trust node corresponding to rewritten node via
    * preprocessing.
    */
   theory::TrustNode preprocess(TNode node,
                                std::vector<theory::TrustNode>& ppLemmas,
-                               std::vector<Node>& ppSkolems,
-                               bool doTheoryPreprocess);
-
+                               std::vector<Node>& ppSkolems);
+  /**
+   * Remove term ITEs (and more generally, term formulas) from the given node.
+   * Return the REWRITE trust node corresponding to rewriting node. New lemmas
+   * and skolems are added to ppLemmas and ppSkolems respectively. This can
+   * be seen a subset of the above preprocess method, which also does theory
+   * preprocessing and rewriting.
+   *
+   * @param node The assertion to preprocess,
+   * @param ppLemmas The lemmas to add to the set of assertions,
+   * @param ppSkolems The skolems that newLemmas correspond to,
+   * @return The (REWRITE) trust node corresponding to rewritten node via
+   * preprocessing.
+   */
+  theory::TrustNode removeItes(TNode node,
+                               std::vector<theory::TrustNode>& ppLemmas,
+                               std::vector<Node>& ppSkolems);
   /**
    * Notify preprocessed assertions. This method is called just before the
    * assertions are asserted to this prop engine. This method notifies the
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 8e54064e1..c604c47f7 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -172,22 +172,26 @@ CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; }
 theory::TrustNode TheoryProxy::preprocessLemma(
     theory::TrustNode trn,
     std::vector<theory::TrustNode>& newLemmas,
-    std::vector<Node>& newSkolems,
-    bool doTheoryPreprocess)
+    std::vector<Node>& newSkolems)
 {
-  return d_tpp.preprocessLemma(
-      trn, newLemmas, newSkolems, doTheoryPreprocess, true);
+  return d_tpp.preprocessLemma(trn, newLemmas, newSkolems);
 }
 
 theory::TrustNode TheoryProxy::preprocess(
     TNode node,
     std::vector<theory::TrustNode>& newLemmas,
-    std::vector<Node>& newSkolems,
-    bool doTheoryPreprocess)
+    std::vector<Node>& newSkolems)
 {
-  theory::TrustNode pnode =
-      d_tpp.preprocess(node, newLemmas, newSkolems, doTheoryPreprocess, true);
-  return pnode;
+  return d_tpp.preprocess(node, newLemmas, newSkolems);
+}
+
+theory::TrustNode TheoryProxy::removeItes(
+    TNode node,
+    std::vector<theory::TrustNode>& newLemmas,
+    std::vector<Node>& newSkolems)
+{
+  RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas();
+  return rtf.run(node, newLemmas, newSkolems, true);
 }
 
 void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); }
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 85cdff00d..57115d660 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -104,16 +104,20 @@ class TheoryProxy : public Registrar
    */
   theory::TrustNode preprocessLemma(theory::TrustNode trn,
                                     std::vector<theory::TrustNode>& newLemmas,
-                                    std::vector<Node>& newSkolems,
-                                    bool doTheoryPreprocess);
+                                    std::vector<Node>& newSkolems);
   /**
    * Call the preprocessor on node, return trust node corresponding to the
    * rewrite.
    */
   theory::TrustNode preprocess(TNode node,
                                std::vector<theory::TrustNode>& newLemmas,
-                               std::vector<Node>& newSkolems,
-                               bool doTheoryPreprocess);
+                               std::vector<Node>& newSkolems);
+  /**
+   * Remove ITEs from the node.
+   */
+  theory::TrustNode removeItes(TNode node,
+                               std::vector<theory::TrustNode>& newLemmas,
+                               std::vector<Node>& newSkolems);
   /** Preregister term */
   void preRegister(Node n) override;
 
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 9a425fc1c..7c01eda0f 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -41,13 +41,6 @@ TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
                       &d_iqtc)
                 : nullptr),
       d_tspg(nullptr),
-      d_tpgRew(pnm ? new TConvProofGenerator(pnm,
-                                             userContext,
-                                             TConvPolicy::FIXPOINT,
-                                             TConvCachePolicy::NEVER,
-                                             "TheoryPreprocessor::rewrite")
-                   : nullptr),
-      d_tspgNoPp(nullptr),
       d_lp(pnm ? new LazyCDProof(pnm,
                                  nullptr,
                                  userContext,
@@ -68,14 +61,6 @@ TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
     ts.push_back(d_tpg.get());
     d_tspg.reset(new TConvSeqProofGenerator(
         pnm, ts, userContext, "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, userContext, "TheoryPreprocessor::sequence_no_pp"));
   }
 }
 
@@ -83,26 +68,27 @@ TheoryPreprocessor::~TheoryPreprocessor() {}
 
 TrustNode TheoryPreprocessor::preprocess(TNode node,
                                          std::vector<TrustNode>& newLemmas,
-                                         std::vector<Node>& newSkolems,
-                                         bool doTheoryPreprocess,
-                                         bool fixedPoint)
+                                         std::vector<Node>& newSkolems)
+{
+  return preprocessInternal(node, newLemmas, newSkolems, true);
+}
+
+TrustNode TheoryPreprocessor::preprocessInternal(
+    TNode node,
+    std::vector<TrustNode>& newLemmas,
+    std::vector<Node>& newSkolems,
+    bool procLemmas)
 {
   // In this method, all rewriting steps of node are stored in d_tpg.
 
   Trace("tpp-debug") << "TheoryPreprocessor::preprocess: start " << node
-                     << ", doTheoryPreprocess=" << doTheoryPreprocess
                      << std::endl;
-  // Run theory preprocessing, maybe
-  Node ppNode = node;
-  if (doTheoryPreprocess)
-  {
-    // run theory preprocessing
-    TrustNode tpp = theoryPreprocess(node);
-    ppNode = tpp.getNode();
-  }
+  // run theory preprocessing
+  TrustNode tpp = theoryPreprocess(node);
+  Node ppNode = tpp.getNode();
 
   // Remove the ITEs, fixed point
-  TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems, fixedPoint);
+  TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems, true);
   Node rtfNode = ttfr.isNull() ? ppNode : ttfr.getNode();
 
   if (Debug.isOn("lemma-ites"))
@@ -141,7 +127,6 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
     Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned no change"
                        << std::endl;
     // no change
-    Assert(newLemmas.empty());
     return TrustNode::null();
   }
 
@@ -151,31 +136,14 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
   {
     std::vector<Node> cterms;
     cterms.push_back(node);
-    if (doTheoryPreprocess)
-    {
-      cterms.push_back(ppNode);
-    }
+    cterms.push_back(ppNode);
     cterms.push_back(rtfNode);
     cterms.push_back(retNode);
     // We have that:
-    // node -> ppNode via preprocessing + rewriting (if doTheoryPreprocess)
+    // node -> ppNode via preprocessing + rewriting
     // 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 = d_tspg->mkTrustRewriteSequence(cterms);
     tret.debugCheckClosed("tpp-debug", "TheoryPreprocessor::lemma_ret");
   }
   else
@@ -220,27 +188,40 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
   }
   Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned "
                      << tret.getNode() << std::endl;
+  if (procLemmas)
+  {
+    // Also must preprocess the new lemmas. This is especially important for
+    // formulas containing witness terms whose bodies are not in preprocessed
+    // form, as term formula removal introduces new lemmas for these that
+    // require theory-preprocessing.
+    size_t i = 0;
+    while (i < newLemmas.size())
+    {
+      TrustNode cur = newLemmas[i];
+      newLemmas[i] = preprocessLemmaInternal(cur, newLemmas, newSkolems, false);
+      i++;
+    }
+  }
   return tret;
 }
 
-TrustNode TheoryPreprocessor::preprocess(TNode node, bool doTheoryPreprocess)
+TrustNode TheoryPreprocessor::preprocessLemma(TrustNode node,
+                                              std::vector<TrustNode>& newLemmas,
+                                              std::vector<Node>& newSkolems)
 {
-  // ignore lemmas, no fixed point
-  std::vector<TrustNode> newLemmas;
-  std::vector<Node> newSkolems;
-  return preprocess(node, newLemmas, newSkolems, doTheoryPreprocess, false);
+  return preprocessLemmaInternal(node, newLemmas, newSkolems, true);
 }
 
-TrustNode TheoryPreprocessor::preprocessLemma(TrustNode node,
-                                              std::vector<TrustNode>& newLemmas,
-                                              std::vector<Node>& newSkolems,
-                                              bool doTheoryPreprocess,
-                                              bool fixedPoint)
+TrustNode TheoryPreprocessor::preprocessLemmaInternal(
+    TrustNode node,
+    std::vector<TrustNode>& newLemmas,
+    std::vector<Node>& newSkolems,
+    bool procLemmas)
 {
   // what was originally proven
   Node lemma = node.getProven();
   TrustNode tplemma =
-      preprocess(lemma, newLemmas, newSkolems, doTheoryPreprocess, fixedPoint);
+      preprocessInternal(lemma, newLemmas, newSkolems, procLemmas);
   if (tplemma.isNull())
   {
     // no change needed
@@ -277,16 +258,6 @@ TrustNode TheoryPreprocessor::preprocessLemma(TrustNode node,
   return TrustNode::mkTrustLemma(lemmap, d_lp.get());
 }
 
-TrustNode TheoryPreprocessor::preprocessLemma(TrustNode node,
-                                              bool doTheoryPreprocess)
-{
-  // ignore lemmas, no fixed point
-  std::vector<TrustNode> newLemmas;
-  std::vector<Node> newSkolems;
-  return preprocessLemma(
-      node, newLemmas, newSkolems, doTheoryPreprocess, false);
-}
-
 RemoveTermFormulas& TheoryPreprocessor::getRemoveTermFormulas()
 {
   return d_tfr;
@@ -365,10 +336,8 @@ TrustNode TheoryPreprocessor::theoryPreprocess(TNode assertion)
       }
       // Mark the substitution and continue
       Node result = builder;
-      if (result != current)
-      {
-        result = rewriteWithProof(result);
-      }
+      // always rewrite here, since current may not be in rewritten form
+      result = rewriteWithProof(result);
       Trace("theory::preprocess-debug")
           << "TheoryPreprocessor::theoryPreprocess(" << assertion
           << "): setting " << current << " -> " << result << endl;
diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h
index d7c22270d..6a1f6b3ef 100644
--- a/src/theory/theory_preprocessor.h
+++ b/src/theory/theory_preprocessor.h
@@ -56,26 +56,17 @@ class TheoryPreprocessor
    * additional lemmas in newLemmas, which are trust nodes of kind
    * TrustNodeKind::LEMMA. These correspond to e.g. lemmas corresponding to ITE
    * removal. For each lemma in newLemmas, we add the corresponding skolem that
-   * the lemma defines. The flag doTheoryPreprocess is whether we should run
-   * theory-specific preprocessing.
+   * the lemma defines.
    *
    * @param node The assertion to preprocess,
    * @param newLemmas The lemmas to add to the set of assertions,
    * @param newSkolems The skolems that newLemmas correspond to,
-   * @param doTheoryPreprocess whether to run theory-specific preprocessing.
    * @return The (REWRITE) trust node corresponding to rewritten node via
    * preprocessing.
    */
   TrustNode preprocess(TNode node,
                        std::vector<TrustNode>& newLemmas,
-                       std::vector<Node>& newSkolems,
-                       bool doTheoryPreprocess,
-                       bool fixedPoint);
-  /**
-   * Same as above, without lemma tracking or fixed point. Lemmas for skolems
-   * can be extracted from the RemoveTermFormulas utility.
-   */
-  TrustNode preprocess(TNode node, bool doTheoryPreprocess);
+                       std::vector<Node>& newSkolems);
   /**
    * Same as above, but transforms the proof of node into a proof of the
    * preprocessed node and returns the LEMMA trust node.
@@ -83,20 +74,12 @@ class TheoryPreprocessor
    * @param node The assertion to preprocess,
    * @param newLemmas The lemmas to add to the set of assertions,
    * @param newSkolems The skolems that newLemmas correspond to,
-   * @param doTheoryPreprocess whether to run theory-specific preprocessing.
    * @return The (LEMMA) trust node corresponding to the proof of the rewritten
    * form of the proven field of node.
    */
   TrustNode preprocessLemma(TrustNode node,
                             std::vector<TrustNode>& newLemmas,
-                            std::vector<Node>& newSkolems,
-                            bool doTheoryPreprocess,
-                            bool fixedPoint);
-  /**
-   * Same as above, without lemma tracking or fixed point. Lemmas for skolems
-   * can be extracted from the RemoveTermFormulas utility.
-   */
-  TrustNode preprocessLemma(TrustNode node, bool doTheoryPreprocess);
+                            std::vector<Node>& newSkolems);
 
   /** Get the term formula removal utility */
   RemoveTermFormulas& getRemoveTermFormulas();
@@ -107,6 +90,24 @@ class TheoryPreprocessor
    * parts of the node.
    */
   TrustNode theoryPreprocess(TNode node);
+  /**
+   * Internal helper for preprocess, which also optionally preprocesses the
+   * new lemmas generated until a fixed point is reached based on argument
+   * procLemmas.
+   */
+  TrustNode preprocessInternal(TNode node,
+                               std::vector<TrustNode>& newLemmas,
+                               std::vector<Node>& newSkolems,
+                               bool procLemmas);
+  /**
+   * Internal helper for preprocessLemma, which also optionally preprocesses the
+   * new lemmas generated until a fixed point is reached based on argument
+   * procLemmas.
+   */
+  TrustNode preprocessLemmaInternal(TrustNode node,
+                                    std::vector<TrustNode>& newLemmas,
+                                    std::vector<Node>& newSkolems,
+                                    bool procLemmas);
   /** Reference to owning theory engine */
   TheoryEngine& d_engine;
   /** Logic info of theory engine */
@@ -134,12 +135,6 @@ class TheoryPreprocessor
    * 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 */
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a3eaeee57..94be987f7 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1816,6 +1816,7 @@ set(regress_1_tests
   regress1/quantifiers/smtlibf957ea.smt2
   regress1/quantifiers/sygus-infer-nested.smt2
   regress1/quantifiers/symmetric_unsat_7.smt2
+  regress1/quantifiers/tpp-unit-fail-qbv.smt2
   regress1/quantifiers/var-eq-trigger.smt2
   regress1/quantifiers/var-eq-trigger-simple.smt2
   regress1/quantifiers/z3.620661-no-fv-trigger.smt2
diff --git a/test/regress/regress1/quantifiers/tpp-unit-fail-qbv.smt2 b/test/regress/regress1/quantifiers/tpp-unit-fail-qbv.smt2
new file mode 100644
index 000000000..2ef929551
--- /dev/null
+++ b/test/regress/regress1/quantifiers/tpp-unit-fail-qbv.smt2
@@ -0,0 +1,8 @@
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun t () (_ BitVec 4))
+(declare-fun s () (_ BitVec 4))
+(assert
+(distinct (bvult t (bvnot (bvneg s))) (exists ((BOUND_VARIABLE_273 (_ BitVec 4))) (bvugt (bvurem BOUND_VARIABLE_273 s) t)))
+)
+(check-sat)