Make quantifiers-preprocess preprocessing pass (#2322)

4 files changed, 113 insertions, 10 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 59a2a64c0..f3737e506 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -85,6 +85,8 @@ libcvc4_la_SOURCES = \
 	preprocessing/passes/bool_to_bv.h \
 	preprocessing/passes/bv_to_bool.cpp \
 	preprocessing/passes/bv_to_bool.h \
+	preprocessing/passes/quantifiers_preprocess.cpp \
+	preprocessing/passes/quantifiers_preprocess.h \
 	preprocessing/passes/real_to_int.cpp \
 	preprocessing/passes/real_to_int.h \
 	preprocessing/passes/rewrite.cpp \
diff --git a/src/preprocessing/passes/quantifiers_preprocess.cpp b/src/preprocessing/passes/quantifiers_preprocess.cpp
new file mode 100644
index 000000000..e6c1557c0
--- /dev/null
+++ b/src/preprocessing/passes/quantifiers_preprocess.cpp
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file quantifiers_preprocess.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 Remove rewrite rules, apply pre-skolemization to existential
+ *quantifiers
+ **
+ **
+ ** Calls the quantifier rewriter, removing rewrite rules and applying
+ ** pre-skolemization to existential quantifiers
+ **/
+
+#include "preprocessing/passes/quantifiers_preprocess.h"
+
+#include "base/output.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using namespace CVC4::theory;
+
+QuantifiersPreprocess::QuantifiersPreprocess(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "quantifiers-preprocess"){};
+
+PreprocessingPassResult QuantifiersPreprocess::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  size_t size = assertionsToPreprocess->size();
+  for (size_t i = 0; i < size; ++i)
+  {
+    Node prev = (*assertionsToPreprocess)[i];
+    Node next = quantifiers::QuantifiersRewriter::preprocess(prev);
+    if (next != prev)
+    {
+      assertionsToPreprocess->replace(i, Rewriter::rewrite(next));
+      Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev << endl;
+      Trace("quantifiers-preprocess")
+          << "   ...got " << (*assertionsToPreprocess)[i] << endl;
+    }
+  }
+
+  return PreprocessingPassResult::NO_CONFLICT;
+}
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/passes/quantifiers_preprocess.h b/src/preprocessing/passes/quantifiers_preprocess.h
new file mode 100644
index 000000000..56ad2f175
--- /dev/null
+++ b/src/preprocessing/passes/quantifiers_preprocess.h
@@ -0,0 +1,46 @@
+/*********************                                                        */
+/*! \file quantifiers_preprocess.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 Remove rewrite rules, apply pre-skolemization to existential
+ *quantifiers
+ **
+ **
+ ** Calls the quantifier rewriter, removing rewrite rules and applying
+ ** pre-skolemization to existential quantifiers
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H
+#define __CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class QuantifiersPreprocess : public PreprocessingPass
+{
+ public:
+  QuantifiersPreprocess(PreprocessingPassContext* preprocContext);
+
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d2e9c2f36..ee447527e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -81,6 +81,7 @@
 #include "preprocessing/passes/int_to_bv.h"
 #include "preprocessing/passes/ite_removal.h"
 #include "preprocessing/passes/pseudo_boolean_processor.h"
+#include "preprocessing/passes/quantifiers_preprocess.h"
 #include "preprocessing/passes/real_to_int.h"
 #include "preprocessing/passes/rewrite.h"
 #include "preprocessing/passes/sep_skolem_emp.h"
@@ -2664,6 +2665,8 @@ void SmtEnginePrivate::finishInit()
       new ExtRewPre(d_preprocessingPassContext.get()));
   std::unique_ptr<IntToBV> intToBV(
       new IntToBV(d_preprocessingPassContext.get()));
+  std::unique_ptr<QuantifiersPreprocess> quantifiersPreprocess(
+      new QuantifiersPreprocess(d_preprocessingPassContext.get()));
   std::unique_ptr<PseudoBooleanProcessor> pbProc(
       new PseudoBooleanProcessor(d_preprocessingPassContext.get()));
   std::unique_ptr<IteRemoval> iteRemoval(
@@ -2698,6 +2701,8 @@ void SmtEnginePrivate::finishInit()
   d_preprocessingPassRegistry.registerPass("bv-to-bool", std::move(bvToBool));
   d_preprocessingPassRegistry.registerPass("ext-rew-pre", std::move(extRewPre));
   d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV));
+  d_preprocessingPassRegistry.registerPass("quantifiers-preprocess",
+                                           std::move(quantifiersPreprocess));
   d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor",
                                            std::move(pbProc));
   d_preprocessingPassRegistry.registerPass("ite-removal",
@@ -4165,7 +4170,7 @@ void SmtEnginePrivate::processAssertions() {
   {
     // special rewriting pass for unsat cores, since many of the passes below
     // are skipped
-	  d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions);
+    d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions);
   }
   else
   {
@@ -4207,15 +4212,8 @@ void SmtEnginePrivate::processAssertions() {
 
     dumpAssertions("pre-skolem-quant", d_assertions);
     //remove rewrite rules, apply pre-skolemization to existential quantifiers
-    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
-      Node prev = d_assertions[i];
-      Node next = quantifiers::QuantifiersRewriter::preprocess( prev );
-      if( next!=prev ){
-        d_assertions.replace( i, Rewriter::rewrite( next ) );
-        Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev << endl;
-        Trace("quantifiers-preprocess") << "   ...got " << d_assertions[i] << endl;
-      }
-    }
+    d_preprocessingPassRegistry.getPass("quantifiers-preprocess")
+        ->apply(&d_assertions);
     dumpAssertions("post-skolem-quant", d_assertions);
     if( options::macrosQuant() ){
       //quantifiers macro expansion