Simplify preprocessing (#5647)

This simplifies preprocessing so that the only call to theory-preprocess and ite-removal is at the very end. (One exception is early-theory-pp which is used by default in combination with ite-simp to maintain the performance on QF_LIA/nec).

This is in preparation for making theory preprocessing happen lazily, post-CNF conversion.

@HanielB has done SMT-LIB performance runs, see below.

6 files changed, 31 insertions, 182 deletions

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 08d53855c..b01b7780f 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -362,6 +362,14 @@ header = "options/smt_options.h"
   help       = "enables compressing ites after ite simplification"
 
 [[option]]
+  name       = "earlyIteRemoval"
+  category   = "experimental"
+  long       = "early-ite-removal"
+  type       = "bool"
+  default    = "false"
+  help       = "remove ITEs early in preprocessing"
+
+[[option]]
   name       = "unconstrainedSimp"
   category   = "regular"
   long       = "unconstrained-simp"
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 51434e369..6ebf1b8c8 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -358,6 +358,8 @@ void UnconstrainedSimplifier::processUnconstrained()
         case kind::BITVECTOR_SHL:
         case kind::BITVECTOR_LSHR:
         case kind::BITVECTOR_ASHR:
+        case kind::BITVECTOR_UDIV:
+        case kind::BITVECTOR_UREM:
         case kind::BITVECTOR_UDIV_TOTAL:
         case kind::BITVECTOR_UREM_TOTAL:
         case kind::BITVECTOR_SDIV:
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index c2374c6ff..77c7d450e 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -203,10 +203,6 @@ bool ProcessAssertions::apply(Assertions& as)
   if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF)
   {
     d_passes["bv-to-int"]->apply(&assertions);
-    // after running bv-to-int, we need to immediately run
-    // theory-preprocess and ite-removal so that newlly created
-    // terms and assertions are normalized (e.g., div is expanded).
-    d_passes["theory-preprocess"]->apply(&assertions);
   }
 
   // Since this pass is not robust for the information tracking necessary for
@@ -290,6 +286,7 @@ bool ProcessAssertions::apply(Assertions& as)
   }
   Debug("smt") << " assertions     : " << assertions.size() << endl;
 
