Refactor ITE simplification preprocessing pass. (#2360)

3 files changed, 38 insertions, 31 deletions

diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index a683d2bbb..5b51e162d 100644
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -2,7 +2,7 @@
 /*! \file arith_ite_utils.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Kshitij Bansal
+ **   Tim King, Aina Niemetz, Kshitij Bansal
  ** 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.
@@ -21,9 +21,9 @@
 
 #include "base/output.h"
 #include "options/smt_options.h"
+#include "preprocessing/util/ite_utilities.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/normal_form.h"
-#include "theory/ite_utilities.h"
 #include "theory/rewriter.h"
 #include "theory/substitutions.h"
 #include "theory/theory_model.h"
@@ -140,18 +140,19 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){
   Unreachable();
 }
 
-ArithIteUtils::ArithIteUtils(ContainsTermITEVisitor& contains,
-                             context::Context* uc,
-                             TheoryModel* model)
-  : d_contains(contains)
-  , d_subs(NULL)
-  , d_model(model)
-  , d_one(1)
-  , d_subcount(uc, 0)
-  , d_skolems(uc)
-  , d_implies()
-  , d_skolemsAdded()
-  , d_orBinEqs()
+ArithIteUtils::ArithIteUtils(
+    preprocessing::util::ContainsTermITEVisitor& contains,
+    context::Context* uc,
+    TheoryModel* model)
+    : d_contains(contains),
+      d_subs(NULL),
+      d_model(model),
+      d_one(1),
+      d_subcount(uc, 0),
+      d_skolems(uc),
+      d_implies(),
+      d_skolemsAdded(),
+      d_orBinEqs()
 {
   d_subs = new SubstitutionMap(uc);
 }
diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h
index 7950ef05f..2c6a30758 100644
--- a/src/theory/arith/arith_ite_utils.h
+++ b/src/theory/arith/arith_ite_utils.h
@@ -2,7 +2,7 @@
 /*! \file arith_ite_utils.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King
+ **   Tim King, Aina Niemetz
  ** 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.
@@ -29,15 +29,21 @@
 #include "context/cdinsert_hashmap.h"
 
 namespace CVC4 {
-namespace theory {
+namespace preprocessing {
+namespace util {
 class ContainsTermITEVisitor;
+}
+}  // namespace preprocessing
+
+namespace theory {
+
 class SubstitutionMap;
 class TheoryModel;
 
 namespace arith {
 
 class ArithIteUtils {
-  ContainsTermITEVisitor& d_contains;
+  preprocessing::util::ContainsTermITEVisitor& d_contains;
   SubstitutionMap* d_subs;
   TheoryModel* d_model;
 
@@ -68,24 +74,24 @@ class ArithIteUtils {
   std::vector<Node> d_orBinEqs;
 
 public:
-  ArithIteUtils(ContainsTermITEVisitor& contains,
-                context::Context* userContext,
-                TheoryModel* model);
-  ~ArithIteUtils();
+ ArithIteUtils(preprocessing::util::ContainsTermITEVisitor& contains,
+               context::Context* userContext,
+               TheoryModel* model);
+ ~ArithIteUtils();
 
-  //(ite ?v_2 ?v_1 (ite ?v_3 (- ?v_1 128) (- ?v_1 256)))
+ //(ite ?v_2 ?v_1 (ite ?v_3 (- ?v_1 128) (- ?v_1 256)))
 
-  /** removes common sums variables sums from term ites. */
-  Node reduceVariablesInItes(Node n);
+ /** removes common sums variables sums from term ites. */
+ Node reduceVariablesInItes(Node n);
 
-  Node reduceConstantIteByGCD(Node n);
+ Node reduceConstantIteByGCD(Node n);
 
-  void clear();
+ void clear();
 
-  Node applySubstitutions(TNode f);
-  unsigned getSubCount() const;
+ Node applySubstitutions(TNode f);
+ unsigned getSubCount() const;
 
-  void learnSubstitutions(const std::vector<Node>& assertions);
+ void learnSubstitutions(const std::vector<Node>& assertions);
 
 private:
   /* applies this to all children of n and constructs the result */
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 968970049..89550295a 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -36,6 +36,7 @@
 #include "expr/node_builder.h"
 #include "options/arith_options.h"
 #include "options/smt_options.h"  // for incrementalSolving()
+#include "preprocessing/util/ite_utilities.h"
 #include "smt/logic_exception.h"
 #include "smt/logic_request.h"
 #include "smt/smt_statistics_registry.h"
@@ -59,7 +60,6 @@
 #include "theory/arith/simplex.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/ext_theory.h"
-#include "theory/ite_utilities.h"
 #include "theory/quantifiers/fmf/bounded_integers.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
@@ -5374,7 +5374,7 @@ bool TheoryArithPrivate::decomposeTerm(Node term, Rational& m, Node& p, Rational
   }
 
   // TODO Speed up
-  ContainsTermITEVisitor ctv;
+  preprocessing::util::ContainsTermITEVisitor ctv;
   if(ctv.containsTermITE(t)){
     return false;
   }