Move rewrite to pass (#2128)

diff --git a/src/Makefile.am b/src/Makefile.am
index 71a66db599da367daef613ac68abfd095335c99a..d0621bf5bda8e766c12981395b92a3d0605e4f78 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -84,6 +84,8 @@ libcvc4_la_SOURCES = \
        preprocessing/passes/bv_to_bool.h \
        preprocessing/passes/real_to_int.cpp \
        preprocessing/passes/real_to_int.h \
+       preprocessing/passes/rewrite.cpp \
+       preprocessing/passes/rewrite.h \
        preprocessing/passes/static_learning.cpp \
        preprocessing/passes/static_learning.h \
        preprocessing/passes/symmetry_breaker.cpp \

diff --git a/src/preprocessing/passes/rewrite.cpp b/src/preprocessing/passes/rewrite.cpp
new file mode 100644 (file)
index 0000000..dff807d
--- /dev/null
+++ b/src/preprocessing/passes/rewrite.cpp
@@ -0,0 +1,44 @@
+/*********************                                                        */
+/*! \file rewrite.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Caleb Donovick
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 rewrite preprocessing pass
+ **
+ ** Calls the rewriter on every assertion
+ **/
+
+#include "preprocessing/passes/rewrite.h"
+
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using namespace CVC4::theory;
+
+
+Rewrite::Rewrite(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "rewrite"){};
+
+
+PreprocessingPassResult Rewrite::applyInternal(
+  AssertionPipeline* assertionsToPreprocess)
+{      
+  for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) {
+    assertionsToPreprocess->replace(i, Rewriter::rewrite((*assertionsToPreprocess)[i]));
+  }
+
+  return PreprocessingPassResult::NO_CONFLICT;
+}
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4

diff --git a/src/preprocessing/passes/rewrite.h b/src/preprocessing/passes/rewrite.h
new file mode 100644 (file)
index 0000000..1ab614f
--- /dev/null
+++ b/src/preprocessing/passes/rewrite.h
@@ -0,0 +1,44 @@
+/*********************                                                        */
+/*! \file rewrite.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Caleb Donovick
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 rewrite preprocessing pass
+ **
+ ** Calls the rewriter on every assertion
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__REWRITE_H
+#define __CVC4__PREPROCESSING__PASSES__REWRITE_H
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class Rewrite : public PreprocessingPass
+{
+ public:
+  Rewrite(PreprocessingPassContext* preprocContext);
+
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PASSES__REWRITE_H */
+

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 22916e35474bff7f49161030af630551b91cc68c..5d9f083431a4d14f9dd1a9f67fba213caabf7887 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -78,6 +78,7 @@
 #include "preprocessing/passes/int_to_bv.h"
 #include "preprocessing/passes/pseudo_boolean_processor.h"
 #include "preprocessing/passes/real_to_int.h"
+#include "preprocessing/passes/rewrite.h"
 #include "preprocessing/passes/static_learning.h"
 #include "preprocessing/passes/symmetry_breaker.h"
 #include "preprocessing/passes/symmetry_detect.h"
@@ -2716,6 +2717,8 @@ void SmtEnginePrivate::finishInit()
       new PseudoBooleanProcessor(d_preprocessingPassContext.get()));
   std::unique_ptr<RealToInt> realToInt(
       new RealToInt(d_preprocessingPassContext.get()));
+  std::unique_ptr<Rewrite> rewrite(
+      new Rewrite(d_preprocessingPassContext.get()));
   std::unique_ptr<StaticLearning> staticLearning(
       new StaticLearning(d_preprocessingPassContext.get()));
   std::unique_ptr<SymBreakerPass> sbProc(
@@ -2737,6 +2740,7 @@ void SmtEnginePrivate::finishInit()
   d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor",
                                            std::move(pbProc));
   d_preprocessingPassRegistry.registerPass("real-to-int", std::move(realToInt));
+  d_preprocessingPassRegistry.registerPass("rewrite", std::move(rewrite));
   d_preprocessingPassRegistry.registerPass("static-learning", 
                                            std::move(staticLearning));
   d_preprocessingPassRegistry.registerPass("sym-break", std::move(sbProc));
@@ -4168,10 +4172,7 @@ void SmtEnginePrivate::processAssertions() {
   if(options::unconstrainedSimp()) {
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << endl;
     dumpAssertions("pre-unconstrained-simp", d_assertions);
-    Chat() << "...doing unconstrained simplification..." << endl;
-    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
-      d_assertions.replace(i, Rewriter::rewrite(d_assertions[i]));
-    }
+       d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions);
     unconstrainedSimp();
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-unconstrained-simp" << endl;
     dumpAssertions("post-unconstrained-simp", d_assertions);
@@ -4189,10 +4190,7 @@ void SmtEnginePrivate::processAssertions() {
   {
     // special rewriting pass for unsat cores, since many of the passes below
     // are skipped
-    for (unsigned i = 0; i < d_assertions.size(); ++i)
-    {
-      d_assertions.replace(i, Rewriter::rewrite(d_assertions[i]));
-    }
+         d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions);
   }
   else
   {