+  if (options::earlyIteRemoval())
   {
     d_smtStats.d_numAssertionsPre += assertions.size();
     d_passes["ite-removal"]->apply(&assertions);
@@ -309,84 +306,6 @@ bool ProcessAssertions::apply(Assertions& as)
     Chat() << "re-simplifying assertions..." << endl;
     ScopeCounter depth(d_simplifyAssertionsDepth);
     noConflict &= simplifyAssertions(assertions);
-    if (noConflict)
-    {
-      // Need to fix up assertion list to maintain invariants:
-      // Let Sk be the set of Skolem variables introduced by ITE's.  Let <_sk be
-      // the order in which these variables were introduced during ite removal.
-      // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr
-      // mapped to by sk.
-
-      // cache for expression traversal
-      unordered_map<Node, bool, NodeHashFunction> cache;
-
-      IteSkolemMap& iskMap = assertions.getIteSkolemMap();
-      // First, find all skolems that appear in the substitution map - their
-      // associated iteExpr will need to be moved to the main assertion set
-      set<TNode> skolemSet;
-      SubstitutionMap& top_level_substs =
-          d_preprocessingPassContext->getTopLevelSubstitutions().get();
-      SubstitutionMap::iterator pos = top_level_substs.begin();
-      for (; pos != top_level_substs.end(); ++pos)
-      {
-        collectSkolems(iskMap, (*pos).first, skolemSet, cache);
-        collectSkolems(iskMap, (*pos).second, skolemSet, cache);
-      }
-      // We need to ensure:
-      // 1. iteExpr has the form (ite cond (sk = t) (sk = e))
-      // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk
-      // If either of these is violated, we must add iteExpr as a proper
-      // assertion
-      IteSkolemMap::iterator it = iskMap.begin();
-      IteSkolemMap::iterator iend = iskMap.end();
-      std::vector<Node> newConj;
-      vector<TNode> toErase;
-      for (; it != iend; ++it)
-      {
-        if (skolemSet.find((*it).first) == skolemSet.end())
-        {
-          TNode iteExpr = assertions[(*it).second];
-          if (iteExpr.getKind() == ITE && iteExpr[1].getKind() == EQUAL
-              && iteExpr[1][0] == (*it).first && iteExpr[2].getKind() == EQUAL
-              && iteExpr[2][0] == (*it).first)
-          {
-            cache.clear();
-            bool bad =
-                checkForBadSkolems(iskMap, iteExpr[0], (*it).first, cache);
-            bad = bad
-                  || checkForBadSkolems(
-                         iskMap, iteExpr[1][1], (*it).first, cache);
-            bad = bad
-                  || checkForBadSkolems(
-                         iskMap, iteExpr[2][1], (*it).first, cache);
-            if (!bad)
-            {
-              continue;
-            }
-          }
-        }
-        // Move this iteExpr into the main assertions
-        newConj.push_back(assertions[(*it).second]);
-        assertions.replace((*it).second, d_true);
-        toErase.push_back((*it).first);
-      }
-      if (!newConj.empty())
-      {
-        while (!toErase.empty())
-        {
-          iskMap.erase(toErase.back());
-          toErase.pop_back();
-        }
-        size_t index = assertions.getRealAssertionsEnd() - 1;
-        Node newAssertion = NodeManager::currentNM()->mkAnd(newConj);
-        assertions.conjoin(index, newAssertion);
-      }
-      // TODO(b/1256): For some reason this is needed for some benchmarks, such
-      // as
-      // QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
-      d_passes["ite-removal"]->apply(&assertions);
-      d_passes["apply-substs"]->apply(&assertions);
-    }
     Trace("smt-proc")
         << "ProcessAssertions::processAssertions() : post-repeat-simplify"
         << endl;
@@ -407,12 +326,19 @@ bool ProcessAssertions::apply(Assertions& as)
                << endl;
   Debug("smt") << " assertions     : " << assertions.size() << endl;
 
+  // ensure rewritten
+  d_passes["rewrite"]->apply(&assertions);
+  // apply theory preprocess
   d_passes["theory-preprocess"]->apply(&assertions);
   // Must remove ITEs again since theory preprocessing may introduce them.
   // Notice that we alternatively could ensure that the theory-preprocess
   // pass above calls TheoryPreprocess::preprocess instead of
   // TheoryPreprocess::theoryPreprocess, as the former also does ITE removal.
   d_passes["ite-removal"]->apply(&assertions);
+  // This is needed because when solving incrementally, removeITEs may
+  // introduce skolems that were solved for earlier and thus appear in the
+  // substitution map.
+  d_passes["apply-substs"]->apply(&assertions);
 
   if (options::bitblastMode() == options::BitblastMode::EAGER)
   {
@@ -470,13 +396,6 @@ bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions)
 
     Debug("smt") << " assertions     : " << assertions.size() << endl;
 
-    // Theory preprocessing
-    bool doEarlyTheoryPp = !options::arithRewriteEq();
-    if (doEarlyTheoryPp)
-    {
-      d_passes["theory-preprocess"]->apply(&assertions);
-    }
-
     // ITE simplification
     if (options::doITESimp()
         && (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat()))
@@ -542,80 +461,5 @@ void ProcessAssertions::dumpAssertions(const char* key,
   }
 }
 
