global-negate preprocessing pass (#2317)

5 files changed, 85 insertions, 77 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 40aa1a5af..6a21566e0 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -77,6 +77,8 @@ libcvc4_la_SOURCES = \
 	preprocessing/passes/bv_intro_pow2.h \
 	preprocessing/passes/extended_rewriter_pass.cpp \
 	preprocessing/passes/extended_rewriter_pass.h \
+	preprocessing/passes/global_negate.cpp \
+	preprocessing/passes/global_negate.h \
 	preprocessing/passes/int_to_bv.cpp \
 	preprocessing/passes/int_to_bv.h \
 	preprocessing/passes/ite_removal.cpp \
@@ -462,8 +464,6 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/fmf/model_engine.h \
 	theory/quantifiers/fun_def_process.cpp \
 	theory/quantifiers/fun_def_process.h \
-	theory/quantifiers/global_negate.cpp \
-	theory/quantifiers/global_negate.h \
 	theory/quantifiers/instantiate.cpp \
 	theory/quantifiers/instantiate.h \
 	theory/quantifiers/inst_match.cpp \
diff --git a/src/theory/quantifiers/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp
index 0670b5c5b..ddebf961f 100644
--- a/src/theory/quantifiers/global_negate.cpp
+++ b/src/preprocessing/passes/global_negate.cpp
@@ -12,21 +12,22 @@
  ** \brief Implementation of global_negate
  **/
 
-#include "theory/quantifiers/global_negate.h"
+#include "preprocessing/passes/global_negate.h"
+#include <vector>
+#include "expr/node.h"
 #include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;
+using namespace CVC4::theory;
 
 namespace CVC4 {
-namespace theory {
-namespace quantifiers {
+namespace preprocessing {
+namespace passes {
 
-void GlobalNegate::simplify(std::vector<Node>& assertions)
+Node GlobalNegate::simplify(std::vector<Node>& assertions, NodeManager* nm)
 {
-  NodeManager* nm = NodeManager::currentNM();
   Assert(!assertions.empty());
-
   Trace("cbqi-gn") << "Global negate : " << std::endl;
   // collect free variables in all assertions
   std::vector<Node> free_vars;
@@ -90,21 +91,26 @@ void GlobalNegate::simplify(std::vector<Node>& assertions)
   Trace("cbqi-gn-debug") << "...got (pre-rewrite) : " << body << std::endl;
   body = Rewriter::rewrite(body);
   Trace("cbqi-gn") << "...got (post-rewrite) : " << body << std::endl;
+  return body;
+}
 
-  Node truen = nm->mkConst(true);
-  for (unsigned i = 0, size = assertions.size(); i < size; i++)
+GlobalNegate::GlobalNegate(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "global-negate"){};
+
+PreprocessingPassResult GlobalNegate::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node simplifiedNode = simplify(assertionsToPreprocess->ref(), nm);
+  Node trueNode = nm->mkConst(true);
+  for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
   {
-    if (i == 0)
-    {
-      assertions[i] = body;
-    }
-    else
-    {
-      assertions[i] = truen;
-    }
+    assertionsToPreprocess->replace(i, trueNode);
   }
+  assertionsToPreprocess->push_back(simplifiedNode);
+  return PreprocessingPassResult::NO_CONFLICT;
 }
 
-} /* CVC4::theory::quantifiers namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h
new file mode 100644
index 000000000..0330aa10e
--- /dev/null
+++ b/src/preprocessing/passes/global_negate.h
@@ -0,0 +1,52 @@
+/*********************                                                        */
+/*! \file global_negate.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** 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 global_negate preprocessing pass
+  * Updates a set of assertions to the negation of
+ * these assertions. In detail, if assertions is:
+ *    F1, ..., Fn
+ * then we update this vector to:
+ *    forall x1...xm. ~( F1 ^ ... ^ Fn ), true, ..., true
+ * where x1...xm are the free variables of F1...Fn.
+ * When this is done, d_globalNegation flag is marked, so that the solver checks
+ *for unsat instead of sat.
+**/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H
+#define __CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class GlobalNegate : public PreprocessingPass
+{
+ public:
+  GlobalNegate(PreprocessingPassContext* preprocContext);
+
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+  Node simplify(std::vector<Node>& assertions, NodeManager* nm);
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING_PASSES__GLOBAL_NEGATE_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f9ea2f1ac..33ca6eb3d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -79,6 +79,7 @@
 #include "preprocessing/passes/bv_intro_pow2.h"
 #include "preprocessing/passes/bv_to_bool.h"
 #include "preprocessing/passes/extended_rewriter_pass.h"
+#include "preprocessing/passes/global_negate.h"
 #include "preprocessing/passes/int_to_bv.h"
 #include "preprocessing/passes/ite_removal.h"
 #include "preprocessing/passes/pseudo_boolean_processor.h"
@@ -115,7 +116,6 @@
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/logic_info.h"
 #include "theory/quantifiers/fun_def_process.h"
-#include "theory/quantifiers/global_negate.h"
 #include "theory/quantifiers/macros.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/single_inv_partition.h"
@@ -2660,6 +2660,8 @@ void SmtEnginePrivate::finishInit()
       new BVToBool(d_preprocessingPassContext.get()));
   std::unique_ptr<ExtRewPre> extRewPre(
       new ExtRewPre(d_preprocessingPassContext.get()));
+  std::unique_ptr<GlobalNegate> globalNegate(
+      new GlobalNegate(d_preprocessingPassContext.get()));
   std::unique_ptr<IntToBV> intToBV(
       new IntToBV(d_preprocessingPassContext.get()));
   std::unique_ptr<QuantifiersPreprocess> quantifiersPreprocess(
@@ -2701,6 +2703,8 @@ void SmtEnginePrivate::finishInit()
                                            std::move(bvIntroPow2));
   d_preprocessingPassRegistry.registerPass("bv-to-bool", std::move(bvToBool));
   d_preprocessingPassRegistry.registerPass("ext-rew-pre", std::move(extRewPre));
+  d_preprocessingPassRegistry.registerPass("global-negate",
+                                           std::move(globalNegate));
   d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV));
   d_preprocessingPassRegistry.registerPass("quantifiers-preprocess",
                                            std::move(quantifiersPreprocess));
@@ -4085,8 +4089,7 @@ void SmtEnginePrivate::processAssertions() {
   if (options::globalNegate())
   {
     // global negation of the formula
-    quantifiers::GlobalNegate gn;
-    gn.simplify(d_assertions.ref());
+    d_preprocessingPassRegistry.getPass("global-negate")->apply(&d_assertions);
     d_smt.d_globalNegation = !d_smt.d_globalNegation;
   }
 
diff --git a/src/theory/quantifiers/global_negate.h b/src/theory/quantifiers/global_negate.h
deleted file mode 100644
index f5d92c478..000000000
--- a/src/theory/quantifiers/global_negate.h
+++ /dev/null
@@ -1,53 +0,0 @@
-/*********************                                                        */
-/*! \file global_negate.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** 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 global_negate
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__QUANTIFIERS__GLOBAL_NEGATE_H
-#define __CVC4__THEORY__QUANTIFIERS__GLOBAL_NEGATE_H
-
-#include <vector>
-#include "expr/node.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-/** GlobalNegate
- *
- * This class updates a set of assertions to be equivalent to the negation of
- * these assertions. In detail, if assertions is:
- *    F1, ..., Fn
- * then we update this vector to:
- *    forall x1...xm. ~( F1 ^ ... ^ Fn ), true, ..., true
- * where x1...xm are the free variables of F1...Fn.
- */
-class GlobalNegate
-{
- public:
-  GlobalNegate() {}
-  ~GlobalNegate() {}
-  /** simplify assertions
-   *
-   * Replaces assertions with a set of assertions that is equivalent to its
-   * negation.
-   */
-  void simplify(std::vector<Node>& assertions);
-};
-
-} /* CVC4::theory::quantifiers namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__QUANTIFIERS__GLOBAL_NEGATE_H */