Refactor ITE simplification preprocessing pass. (#2360)

12 files changed, 1192 insertions, 744 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 6a21566e0..3b8a12fa5 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -83,6 +83,8 @@ libcvc4_la_SOURCES = \
 	preprocessing/passes/int_to_bv.h \
 	preprocessing/passes/ite_removal.cpp \
 	preprocessing/passes/ite_removal.h \
+	preprocessing/passes/ite_simp.cpp \
+	preprocessing/passes/ite_simp.h \
 	preprocessing/passes/pseudo_boolean_processor.cpp \
 	preprocessing/passes/pseudo_boolean_processor.h \
 	preprocessing/passes/bool_to_bv.cpp \
@@ -115,6 +117,8 @@ libcvc4_la_SOURCES = \
 	preprocessing/preprocessing_pass_context.h \
 	preprocessing/preprocessing_pass_registry.cpp \
 	preprocessing/preprocessing_pass_registry.h \
+	preprocessing/util/ite_utilities.cpp \
+	preprocessing/util/ite_utilities.h \
 	printer/dagification_visitor.cpp \
 	printer/dagification_visitor.h \
 	printer/printer.cpp \
@@ -205,8 +209,6 @@ libcvc4_la_SOURCES = \
 	theory/evaluator.cpp \
 	theory/evaluator.h \
 	theory/interrupted.h \
-	theory/ite_utilities.cpp \
-	theory/ite_utilities.h \
 	theory/logic_info.cpp \
 	theory/logic_info.h \
 	theory/output_channel.h \
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
new file mode 100644
index 000000000..137925f77
--- /dev/null
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -0,0 +1,263 @@
+/*********************                                                        */
+/*! \file ite_simp.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   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.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief ITE simplification preprocessing pass.
+ **/
+
+#include "preprocessing/passes/ite_simp.h"
+
+#include "options/proof_options.h"
+#include "smt/smt_statistics_registry.h"
+#include "smt_util/nary_builder.h"
+#include "theory/arith/arith_ite_utils.h"
+
+#include <vector>
+
+using namespace CVC4;
+using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+/* -------------------------------------------------------------------------- */
+
+namespace {
+
+Node simpITE(util::ITEUtilities* ite_utils, TNode assertion)
+{
+  if (!ite_utils->containsTermITE(assertion))
+  {
+    return assertion;
+  }
+  else
+  {
+    Node result = ite_utils->simpITE(assertion);
+    Node res_rewritten = Rewriter::rewrite(result);
+
+    if (options::simplifyWithCareEnabled())
+    {
+      Chat() << "starting simplifyWithCare()" << endl;
+      Node postSimpWithCare = ite_utils->simplifyWithCare(res_rewritten);
+      Chat() << "ending simplifyWithCare()"
+             << " post simplifyWithCare()" << postSimpWithCare.getId() << endl;
+      result = Rewriter::rewrite(postSimpWithCare);
+    }
+    else
+    {
+      result = res_rewritten;
+    }
+    return result;
+  }
+}
+
+/**
+ * Ensures the assertions asserted after index 'before' now effectively come
+ * before 'real_assertions_end'.
+ */
+void compressBeforeRealAssertions(AssertionPipeline* assertionsToPreprocess,
+                                  size_t before)
+{
+  size_t cur_size = assertionsToPreprocess->size();
+  if (before >= cur_size || assertionsToPreprocess->getRealAssertionsEnd() <= 0
+      || assertionsToPreprocess->getRealAssertionsEnd() >= cur_size)
+  {
+    return;
+  }
+
+  // assertions
+  // original: [0 ... assertionsToPreprocess.getRealAssertionsEnd())
+  //  can be modified
+  // ites skolems [assertionsToPreprocess.getRealAssertionsEnd(), before)
+  //  cannot be moved
+  // added [before, cur_size)
+  //  can be modified
+  Assert(0 < assertionsToPreprocess->getRealAssertionsEnd());
+  Assert(assertionsToPreprocess->getRealAssertionsEnd() <= before);
+  Assert(before < cur_size);
+
+  std::vector<Node> intoConjunction;
+  for (size_t i = before; i < cur_size; ++i)
+  {
+    intoConjunction.push_back((*assertionsToPreprocess)[i]);
+  }
+  assertionsToPreprocess->resize(before);
+  size_t lastBeforeItes = assertionsToPreprocess->getRealAssertionsEnd() - 1;
+  intoConjunction.push_back((*assertionsToPreprocess)[lastBeforeItes]);
+  Node newLast = CVC4::util::NaryBuilder::mkAssoc(kind::AND, intoConjunction);
+  assertionsToPreprocess->replace(lastBeforeItes, newLast);
+  Assert(assertionsToPreprocess->size() == before);
+}
+
+}  // namespace
+
+/* -------------------------------------------------------------------------- */
+
+ITESimp::Statistics::Statistics()
+    : d_arithSubstitutionsAdded(
+          "preprocessing::passes::ITESimp::ArithSubstitutionsAdded", 0)
+{
+  smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded);
+}
+
+ITESimp::Statistics::~Statistics()
+{
+  smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded);
+}
+
+bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
+{
+  // This pass does not support dependency tracking yet
+  // (learns substitutions from all assertions so just
+  // adding addDependence is not enough)
+  if (options::unsatCores() || options::fewerPreprocessingHoles())
+  {
+    return true;
+  }
+  bool result = true;
+  bool simpDidALotOfWork = d_iteUtilities.simpIteDidALotOfWorkHeuristic();
+  if (simpDidALotOfWork)
+  {
+    if (options::compressItes())
+    {
+      result = d_iteUtilities.compress(assertionsToPreprocess->ref());
+    }
+
+    if (result)
+    {
+      // if false, don't bother to reclaim memory here.
+      NodeManager* nm = NodeManager::currentNM();
+      if (nm->poolSize() >= options::zombieHuntThreshold())
+      {
+        Chat() << "..ite simplifier did quite a bit of work.. "
+               << nm->poolSize() << endl;
+        Chat() << "....node manager contains " << nm->poolSize()
+               << " nodes before cleanup" << endl;
+        d_iteUtilities.clear();
+        Rewriter::clearCaches();
+        nm->reclaimZombiesUntil(options::zombieHuntThreshold());
+        Chat() << "....node manager contains " << nm->poolSize()
+               << " nodes after cleanup" << endl;
+      }
+    }
+  }
+
+  // Do theory specific preprocessing passes
+  TheoryEngine* theory_engine = d_preprocContext->getTheoryEngine();
+  if (theory_engine->getLogicInfo().isTheoryEnabled(theory::THEORY_ARITH)
+      && !options::incrementalSolving())
+  {
+    if (!simpDidALotOfWork)
+    {
+      util::ContainsTermITEVisitor& contains =
+          *(d_iteUtilities.getContainsVisitor());
+      arith::ArithIteUtils aiteu(contains,
+                                 d_preprocContext->getUserContext(),
+                                 theory_engine->getModel());
+      bool anyItes = false;
+      for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
+      {
+        Node curr = (*assertionsToPreprocess)[i];
+        if (contains.containsTermITE(curr))
+        {
+          anyItes = true;
+          Node res = aiteu.reduceVariablesInItes(curr);
+          Debug("arith::ite::red") << "@ " << i << " ... " << curr << endl
+                                   << "   ->" << res << endl;
+          if (curr != res)
+          {
+            Node more = aiteu.reduceConstantIteByGCD(res);
+            Debug("arith::ite::red") << "  gcd->" << more << endl;
+            (*assertionsToPreprocess)[i] = Rewriter::rewrite(more);
+          }
+        }
+      }
+      if (!anyItes)
+      {
+        unsigned prevSubCount = aiteu.getSubCount();
+        aiteu.learnSubstitutions(assertionsToPreprocess->ref());
+        if (prevSubCount < aiteu.getSubCount())
+        {
+          d_statistics.d_arithSubstitutionsAdded +=
+              aiteu.getSubCount() - prevSubCount;
+          bool anySuccess = false;
+          for (size_t i = 0, N = assertionsToPreprocess->size(); i < N; ++i)
+          {
+            Node curr = (*assertionsToPreprocess)[i];
+            Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr));
+            Node res = aiteu.reduceVariablesInItes(next);
+            Debug("arith::ite::red") << "@ " << i << " ... " << next << endl
+                                     << "   ->" << res << endl;
+            Node more = aiteu.reduceConstantIteByGCD(res);
+            Debug("arith::ite::red") << "  gcd->" << more << endl;
+            if (more != next)
+            {
+              anySuccess = true;
+              break;
+            }
+          }
+          for (size_t i = 0, N = assertionsToPreprocess->size();
+               anySuccess && i < N;
+               ++i)
+          {
+            Node curr = (*assertionsToPreprocess)[i];
+            Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr));
+            Node res = aiteu.reduceVariablesInItes(next);
+            Debug("arith::ite::red") << "@ " << i << " ... " << next << endl
+                                     << "   ->" << res << endl;
+            Node more = aiteu.reduceConstantIteByGCD(res);
+            Debug("arith::ite::red") << "  gcd->" << more << endl;
+            (*assertionsToPreprocess)[i] = Rewriter::rewrite(more);
+          }
+        }
+      }
+    }
+  }
+  return result;
+}
+
+/* -------------------------------------------------------------------------- */
+
+ITESimp::ITESimp(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "ite-simp")
+{
+}
+
+PreprocessingPassResult ITESimp::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  d_preprocContext->spendResource(options::preprocessStep());
+
+  size_t nasserts = assertionsToPreprocess->size();
+  for (size_t i = 0; i < nasserts; ++i)
+  {
+    d_preprocContext->spendResource(options::preprocessStep());
+    Node simp = simpITE(&d_iteUtilities, (*assertionsToPreprocess)[i]);
+    assertionsToPreprocess->replace(i, simp);
+    if (simp.isConst() && !simp.getConst<bool>())
+    {
+      return PreprocessingPassResult::CONFLICT;
+    }
+  }
+  bool done = doneSimpITE(assertionsToPreprocess);
+  if (nasserts < assertionsToPreprocess->size())
+  {
+    compressBeforeRealAssertions(assertionsToPreprocess, nasserts);
+  }
+  return done ? PreprocessingPassResult::NO_CONFLICT
+              : PreprocessingPassResult::CONFLICT;
+}
+
+/* -------------------------------------------------------------------------- */
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/passes/ite_simp.h b/src/preprocessing/passes/ite_simp.h
new file mode 100644
index 000000000..2296d663e
--- /dev/null
+++ b/src/preprocessing/passes/ite_simp.h
@@ -0,0 +1,56 @@
+/*********************                                                        */
+/*! \file ite_simp.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   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.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief ITE simplification preprocessing pass.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__ITE_SIMP_H
+#define __CVC4__PREPROCESSING__PASSES__ITE_SIMP_H
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class ITESimp : public PreprocessingPass
+{
+ public:
+   ITESimp(PreprocessingPassContext* preprocContext);
+
+ protected:
+   PreprocessingPassResult applyInternal(
+       AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+  struct Statistics
+  {
+    IntStat d_arithSubstitutionsAdded;
+    Statistics();
+    ~Statistics();
+  };
+
+  bool doneSimpITE(AssertionPipeline *assertionsToPreprocesss);
+
+  /** A collection of ite preprocessing passes. */
+  util::ITEUtilities d_iteUtilities;
+
+  Statistics d_statistics;
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index b50421e6c..a289752fa 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -2,7 +2,7 @@
 /*! \file preprocessing_pass_context.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Justin Xu, Aina Niemetz, Mathias Preiner
+ **   Justin Xu, Andres Noetzli, 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.
@@ -23,6 +23,7 @@
 
 #include "context/context.h"
 #include "decision/decision_engine.h"
+#include "preprocessing/util/ite_utilities.h"
 #include "smt/smt_engine.h"
 #include "smt/term_formula_removal.h"
 #include "theory/theory_engine.h"
diff --git a/src/theory/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp
index 40a58cf57..66d9151df 100644
--- a/src/theory/ite_utilities.cpp
+++ b/src/preprocessing/util/ite_utilities.cpp
@@ -2,7 +2,7 @@
 /*! \file ite_utilities.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Andres Noetzli
+ **   Tim King, Aina Niemetz, Andres Noetzli
  ** 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.
@@ -14,70 +14,74 @@
  ** This module implements preprocessing phases designed to simplify ITE
  ** expressions.  Based on:
  ** Kim, Somenzi, Jin.  Efficient Term-ITE Conversion for SMT.  FMCAD 2009.
- ** Burch, Jerry.  Techniques for Verifying Superscalar Microprocessors.  DAC '96
+ ** Burch, Jerry.  Techniques for Verifying Superscalar Microprocessors.  DAC
+ *'96
  **/
-#include "theory/ite_utilities.h"
+#include "preprocessing/util/ite_utilities.h"
 
 #include <utility>
 