-void ProcessAssertions::collectSkolems(
-    IteSkolemMap& iskMap,
-    TNode n,
-    set<TNode>& skolemSet,
-    unordered_map<Node, bool, NodeHashFunction>& cache)
-{
-  unordered_map<Node, bool, NodeHashFunction>::iterator it;
-  it = cache.find(n);
-  if (it != cache.end())
-  {
-    return;
-  }
-
-  size_t sz = n.getNumChildren();
-  if (sz == 0)
-  {
-    if (iskMap.find(n) != iskMap.end())
-    {
-      skolemSet.insert(n);
-    }
-    cache[n] = true;
-    return;
-  }
-
-  size_t k = 0;
-  for (; k < sz; ++k)
-  {
-    collectSkolems(iskMap, n[k], skolemSet, cache);
-  }
-  cache[n] = true;
-}
-
-bool ProcessAssertions::checkForBadSkolems(
-    IteSkolemMap& iskMap,
-    TNode n,
-    TNode skolem,
-    unordered_map<Node, bool, NodeHashFunction>& cache)
-{
-  unordered_map<Node, bool, NodeHashFunction>::iterator it;
-  it = cache.find(n);
-  if (it != cache.end())
-  {
-    return (*it).second;
-  }
-
-  size_t sz = n.getNumChildren();
-  if (sz == 0)
-  {
-    IteSkolemMap::iterator iit = iskMap.find(n);
-    bool bad = false;
-    if (iit != iskMap.end())
-    {
-      if (!((*iit).first < n))
-      {
-        bad = true;
-      }
-    }
-    cache[n] = bad;
-    return bad;
-  }
-
-  size_t k = 0;
-  for (; k < sz; ++k)
-  {
-    if (checkForBadSkolems(iskMap, n[k], skolem, cache))
-    {
-      cache[n] = true;
-      return true;
-    }
-  }
-
-  cache[n] = false;
-  return false;
-}
-
 }  // namespace smt
 }  // namespace CVC4
diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h
index 072603e7d..ca834459d 100644
--- a/src/smt/process_assertions.h
+++ b/src/smt/process_assertions.h
@@ -118,22 +118,6 @@ class ProcessAssertions
    */
   void dumpAssertions(const char* key,
                       const preprocessing::AssertionPipeline& assertionList);
-  /**
-   * Helper function to fix up assertion list to restore invariants needed after
-   * ite removal.
-   */
-  void collectSkolems(IteSkolemMap& iskMap,
-                      TNode n,
-                      set<TNode>& skolemSet,
-                      NodeToBoolHashMap& cache);
-  /**
-   * Helper function to fix up assertion list to restore invariants needed after
-   * ite removal.
-   */
-  bool checkForBadSkolems(IteSkolemMap& iskMap,
-                          TNode n,
-                          TNode skolem,
-                          NodeToBoolHashMap& cache);
 };
 
 }  // namespace smt
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index c8aecf288..bbbe73cb1 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -210,6 +210,18 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
   }
 
+  // --ite-simp is an experimental option designed for QF_LIA/nec. This
+  // technique is experimental. This benchmark set also requires removing ITEs
+  // during preprocessing, before repeating simplification. Hence, we enable
+  // this by default.
+  if (options::doITESimp())
+  {
+    if (!options::earlyIteRemoval.wasSetByUser())
+    {
+      options::earlyIteRemoval.set(true);
+    }
+  }
+
   // Set default options associated with strings-exp. We also set these options
   // if we are using eager string preprocessing, which may introduce quantified
   // formulas at preprocess time.
diff --git a/test/regress/regress0/unconstrained/4481.smt2 b/test/regress/regress0/unconstrained/4481.smt2
index 19179f4d7..028607093 100644
--- a/test/regress/regress0/unconstrained/4481.smt2
+++ b/test/regress/regress0/unconstrained/4481.smt2
@@ -1,6 +1,5 @@
 ; COMMAND-LINE: --unconstrained-simp
-; EXPECT: (error "Cannot use unconstrained simplification in this logic, due to (possibly internally introduced) quantified formula.")
-; EXIT: 1
+; EXPECT: unsat
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun a () Int)