Implement --no-strings-lazy-pp as a preprocessing pass (#5777)

This option eliminates extended functions in strings eagerly. This was incorrectly done at ppRewrite previously, which should not add lemmas. Instead, this makes this technique into a preprocessing pass. To do this, the interface for the strings preprocessor was cleaned to have fewer dependencies, and made to track a cache internally.

Fixes #5608, fixes #5745, fixes #5767, fixes #5771, fixes #5406.

16 files changed, 187 insertions, 90 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 6f5647e9a..dd944f929 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -68,6 +68,8 @@ libcvc4_add_sources(
   preprocessing/passes/bv_to_int.h
   preprocessing/passes/extended_rewriter_pass.cpp
   preprocessing/passes/extended_rewriter_pass.h
+  preprocessing/passes/foreign_theory_rewrite.cpp
+  preprocessing/passes/foreign_theory_rewrite.h
   preprocessing/passes/fun_def_fmf.cpp
   preprocessing/passes/fun_def_fmf.h
   preprocessing/passes/global_negate.cpp
@@ -102,8 +104,8 @@ libcvc4_add_sources(
   preprocessing/passes/sort_infer.h
   preprocessing/passes/static_learning.cpp
   preprocessing/passes/static_learning.h
-  preprocessing/passes/foreign_theory_rewrite.cpp
-  preprocessing/passes/foreign_theory_rewrite.h
+  preprocessing/passes/strings_eager_pp.cpp
+  preprocessing/passes/strings_eager_pp.h
   preprocessing/passes/sygus_inference.cpp
   preprocessing/passes/sygus_inference.h
   preprocessing/passes/synth_rew_rules.cpp
diff --git a/src/preprocessing/passes/rewrite.cpp b/src/preprocessing/passes/rewrite.cpp
index b4a353862..b8c9498e1 100644
--- a/src/preprocessing/passes/rewrite.cpp
+++ b/src/preprocessing/passes/rewrite.cpp
@@ -31,7 +31,7 @@ Rewrite::Rewrite(PreprocessingPassContext* preprocContext)
 
 PreprocessingPassResult Rewrite::applyInternal(
   AssertionPipeline* assertionsToPreprocess)
-{	
+{
   for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) {
     assertionsToPreprocess->replace(i, Rewriter::rewrite((*assertionsToPreprocess)[i]));
   }
diff --git a/src/preprocessing/passes/strings_eager_pp.cpp b/src/preprocessing/passes/strings_eager_pp.cpp
new file mode 100644
index 000000000..69cb8914c
--- /dev/null
+++ b/src/preprocessing/passes/strings_eager_pp.cpp
@@ -0,0 +1,59 @@
+/*********************                                                        */
+/*! \file strings_eager_pp.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The strings eager preprocess utility
+ **/
+
+#include "preprocessing/passes/strings_eager_pp.h"
+
+#include "theory/strings/theory_strings_preprocess.h"
+#include "theory/rewriter.h"
+
+using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+StringsEagerPp::StringsEagerPp(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "strings-eager-pp"){};
+
+PreprocessingPassResult StringsEagerPp::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  theory::strings::SkolemCache skc(false);
+  theory::strings::StringsPreprocess pp(&skc);
+  for (size_t i = 0, nasserts = assertionsToPreprocess->size(); i < nasserts;
+       ++i)
+  {
+    Node prev = (*assertionsToPreprocess)[i];
+    std::vector<Node> asserts;
+    Node rew = pp.processAssertion(prev, asserts);
+    if (!asserts.empty())
+    {
+      std::vector<Node> conj;
+      conj.push_back(rew);
+      conj.insert(conj.end(), asserts.begin(), asserts.end());
+      rew = nm->mkAnd(conj);
+    }
+    if (prev != rew)
+    {
+      assertionsToPreprocess->replace(i, theory::Rewriter::rewrite(rew));
+    }
+  }
+
+  return PreprocessingPassResult::NO_CONFLICT;
+}
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/passes/strings_eager_pp.h b/src/preprocessing/passes/strings_eager_pp.h
new file mode 100644
index 000000000..299260c61
--- /dev/null
+++ b/src/preprocessing/passes/strings_eager_pp.h
@@ -0,0 +1,45 @@
+/*********************                                                        */
+/*! \file strings_eager_pp.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The strings eager preprocess utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H
+#define CVC4__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+/**
+ * Eliminate all extended string functions in the input problem using
+ * reductions to bounded string quantifiers.
+ */
+class StringsEagerPp : public PreprocessingPass
+{
+ public:
+  StringsEagerPp(PreprocessingPassContext* preprocContext);
+
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* CVC4__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H */
diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp
index da09f6363..f14b8b4a7 100644
--- a/src/preprocessing/preprocessing_pass_registry.cpp
+++ b/src/preprocessing/preprocessing_pass_registry.cpp
@@ -33,6 +33,7 @@
 #include "preprocessing/passes/bv_to_bool.h"
 #include "preprocessing/passes/bv_to_int.h"
 #include "preprocessing/passes/extended_rewriter_pass.h"
+#include "preprocessing/passes/foreign_theory_rewrite.h"
 #include "preprocessing/passes/fun_def_fmf.h"
 #include "preprocessing/passes/global_negate.h"
 #include "preprocessing/passes/ho_elim.h"
@@ -50,7 +51,7 @@
 #include "preprocessing/passes/sep_skolem_emp.h"
 #include "preprocessing/passes/sort_infer.h"
 #include "preprocessing/passes/static_learning.h"
-#include "preprocessing/passes/foreign_theory_rewrite.h"
+#include "preprocessing/passes/strings_eager_pp.h"
 #include "preprocessing/passes/sygus_inference.h"
 #include "preprocessing/passes/synth_rew_rules.h"
 #include "preprocessing/passes/theory_preprocess.h"
@@ -153,6 +154,7 @@ PreprocessingPassRegistry::PreprocessingPassRegistry()
   registerPassInfo("ho-elim", callCtor<HoElim>);
   registerPassInfo("fun-def-fmf", callCtor<FunDefFmf>);
   registerPassInfo("theory-rewrite-eq", callCtor<TheoryRewriteEq>);
+  registerPassInfo("strings-eager-pp", callCtor<StringsEagerPp>);
 }
 
 }  // namespace preprocessing
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 6d6c81e3c..0c01abbbb 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -24,6 +24,7 @@
 #include "options/quantifiers_options.h"
 #include "options/sep_options.h"
 #include "options/smt_options.h"
+#include "options/strings_options.h"
 #include "options/uf_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_registry.h"
@@ -243,7 +244,10 @@ bool ProcessAssertions::apply(Assertions& as)
       d_passes["fun-def-fmf"]->apply(&assertions);
     }
   }
