4 files changed, 108 insertions, 2 deletions
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