+#include "preprocessing/passes/rewrite.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 
 using namespace std;
 namespace CVC4 {
-namespace theory {
+namespace preprocessing {
+namespace util {
 
 namespace ite {
 
-inline static bool isTermITE(TNode e) {
+inline static bool isTermITE(TNode e)
+{
   return (e.getKind() == kind::ITE && !e.getType().isBoolean());
 }
 
-inline static bool triviallyContainsNoTermITEs(TNode e) {
+inline static bool triviallyContainsNoTermITEs(TNode e)
+{
   return e.isConst() || e.isVar();
 }
 
-static bool isTheoryAtom(TNode a){
+static bool isTheoryAtom(TNode a)
+{
   using namespace kind;
-  switch(a.getKind()){
-  case EQUAL:
-  case DISTINCT:
-    return !(a[0].getType().isBoolean());
-
-  /* from uf */
-  case APPLY_UF:
-    return a.getType().isBoolean();
-  case CARDINALITY_CONSTRAINT:
-  case DIVISIBLE:
-  case LT:
-  case LEQ:
-  case GT:
-  case GEQ:
-  case IS_INTEGER:
-  case BITVECTOR_COMP:
-  case BITVECTOR_ULT:
-  case BITVECTOR_ULE:
-  case BITVECTOR_UGT:
-  case BITVECTOR_UGE:
-  case BITVECTOR_SLT:
-  case BITVECTOR_SLE:
-  case BITVECTOR_SGT:
-  case BITVECTOR_SGE:
-    return true;
-  default:
-    return false;
+  switch (a.getKind())
+  {
+    case EQUAL:
+    case DISTINCT: return !(a[0].getType().isBoolean());
+
+    /* from uf */
+    case APPLY_UF: return a.getType().isBoolean();
+    case CARDINALITY_CONSTRAINT:
+    case DIVISIBLE:
+    case LT:
+    case LEQ:
+    case GT:
+    case GEQ:
+    case IS_INTEGER:
+    case BITVECTOR_COMP:
+    case BITVECTOR_ULT:
+    case BITVECTOR_ULE:
+    case BITVECTOR_UGT:
+    case BITVECTOR_UGE:
+    case BITVECTOR_SLT:
+    case BITVECTOR_SLE:
+    case BITVECTOR_SGT:
+    case BITVECTOR_SGE: return true;
+    default: return false;
   }
 }
 
-struct CTIVStackElement {
+struct CTIVStackElement
+{
   TNode curr;
   unsigned pos;
   CTIVStackElement() : curr(), pos(0) {}
   CTIVStackElement(TNode c) : curr(c), pos(0) {}
 }; /* CTIVStackElement */
 
-} /* CVC4::theory::ite */
+}  // namespace ite
 
 ITEUtilities::ITEUtilities()
     : d_containsVisitor(new ContainsTermITEVisitor()),
@@ -88,57 +92,74 @@ ITEUtilities::ITEUtilities()
   Assert(d_containsVisitor != NULL);
 }
 
-ITEUtilities::~ITEUtilities(){
-
-  if(d_simplifier != NULL){
+ITEUtilities::~ITEUtilities()
+{
+  if (d_simplifier != NULL)
+  {
     delete d_simplifier;
   }
-  if(d_compressor != NULL){
+  if (d_compressor != NULL)
+  {
     delete d_compressor;
   }
-  if(d_careSimp != NULL){
+  if (d_careSimp != NULL)
+  {
     delete d_careSimp;
   }
 }
 
-Node ITEUtilities::simpITE(TNode assertion){
-  if(d_simplifier == NULL){
+Node ITEUtilities::simpITE(TNode assertion)
+{
+  if (d_simplifier == NULL)
+  {
     d_simplifier = new ITESimplifier(d_containsVisitor.get());
   }
   return d_simplifier->simpITE(assertion);
 }
 
-bool ITEUtilities::simpIteDidALotOfWorkHeuristic() const{
-  if(d_simplifier == NULL){
+bool ITEUtilities::simpIteDidALotOfWorkHeuristic() const
+{
+  if (d_simplifier == NULL)
+  {
     return false;
-  }else{
+  }
+  else
+  {
     return d_simplifier->doneALotOfWorkHeuristic();
   }
 }
 
 /* returns false if an assertion is discovered to be equal to false. */
-bool ITEUtilities::compress(std::vector<Node>& assertions){
-  if(d_compressor == NULL){
+bool ITEUtilities::compress(std::vector<Node>& assertions)
+{
+  if (d_compressor == NULL)
+  {
     d_compressor = new ITECompressor(d_containsVisitor.get());
   }
   return d_compressor->compress(assertions);
 }
 
-Node ITEUtilities::simplifyWithCare(TNode e){
-  if(d_careSimp == NULL){
-     d_careSimp = new ITECareSimplifier();
+Node ITEUtilities::simplifyWithCare(TNode e)
+{
+  if (d_careSimp == NULL)
+  {
+    d_careSimp = new ITECareSimplifier();
   }
   return d_careSimp->simplifyWithCare(e);
 }
 
-void ITEUtilities::clear(){
-  if(d_simplifier != NULL){
+void ITEUtilities::clear()
+{
+  if (d_simplifier != NULL)
+  {
     d_simplifier->clearSimpITECaches();
   }
-  if(d_compressor != NULL){
+  if (d_compressor != NULL)
+  {
     d_compressor->garbageCollect();
   }
-  if(d_careSimp != NULL){
+  if (d_careSimp != NULL)
+  {
     d_careSimp->clear();
   }
   d_containsVisitor->garbageCollect();
@@ -147,50 +168,67 @@ void ITEUtilities::clear(){
 /*********************                                                        */
 /* ContainsTermITEVisitor
  */
-ContainsTermITEVisitor::ContainsTermITEVisitor(): d_cache() {}
-ContainsTermITEVisitor::~ContainsTermITEVisitor(){}
-bool ContainsTermITEVisitor::containsTermITE(TNode e){
+ContainsTermITEVisitor::ContainsTermITEVisitor() : d_cache() {}
+ContainsTermITEVisitor::~ContainsTermITEVisitor() {}
+bool ContainsTermITEVisitor::containsTermITE(TNode e)
+{
   /* throughout execution skip through NOT nodes. */
   e = (e.getKind() == kind::NOT) ? e[0] : e;
-  if(ite::triviallyContainsNoTermITEs(e)){ return false; }
+  if (ite::triviallyContainsNoTermITEs(e))
+  {
+    return false;
+  }
 
   NodeBoolMap::const_iterator end = d_cache.end();
   NodeBoolMap::const_iterator tmp_it = d_cache.find(e);
-  if(tmp_it != end){
+  if (tmp_it != end)
+  {
     return (*tmp_it).second;
   }
 
   bool foundTermIte = false;
   std::vector<ite::CTIVStackElement> stack;
   stack.push_back(ite::CTIVStackElement(e));
-  while(!foundTermIte && !stack.empty()){
+  while (!foundTermIte && !stack.empty())
+  {
     ite::CTIVStackElement& top = stack.back();
     TNode curr = top.curr;
-    if(top.pos >= curr.getNumChildren()){
+    if (top.pos >= curr.getNumChildren())
+    {
       // all of the children have been visited
       // no term ites were found
       d_cache[curr] = false;
       stack.pop_back();
-    }else{
+    }
+    else
+    {
       // this is someone's child
       TNode child = curr[top.pos];
       child = (child.getKind() == kind::NOT) ? child[0] : child;
       ++top.pos;
-      if(ite::triviallyContainsNoTermITEs(child)){
+      if (ite::triviallyContainsNoTermITEs(child))
+      {
         // skip
-      }else{
+      }
+      else
+      {
         tmp_it = d_cache.find(child);
-        if(tmp_it != end){
+        if (tmp_it != end)
+        {
           foundTermIte = (*tmp_it).second;
-        }else{
+        }
+        else
+        {
           stack.push_back(ite::CTIVStackElement(child));
           foundTermIte = ite::isTermITE(child);
         }
       }
     }
   }
-  if(foundTermIte){
-    while(!stack.empty()){
+  if (foundTermIte)
+  {
+    while (!stack.empty())
+    {
       TNode curr = stack.back().curr;
       stack.pop_back();
       d_cache[curr] = true;
@@ -198,62 +236,62 @@ bool ContainsTermITEVisitor::containsTermITE(TNode e){
   }
   return foundTermIte;
 }
-void ContainsTermITEVisitor::garbageCollect() {
-  d_cache.clear();
-}
+void ContainsTermITEVisitor::garbageCollect() { d_cache.clear(); }
 
 /*********************                                                        */
 /* IncomingArcCounter
  */
 IncomingArcCounter::IncomingArcCounter(bool skipVars, bool skipConstants)
-  : d_reachCount()
-  , d_skipVariables(skipVars)
-  , d_skipConstants(skipConstants)
-{}
-IncomingArcCounter::~IncomingArcCounter(){}
+    : d_reachCount(), d_skipVariables(skipVars), d_skipConstants(skipConstants)
+{
+}
+IncomingArcCounter::~IncomingArcCounter() {}
 
-void IncomingArcCounter::computeReachability(const std::vector<Node>& assertions){
+void IncomingArcCounter::computeReachability(
+    const std::vector<Node>& assertions)
+{
   std::vector<TNode> tovisit(assertions.begin(), assertions.end());
 
-  while(!tovisit.empty()){
+  while (!tovisit.empty())
+  {
     TNode back = tovisit.back();
     tovisit.pop_back();
 
     bool skip = false;
-    switch(back.getMetaKind()){
-    case kind::metakind::CONSTANT:
-      skip = d_skipConstants;
-      break;
-    case kind::metakind::VARIABLE:
-      skip = d_skipVariables;
-      break;
-    default:
-      break;
+    switch (back.getMetaKind())
+    {
+      case kind::metakind::CONSTANT: skip = d_skipConstants; break;
+      case kind::metakind::VARIABLE: skip = d_skipVariables; break;
+      default: break;
     }
 
-    if(skip) { continue; }
-    if(d_reachCount.find(back) != d_reachCount.end()){
+    if (skip)
+    {
+      continue;
+    }
+    if (d_reachCount.find(back) != d_reachCount.end())
+    {
       d_reachCount[back] = 1 + d_reachCount[back];
-    }else{
+    }
+    else
+    {
       d_reachCount[back] = 1;
-      for(TNode::iterator cit=back.begin(), end = back.end(); cit != end; ++cit){
+      for (TNode::iterator cit = back.begin(), end = back.end(); cit != end;
+           ++cit)
+      {
         tovisit.push_back(*cit);
       }
     }
   }
 }
 
-void IncomingArcCounter::clear() {
-  d_reachCount.clear();
-}
+void IncomingArcCounter::clear() { d_reachCount.clear(); }
 
 /*********************                                                        */
 /* ITECompressor
  */
 ITECompressor::ITECompressor(ContainsTermITEVisitor* contains)
-  : d_contains(contains)
-  , d_assertions(NULL)
-  , d_incoming(true, true)
+    : d_contains(contains), d_assertions(NULL), d_incoming(true, true)
 {
   Assert(d_contains != NULL);
 
@@ -261,53 +299,58 @@ ITECompressor::ITECompressor(ContainsTermITEVisitor* contains)
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 }
 
-ITECompressor::~ITECompressor() {
-  reset();
-}
+ITECompressor::~ITECompressor() { reset(); }
 
-void ITECompressor::reset(){
+void ITECompressor::reset()
+{
   d_incoming.clear();
   d_compressed.clear();
 }
 
-void ITECompressor::garbageCollect(){
-  reset();
-}
+void ITECompressor::garbageCollect() { reset(); }
 
-ITECompressor::Statistics::Statistics():
-  d_compressCalls("ite-simp::compressCalls", 0),
-  d_skolemsAdded("ite-simp::skolems", 0)
+ITECompressor::Statistics::Statistics()
+    : d_compressCalls("ite-simp::compressCalls", 0),
+      d_skolemsAdded("ite-simp::skolems", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_compressCalls);
   smtStatisticsRegistry()->registerStat(&d_skolemsAdded);
-
 }
-ITECompressor::Statistics::~Statistics(){
+ITECompressor::Statistics::~Statistics()
+{
   smtStatisticsRegistry()->unregisterStat(&d_compressCalls);
   smtStatisticsRegistry()->unregisterStat(&d_skolemsAdded);
 }
 
-Node ITECompressor::push_back_boolean(Node original, Node compressed){
-  Node rewritten = Rewriter::rewrite(compressed);
+Node ITECompressor::push_back_boolean(Node original, Node compressed)
+{
+  Node rewritten = theory::Rewriter::rewrite(compressed);
   // There is a bug if the rewritter takes a pure boolean expression
   // and changes its theory
-  if(rewritten.isConst()){
+  if (rewritten.isConst())
+  {
     d_compressed[compressed] = rewritten;
     d_compressed[original] = rewritten;
     d_compressed[rewritten] = rewritten;
     return rewritten;
-  }else if(d_compressed.find(rewritten) != d_compressed.end()){
+  }
+  else if (d_compressed.find(rewritten) != d_compressed.end())
+  {
     Node res = d_compressed[rewritten];
     d_compressed[original] = res;
     d_compressed[compressed] = res;
     return res;
-  }else if(rewritten.isVar() ||
-           (rewritten.getKind() == kind::NOT && rewritten[0].isVar())){
+  }
+  else if (rewritten.isVar()
+           || (rewritten.getKind() == kind::NOT && rewritten[0].isVar()))
+  {
     d_compressed[original] = rewritten;
     d_compressed[compressed] = rewritten;
     d_compressed[rewritten] = rewritten;
     return rewritten;
-  }else{
+  }
+  else
+  {
     NodeManager* nm = NodeManager::currentNM();
     Node skolem = nm->mkSkolem("compress", nm->booleanType());
     d_compressed[rewritten] = skolem;
@@ -321,28 +364,37 @@ Node ITECompressor::push_back_boolean(Node original, Node compressed){
   }
 }
 
-bool ITECompressor::multipleParents(TNode c){
+bool ITECompressor::multipleParents(TNode c)
+{
   return d_incoming.lookupIncoming(c) >= 2;
 }
 
-Node ITECompressor::compressBooleanITEs(Node toCompress){
+Node ITECompressor::compressBooleanITEs(Node toCompress)
+{
   Assert(toCompress.getKind() == kind::ITE);
   Assert(toCompress.getType().isBoolean());
 
-  if(!(toCompress[1] == d_false || toCompress[2] == d_false)){
+  if (!(toCompress[1] == d_false || toCompress[2] == d_false))
+  {
     Node cmpCnd = compressBoolean(toCompress[0]);
-    if(cmpCnd.isConst()){
+    if (cmpCnd.isConst())
+    {
       Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2];
       Node res = compressBoolean(branch);
       d_compressed[toCompress] = res;
       return res;
-    }else{
+    }
+    else
+    {
       Node cmpThen = compressBoolean(toCompress[1]);
       Node cmpElse = compressBoolean(toCompress[2]);
       Node newIte = cmpCnd.iteNode(cmpThen, cmpElse);
-      if(multipleParents(toCompress)){
+      if (multipleParents(toCompress))
+      {
         return push_back_boolean(toCompress, newIte);
-      }else{
+      }
+      else
+      {
         return newIte;
       }
     }
@@ -350,19 +402,25 @@ Node ITECompressor::compressBooleanITEs(Node toCompress){
 
   NodeBuilder<> nb(kind::AND);
   Node curr = toCompress;
-  while(curr.getKind() == kind::ITE &&
-        (curr[1] == d_false || curr[2] == d_false) &&
-        (!multipleParents(curr) || curr == toCompress)){
-
+  while (curr.getKind() == kind::ITE
+         && (curr[1] == d_false || curr[2] == d_false)
+         && (!multipleParents(curr) || curr == toCompress))
+  {
     bool negateCnd = (curr[1] == d_false);
     Node compressCnd = compressBoolean(curr[0]);
-    if(compressCnd.isConst()){
-      if(compressCnd.getConst<bool>() == negateCnd){
+    if (compressCnd.isConst())
+    {
+      if (compressCnd.getConst<bool>() == negateCnd)
+      {
         return push_back_boolean(toCompress, d_false);
-      }else{
+      }
+      else
+      {
         // equivalent to true don't push back
       }
-    }else{
+    }
+    else
+    {
       Node pb = negateCnd ? compressCnd.notNode() : compressCnd;
       nb << pb;
     }
@@ -375,22 +433,29 @@ Node ITECompressor::compressBooleanITEs(Node toCompress){
   return push_back_boolean(toCompress, res);
 }
 
-Node ITECompressor::compressTerm(Node toCompress){
-  if(toCompress.isConst() || toCompress.isVar()){
+Node ITECompressor::compressTerm(Node toCompress)
+{
+  if (toCompress.isConst() || toCompress.isVar())
+  {
     return toCompress;
   }
 
-  if(d_compressed.find(toCompress) != d_compressed.end()){
+  if (d_compressed.find(toCompress) != d_compressed.end())
+  {
     return d_compressed[toCompress];
   }
-  if(toCompress.getKind() == kind::ITE){
+  if (toCompress.getKind() == kind::ITE)
+  {
     Node cmpCnd = compressBoolean(toCompress[0]);
-    if(cmpCnd.isConst()){
+    if (cmpCnd.isConst())
+    {
       Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2];
       Node res = compressTerm(toCompress);
       d_compressed[toCompress] = res;
       return res;
-    }else{
+    }
+    else
+    {
       Node cmpThen = compressTerm(toCompress[1]);
       Node cmpElse = compressTerm(toCompress[2]);
       Node newIte = cmpCnd.iteNode(cmpThen, cmpElse);
@@ -401,51 +466,69 @@ Node ITECompressor::compressTerm(Node toCompress){
 
   NodeBuilder<> nb(toCompress.getKind());
 
-  if(toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) {
+  if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED)
+  {
     nb << (toCompress.getOperator());
   }
-  for(Node::iterator it = toCompress.begin(), end = toCompress.end(); it != end; ++it){
+  for (Node::iterator it = toCompress.begin(), end = toCompress.end();
+       it != end;
+       ++it)
+  {
     nb << compressTerm(*it);
   }
   Node compressed = (Node)nb;
-  if(multipleParents(toCompress)){
+  if (multipleParents(toCompress))
+  {
     d_compressed[toCompress] = compressed;
   }
   return compressed;
 }
 
-Node ITECompressor::compressBoolean(Node toCompress){
+Node ITECompressor::compressBoolean(Node toCompress)
+{
   static int instance = 0;
   ++instance;
-  if(toCompress.isConst() || toCompress.isVar()){
+  if (toCompress.isConst() || toCompress.isVar())
+  {
     return toCompress;
   }
-  if(d_compressed.find(toCompress) != d_compressed.end()){
+  if (d_compressed.find(toCompress) != d_compressed.end())
+  {
     return d_compressed[toCompress];
-  }else if(toCompress.getKind() == kind::ITE){
+  }
+  else if (toCompress.getKind() == kind::ITE)
+  {
     return compressBooleanITEs(toCompress);
-  }else{
+  }
+  else
+  {
     bool ta = ite::isTheoryAtom(toCompress);
     NodeBuilder<> nb(toCompress.getKind());
-    if(toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) {
+    if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED)
+    {
       nb << (toCompress.getOperator());
     }
-    for(Node::iterator it = toCompress.begin(), end = toCompress.end(); it != end; ++it){
+    for (Node::iterator it = toCompress.begin(), end = toCompress.end();
+         it != end;
+         ++it)
+    {
       Node pb = (ta) ? compressTerm(*it) : compressBoolean(*it);
       nb << pb;
     }
     Node compressed = nb;
-    if(ta || multipleParents(toCompress)){
+    if (ta || multipleParents(toCompress))
+    {
       return push_back_boolean(toCompress, compressed);
-    }else{
+    }
+    else
+    {
       return compressed;
     }
   }
 }
 
-
-
-bool ITECompressor::compress(std::vector<Node>& assertions){
+bool ITECompressor::compress(std::vector<Node>& assertions)
+{
   reset();
 
   d_assertions = &assertions;
@@ -456,11 +539,12 @@ bool ITECompressor::compress(std::vector<Node>& assertions){
 
   bool nofalses = true;
   size_t original_size = assertions.size();
-  Chat () << "compressing " << original_size << endl;
-  for(size_t i = 0; i < original_size && nofalses; ++i){
+  Chat() << "compressing " << original_size << endl;
+  for (size_t i = 0; i < original_size && nofalses; ++i)
+  {
     Node assertion = assertions[i];
-    Node compressed =  compressBoolean(assertion);
-    Node rewritten = Rewriter::rewrite(compressed);
+    Node compressed = compressBoolean(assertion);
+    Node rewritten = theory::Rewriter::rewrite(compressed);
     assertions[i] = rewritten;
     Assert(!d_contains->containsTermITE(rewritten));
 
@@ -472,22 +556,20 @@ bool ITECompressor::compress(std::vector<Node>& assertions){
   return nofalses;
 }
 
-TermITEHeightCounter::TermITEHeightCounter()
-  :d_termITEHeight()
-{}
+TermITEHeightCounter::TermITEHeightCounter() : d_termITEHeight() {}
 
-TermITEHeightCounter::~TermITEHeightCounter(){}
+TermITEHeightCounter::~TermITEHeightCounter() {}
 
-void TermITEHeightCounter::clear(){
-  d_termITEHeight.clear();
-}
+void TermITEHeightCounter::clear() { d_termITEHeight.clear(); }
 
-size_t TermITEHeightCounter::cache_size() const{
+size_t TermITEHeightCounter::cache_size() const
+{
   return d_termITEHeight.size();
 }
 
 namespace ite {
-struct TITEHStackElement {
+struct TITEHStackElement
+{
   TNode curr;
   unsigned pos;
   uint32_t maxChildHeight;
@@ -496,34 +578,42 @@ struct TITEHStackElement {
 };
 } /* namespace ite */
 
-uint32_t TermITEHeightCounter::termITEHeight(TNode e){
-
-  if(ite::triviallyContainsNoTermITEs(e)){ return 0; }
+uint32_t TermITEHeightCounter::termITEHeight(TNode e)
+{
+  if (ite::triviallyContainsNoTermITEs(e))
+  {
+    return 0;
+  }
 
   NodeCountMap::const_iterator end = d_termITEHeight.end();
   NodeCountMap::const_iterator tmp_it = d_termITEHeight.find(e);
-  if(tmp_it != end){
+  if (tmp_it != end)
+  {
     return (*tmp_it).second;
   }
 
-
   uint32_t returnValue = 0;
   // This is initially 0 as the very first call this is included in the max,
   // but this has no effect.
   std::vector<ite::TITEHStackElement> stack;
   stack.push_back(ite::TITEHStackElement(e));
-  while(!stack.empty()){
+  while (!stack.empty())
+  {
     ite::TITEHStackElement& top = stack.back();
     top.maxChildHeight = std::max(top.maxChildHeight, returnValue);
     TNode curr = top.curr;
-    if(top.pos >= curr.getNumChildren()){
+    if (top.pos >= curr.getNumChildren())
+    {
       // done with the current node
       returnValue = top.maxChildHeight + (ite::isTermITE(curr) ? 1 : 0);
       d_termITEHeight[curr] = returnValue;
       stack.pop_back();
       continue;
-    }else{
-      if(top.pos == 0 && curr.getKind() == kind::ITE){
+    }
+    else
+    {
+      if (top.pos == 0 && curr.getKind() == kind::ITE)
+      {
         ++top.pos;
         returnValue = 0;
         continue;
@@ -531,13 +621,19 @@ uint32_t TermITEHeightCounter::termITEHeight(TNode e){
       // this is someone's child
       TNode child = curr[top.pos];
       ++top.pos;
-      if(ite::triviallyContainsNoTermITEs(child)){
+      if (ite::triviallyContainsNoTermITEs(child))
+      {
         returnValue = 0;
-      }else{
+      }
+      else
+      {
         tmp_it = d_termITEHeight.find(child);
-        if(tmp_it != end){
+        if (tmp_it != end)
+        {
           returnValue = (*tmp_it).second;
-        }else{
+        }
+        else
+        {
           stack.push_back(ite::TITEHStackElement(child));
         }
       }
@@ -546,40 +642,42 @@ uint32_t TermITEHeightCounter::termITEHeight(TNode e){
   return returnValue;
 }
 
-
-
 ITESimplifier::ITESimplifier(ContainsTermITEVisitor* contains)
-  : d_containsVisitor(contains)
-  , d_termITEHeight()
-  , d_constantLeaves()
-  , d_allocatedConstantLeaves()
-  , d_citeEqConstApplications(0)
-  , d_constantIteEqualsConstantCache()
-  , d_replaceOverCache()
-  , d_replaceOverTermIteCache()
-  , d_leavesConstCache()
-  , d_simpConstCache()
-  , d_simpContextCache()
-  , d_simpITECache()
+    : d_containsVisitor(contains),
+      d_termITEHeight(),
+      d_constantLeaves(),
+      d_allocatedConstantLeaves(),
+      d_citeEqConstApplications(0),
+      d_constantIteEqualsConstantCache(),
+      d_replaceOverCache(),
+      d_replaceOverTermIteCache(),
+      d_leavesConstCache(),
+      d_simpConstCache(),
+      d_simpContextCache(),
+      d_simpITECache()
 {
   Assert(d_containsVisitor != NULL);
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 }
 
-ITESimplifier::~ITESimplifier() {
+ITESimplifier::~ITESimplifier()
+{
   clearSimpITECaches();
   Assert(d_constantLeaves.empty());
   Assert(d_allocatedConstantLeaves.empty());
 }
 
-bool ITESimplifier::leavesAreConst(TNode e){
+bool ITESimplifier::leavesAreConst(TNode e)
+{
   return leavesAreConst(e, theory::Theory::theoryOf(e));
 }
 
-void ITESimplifier::clearSimpITECaches(){
+void ITESimplifier::clearSimpITECaches()
+{
   Chat() << "clear ite caches " << endl;
-  for(size_t i = 0, N = d_allocatedConstantLeaves.size(); i < N; ++i){
+  for (size_t i = 0, N = d_allocatedConstantLeaves.size(); i < N; ++i)
+  {
     NodeVec* curr = d_allocatedConstantLeaves[i];
     delete curr;
   }
@@ -597,21 +695,23 @@ void ITESimplifier::clearSimpITECaches(){
   d_simpContextCache.clear();
 }
 
-bool ITESimplifier::doneALotOfWorkHeuristic() const {
+bool ITESimplifier::doneALotOfWorkHeuristic() const
+{
   static const size_t SIZE_BOUND = 1000;
-  Chat() << "d_citeEqConstApplications size " << d_citeEqConstApplications << endl;
+  Chat() << "d_citeEqConstApplications size " << d_citeEqConstApplications
+         << endl;
   return (d_citeEqConstApplications > SIZE_BOUND);
 }
 
-ITESimplifier::Statistics::Statistics():
-  d_maxNonConstantsFolded("ite-simp::maxNonConstantsFolded", 0),
-  d_unexpected("ite-simp::unexpected", 0),
-  d_unsimplified("ite-simp::unsimplified", 0),
-  d_exactMatchFold("ite-simp::exactMatchFold", 0),
-  d_binaryPredFold("ite-simp::binaryPredFold", 0),
-  d_specialEqualityFolds("ite-simp::specialEqualityFolds", 0),
-  d_simpITEVisits("ite-simp::simpITE.visits", 0),
-  d_inSmaller("ite-simp::inSmaller")
+ITESimplifier::Statistics::Statistics()
+    : d_maxNonConstantsFolded("ite-simp::maxNonConstantsFolded", 0),
+      d_unexpected("ite-simp::unexpected", 0),
+      d_unsimplified("ite-simp::unsimplified", 0),
+      d_exactMatchFold("ite-simp::exactMatchFold", 0),
+      d_binaryPredFold("ite-simp::binaryPredFold", 0),
+      d_specialEqualityFolds("ite-simp::specialEqualityFolds", 0),
+      d_simpITEVisits("ite-simp::simpITE.visits", 0),
+      d_inSmaller("ite-simp::inSmaller")
 {
   smtStatisticsRegistry()->registerStat(&d_maxNonConstantsFolded);
   smtStatisticsRegistry()->registerStat(&d_unexpected);
@@ -623,7 +723,8 @@ ITESimplifier::Statistics::Statistics():
   smtStatisticsRegistry()->registerStat(&d_inSmaller);
 }
 
-ITESimplifier::Statistics::~Statistics(){
+ITESimplifier::Statistics::~Statistics()
+{
   smtStatisticsRegistry()->unregisterStat(&d_maxNonConstantsFolded);
   smtStatisticsRegistry()->unregisterStat(&d_unexpected);
   smtStatisticsRegistry()->unregisterStat(&d_unsimplified);
@@ -634,29 +735,38 @@ ITESimplifier::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_inSmaller);
 }
 
-bool ITESimplifier::isConstantIte(TNode e){
-  if(e.isConst()){
+bool ITESimplifier::isConstantIte(TNode e)
+{
+  if (e.isConst())
+  {
     return true;
-  }else if(ite::isTermITE(e)){
+  }
+  else if (ite::isTermITE(e))
+  {
     NodeVec* constants = computeConstantLeaves(e);
     return constants != NULL;
-  }else{
+  }
+  else
+  {
     return false;
   }
 }
 
-ITESimplifier::NodeVec* ITESimplifier::computeConstantLeaves(TNode ite){
+ITESimplifier::NodeVec* ITESimplifier::computeConstantLeaves(TNode ite)
+{
   Assert(ite::isTermITE(ite));
   ConstantLeavesMap::const_iterator it = d_constantLeaves.find(ite);
   ConstantLeavesMap::const_iterator end = d_constantLeaves.end();
-  if(it != end){
+  if (it != end)
+  {
     return (*it).second;
   }
   TNode thenB = ite[1];
   TNode elseB = ite[2];
 
   // special case 2 constant children
-  if(thenB.isConst() && elseB.isConst()){
+  if (thenB.isConst() && elseB.isConst())
+  {
     NodeVec* pair = new NodeVec(2);
     d_allocatedConstantLeaves.push_back(pair);
 
@@ -666,8 +776,9 @@ ITESimplifier::NodeVec* ITESimplifier::computeConstantLeaves(TNode ite){
     return pair;
   }
   // At least 1 is an ITE
-  if(!(thenB.isConst() || thenB.getKind() == kind::ITE) ||
-     !(elseB.isConst() || elseB.getKind() == kind::ITE)){
+  if (!(thenB.isConst() || thenB.getKind() == kind::ITE)
+      || !(elseB.isConst() || elseB.getKind() == kind::ITE))
+  {
     // Cannot be a termITE tree
     d_constantLeaves[ite] = NULL;
     return NULL;
@@ -678,29 +789,36 @@ ITESimplifier::NodeVec* ITESimplifier::computeConstantLeaves(TNode ite){
   TNode maybeITE = thenB.isConst() ? thenB : elseB;
 
   NodeVec* defChildren = computeConstantLeaves(definitelyITE);
-  if(defChildren == NULL){
+  if (defChildren == NULL)
+  {
     d_constantLeaves[ite] = NULL;
     return NULL;
   }
 
   NodeVec scratch;
   NodeVec* maybeChildren = NULL;
-  if(maybeITE.getKind() == kind::ITE){
+  if (maybeITE.getKind() == kind::ITE)
+  {
     maybeChildren = computeConstantLeaves(maybeITE);
-  }else{
+  }
+  else
+  {
     scratch.push_back(maybeITE);
     maybeChildren = &scratch;
   }
-  if(maybeChildren == NULL){
+  if (maybeChildren == NULL)
+  {
     d_constantLeaves[ite] = NULL;
     return NULL;
   }
 
-  NodeVec* both = new NodeVec(defChildren->size()+maybeChildren->size());
+  NodeVec* both = new NodeVec(defChildren->size() + maybeChildren->size());
   d_allocatedConstantLeaves.push_back(both);
   NodeVec::iterator newEnd;
-  newEnd = std::set_union(defChildren->begin(), defChildren->end(),
-                          maybeChildren->begin(), maybeChildren->end(),
+  newEnd = std::set_union(defChildren->begin(),
+                          defChildren->end(),
+                          maybeChildren->begin(),
+                          maybeChildren->end(),
                           both->begin());
   both->resize(newEnd - both->begin());
   d_constantLeaves[ite] = both;
@@ -708,7 +826,8 @@ ITESimplifier::NodeVec* ITESimplifier::computeConstantLeaves(TNode ite){
 }
 
 // This is uncached! Better for protoyping or getting limited size examples
-struct IteTreeSearchData{
+struct IteTreeSearchData
+{
   set<Node> visited;
   set<Node> constants;
   set<Node> nonConstants;
@@ -717,60 +836,81 @@ struct IteTreeSearchData{
   int maxDepth;
   bool failure;
   IteTreeSearchData()
-    : maxConstants(-1), maxNonconstants(-1), maxDepth(-1), failure(false)
-  {}
+      : maxConstants(-1), maxNonconstants(-1), maxDepth(-1), failure(false)
+  {
+  }
 };
-void iteTreeSearch(Node e, int depth, IteTreeSearchData& search){
-  if(search.maxDepth >= 0 && depth > search.maxDepth){
+void iteTreeSearch(Node e, int depth, IteTreeSearchData& search)
+{
+  if (search.maxDepth >= 0 && depth > search.maxDepth)
+  {
     search.failure = true;
   }
-  if(search.failure){
+  if (search.failure)
+  {
     return;
   }
-  if(search.visited.find(e) != search.visited.end()){
+  if (search.visited.find(e) != search.visited.end())
+  {
     return;
-  }else{
+  }
+  else
+  {
     search.visited.insert(e);
   }
 
-  if(e.isConst()){
+  if (e.isConst())
+  {
     search.constants.insert(e);
-    if(search.maxConstants >= 0 &&
-       search.constants.size() > (unsigned)search.maxConstants){
+    if (search.maxConstants >= 0
+        && search.constants.size() > (unsigned)search.maxConstants)
+    {
       search.failure = true;
     }
-  }else if(e.getKind() == kind::ITE){
-    iteTreeSearch(e[1], depth+1, search);
-    iteTreeSearch(e[2], depth+1, search);
-  }else{
+  }
+  else if (e.getKind() == kind::ITE)
+  {
+    iteTreeSearch(e[1], depth + 1, search);
+    iteTreeSearch(e[2], depth + 1, search);
+  }
+  else
+  {
     search.nonConstants.insert(e);
-    if(search.maxNonconstants >= 0 &&
-       search.nonConstants.size() > (unsigned)search.maxNonconstants){
+    if (search.maxNonconstants >= 0
+        && search.nonConstants.size() > (unsigned)search.maxNonconstants)
+    {
       search.failure = true;
     }
   }
 }
 
-Node ITESimplifier::replaceOver(Node n, Node replaceWith, Node simpVar){
-  if(n == simpVar){
+Node ITESimplifier::replaceOver(Node n, Node replaceWith, Node simpVar)
+{
+  if (n == simpVar)
+  {
     return replaceWith;
-  }else if(n.getNumChildren() == 0){
+  }
+  else if (n.getNumChildren() == 0)
+  {
     return n;
   }
   Assert(n.getNumChildren() > 0);
   Assert(!n.isVar());
 
   pair<Node, Node> p = make_pair(n, replaceWith);
-  if(d_replaceOverCache.find(p) != d_replaceOverCache.end()){
+  if (d_replaceOverCache.find(p) != d_replaceOverCache.end())
+  {
     return d_replaceOverCache[p];
   }
 
   NodeBuilder<> builder(n.getKind());
-  if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+  if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
+  {
     builder << n.getOperator();
   }
   unsigned i = 0;
-  for (; i < n.getNumChildren(); ++ i) {
+  for (; i < n.getNumChildren(); ++i)
+  {
     Node newChild = replaceOver(n[i], replaceWith, simpVar);
     builder << newChild;
   }
@@ -780,10 +920,13 @@ Node ITESimplifier::replaceOver(Node n, Node replaceWith, Node simpVar){
   return result;
 }
 
-Node ITESimplifier::replaceOverTermIte(Node e, Node simpAtom, Node simpVar){
-  if(e.getKind() == kind::ITE){
+Node ITESimplifier::replaceOverTermIte(Node e, Node simpAtom, Node simpVar)
+{
+  if (e.getKind() == kind::ITE)
+  {
     pair<Node, Node> p = make_pair(e, simpAtom);
-    if(d_replaceOverTermIteCache.find(p) != d_replaceOverTermIteCache.end()){
+    if (d_replaceOverTermIteCache.find(p) != d_replaceOverTermIteCache.end())
+    {
       return d_replaceOverTermIteCache[p];
     }
     Assert(!e.getType().isBoolean());
@@ -793,61 +936,72 @@ Node ITESimplifier::replaceOverTermIte(Node e, Node simpAtom, Node simpVar){
     Node newIte = cnd.iteNode(newThen, newElse);
     d_replaceOverTermIteCache[p] = newIte;
     return newIte;
-  }else{
+  }
+  else
+  {
     return replaceOver(simpAtom, e, simpVar);
   }
 }
 
-Node ITESimplifier::attemptLiftEquality(TNode atom){
-  if(atom.getKind() == kind::EQUAL){
+Node ITESimplifier::attemptLiftEquality(TNode atom)
+{
+  if (atom.getKind() == kind::EQUAL)
+  {
     TNode left = atom[0];
     TNode right = atom[1];
-    if((left.getKind() == kind::ITE || right.getKind() == kind::ITE)&&
-       !(left.getKind() == kind::ITE && right.getKind() == kind::ITE)){
-
+    if ((left.getKind() == kind::ITE || right.getKind() == kind::ITE)
+        && !(left.getKind() == kind::ITE && right.getKind() == kind::ITE))
+    {
       // exactly 1 is an ite
-      TNode ite = left.getKind() == kind::ITE ? left :right;
+      TNode ite = left.getKind() == kind::ITE ? left : right;
       TNode notIte = left.getKind() == kind::ITE ? right : left;
 
-      if(notIte == ite[1]){
+      if (notIte == ite[1])
+      {
         ++(d_statistics.d_exactMatchFold);
         return ite[0].iteNode(d_true, notIte.eqNode(ite[2]));
-      }else if(notIte == ite[2]){
+      }
+      else if (notIte == ite[2])
+      {
         ++(d_statistics.d_exactMatchFold);
         return ite[0].iteNode(notIte.eqNode(ite[1]), d_true);
       }
-      if(notIte.isConst() &&
-         (ite[1].isConst() || ite[2].isConst())){
+      if (notIte.isConst() && (ite[1].isConst() || ite[2].isConst()))
+      {
         ++(d_statistics.d_exactMatchFold);
-        return ite[0].iteNode(notIte.eqNode(ite[1]),  notIte.eqNode(ite[2]));
+        return ite[0].iteNode(notIte.eqNode(ite[1]), notIte.eqNode(ite[2]));
       }
     }
   }
 
   // try a similar more relaxed version for non-equality operators
-  if(atom.getMetaKind() == kind::metakind::OPERATOR &&
-     atom.getNumChildren() == 2 &&
-     !atom[1].getType().isBoolean()){
-
+  if (atom.getMetaKind() == kind::metakind::OPERATOR
+      && atom.getNumChildren() == 2 && !atom[1].getType().isBoolean())
+  {
     TNode left = atom[0];
     TNode right = atom[1];
-    if( (left.getKind() == kind::ITE || right.getKind() == kind::ITE)&&
-       !(left.getKind() == kind::ITE && right.getKind() == kind::ITE)){
+    if ((left.getKind() == kind::ITE || right.getKind() == kind::ITE)
+        && !(left.getKind() == kind::ITE && right.getKind() == kind::ITE))
+    {
       // exactly 1 is an ite
       bool leftIsIte = left.getKind() == kind::ITE;
-      Node ite = leftIsIte ? left :right;
+      Node ite = leftIsIte ? left : right;
       Node notIte = leftIsIte ? right : left;
 
-      if(notIte.isConst()){
+      if (notIte.isConst())
+      {
         IteTreeSearchData search;
         search.maxNonconstants = 2;
         iteTreeSearch(ite, 0, search);
-        if(!search.failure){
-          d_statistics.d_maxNonConstantsFolded.maxAssign(search.nonConstants.size());
-          Debug("ite::simpite") << "used " << search.nonConstants.size() << " nonconstants" << endl;
+        if (!search.failure)
+        {
+          d_statistics.d_maxNonConstantsFolded.maxAssign(
+              search.nonConstants.size());
+          Debug("ite::simpite") << "used " << search.nonConstants.size()
+                                << " nonconstants" << endl;
           NodeManager* nm = NodeManager::currentNM();
           Node simpVar = getSimpVar(notIte.getType());
-          TNode newLeft = leftIsIte  ? simpVar : notIte;
+          TNode newLeft = leftIsIte ? simpVar : notIte;
           TNode newRight = leftIsIte ? notIte : simpVar;
           Node newAtom = nm->mkNode(atom.getKind(), newLeft, newRight);
 
@@ -859,18 +1013,16 @@ Node ITESimplifier::attemptLiftEquality(TNode atom){
   }
 
   // TODO "This is way too tailored. Must generalize!"
-  if(atom.getKind() == kind::EQUAL &&
-     atom.getNumChildren() == 2 &&
-     ite::isTermITE(atom[0]) &&
-     atom[1].getKind() == kind::MULT &&
-     atom[1].getNumChildren() == 2 &&
-     atom[1][0].isConst() &&
-     atom[1][0].getConst<Rational>().isNegativeOne() &&
-     ite::isTermITE(atom[1][1]) &&
-     d_termITEHeight.termITEHeight(atom[0]) == 1 &&
-     d_termITEHeight.termITEHeight(atom[1][1]) == 1 &&
-     (atom[0][1].isConst() || atom[0][2].isConst()) &&
-     (atom[1][1][1].isConst() || atom[1][1][2].isConst()) ){
+  if (atom.getKind() == kind::EQUAL && atom.getNumChildren() == 2
+      && ite::isTermITE(atom[0]) && atom[1].getKind() == kind::MULT
+      && atom[1].getNumChildren() == 2 && atom[1][0].isConst()
+      && atom[1][0].getConst<Rational>().isNegativeOne()
+      && ite::isTermITE(atom[1][1])
+      && d_termITEHeight.termITEHeight(atom[0]) == 1
+      && d_termITEHeight.termITEHeight(atom[1][1]) == 1
+      && (atom[0][1].isConst() || atom[0][2].isConst())
+      && (atom[1][1][1].isConst() || atom[1][1][2].isConst()))
+  {
     // expand all 4 cases
 
     Node negOne = atom[1][0];
@@ -908,17 +1060,22 @@ Node ITESimplifier::attemptLiftEquality(TNode atom){
 // Interesting classes of atoms:
 // 2. Contains constants and 1 constant term ite
 // 3. Contains 2 constant term ites
-Node ITESimplifier::transformAtom(TNode atom){
-  if(! d_containsVisitor->containsTermITE(atom)){
-    if(atom.getKind() == kind::EQUAL &&
-       atom[0].isConst() && atom[1].isConst()){
+Node ITESimplifier::transformAtom(TNode atom)
+{
+  if (!d_containsVisitor->containsTermITE(atom))
+  {
+    if (atom.getKind() == kind::EQUAL && atom[0].isConst() && atom[1].isConst())
+    {
       // constant equality
       return NodeManager::currentNM()->mkConst<bool>(atom[0] == atom[1]);
     }
     return Node::null();
-  }else{
+  }
+  else
+  {
     Node acr = attemptConstantRemoval(atom);
-    if(!acr.isNull()){
+    if (!acr.isNull())
+    {
       return acr;
     }
     // Node ale = attemptLiftEquality(atom);
@@ -933,20 +1090,27 @@ static unsigned numBranches = 0;
 static unsigned numFalseBranches = 0;
 static unsigned itesMade = 0;
 
-Node ITESimplifier::constantIteEqualsConstant(TNode cite, TNode constant){
+Node ITESimplifier::constantIteEqualsConstant(TNode cite, TNode constant)
+{
   static int instance = 0;
   ++instance;
-  Debug("ite::constantIteEqualsConstant") << instance << "constantIteEqualsConstant("<<cite << ", " << constant<<")"<< endl;
-  if(cite.isConst()){
+  Debug("ite::constantIteEqualsConstant")
+      << instance << "constantIteEqualsConstant(" << cite << ", " << constant
+      << ")" << endl;
+  if (cite.isConst())
+  {
     Node res = (cite == constant) ? d_true : d_false;
     Debug("ite::constantIteEqualsConstant") << instance << "->" << res << endl;
     return res;
   }
-  std::pair<Node,Node> pair = make_pair(cite, constant);
+  std::pair<Node, Node> pair = make_pair(cite, constant);
 
-  NodePairMap::const_iterator eq_pos = d_constantIteEqualsConstantCache.find(pair);
-  if(eq_pos != d_constantIteEqualsConstantCache.end()){
-    Debug("ite::constantIteEqualsConstant") << instance << "->" << (*eq_pos).second << endl;
+  NodePairMap::const_iterator eq_pos =
+      d_constantIteEqualsConstantCache.find(pair);
+  if (eq_pos != d_constantIteEqualsConstantCache.end())
+  {
+    Debug("ite::constantIteEqualsConstant")
+        << instance << "->" << (*eq_pos).second << endl;
     return (*eq_pos).second;
   }
 
@@ -954,13 +1118,18 @@ Node ITESimplifier::constantIteEqualsConstant(TNode cite, TNode constant){
 
   NodeVec* leaves = computeConstantLeaves(cite);
   Assert(leaves != NULL);
-  if(std::binary_search(leaves->begin(), leaves->end(), constant)){
-    if(leaves->size() == 1){
+  if (std::binary_search(leaves->begin(), leaves->end(), constant))
+  {
+    if (leaves->size() == 1)
+    {
       // probably unreachable
       d_constantIteEqualsConstantCache[pair] = d_true;
-      Debug("ite::constantIteEqualsConstant") << instance << "->" << d_true << endl;
+      Debug("ite::constantIteEqualsConstant")
+          << instance << "->" << d_true << endl;
       return d_true;
-    }else{
+    }
+    else
+    {
       Assert(cite.getKind() == kind::ITE);
       TNode cnd = cite[0];
       TNode tB = cite[1];
@@ -968,42 +1137,48 @@ Node ITESimplifier::constantIteEqualsConstant(TNode cite, TNode constant){
       Node tEqs = constantIteEqualsConstant(tB, constant);
       Node fEqs = constantIteEqualsConstant(fB, constant);
       Node boolIte = cnd.iteNode(tEqs, fEqs);
-      if(!(tEqs.isConst() || fEqs.isConst())){
+      if (!(tEqs.isConst() || fEqs.isConst()))
+      {
         ++numBranches;
       }
-      if(!(tEqs == d_false || fEqs == d_false)){
+      if (!(tEqs == d_false || fEqs == d_false))
+      {
         ++numFalseBranches;
       }
       ++itesMade;
       d_constantIteEqualsConstantCache[pair] = boolIte;
-      //Debug("ite::constantIteEqualsConstant") << instance << "->" << boolIte << endl;
+      // Debug("ite::constantIteEqualsConstant") << instance << "->" << boolIte
+      // << endl;
       return boolIte;
     }
-  }else{
+  }
+  else
+  {
     d_constantIteEqualsConstantCache[pair] = d_false;
-    Debug("ite::constantIteEqualsConstant") << instance << "->" << d_false << endl;
+    Debug("ite::constantIteEqualsConstant")
+        << instance << "->" << d_false << endl;
     return d_false;
   }
 }
 
-
-Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite){
+Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite)
+{
   // intersect the constant ite trees lcite and rcite
 
-  if(lcite.isConst() || rcite.isConst()){
+  if (lcite.isConst() || rcite.isConst())
+  {
     bool lIsConst = lcite.isConst();
     TNode constant = lIsConst ? lcite : rcite;
     TNode cite = lIsConst ? rcite : lcite;
 
-    (d_statistics.d_inSmaller)<< 1;
+    (d_statistics.d_inSmaller) << 1;
     unsigned preItesMade = itesMade;
     unsigned preNumBranches = numBranches;
     unsigned preNumFalseBranches = numFalseBranches;
     Node bterm = constantIteEqualsConstant(cite, constant);
-    Debug("intersectConstantIte")
-      << (numBranches - preNumBranches)
-      << " " << (numFalseBranches - preNumFalseBranches)
-      << " " << (itesMade - preItesMade) << endl;
+    Debug("intersectConstantIte") << (numBranches - preNumBranches) << " "
+                                  << (numFalseBranches - preNumFalseBranches)
+                                  << " " << (itesMade - preItesMade) << endl;
     return bterm;
   }
   Assert(lcite.getKind() == kind::ITE);
@@ -1014,19 +1189,25 @@ Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite){
 
   uint32_t smaller = std::min(leftValues->size(), rightValues->size());
 
-  (d_statistics.d_inSmaller)<< smaller;
+  (d_statistics.d_inSmaller) << smaller;
   NodeVec intersection(smaller, Node::null());
   NodeVec::iterator newEnd;
-  newEnd = std::set_intersection(leftValues->begin(), leftValues->end(),
-                                 rightValues->begin(), rightValues->end(),
+  newEnd = std::set_intersection(leftValues->begin(),
+                                 leftValues->end(),
+                                 rightValues->begin(),
+                                 rightValues->end(),
                                  intersection.begin());
   intersection.resize(newEnd - intersection.begin());
-  if(intersection.empty()){
+  if (intersection.empty())
+  {
     return d_false;
-  }else{
+  }
+  else
+  {
     NodeBuilder<> nb(kind::OR);
-    NodeVec::const_iterator it = intersection.begin(), end=intersection.end();
-    for(; it != end; ++it){
+    NodeVec::const_iterator it = intersection.begin(), end = intersection.end();
+    for (; it != end; ++it)
+    {
       Node inBoth = *it;
       Node lefteq = constantIteEqualsConstant(lcite, inBoth);
       Node righteq = constantIteEqualsConstant(rcite, inBoth);
@@ -1038,33 +1219,40 @@ Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite){
   }
 }
 
-
-Node ITESimplifier::attemptEagerRemoval(TNode atom){
-  if(atom.getKind() == kind::EQUAL){
+Node ITESimplifier::attemptEagerRemoval(TNode atom)
+{
+  if (atom.getKind() == kind::EQUAL)
+  {
     TNode left = atom[0];
     TNode right = atom[1];
-    if((left.isConst() &&
-        right.getKind() == kind::ITE && isConstantIte(right)) ||
-       (right.isConst() &&
-        left.getKind() == kind::ITE && isConstantIte(left))){
+    if ((left.isConst() && right.getKind() == kind::ITE && isConstantIte(right))
+        || (right.isConst() && left.getKind() == kind::ITE
+            && isConstantIte(left)))
+    {
       TNode constant = left.isConst() ? left : right;
       TNode cite = left.isConst() ? right : left;
 
-      std::pair<Node,Node> pair = make_pair(cite, constant);
-      NodePairMap::const_iterator eq_pos = d_constantIteEqualsConstantCache.find(pair);
-      if(eq_pos != d_constantIteEqualsConstantCache.end()){
+      std::pair<Node, Node> pair = make_pair(cite, constant);
+      NodePairMap::const_iterator eq_pos =
+          d_constantIteEqualsConstantCache.find(pair);
+      if (eq_pos != d_constantIteEqualsConstantCache.end())
+      {
         Node ret = (*eq_pos).second;
-        if(ret.isConst()){
+        if (ret.isConst())
+        {
           return ret;
-        }else{
+        }
+        else
+        {
           return Node::null();
         }
       }
 
       NodeVec* leaves = computeConstantLeaves(cite);
       Assert(leaves != NULL);
-      if(!std::binary_search(leaves->begin(), leaves->end(), constant)){
-        std::pair<Node,Node> pair = make_pair(cite, constant);
+      if (!std::binary_search(leaves->begin(), leaves->end(), constant))
+      {
+        std::pair<Node, Node> pair = make_pair(cite, constant);
         d_constantIteEqualsConstantCache[pair] = d_false;
         return d_false;
       }
@@ -1073,33 +1261,38 @@ Node ITESimplifier::attemptEagerRemoval(TNode atom){
   return Node::null();
 }
 
-Node ITESimplifier::attemptConstantRemoval(TNode atom){
-  if(atom.getKind() == kind::EQUAL){
+Node ITESimplifier::attemptConstantRemoval(TNode atom)
+{
+  if (atom.getKind() == kind::EQUAL)
+  {
     TNode left = atom[0];
     TNode right = atom[1];
-    if(isConstantIte(left) && isConstantIte(right)){
+    if (isConstantIte(left) && isConstantIte(right))
+    {
       return intersectConstantIte(left, right);
     }
   }
   return Node::null();
 }
 
-
-bool ITESimplifier::leavesAreConst(TNode e, TheoryId tid)
+bool ITESimplifier::leavesAreConst(TNode e, theory::TheoryId tid)
 {
-  Assert((e.getKind() == kind::ITE && !e.getType().isBoolean()) ||
-         Theory::theoryOf(e) != THEORY_BOOL);
-  if (e.isConst()) {
+  Assert((e.getKind() == kind::ITE && !e.getType().isBoolean())
+         || theory::Theory::theoryOf(e) != theory::THEORY_BOOL);
+  if (e.isConst())
+  {
     return true;
   }
 
   unordered_map<Node, bool, NodeHashFunction>::iterator it;
   it = d_leavesConstCache.find(e);
-  if (it != d_leavesConstCache.end()) {
+  if (it != d_leavesConstCache.end())
+  {
     return (*it).second;
   }
 
-  if (!containsTermITE(e) && Theory::isLeafOf(e, tid)) {
+  if (!containsTermITE(e) && theory::Theory::isLeafOf(e, tid))
+  {
     d_leavesConstCache[e] = false;
     return false;
   }
@@ -1107,12 +1300,15 @@ bool ITESimplifier::leavesAreConst(TNode e, TheoryId tid)
   Assert(e.getNumChildren() > 0);
   size_t k = 0, sz = e.getNumChildren();
 
-  if (e.getKind() == kind::ITE) {
+  if (e.getKind() == kind::ITE)
+  {
     k = 1;
   }
 
-  for (; k < sz; ++k) {
-    if (!leavesAreConst(e[k], tid)) {
+  for (; k < sz; ++k)
+  {
+    if (!leavesAreConst(e[k], tid))
+    {
       d_leavesConstCache[e] = false;
       return false;
     }
@@ -1121,35 +1317,42 @@ bool ITESimplifier::leavesAreConst(TNode e, TheoryId tid)
   return true;
 }
 
-
-Node ITESimplifier::simpConstants(TNode simpContext, TNode iteNode, TNode simpVar)
+Node ITESimplifier::simpConstants(TNode simpContext,
+                                  TNode iteNode,
+                                  TNode simpVar)
 {
   NodePairMap::iterator it;
-  it = d_simpConstCache.find(pair<Node, Node>(simpContext,iteNode));
-  if (it != d_simpConstCache.end()) {
+  it = d_simpConstCache.find(pair<Node, Node>(simpContext, iteNode));
+  if (it != d_simpConstCache.end())
+  {
     return (*it).second;
   }
 
-  if (iteNode.getKind() == kind::ITE) {
+  if (iteNode.getKind() == kind::ITE)
+  {
     NodeBuilder<> builder(kind::ITE);
     builder << iteNode[0];
     unsigned i = 1;
-    for (; i < iteNode.getNumChildren(); ++ i) {
+    for (; i < iteNode.getNumChildren(); ++i)
+    {
       Node n = simpConstants(simpContext, iteNode[i], simpVar);
-      if (n.isNull()) {
+      if (n.isNull())
+      {
         return n;
       }
       builder << n;
     }
     // Mark the substitution and continue
     Node result = builder;
-    result = Rewriter::rewrite(result);
+    result = theory::Rewriter::rewrite(result);
     d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = result;
     return result;
   }
 
-  if (!containsTermITE(iteNode)) {
-    Node n = Rewriter::rewrite(simpContext.substitute(simpVar, iteNode));
+  if (!containsTermITE(iteNode))
+  {
+    Node n =
+        theory::Rewriter::rewrite(simpContext.substitute(simpVar, iteNode));
     d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
     return n;
   }
@@ -1158,11 +1361,13 @@ Node ITESimplifier::simpConstants(TNode simpContext, TNode iteNode, TNode simpVa
   Node simpVar2;
   d_simpContextCache.clear();
   Node simpContext2 = createSimpContext(iteNode, iteNode2, simpVar2);
-  if (!simpContext2.isNull()) {
+  if (!simpContext2.isNull())
+  {
     Assert(!iteNode2.isNull());
     simpContext2 = simpContext.substitute(simpVar, simpContext2);
     Node n = simpConstants(simpContext2, iteNode2, simpVar2);
-    if (n.isNull()) {
+    if (n.isNull())
+    {
       return n;
     }
     d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
@@ -1171,43 +1376,49 @@ Node ITESimplifier::simpConstants(TNode simpContext, TNode iteNode, TNode simpVa
   return Node();
 }
 
-
 Node ITESimplifier::getSimpVar(TypeNode t)
 {
   std::unordered_map<TypeNode, Node, TypeNode::HashFunction>::iterator it;
   it = d_simpVars.find(t);
-  if (it != d_simpVars.end()) {
+  if (it != d_simpVars.end())
+  {
     return (*it).second;
   }
-  else {
-    Node var = NodeManager::currentNM()->mkSkolem("iteSimp", t, "is a variable resulting from ITE simplification");
+  else
+  {
+    Node var = NodeManager::currentNM()->mkSkolem(
+        "iteSimp", t, "is a variable resulting from ITE simplification");
     d_simpVars[t] = var;
     return var;
   }
 }
 
-
 Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar)
 {
   NodeMap::iterator it;
   it = d_simpContextCache.find(c);
-  if (it != d_simpContextCache.end()) {
+  if (it != d_simpContextCache.end())
+  {
     return (*it).second;
   }
 
-  if (!containsTermITE(c)) {
+  if (!containsTermITE(c))
+  {
     d_simpContextCache[c] = c;
     return c;
   }
 
-  if (c.getKind() == kind::ITE && !c.getType().isBoolean()) {
+  if (c.getKind() == kind::ITE && !c.getType().isBoolean())
+  {
     // Currently only support one ite node in a simp context
     // Return Null if more than one is found
-    if (!iteNode.isNull()) {
+    if (!iteNode.isNull())
+    {
       return Node();
     }
     simpVar = getSimpVar(c.getType());
-    if (simpVar.isNull()) {
+    if (simpVar.isNull())
+    {
       return Node();
     }
     d_simpContextCache[c] = simpVar;
@@ -1216,13 +1427,16 @@ Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar)
   }
 
   NodeBuilder<> builder(c.getKind());
-  if (c.getMetaKind() == kind::metakind::PARAMETERIZED) {
+  if (c.getMetaKind() == kind::metakind::PARAMETERIZED)
+  {
     builder << c.getOperator();
   }
   unsigned i = 0;
-  for (; i < c.getNumChildren(); ++ i) {
+  for (; i < c.getNumChildren(); ++i)
+  {
     Node newChild = createSimpContext(c[i], iteNode, simpVar);
-    if (newChild.isNull()) {
+    if (newChild.isNull())
+    {
       return newChild;
     }
     builder << newChild;
@@ -1233,20 +1447,25 @@ Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar)
   return result;
 }
 typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
-void countReachable_(Node x, Kind k, NodeSet& visited, uint32_t& reached){
-  if(visited.find(x) != visited.end()){
+void countReachable_(Node x, Kind k, NodeSet& visited, uint32_t& reached)
+{
+  if (visited.find(x) != visited.end())
+  {
     return;
   }
   visited.insert(x);
-  if(x.getKind() == k){
+  if (x.getKind() == k)
+  {
     ++reached;
   }
-  for(unsigned i =0, N=x.getNumChildren(); i < N; ++i){
+  for (unsigned i = 0, N = x.getNumChildren(); i < N; ++i)
+  {
     countReachable_(x[i], k, visited, reached);
   }
 }
 
-uint32_t countReachable(TNode x, Kind k){
+uint32_t countReachable(TNode x, Kind k)
+{
   NodeSet visited;
   uint32_t reached = 0;
   countReachable_(x, k, visited, reached);
@@ -1259,34 +1478,39 @@ Node ITESimplifier::simpITEAtom(TNode atom)
   Debug("ite::atom") << "still simplifying " << (++instance) << endl;
   Node attempt = transformAtom(atom);
   Debug("ite::atom") << "  finished " << instance << endl;
-  if(!attempt.isNull()){
-    Node rewritten = Rewriter::rewrite(attempt);
+  if (!attempt.isNull())
+  {
+    Node rewritten = theory::Rewriter::rewrite(attempt);
     Debug("ite::print-success")
-      << instance << " "
-      << "rewriting " << countReachable(rewritten, kind::ITE)
-      <<  " from " <<  countReachable(atom, kind::ITE) << endl
-      << "\t rewritten " << rewritten << endl
-      << "\t input " << atom << endl;
+        << instance << " "
+        << "rewriting " << countReachable(rewritten, kind::ITE) << " from "
+        << countReachable(atom, kind::ITE) << endl
+        << "\t rewritten " << rewritten << endl
+        << "\t input " << atom << endl;
     return rewritten;
   }
 
-  if (leavesAreConst(atom)) {
+  if (leavesAreConst(atom))
+  {
     Node iteNode;
     Node simpVar;
     d_simpContextCache.clear();
     Node simpContext = createSimpContext(atom, iteNode, simpVar);
-    if (!simpContext.isNull()) {
-      if (iteNode.isNull()) {
+    if (!simpContext.isNull())
+    {
+      if (iteNode.isNull())
+      {
         Assert(leavesAreConst(simpContext) && !containsTermITE(simpContext));
         ++(d_statistics.d_unexpected);
         Debug("ite::simpite") << instance << " "
                               << "how about?" << atom << endl;
         Debug("ite::simpite") << instance << " "
                               << "\t" << simpContext << endl;
-        return Rewriter::rewrite(simpContext);
+        return theory::Rewriter::rewrite(simpContext);
       }
       Node n = simpConstants(simpContext, iteNode, simpVar);
-      if (!n.isNull()) {
+      if (!n.isNull())
+      {
         ++(d_statistics.d_unexpected);
         Debug("ite::simpite") << instance << " "
                               << "here?" << atom << endl;
@@ -1296,8 +1520,10 @@ Node ITESimplifier::simpITEAtom(TNode atom)
       }
     }
   }
-  if(Debug.isOn("ite::simpite")){
-    if(countReachable(atom, kind::ITE) > 0){
+  if (Debug.isOn("ite::simpite"))
+  {
+    if (countReachable(atom, kind::ITE) > 0)
+    {
       Debug("ite::simpite") << instance << " "
                             << "remaining " << atom << endl;
     }
@@ -1306,14 +1532,12 @@ Node ITESimplifier::simpITEAtom(TNode atom)
   return atom;
 }
 
-
-struct preprocess_stack_element {
+struct preprocess_stack_element
+{
   TNode node;
   bool children_added;
-  preprocess_stack_element(TNode node)
-  : node(node), children_added(false) {}
-};/* struct preprocess_stack_element */
-
+  preprocess_stack_element(TNode node) : node(node), children_added(false) {}
+}; /* struct preprocess_stack_element */
 
 Node ITESimplifier::simpITE(TNode assertion)
 {
@@ -1327,35 +1551,42 @@ Node ITESimplifier::simpITE(TNode assertion)
 
   while (!toVisit.empty())
   {
-    iteration ++;
-    //cout << "call  " << call << " : " << iteration << endl;
+    iteration++;
+    // cout << "call  " << call << " : " << iteration << endl;
     // The current node we are processing
     preprocess_stack_element& stackHead = toVisit.back();
     TNode current = stackHead.node;
 
-    // If node has no ITE's or already in the cache we're done, pop from the stack
-    if (current.getNumChildren() == 0 ||
-        (Theory::theoryOf(current) != THEORY_BOOL && !containsTermITE(current))) {
-       d_simpITECache[current] = current;
-       ++(d_statistics.d_simpITEVisits);
-       toVisit.pop_back();
-       continue;
+    // If node has no ITE's or already in the cache we're done, pop from the
+    // stack
+    if (current.getNumChildren() == 0
+        || (theory::Theory::theoryOf(current) != theory::THEORY_BOOL
+            && !containsTermITE(current)))
+    {
+      d_simpITECache[current] = current;
+      ++(d_statistics.d_simpITEVisits);
+      toVisit.pop_back();
+      continue;
     }
 
     NodeMap::iterator find = d_simpITECache.find(current);
-    if (find != d_simpITECache.end()) {
+    if (find != d_simpITECache.end())
+    {
       toVisit.pop_back();
       continue;
     }
 
     // Not yet substituted, so process
-    if (stackHead.children_added) {
+    if (stackHead.children_added)
+    {
       // Children have been processed, so substitute
       NodeBuilder<> builder(current.getKind());
-      if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
+      if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
+      {
         builder << current.getOperator();
       }
-      for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
+      for (unsigned i = 0; i < current.getNumChildren(); ++i)
+      {
         Assert(d_simpITECache.find(current[i]) != d_simpITECache.end());
         Node child = current[i];
         Node childRes = d_simpITECache[current[i]];
@@ -1365,8 +1596,9 @@ Node ITESimplifier::simpITE(TNode assertion)
       Node result = builder;
 
       // If this is an atom, we process it
-      if (Theory::theoryOf(result) != THEORY_BOOL &&
-          result.getType().isBoolean()) {
+      if (theory::Theory::theoryOf(result) != theory::THEORY_BOOL
+          && result.getType().isBoolean())
+      {
         result = simpITEAtom(result);
       }
 
@@ -1375,23 +1607,32 @@ Node ITESimplifier::simpITE(TNode assertion)
       //   //cout << instance << " " << result << current << endl;
       // }
 
-      result = Rewriter::rewrite(result);
+      result = theory::Rewriter::rewrite(result);
       d_simpITECache[current] = result;
       ++(d_statistics.d_simpITEVisits);
       toVisit.pop_back();
-    } else {
+    }
+    else
+    {
       // Mark that we have added the children if any
-      if (current.getNumChildren() > 0) {
+      if (current.getNumChildren() > 0)
+      {
         stackHead.children_added = true;
         // We need to add the children
-        for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
+        for (TNode::iterator child_it = current.begin();
+             child_it != current.end();
+             ++child_it)
+        {
           TNode childNode = *child_it;
           NodeMap::iterator childFind = d_simpITECache.find(childNode);
-          if (childFind == d_simpITECache.end()) {
+          if (childFind == d_simpITECache.end())
+          {
             toVisit.push_back(childNode);
           }
         }
-      } else {
+      }
+      else
+      {
         // No children, so we're done
         d_simpITECache[current] = current;
         ++(d_statistics.d_simpITEVisits);
@@ -1402,31 +1643,33 @@ Node ITESimplifier::simpITE(TNode assertion)
   return d_simpITECache[assertion];
 }
 
-ITECareSimplifier::ITECareSimplifier()
-    : d_careSetsOutstanding(0)
-    , d_usedSets()
+ITECareSimplifier::ITECareSimplifier() : d_careSetsOutstanding(0), d_usedSets()
 {
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 }
 
-ITECareSimplifier::~ITECareSimplifier(){
+ITECareSimplifier::~ITECareSimplifier()
+{
   Assert(d_usedSets.empty());
   Assert(d_careSetsOutstanding == 0);
 }
 
-void ITECareSimplifier::clear(){
+void ITECareSimplifier::clear()
+{
   Assert(d_usedSets.empty());
   Assert(d_careSetsOutstanding == 0);
 }
 
 ITECareSimplifier::CareSetPtr ITECareSimplifier::getNewSet()
 {
-  if (d_usedSets.empty()) {
+  if (d_usedSets.empty())
+  {
     d_careSetsOutstanding++;
     return ITECareSimplifier::CareSetPtr::mkNew(*this);
   }
-  else {
+  else
+  {
     ITECareSimplifier::CareSetPtr cs =
         ITECareSimplifier::CareSetPtr::recycle(d_usedSets.back());
     cs.getCareSet().clear();
@@ -1435,54 +1678,62 @@ ITECareSimplifier::CareSetPtr ITECareSimplifier::getNewSet()
   }
 }
 
-
 void ITECareSimplifier::updateQueue(CareMap& queue,
                                     TNode e,
                                     ITECareSimplifier::CareSetPtr& careSet)
 {
   CareMap::iterator it = queue.find(e), iend = queue.end();
-  if (it != iend) {
+  if (it != iend)
+  {
     set<Node>& cs2 = (*it).second.getCareSet();
     ITECareSimplifier::CareSetPtr csNew = getNewSet();
     set_intersection(careSet.getCareSet().begin(),
                      careSet.getCareSet().end(),
-                     cs2.begin(), cs2.end(),
+                     cs2.begin(),
+                     cs2.end(),
                      inserter(csNew.getCareSet(), csNew.getCareSet().begin()));
     (*it).second = csNew;
   }
-  else {
+  else
+  {
     queue[e] = careSet;
   }
 }
 
-
-Node ITECareSimplifier::substitute(TNode e, TNodeMap& substTable, TNodeMap& cache)
+Node ITECareSimplifier::substitute(TNode e,
+                                   TNodeMap& substTable,
+                                   TNodeMap& cache)
 {
   TNodeMap::iterator it = cache.find(e), iend = cache.end();
-  if (it != iend) {
+  if (it != iend)
+  {
     return it->second;
   }
 
   // do substitution?
   it = substTable.find(e);
   iend = substTable.end();
-  if (it != iend) {
+  if (it != iend)
+  {
     Node result = substitute(it->second, substTable, cache);
     cache[e] = result;
     return result;
   }
 
   size_t sz = e.getNumChildren();
-  if (sz == 0) {
+  if (sz == 0)
+  {
     cache[e] = e;
     return e;
   }
 
   NodeBuilder<> builder(e.getKind());
-  if (e.getMetaKind() == kind::metakind::PARAMETERIZED) {
+  if (e.getMetaKind() == kind::metakind::PARAMETERIZED)
+  {
     builder << e.getOperator();
   }
-  for (unsigned i = 0; i < e.getNumChildren(); ++ i) {
+  for (unsigned i = 0; i < e.getNumChildren(); ++i)
+  {
     builder << substitute(e[i], substTable, cache);
   }
 
@@ -1495,7 +1746,6 @@ Node ITECareSimplifier::substitute(TNode e, TNodeMap& substTable, TNodeMap& cach
   return result;
 }
 
-
 Node ITECareSimplifier::simplifyWithCare(TNode e)
 {
   TNodeMap substTable;
@@ -1514,7 +1764,8 @@ Node ITECareSimplifier::simplifyWithCare(TNode e)
     bool done;
     unsigned i;
 
-    while (!queue.empty()) {
+    while (!queue.empty())
+    {
       it = queue.end();
       --it;
       v = it->first;
@@ -1525,19 +1776,24 @@ Node ITECareSimplifier::simplifyWithCare(TNode e)
       done = false;
       set<Node>::iterator iCare, iCareEnd = css.end();
 
-      switch (v.getKind()) {
-        case kind::ITE: {
+      switch (v.getKind())
+      {
+        case kind::ITE:
+        {
           iCare = css.find(v[0]);
-          if (iCare != iCareEnd) {
+          if (iCare != iCareEnd)
+          {
             Assert(substTable.find(v) == substTable.end());
             substTable[v] = v[1];
             updateQueue(queue, v[1], cs);
             done = true;
             break;
           }
-          else {
+          else
+          {
             iCare = css.find(v[0].negate());
-            if (iCare != iCareEnd) {
+            if (iCare != iCareEnd)
+            {
               Assert(substTable.find(v) == substTable.end());
               substTable[v] = v[2];
               updateQueue(queue, v[2], cs);
@@ -1557,10 +1813,13 @@ Node ITECareSimplifier::simplifyWithCare(TNode e)
           done = true;
           break;
         }
-        case kind::AND: {
-          for (i = 0; i < v.getNumChildren(); ++i) {
+        case kind::AND:
+        {
+          for (i = 0; i < v.getNumChildren(); ++i)
+          {
             iCare = css.find(v[i].negate());
-            if (iCare != iCareEnd) {
+            if (iCare != iCareEnd)
+            {
               Assert(substTable.find(v) == substTable.end());
               substTable[v] = d_false;
               done = true;
@@ -1574,16 +1833,20 @@ Node ITECareSimplifier::simplifyWithCare(TNode e)
           cs2 = getNewSet();
           cs2.getCareSet() = css;
           cs2.getCareSet().insert(v[0]);
-          for (i = 1; i < v.getNumChildren(); ++i) {
+          for (i = 1; i < v.getNumChildren(); ++i)
+          {
             updateQueue(queue, v[i], cs2);
           }
           done = true;
           break;
         }
-        case kind::OR: {
-          for (i = 0; i < v.getNumChildren(); ++i) {
+        case kind::OR:
+        {
+          for (i = 0; i < v.getNumChildren(); ++i)
+          {
             iCare = css.find(v[i]);
-            if (iCare != iCareEnd) {
+            if (iCare != iCareEnd)
+            {
               Assert(substTable.find(v) == substTable.end());
               substTable[v] = d_true;
               done = true;
@@ -1597,27 +1860,30 @@ Node ITECareSimplifier::simplifyWithCare(TNode e)
           cs2 = getNewSet();
           cs2.getCareSet() = css;
           cs2.getCareSet().insert(v[0].negate());
-          for (i = 1; i < v.getNumChildren(); ++i) {
+          for (i = 1; i < v.getNumChildren(); ++i)
+          {
             updateQueue(queue, v[i], cs2);
           }
           done = true;
           break;
         }
-        default:
-          break;
+        default: break;
       }
 
-      if (done) {
+      if (done)
+      {
         continue;
       }
 
-      for (unsigned i = 0; i < v.getNumChildren(); ++i) {
+      for (unsigned i = 0; i < v.getNumChildren(); ++i)
+      {
         updateQueue(queue, v[i], cs);
       }
     }
   }
   /* Perform garbage collection. */
-  while (!d_usedSets.empty()) {
+  while (!d_usedSets.empty())
+  {
     CareSetPtrVal* used = d_usedSets.back();
     d_usedSets.pop_back();
     Assert(used->safeToGarbageCollect());
@@ -1631,12 +1897,12 @@ Node ITECareSimplifier::simplifyWithCare(TNode e)
 }
 
 ITECareSimplifier::CareSetPtr ITECareSimplifier::CareSetPtr::mkNew(
-    ITECareSimplifier& simp) {
+    ITECareSimplifier& simp)
+{
   CareSetPtrVal* val = new CareSetPtrVal(simp);
   return CareSetPtr(val);
 }
 
-
-
-} /* namespace theory */
-} /* namespace CVC4 */
+}  // namespace util
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/theory/ite_utilities.h b/src/preprocessing/util/ite_utilities.h
index bfce390eb..e137749db 100644
--- a/src/theory/ite_utilities.h
+++ b/src/preprocessing/util/ite_utilities.h
@@ -2,7 +2,7 @@
 /*! \file ite_utilities.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Paul Meng, Andres Noetzli
+ **   Tim King, Aina Niemetz, Paul Meng
  ** 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.
@@ -14,7 +14,8 @@
  ** This module implements preprocessing phases designed to simplify ITE
  ** expressions.  Based on:
  ** Kim, Somenzi, Jin.  Efficient Term-ITE Conversion for SMT.  FMCAD 2009.
- ** Burch, Jerry.  Techniques for Verifying Superscalar Microprocessors.  DAC '96
+ ** Burch, Jerry.  Techniques for Verifying Superscalar Microprocessors.  DAC
+ *'96
  **/
 
 #include "cvc4_private.h"
@@ -30,7 +31,8 @@
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
-namespace theory {
+namespace preprocessing {
+namespace util {
 
 class IncomingArcCounter;
 class TermITEHeightCounter;
@@ -41,8 +43,9 @@ class ITECareSimplifier;
 /**
  * A caching visitor that computes whether a node contains a term ite.
  */
-class ContainsTermITEVisitor {
-public:
+class ContainsTermITEVisitor
+{
+ public:
   ContainsTermITEVisitor();
   ~ContainsTermITEVisitor();
 
@@ -55,7 +58,7 @@ public:
   /** returns the size of the cache. */
   size_t cache_size() const { return d_cache.size(); }
 
-private:
+ private:
   typedef std::unordered_map<Node, bool, NodeHashFunction> NodeBoolMap;
   NodeBoolMap d_cache;
 };
@@ -94,22 +97,28 @@ class ITEUtilities
   ITECareSimplifier* d_careSimp;
 };
 
-class IncomingArcCounter {
-public:
+class IncomingArcCounter
+{
+ public:
   IncomingArcCounter(bool skipVars = false, bool skipConstants = false);
   ~IncomingArcCounter();
   void computeReachability(const std::vector<Node>& assertions);
 
-  inline uint32_t lookupIncoming(Node n) const {
+  inline uint32_t lookupIncoming(Node n) const
+  {
     NodeCountMap::const_iterator it = d_reachCount.find(n);
-    if(it == d_reachCount.end()){
+    if (it == d_reachCount.end())
+    {
       return 0;
-    }else{
+    }
+    else
+    {
       return (*it).second;
     }
   }
   void clear();
-private:
+
+ private:
   typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
   NodeCountMap d_reachCount;
 
@@ -117,8 +126,9 @@ private:
   bool d_skipConstants;
 };
 
-class TermITEHeightCounter {
-public:
+class TermITEHeightCounter
+{
+ public:
   TermITEHeightCounter();
   ~TermITEHeightCounter();
 
@@ -130,7 +140,8 @@ public:
    *  - termITEHeight(leaves) = 0
    *  - termITEHeight(e: term-ite(c, t, e) ) =
    *     1 + max(termITEHeight(t), termITEHeight(e)) ; Don't include c
-   *  - termITEHeight(e not term ite) = max_{c in children(e)) (termITEHeight(c))
+   *  - termITEHeight(e not term ite) = max_{c in children(e))
+   * (termITEHeight(c))
    */
   uint32_t termITEHeight(TNode e);
 
@@ -140,7 +151,7 @@ public:
   /** Size of the cache. */
   size_t cache_size() const;
 
-private:
+ private:
   typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
   NodeCountMap d_termITEHeight;
 }; /* class TermITEHeightCounter */
@@ -149,8 +160,9 @@ private:
  * A routine designed to undo the potentially large blow up
  * due to expansion caused by the ite simplifier.
  */
-class ITECompressor {
-public:
+class ITECompressor
+{
+ public:
   ITECompressor(ContainsTermITEVisitor* contains);
   ~ITECompressor();
 
@@ -160,9 +172,8 @@ public:
   /* garbage Collects the compressor. */
   void garbageCollect();
 
-private:
-
-  Node d_true; /* Copy of true. */
+ private:
+  Node d_true;  /* Copy of true. */
   Node d_false; /* Copy of false. */
   ContainsTermITEVisitor* d_contains;
   std::vector<Node>* d_assertions;
@@ -179,8 +190,9 @@ private:
   Node compressTerm(Node toCompress);
   Node compressBoolean(Node toCompress);
 
-  class Statistics {
-  public:
+  class Statistics
+  {
+   public:
     IntStat d_compressCalls;
     IntStat d_skolemsAdded;
     Statistics();
@@ -189,8 +201,9 @@ private:
   Statistics d_statistics;
 }; /* class ITECompressor */
 
-class ITESimplifier {
-public:
+class ITESimplifier
+{
+ public:
   ITESimplifier(ContainsTermITEVisitor* d_containsVisitor);
   ~ITESimplifier();
 
@@ -199,16 +212,18 @@ public:
   bool doneALotOfWorkHeuristic() const;
   void clearSimpITECaches();
 
-private:
+ private:
   Node d_true;
   Node d_false;
 
   ContainsTermITEVisitor* d_containsVisitor;
-  inline bool containsTermITE(TNode n) {
+  inline bool containsTermITE(TNode n)
+  {
     return d_containsVisitor->containsTermITE(n);
   }
   TermITEHeightCounter d_termITEHeight;
-  inline uint32_t termITEHeight(TNode e) {
+  inline uint32_t termITEHeight(TNode e)
+  {
     return d_termITEHeight.termITEHeight(e);
   }
 
@@ -216,7 +231,8 @@ private:
   //     constant
   // or  termITE(cnd, ConstantIte, ConstantIte)
   typedef std::vector<Node> NodeVec;
-  typedef std::unordered_map<Node, NodeVec*, NodeHashFunction > ConstantLeavesMap;
+  typedef std::unordered_map<Node, NodeVec*, NodeHashFunction>
+      ConstantLeavesMap;
   ConstantLeavesMap d_constantLeaves;
 
   // d_constantLeaves satisfies the following invariants:
@@ -224,7 +240,8 @@ private:
   // containsTermITE(x):
   // - not isKey(x) then this value is uncomputed
   // - d_constantLeaves[x] == NULL, then this contains a non-constant leaf
-  // - d_constantLeaves[x] != NULL, then this contains a sorted list of constant leaf
+  // - d_constantLeaves[x] != NULL, then this contains a sorted list of constant
+  // leaf
   bool isConstantIte(TNode e);
 
   /** If its not a constant and containsTermITE(ite),
@@ -234,7 +251,6 @@ private:
   // Lists all of the vectors in d_constantLeaves for fast deletion.
   std::vector<NodeVec*> d_allocatedConstantLeaves;
 
-
   /* transforms */
   Node transformAtom(TNode atom);
   Node attemptConstantRemoval(TNode atom);
@@ -276,10 +292,10 @@ private:
   NodeMap d_simpITECache;
   Node simpITEAtom(TNode atom);
 
-
-private:
-  class Statistics {
-  public:
+ private:
+  class Statistics
+  {
+   public:
     IntStat d_maxNonConstantsFolded;
     IntStat d_unexpected;
     IntStat d_unsimplified;
@@ -297,16 +313,17 @@ private:
   Statistics d_statistics;
 };
 
-class ITECareSimplifier {
-public:
+class ITECareSimplifier
+{
+ public:
   ITECareSimplifier();
   ~ITECareSimplifier();
 
   Node simplifyWithCare(TNode e);
 
   void clear();
-private:
 
+ private:
   /**
    * This should always equal the number of care sets allocated by
    * this object - the number of these that have been deleted. This is
@@ -321,46 +338,58 @@ private:
   typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap;
 
   class CareSetPtr;
-  class CareSetPtrVal {
+  class CareSetPtrVal
+  {
    public:
     bool safeToGarbageCollect() const { return d_refCount == 0; }
+
    private:
     friend class ITECareSimplifier::CareSetPtr;
     ITECareSimplifier& d_iteSimplifier;
     unsigned d_refCount;
     std::set<Node> d_careSet;
     CareSetPtrVal(ITECareSimplifier& simp)
-        : d_iteSimplifier(simp), d_refCount(1) {}
+        : d_iteSimplifier(simp), d_refCount(1)
+    {
+    }
   }; /* class ITECareSimplifier::CareSetPtrVal */
 
   std::vector<CareSetPtrVal*> d_usedSets;
-  void careSetPtrGC(CareSetPtrVal* val) {
-    d_usedSets.push_back(val);
-  }
+  void careSetPtrGC(CareSetPtrVal* val) { d_usedSets.push_back(val); }
 
-  class CareSetPtr {
+  class CareSetPtr
+  {
     CareSetPtrVal* d_val;
     CareSetPtr(CareSetPtrVal* val) : d_val(val) {}
-  public:
+
+   public:
     CareSetPtr() : d_val(NULL) {}
-    CareSetPtr(const CareSetPtr& cs) {
+    CareSetPtr(const CareSetPtr& cs)
+    {
       d_val = cs.d_val;
-      if (d_val != NULL) {
+      if (d_val != NULL)
+      {
         ++(d_val->d_refCount);
       }
     }
-    ~CareSetPtr() {
-      if (d_val != NULL && (--(d_val->d_refCount) == 0)) {
+    ~CareSetPtr()
+    {
+      if (d_val != NULL && (--(d_val->d_refCount) == 0))
+      {
         d_val->d_iteSimplifier.careSetPtrGC(d_val);
       }
     }
-    CareSetPtr& operator=(const CareSetPtr& cs) {
-      if (d_val != cs.d_val) {
-        if (d_val != NULL && (--(d_val->d_refCount) == 0)) {
+    CareSetPtr& operator=(const CareSetPtr& cs)
+    {
+      if (d_val != cs.d_val)
+      {
+        if (d_val != NULL && (--(d_val->d_refCount) == 0))
+        {
           d_val->d_iteSimplifier.careSetPtrGC(d_val);
         }
         d_val = cs.d_val;
-        if (d_val != NULL) {
+        if (d_val != NULL)
+        {
           ++(d_val->d_refCount);
         }
       }
@@ -369,7 +398,8 @@ private:
     std::set<Node>& getCareSet() { return d_val->d_careSet; }
 
     static CareSetPtr mkNew(ITECareSimplifier& simp);
-    static CareSetPtr recycle(CareSetPtrVal* val) {
+    static CareSetPtr recycle(CareSetPtrVal* val)
+    {
       Assert(val != NULL && val->d_refCount == 0);
       val->d_refCount = 1;
       return CareSetPtr(val);
@@ -383,7 +413,8 @@ private:
   Node substitute(TNode e, TNodeMap& substTable, TNodeMap& cache);
 };
 
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace util
+}  // namespace preprocessing
+}  // namespace CVC4
 
 #endif
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5e7d52676..7b45bcb3c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -82,6 +82,7 @@
 #include "preprocessing/passes/global_negate.h"
 #include "preprocessing/passes/int_to_bv.h"
 #include "preprocessing/passes/ite_removal.h"
+#include "preprocessing/passes/ite_simp.h"
 #include "preprocessing/passes/pseudo_boolean_processor.h"
 #include "preprocessing/passes/quantifiers_preprocess.h"
 #include "preprocessing/passes/real_to_int.h"
@@ -202,8 +203,6 @@ struct SmtEngineStatistics {
   /** number of constant propagations found during nonclausal simp */
   IntStat d_numConstantProps;
   /** time spent in simplifying ITEs */
-  TimerStat d_simpITETime;
-  /** time spent in simplifying ITEs */
   TimerStat d_unconstrainedSimpTime;
   /** time spent in theory preprocessing */
   TimerStat d_theoryPreprocessTime;
@@ -237,7 +236,6 @@ struct SmtEngineStatistics {
     d_miplibPassTime("smt::SmtEngine::miplibPassTime"),
     d_numMiplibAssertionsRemoved("smt::SmtEngine::numMiplibAssertionsRemoved", 0),
     d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
-    d_simpITETime("smt::SmtEngine::simpITETime"),
     d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"),
     d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
     d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
@@ -257,7 +255,6 @@ struct SmtEngineStatistics {
     smtStatisticsRegistry()->registerStat(&d_miplibPassTime);
     smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved);
     smtStatisticsRegistry()->registerStat(&d_numConstantProps);
-    smtStatisticsRegistry()->registerStat(&d_simpITETime);
     smtStatisticsRegistry()->registerStat(&d_unconstrainedSimpTime);
     smtStatisticsRegistry()->registerStat(&d_theoryPreprocessTime);
     smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
@@ -279,7 +276,6 @@ struct SmtEngineStatistics {
     smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime);
     smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved);
     smtStatisticsRegistry()->unregisterStat(&d_numConstantProps);
-    smtStatisticsRegistry()->unregisterStat(&d_simpITETime);
     smtStatisticsRegistry()->unregisterStat(&d_unconstrainedSimpTime);
     smtStatisticsRegistry()->unregisterStat(&d_theoryPreprocessTime);
     smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
@@ -590,19 +586,10 @@ class SmtEnginePrivate : public NodeManagerListener {
    */
   bool checkForBadSkolems(TNode n, TNode skolem, NodeToBoolHashMap& cache);
 
-  // Simplify ITE structure
-  bool simpITE();
-
   // Simplify based on unconstrained values
   void unconstrainedSimp();
 
   /**
-   * Ensures the assertions asserted after before now effectively come before
-   * d_realAssertionsEnd.
-   */
-  void compressBeforeRealAssertions(size_t before);
-
-  /**
    * Trace nodes back to their assertions using CircuitPropagator's
    * BackEdgesMap.
    */
@@ -2663,6 +2650,8 @@ void SmtEnginePrivate::finishInit()
       new GlobalNegate(d_preprocessingPassContext.get()));
   std::unique_ptr<IntToBV> intToBV(
       new IntToBV(d_preprocessingPassContext.get()));
+  std::unique_ptr<ITESimp> iteSimp(
+      new ITESimp(d_preprocessingPassContext.get()));
   std::unique_ptr<QuantifiersPreprocess> quantifiersPreprocess(
       new QuantifiersPreprocess(d_preprocessingPassContext.get()));
   std::unique_ptr<PseudoBooleanProcessor> pbProc(
@@ -2705,6 +2694,7 @@ void SmtEnginePrivate::finishInit()
   d_preprocessingPassRegistry.registerPass("global-negate",
                                            std::move(globalNegate));
   d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV));
+  d_preprocessingPassRegistry.registerPass("ite-simp", std::move(iteSimp));
   d_preprocessingPassRegistry.registerPass("quantifiers-preprocess",
                                            std::move(quantifiersPreprocess));
   d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor",
@@ -3320,60 +3310,6 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   return true;
 }
 
-bool SmtEnginePrivate::simpITE() {
-  TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime);
-
-  spendResource(options::preprocessStep());
-
-  Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl;
-
-  unsigned numAssertionOnEntry = d_assertions.size();
-  for (unsigned i = 0; i < d_assertions.size(); ++i) {
-    spendResource(options::preprocessStep());
-    Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertions[i]);
-    d_assertions.replace(i, result);
-    if(result.isConst() && !result.getConst<bool>()){
-      return false;
-    }
-  }
-  bool result = d_smt.d_theoryEngine->donePPSimpITE(d_assertions.ref());
-  if(numAssertionOnEntry < d_assertions.size()){
-    compressBeforeRealAssertions(numAssertionOnEntry);
-  }
-  return result;
-}
-
-void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){
-  size_t curr = d_assertions.size();
-  if (before >= curr || d_assertions.getRealAssertionsEnd() <= 0
-      || d_assertions.getRealAssertionsEnd() >= curr)
-  {
-    return;
-  }
-
-  // assertions
-  // original: [0 ... d_assertions.getRealAssertionsEnd())
-  //  can be modified
-  // ites skolems [d_assertions.getRealAssertionsEnd(), before)
-  //  cannot be moved
-  // added [before, curr)
-  //  can be modified
-  Assert(0 < d_assertions.getRealAssertionsEnd());
-  Assert(d_assertions.getRealAssertionsEnd() <= before);
-  Assert(before < curr);
-
-  std::vector<Node> intoConjunction;
-  for(size_t i = before; i<curr; ++i){
-    intoConjunction.push_back(d_assertions[i]);
-  }
-  d_assertions.resize(before);
-  size_t lastBeforeItes = d_assertions.getRealAssertionsEnd() - 1;
-  intoConjunction.push_back(d_assertions[lastBeforeItes]);
-  Node newLast = util::NaryBuilder::mkAssoc(kind::AND, intoConjunction);
-  d_assertions.replace(lastBeforeItes, newLast);
-  Assert(d_assertions.size() == before);
-}
-
 void SmtEnginePrivate::unconstrainedSimp() {
   TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime);
   spendResource(options::preprocessStep());
@@ -3845,11 +3781,14 @@ bool SmtEnginePrivate::simplifyAssertions()
     Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
     // ITE simplification
-    if(options::doITESimp() &&
-       (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat())) {
+    if (options::doITESimp()
+        && (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat()))
+    {
       Chat() << "...doing ITE simplification..." << endl;
-      bool noConflict = simpITE();
-      if(!noConflict){
+      PreprocessingPassResult res =
+          d_preprocessingPassRegistry.getPass("ite-simp")->apply(&d_assertions);
+      if (res == PreprocessingPassResult::CONFLICT)
+      {
         Chat() << "...ITE simplification found unsat..." << endl;
         return false;
       }
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;
   }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f5341b38b..c87a4be02 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -40,7 +40,6 @@
 #include "theory/arith/arith_ite_utils.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/care_graph.h"
-#include "theory/ite_utilities.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/theory_quantifiers.h"
@@ -336,8 +335,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
   ProofManager::currentPM()->initTheoryProofEngine();
 #endif
 
-  d_iteUtilities = new ITEUtilities();
-
   smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded);
 }
 
@@ -366,8 +363,6 @@ TheoryEngine::~TheoryEngine() {
 
   delete d_unconstrainedSimp;
 
-  delete d_iteUtilities;
-
   smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded);
 }
 
@@ -2000,111 +1995,6 @@ void TheoryEngine::staticInitializeBVOptions(
   }
 }
 
-Node TheoryEngine::ppSimpITE(TNode assertion)
-{
-  if (!d_iteUtilities->containsTermITE(assertion))
-  {
-    return assertion;
-  } else {
-    Node result = d_iteUtilities->simpITE(assertion);
-    Node res_rewritten = Rewriter::rewrite(result);
-
-    if(options::simplifyWithCareEnabled()){
-      Chat() << "starting simplifyWithCare()" << endl;
-      Node postSimpWithCare = d_iteUtilities->simplifyWithCare(res_rewritten);
-      Chat() << "ending simplifyWithCare()"
-             << " post simplifyWithCare()" << postSimpWithCare.getId() << endl;
-      result = Rewriter::rewrite(postSimpWithCare);
-    } else {
-      result = res_rewritten;
-    }
-    return result;
-  }
-}
-
-bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){
-  // This pass does not support dependency tracking yet
-  // (learns substitutions from all assertions so just
-  // adding addDependence is not enough)
-  if (options::unsatCores() || options::fewerPreprocessingHoles()) {
-    return true;
-  }
-  bool result = true;
-  bool simpDidALotOfWork = d_iteUtilities->simpIteDidALotOfWorkHeuristic();
-  if(simpDidALotOfWork){
-    if(options::compressItes()){
-      result = d_iteUtilities->compress(assertions);
-    }
-
-    if(result){
-      // if false, don't bother to reclaim memory here.
-      NodeManager* nm = NodeManager::currentNM();
-      if(nm->poolSize() >= options::zombieHuntThreshold()){
-        Chat() << "..ite simplifier did quite a bit of work.. " << nm->poolSize() << endl;
-        Chat() << "....node manager contains " << nm->poolSize() << " nodes before cleanup" << endl;
-        d_iteUtilities->clear();
-        Rewriter::clearCaches();
-        nm->reclaimZombiesUntil(options::zombieHuntThreshold());
-        Chat() << "....node manager contains " << nm->poolSize() << " nodes after cleanup" << endl;
-      }
-    }
-  }
-
-  // Do theory specific preprocessing passes
-  if(d_logicInfo.isTheoryEnabled(theory::THEORY_ARITH)
-     && !options::incrementalSolving() ){
-    if(!simpDidALotOfWork){
-      ContainsTermITEVisitor& contains =
-          *(d_iteUtilities->getContainsVisitor());
-      arith::ArithIteUtils aiteu(contains, d_userContext, getModel());
-      bool anyItes = false;
-      for(size_t i = 0;  i < assertions.size(); ++i){
-        Node curr = assertions[i];
-        if(contains.containsTermITE(curr)){
-          anyItes = true;
-          Node res = aiteu.reduceVariablesInItes(curr);
-          Debug("arith::ite::red") << "@ " << i << " ... " << curr << endl << "   ->" << res << endl;
-          if(curr != res){
-            Node more = aiteu.reduceConstantIteByGCD(res);
-            Debug("arith::ite::red") << "  gcd->" << more << endl;
-            assertions[i] = Rewriter::rewrite(more);
-          }
-        }
-      }
-      if(!anyItes){
-        unsigned prevSubCount = aiteu.getSubCount();
-        aiteu.learnSubstitutions(assertions);
-        if(prevSubCount < aiteu.getSubCount()){
-          d_arithSubstitutionsAdded += aiteu.getSubCount() - prevSubCount;
-          bool anySuccess = false;
-          for(size_t i = 0, N =  assertions.size();  i < N; ++i){
-            Node curr = assertions[i];
-            Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr));
-            Node res = aiteu.reduceVariablesInItes(next);
-            Debug("arith::ite::red") << "@ " << i << " ... " << next << endl << "   ->" << res << endl;
-            Node more = aiteu.reduceConstantIteByGCD(res);
-            Debug("arith::ite::red") << "  gcd->" << more << endl;
-            if(more != next){
-              anySuccess = true;
-              break;
-            }
-          }
-          for(size_t i = 0, N =  assertions.size();  anySuccess && i < N; ++i){
-            Node curr = assertions[i];
-            Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr));
-            Node res = aiteu.reduceVariablesInItes(next);
-            Debug("arith::ite::red") << "@ " << i << " ... " << next << endl << "   ->" << res << endl;
-            Node more = aiteu.reduceConstantIteByGCD(res);
-            Debug("arith::ite::red") << "  gcd->" << more << endl;
-            assertions[i] = Rewriter::rewrite(more);
-          }
-        }
-      }
-    }
-  }
-  return result;
-}
-
 void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* proofRecipe) {
   Assert(explanationVector.size() > 0);
 
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 5763114ca..71a0234ed 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -84,7 +84,6 @@ struct NodeTheoryPairHashFunction {
 namespace theory {
   class TheoryModel;
   class TheoryEngineModelBuilder;
-  class ITEUtilities;
 
   namespace eq {
     class EqualityEngine;
@@ -828,12 +827,6 @@ private:
   /** Dump the assertions to the dump */
   void dumpAssertions(const char* tag);
 
-  /**
-   * A collection of ite preprocessing passes.
-   */
-  theory::ITEUtilities* d_iteUtilities;
-
-
   /** For preprocessing pass simplifying unconstrained expressions */
   UnconstrainedSimplifier* d_unconstrainedSimp;