-
+  if (!options::stringLazyPreproc())
+  {
+    d_passes["strings-eager-pp"]->apply(&assertions);
+  }
   if (options::sortInference() || options::ufssFairnessMonotone())
   {
     d_passes["sort-inference"]->apply(&assertions);
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 7e416d132..352da5ac8 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -43,7 +43,7 @@ ExtfSolver::ExtfSolver(SolverState& s,
       d_csolver(cs),
       d_extt(et),
       d_statistics(statistics),
-      d_preproc(d_termReg.getSkolemCache(), s.getUserContext(), statistics),
+      d_preproc(d_termReg.getSkolemCache(), &statistics.d_reductions),
       d_hasExtf(s.getSatContext(), false),
       d_extfInferCache(s.getSatContext()),
       d_reduced(s.getUserContext())
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 3189b297a..eec59685a 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1032,31 +1032,6 @@ TrustNode TheoryStrings::ppRewrite(TNode atom)
       atomRet = ret.getNode();
     }
   }
-  if( !options::stringLazyPreproc() ){
-    //eager preprocess here
-    std::vector< Node > new_nodes;
-    StringsPreprocess* p = d_esolver.getPreprocess();
-    Node pret = p->processAssertion(atomRet, new_nodes);
-    if (pret != atomRet)
-    {
-      Trace("strings-ppr") << "  rewrote " << atomRet << " -> " << pret
-                           << ", with " << new_nodes.size() << " lemmas."
-                           << std::endl;
-      for (const Node& lem : new_nodes)
-      {
-        Trace("strings-ppr") << "    lemma : " << lem << std::endl;
-        ++(d_statistics.d_lemmasEagerPreproc);
-        d_out->lemma(lem);
-      }
-      atomRet = pret;
-      // Don't support proofs yet, thus we must return nullptr. This is the
-      // case even if we had proven the elimination via regexp elimination
-      // above.
-      ret = TrustNode::mkTrustRewrite(atom, atomRet, nullptr);
-    }else{
-      Assert(new_nodes.empty());
-    }
-  }
   return ret;
 }
 
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 1a46b26f5..f0afe5f26 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -41,9 +41,8 @@ struct QInternalVarAttributeId
 typedef expr::Attribute<QInternalVarAttributeId, Node> QInternalVarAttribute;
 
 StringsPreprocess::StringsPreprocess(SkolemCache* sc,
-                                     context::UserContext* u,
-                                     SequencesStatistics& stats)
-    : d_sc(sc), d_statistics(stats)
+                                     HistogramStat<Kind>* statReductions)
+    : d_sc(sc), d_statReductions(statReductions)
 {
 }
 
@@ -938,7 +937,10 @@ Node StringsPreprocess::simplify(Node t, std::vector<Node>& asserts)
         Trace("strings-preprocess") << "   " << asserts[i] << std::endl;
       }
     }
-    d_statistics.d_reductions << t.getKind();
+    if (d_statReductions != nullptr)
+    {
+      (*d_statReductions) << t.getKind();
+    }
   }
   else
   {
@@ -948,12 +950,11 @@ Node StringsPreprocess::simplify(Node t, std::vector<Node>& asserts)
   return retNode;
 }
 
-Node StringsPreprocess::simplifyRec(Node t,
-                                    std::vector<Node>& asserts,
-                                    std::map<Node, Node>& visited)
+Node StringsPreprocess::simplifyRec(Node t, std::vector<Node>& asserts)
 {
-  std::map< Node, Node >::iterator it = visited.find(t);
-  if( it!=visited.end() ){
+  std::map<Node, Node>::iterator it = d_visited.find(t);
+  if (it != d_visited.end())
+  {
     return it->second;
   }else{
     Node retNode = t;
@@ -968,7 +969,7 @@ Node StringsPreprocess::simplifyRec(Node t,
         cc.push_back( t.getOperator() );
       }
       for(unsigned i=0; i<t.getNumChildren(); i++) {
-        Node s = simplifyRec(t[i], asserts, visited);
+        Node s = simplifyRec(t[i], asserts);
         cc.push_back( s );
         if( s!=t[i] ) {
           changed = true;
@@ -980,22 +981,21 @@ Node StringsPreprocess::simplifyRec(Node t,
       }
       retNode = simplify(tmp, asserts);
     }
-    visited[t] = retNode;
+    d_visited[t] = retNode;
     return retNode;
   }
 }
 
 Node StringsPreprocess::processAssertion(Node n, std::vector<Node>& asserts)
 {
-  std::map< Node, Node > visited;
   std::vector<Node> asserts_curr;
-  Node ret = simplifyRec(n, asserts_curr, visited);
+  Node ret = simplifyRec(n, asserts_curr);
   while (!asserts_curr.empty())
   {
     Node curr = asserts_curr.back();
     asserts_curr.pop_back();
     std::vector<Node> asserts_tmp;
-    curr = simplifyRec(curr, asserts_tmp, visited);
+    curr = simplifyRec(curr, asserts_tmp);
     asserts_curr.insert(
         asserts_curr.end(), asserts_tmp.begin(), asserts_tmp.end());
     asserts.push_back(curr);
@@ -1003,38 +1003,6 @@ Node StringsPreprocess::processAssertion(Node n, std::vector<Node>& asserts)
   return ret;
 }
 
-void StringsPreprocess::processAssertions( std::vector< Node > &vec_node ){
-  std::map< Node, Node > visited;
-  for( unsigned i=0; i<vec_node.size(); i++ ){
-    Trace("strings-preprocess-debug") << "Preprocessing assertion " << vec_node[i] << std::endl;
-    //preprocess until fixed point
-    std::vector<Node> asserts;
-    std::vector<Node> asserts_curr;
-    asserts_curr.push_back(vec_node[i]);
-    while (!asserts_curr.empty())
-    {
-      Node curr = asserts_curr.back();
-      asserts_curr.pop_back();
-      std::vector<Node> asserts_tmp;
-      curr = simplifyRec(curr, asserts_tmp, visited);
-      asserts_curr.insert(
-          asserts_curr.end(), asserts_tmp.begin(), asserts_tmp.end());
-      asserts.push_back(curr);
-    }
-    Node res = asserts.size() == 1
-                   ? asserts[0]
-                   : NodeManager::currentNM()->mkNode(kind::AND, asserts);
-    if( res!=vec_node[i] ){
-      res = Rewriter::rewrite( res );
-      if (options::unsatCores() && !options::proofNew())
-      {
-        ProofManager::currentPM()->addDependence(res, vec_node[i]);
-      }
-      vec_node[i] = res;
-    }
-  }
-}
-
 Node StringsPreprocess::mkForallInternal(Node bvl, Node body)
 {
   NodeManager* nm = NodeManager::currentNM();
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 124a09a4c..b156a5f5e 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -41,8 +41,7 @@ namespace strings {
 class StringsPreprocess {
  public:
   StringsPreprocess(SkolemCache* sc,
-                    context::UserContext* u,
-                    SequencesStatistics& stats);
+                    HistogramStat<Kind>* statReductions = nullptr);
   ~StringsPreprocess();
   /** The reduce routine
    *
@@ -79,27 +78,20 @@ class StringsPreprocess {
    * asserts.
    */
   Node processAssertion(Node t, std::vector<Node>& asserts);
-  /**
-   * Replaces all formulas t in vec_node with an equivalent formula t' that
-   * contains no free instances of extended functions (that is, extended
-   * functions may only appear beneath quantifiers). This applies simplifyRec
-   * on each assertion in vec_node until a fixed point is reached.
-   */
-  void processAssertions(std::vector<Node>& vec_node);
 
  private:
   /** pointer to the skolem cache used by this class */
   SkolemCache* d_sc;
   /** Reference to the statistics for the theory of strings/sequences. */
-  SequencesStatistics& d_statistics;
+  HistogramStat<Kind>* d_statReductions;
+  /** visited cache */
+  std::map<Node, Node> d_visited;
   /**
    * Applies simplify to all top-level extended function subterms of t. New
    * assertions created in this reduction are added to asserts. The argument
    * visited stores a cache of previous results.
    */
-  Node simplifyRec(Node t,
-                   std::vector<Node>& asserts,
-                   std::map<Node, Node>& visited);
+  Node simplifyRec(Node t, std::vector<Node>& asserts);
   /**
    * Make internal quantified formula with bound variable list bvl and body.
    * Internally, we get a node corresponding to marking a quantified formula as
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a2e070daf..e2af099d7 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1101,6 +1101,10 @@ set(regress_0_tests
   regress0/strings/issue5384-double-conflict.smt2
   regress0/strings/issue5428-re-diff-assoc.smt2
   regress0/strings/issue5542-strings-seq-mix.smt2
+  regress0/strings/issue5608-eager-pp.smt2
+  regress0/strings/issue5745-eager-pp.smt2
+  regress0/strings/issue5767-eager-pp.smt2
+  regress0/strings/issue5771-eager-pp.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/large-model.smt2
   regress0/strings/leadingzero001.smt2
@@ -1988,6 +1992,7 @@ set(regress_1_tests
   regress1/strings/issue5330.smt2
   regress1/strings/issue5330_2.smt2
   regress1/strings/issue5374-proxy-i.smt2
+  regress1/strings/issue5406-eager-pp.smt2
   regress1/strings/issue5483-pp-leq.smt2
   regress1/strings/issue5510-re-consume.smt2
   regress1/strings/issue5520-re-consume.smt2
diff --git a/test/regress/regress0/strings/issue5608-eager-pp.smt2 b/test/regress/regress0/strings/issue5608-eager-pp.smt2
new file mode 100644
index 000000000..a1a166277
--- /dev/null
+++ b/test/regress/regress0/strings/issue5608-eager-pp.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --no-strings-lazy-pp -i
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: unsat
+(set-logic QF_SLIA)
+(declare-fun v6 () Bool)
+(declare-fun str6 () String)
+(assert (and v6 (str.in_re (str.replace str6 (str.from_int 12) str6) (str.to_re str6))))
+(check-sat)
+(check-sat)
+(assert (not v6))
+(check-sat)
diff --git a/test/regress/regress0/strings/issue5745-eager-pp.smt2 b/test/regress/regress0/strings/issue5745-eager-pp.smt2
new file mode 100644
index 000000000..b869a9ded
--- /dev/null
+++ b/test/regress/regress0/strings/issue5745-eager-pp.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --no-strings-lazy-pp
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun i0 () Int)
+(declare-fun str4 () String)
+(assert (= str4 (str.substr str4 (mod i0 2) 1)))
+(assert (not (= "" str4)))
+(check-sat)
diff --git a/test/regress/regress0/strings/issue5767-eager-pp.smt2 b/test/regress/regress0/strings/issue5767-eager-pp.smt2
new file mode 100644
index 000000000..5e4d29d5a
--- /dev/null
+++ b/test/regress/regress0/strings/issue5767-eager-pp.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --no-strings-lazy-pp -q
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun s () String)
+(assert (xor (= (str.at s (div 0 0)) "A") (= (div 0 (str.len s)) 0)))
+(check-sat)
diff --git a/test/regress/regress0/strings/issue5771-eager-pp.smt2 b/test/regress/regress0/strings/issue5771-eager-pp.smt2
new file mode 100644
index 000000000..c3049e72f
--- /dev/null
+++ b/test/regress/regress0/strings/issue5771-eager-pp.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --no-strings-lazy-pp
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () Int)
+(assert (str.suffixof "B" (str.from_code a)))
+(check-sat)
diff --git a/test/regress/regress1/strings/issue5406-eager-pp.smt2 b/test/regress/regress1/strings/issue5406-eager-pp.smt2
new file mode 100644
index 000000000..9ea7310fe
--- /dev/null
+++ b/test/regress/regress1/strings/issue5406-eager-pp.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --no-strings-lazy-pp -i
+; EXPECT: unsat
+(set-logic QF_S)
+(declare-fun _substvar_18_ () String)
+(set-option :strings-lazy-pp false)
+(declare-fun str2 () String)
+(declare-fun str3 () String)
+(declare-fun str9 () String)
+(declare-fun str10 () String)
+(assert (not (str.prefixof str3 str9)))
+(push 1)
+(assert (= str3 str2 str10 str9 _substvar_18_))
+(check-sat)