Refactor ITE simplification preprocessing pass. (#2360)

7 files changed, 38 insertions, 2179 deletions

diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index a683d2bbb..5b51e162d 100644
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -2,7 +2,7 @@
 /*! \file arith_ite_utils.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Kshitij Bansal
+ **   Tim King, Aina Niemetz, Kshitij Bansal
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -21,9 +21,9 @@
 
 #include "base/output.h"
 #include "options/smt_options.h"
+#include "preprocessing/util/ite_utilities.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/normal_form.h"
-#include "theory/ite_utilities.h"
 #include "theory/rewriter.h"
 #include "theory/substitutions.h"
 #include "theory/theory_model.h"
@@ -140,18 +140,19 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){
   Unreachable();
 }
 
-ArithIteUtils::ArithIteUtils(ContainsTermITEVisitor& contains,
-                             context::Context* uc,
-                             TheoryModel* model)
-  : d_contains(contains)
-  , d_subs(NULL)
-  , d_model(model)
-  , d_one(1)
-  , d_subcount(uc, 0)
-  , d_skolems(uc)
-  , d_implies()
-  , d_skolemsAdded()
-  , d_orBinEqs()
+ArithIteUtils::ArithIteUtils(
+    preprocessing::util::ContainsTermITEVisitor& contains,
+    context::Context* uc,
+    TheoryModel* model)
+    : d_contains(contains),
+      d_subs(NULL),
+      d_model(model),
+      d_one(1),
+      d_subcount(uc, 0),
+      d_skolems(uc),
+      d_implies(),
+      d_skolemsAdded(),
+      d_orBinEqs()
 {
   d_subs = new SubstitutionMap(uc);
 }
diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h
index 7950ef05f..2c6a30758 100644
--- a/src/theory/arith/arith_ite_utils.h
+++ b/src/theory/arith/arith_ite_utils.h
@@ -2,7 +2,7 @@
 /*! \file arith_ite_utils.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King
+ **   Tim King, Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -29,15 +29,21 @@
 #include "context/cdinsert_hashmap.h"
 
 namespace CVC4 {
-namespace theory {
+namespace preprocessing {
+namespace util {
 class ContainsTermITEVisitor;
+}
+}  // namespace preprocessing
+
+namespace theory {
+
 class SubstitutionMap;
 class TheoryModel;
 
 namespace arith {
 
 class ArithIteUtils {
-  ContainsTermITEVisitor& d_contains;
+  preprocessing::util::ContainsTermITEVisitor& d_contains;
   SubstitutionMap* d_subs;
   TheoryModel* d_model;
 
@@ -68,24 +74,24 @@ class ArithIteUtils {
   std::vector<Node> d_orBinEqs;
 
 public:
-  ArithIteUtils(ContainsTermITEVisitor& contains,
-                context::Context* userContext,
-                TheoryModel* model);
-  ~ArithIteUtils();
+ ArithIteUtils(preprocessing::util::ContainsTermITEVisitor& contains,
+               context::Context* userContext,
+               TheoryModel* model);
+ ~ArithIteUtils();
 
-  //(ite ?v_2 ?v_1 (ite ?v_3 (- ?v_1 128) (- ?v_1 256)))
+ //(ite ?v_2 ?v_1 (ite ?v_3 (- ?v_1 128) (- ?v_1 256)))
 
-  /** removes common sums variables sums from term ites. */
-  Node reduceVariablesInItes(Node n);
+ /** removes common sums variables sums from term ites. */
+ Node reduceVariablesInItes(Node n);
 
-  Node reduceConstantIteByGCD(Node n);
+ Node reduceConstantIteByGCD(Node n);
 
-  void clear();
+ void clear();
 
-  Node applySubstitutions(TNode f);
-  unsigned getSubCount() const;
+ Node applySubstitutions(TNode f);
+ unsigned getSubCount() const;
 
-  void learnSubstitutions(const std::vector<Node>& assertions);
+ void learnSubstitutions(const std::vector<Node>& assertions);
 
 private:
   /* applies this to all children of n and constructs the result */
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 968970049..89550295a 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -36,6 +36,7 @@
 #include "expr/node_builder.h"
 #include "options/arith_options.h"
 #include "options/smt_options.h"  // for incrementalSolving()
+#include "preprocessing/util/ite_utilities.h"
 #include "smt/logic_exception.h"
 #include "smt/logic_request.h"
 #include "smt/smt_statistics_registry.h"
@@ -59,7 +60,6 @@
 #include "theory/arith/simplex.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/ext_theory.h"
-#include "theory/ite_utilities.h"
 #include "theory/quantifiers/fmf/bounded_integers.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
@@ -5374,7 +5374,7 @@ bool TheoryArithPrivate::decomposeTerm(Node term, Rational& m, Node& p, Rational
   }
 
   // TODO Speed up
-  ContainsTermITEVisitor ctv;
+  preprocessing::util::ContainsTermITEVisitor ctv;
   if(ctv.containsTermITE(t)){
     return false;
   }
diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp
deleted file mode 100644
index 40a58cf57..000000000
--- a/src/theory/ite_utilities.cpp
+++ /dev/null
@@ -1,1642 +0,0 @@
-/*********************                                                        */
-/*! \file ite_utilities.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Morgan Deters, 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.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Simplifications for ITE expressions
- **
- ** 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
- **/
-#include "theory/ite_utilities.h"
-
-#include <utility>
-
-#include "smt/smt_statistics_registry.h"
-#include "theory/rewriter.h"
-#include "theory/theory.h"
-
-using namespace std;
-namespace CVC4 {
-namespace theory {
-
-namespace ite {
-
-inline static bool isTermITE(TNode e) {
-  return (e.getKind() == kind::ITE && !e.getType().isBoolean());
-}
-
-inline static bool triviallyContainsNoTermITEs(TNode e) {
-  return e.isConst() || e.isVar();
-}
-
-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;
-  }
-}
-
-struct CTIVStackElement {
-  TNode curr;
-  unsigned pos;
-  CTIVStackElement() : curr(), pos(0) {}
-  CTIVStackElement(TNode c) : curr(c), pos(0) {}
-}; /* CTIVStackElement */
-
-} /* CVC4::theory::ite */
-
-ITEUtilities::ITEUtilities()
-    : d_containsVisitor(new ContainsTermITEVisitor()),
-      d_compressor(NULL),
-      d_simplifier(NULL),
-      d_careSimp(NULL)
-{
-  Assert(d_containsVisitor != NULL);
-}
-
-ITEUtilities::~ITEUtilities(){
-
-  if(d_simplifier != NULL){
-    delete d_simplifier;
-  }
-  if(d_compressor != NULL){
-    delete d_compressor;
-  }
-  if(d_careSimp != NULL){
-    delete d_careSimp;
-  }
-}
-
-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){
-    return false;
-  }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){
-    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();
-  }
-  return d_careSimp->simplifyWithCare(e);
-}
-
-void ITEUtilities::clear(){
-  if(d_simplifier != NULL){
-    d_simplifier->clearSimpITECaches();
-  }
-  if(d_compressor != NULL){
-    d_compressor->garbageCollect();
-  }
-  if(d_careSimp != NULL){
-    d_careSimp->clear();
-  }
-  d_containsVisitor->garbageCollect();
-}
-
-/*********************                                                        */
-/* ContainsTermITEVisitor
- */
-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; }
-
-  NodeBoolMap::const_iterator end = d_cache.end();
-  NodeBoolMap::const_iterator tmp_it = d_cache.find(e);
-  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()){
-    ite::CTIVStackElement& top = stack.back();
-    TNode curr = top.curr;
-    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{
-      // this is someone's child
-      TNode child = curr[top.pos];
-      child = (child.getKind() == kind::NOT) ? child[0] : child;
-      ++top.pos;
-      if(ite::triviallyContainsNoTermITEs(child)){
-        // skip
-      }else{
-        tmp_it = d_cache.find(child);
-        if(tmp_it != end){
-          foundTermIte = (*tmp_it).second;
-        }else{
-          stack.push_back(ite::CTIVStackElement(child));
-          foundTermIte = ite::isTermITE(child);
-        }
-      }
-    }
-  }
-  if(foundTermIte){
-    while(!stack.empty()){
-      TNode curr = stack.back().curr;
-      stack.pop_back();
-      d_cache[curr] = true;
-    }
-  }
-  return foundTermIte;
-}
-void ContainsTermITEVisitor::garbageCollect() {
-  d_cache.clear();
-}
-
-/*********************                                                        */
-/* IncomingArcCounter
- */
-IncomingArcCounter::IncomingArcCounter(bool skipVars, bool skipConstants)
-  : d_reachCount()
-  , d_skipVariables(skipVars)
-  , d_skipConstants(skipConstants)
-{}
-IncomingArcCounter::~IncomingArcCounter(){}
-
-void IncomingArcCounter::computeReachability(const std::vector<Node>& assertions){
-  std::vector<TNode> tovisit(assertions.begin(), assertions.end());
-
-  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;
-    }
-
-    if(skip) { continue; }
-    if(d_reachCount.find(back) != d_reachCount.end()){
-      d_reachCount[back] = 1 + d_reachCount[back];
-    }else{
-      d_reachCount[back] = 1;
-      for(TNode::iterator cit=back.begin(), end = back.end(); cit != end; ++cit){
-        tovisit.push_back(*cit);
-      }
-    }
-  }
-}
-
-void IncomingArcCounter::clear() {
-  d_reachCount.clear();
-}
-
-/*********************                                                        */
-/* ITECompressor
- */
-ITECompressor::ITECompressor(ContainsTermITEVisitor* contains)
-  : d_contains(contains)
-  , d_assertions(NULL)
-  , d_incoming(true, true)
-{
-  Assert(d_contains != NULL);
-
-  d_true = NodeManager::currentNM()->mkConst<bool>(true);
-  d_false = NodeManager::currentNM()->mkConst<bool>(false);
-}
-
-ITECompressor::~ITECompressor() {
-  reset();
-}
-
-void ITECompressor::reset(){
-  d_incoming.clear();
-  d_compressed.clear();
-}
-
-void ITECompressor::garbageCollect(){
-  reset();
-}
-
-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(){
-  smtStatisticsRegistry()->unregisterStat(&d_compressCalls);
-  smtStatisticsRegistry()->unregisterStat(&d_skolemsAdded);
-}
-
-Node ITECompressor::push_back_boolean(Node original, Node compressed){
-  Node rewritten = Rewriter::rewrite(compressed);
-  // There is a bug if the rewritter takes a pure boolean expression
-  // and changes its theory
-  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()){
-    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())){
-    d_compressed[original] = rewritten;
-    d_compressed[compressed] = rewritten;
-    d_compressed[rewritten] = rewritten;
-    return rewritten;
-  }else{
-    NodeManager* nm = NodeManager::currentNM();
-    Node skolem = nm->mkSkolem("compress", nm->booleanType());
-    d_compressed[rewritten] = skolem;
-    d_compressed[original] = skolem;
-    d_compressed[compressed] = skolem;
-
-    Node iff = skolem.eqNode(rewritten);
-    d_assertions->push_back(iff);
-    ++(d_statistics.d_skolemsAdded);
-    return skolem;
-  }
-}
-
-bool ITECompressor::multipleParents(TNode c){
-  return d_incoming.lookupIncoming(c) >= 2;
-}
-
-Node ITECompressor::compressBooleanITEs(Node toCompress){
-  Assert(toCompress.getKind() == kind::ITE);
-  Assert(toCompress.getType().isBoolean());
-
-  if(!(toCompress[1] == d_false || toCompress[2] == d_false)){
-    Node cmpCnd = compressBoolean(toCompress[0]);
-    if(cmpCnd.isConst()){
-      Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2];
-      Node res = compressBoolean(branch);
-      d_compressed[toCompress] = res;
-      return res;
-    }else{
-      Node cmpThen = compressBoolean(toCompress[1]);
-      Node cmpElse = compressBoolean(toCompress[2]);
-      Node newIte = cmpCnd.iteNode(cmpThen, cmpElse);
-      if(multipleParents(toCompress)){
-        return push_back_boolean(toCompress, newIte);
-      }else{
-        return newIte;
-      }
-    }
-  }
-
-  NodeBuilder<> nb(kind::AND);
-  Node 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){
-        return push_back_boolean(toCompress, d_false);
-      }else{
-        // equivalent to true don't push back
-      }
-    }else{
-      Node pb = negateCnd ? compressCnd.notNode() : compressCnd;
-      nb << pb;
-    }
-    curr = negateCnd ? curr[2] : curr[1];
-  }
-  Assert(toCompress != curr);
-
-  nb << compressBoolean(curr);
-  Node res = nb.getNumChildren() == 1 ? nb[0] : (Node)nb;
-  return push_back_boolean(toCompress, res);
-}
-
-Node ITECompressor::compressTerm(Node toCompress){
-  if(toCompress.isConst() || toCompress.isVar()){
-    return toCompress;
-  }
-
-  if(d_compressed.find(toCompress) != d_compressed.end()){
-    return d_compressed[toCompress];
-  }
-  if(toCompress.getKind() == kind::ITE){
-    Node cmpCnd = compressBoolean(toCompress[0]);
-    if(cmpCnd.isConst()){
-      Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2];
-      Node res = compressTerm(toCompress);
-      d_compressed[toCompress] = res;
-      return res;
-    }else{
-      Node cmpThen = compressTerm(toCompress[1]);
-      Node cmpElse = compressTerm(toCompress[2]);
-      Node newIte = cmpCnd.iteNode(cmpThen, cmpElse);
-      d_compressed[toCompress] = newIte;
-      return newIte;
-    }
-  }
-
-  NodeBuilder<> nb(toCompress.getKind());
-
-  if(toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) {
-    nb << (toCompress.getOperator());
-  }
-  for(Node::iterator it = toCompress.begin(), end = toCompress.end(); it != end; ++it){
-    nb << compressTerm(*it);
-  }
-  Node compressed = (Node)nb;
-  if(multipleParents(toCompress)){
-    d_compressed[toCompress] = compressed;
-  }
-  return compressed;
-}
-
-Node ITECompressor::compressBoolean(Node toCompress){
-  static int instance = 0;
-  ++instance;
-  if(toCompress.isConst() || toCompress.isVar()){
-    return toCompress;
-  }
-  if(d_compressed.find(toCompress) != d_compressed.end()){
-    return d_compressed[toCompress];
-  }else if(toCompress.getKind() == kind::ITE){
-    return compressBooleanITEs(toCompress);
-  }else{
-    bool ta = ite::isTheoryAtom(toCompress);
-    NodeBuilder<> nb(toCompress.getKind());
-    if(toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) {
-      nb << (toCompress.getOperator());
-    }
-    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)){
-      return push_back_boolean(toCompress, compressed);
-    }else{
-      return compressed;
-    }
-  }
-}
-
-
-
-bool ITECompressor::compress(std::vector<Node>& assertions){
-  reset();
-
-  d_assertions = &assertions;
-  d_incoming.computeReachability(assertions);
-
-  ++(d_statistics.d_compressCalls);
-  Chat() << "Computed reachability" << endl;
-
-  bool nofalses = true;
-  size_t original_size = assertions.size();
-  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);
-    assertions[i] = rewritten;
-    Assert(!d_contains->containsTermITE(rewritten));
-
-    nofalses = (rewritten != d_false);
-  }
-
-  d_assertions = NULL;
-
-  return nofalses;
-}
-
-TermITEHeightCounter::TermITEHeightCounter()
-  :d_termITEHeight()
-{}
-
-TermITEHeightCounter::~TermITEHeightCounter(){}
-
-void TermITEHeightCounter::clear(){
-  d_termITEHeight.clear();
-}
-
-size_t TermITEHeightCounter::cache_size() const{
-  return d_termITEHeight.size();
-}
-
-namespace ite {
-struct TITEHStackElement {
-  TNode curr;
-  unsigned pos;
-  uint32_t maxChildHeight;
-  TITEHStackElement() : curr(), pos(0), maxChildHeight(0) {}
-  TITEHStackElement(TNode c) : curr(c), pos(0), maxChildHeight(0) {}
-};
-} /* namespace ite */
-
-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){
-    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()){
-    ite::TITEHStackElement& top = stack.back();
-    top.maxChildHeight = std::max(top.maxChildHeight, returnValue);
-    TNode curr = top.curr;
-    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){
-        ++top.pos;
-        returnValue = 0;
-        continue;
-      }
-      // this is someone's child
-      TNode child = curr[top.pos];
-      ++top.pos;
-      if(ite::triviallyContainsNoTermITEs(child)){
-        returnValue = 0;
-      }else{
-        tmp_it = d_termITEHeight.find(child);
-        if(tmp_it != end){
-          returnValue = (*tmp_it).second;
-        }else{
-          stack.push_back(ite::TITEHStackElement(child));
-        }
-      }
-    }
-  }
-  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()
-{
-  Assert(d_containsVisitor != NULL);
-  d_true = NodeManager::currentNM()->mkConst<bool>(true);
-  d_false = NodeManager::currentNM()->mkConst<bool>(false);
-}
-
-ITESimplifier::~ITESimplifier() {
-  clearSimpITECaches();
-  Assert(d_constantLeaves.empty());
-  Assert(d_allocatedConstantLeaves.empty());
-}
-
-bool ITESimplifier::leavesAreConst(TNode e){
-  return leavesAreConst(e, theory::Theory::theoryOf(e));
-}
-
-void ITESimplifier::clearSimpITECaches(){
-  Chat() << "clear ite caches " << endl;
-  for(size_t i = 0, N = d_allocatedConstantLeaves.size(); i < N; ++i){
-    NodeVec* curr = d_allocatedConstantLeaves[i];
-    delete curr;
-  }
-  d_citeEqConstApplications = 0;
-  d_constantLeaves.clear();
-  d_allocatedConstantLeaves.clear();
-  d_termITEHeight.clear();
-  d_constantIteEqualsConstantCache.clear();
-  d_replaceOverCache.clear();
-  d_replaceOverTermIteCache.clear();
-  d_simpITECache.clear();
-  d_simpVars.clear();
-  d_simpConstCache.clear();
-  d_leavesConstCache.clear();
-  d_simpContextCache.clear();
-}
-
-bool ITESimplifier::doneALotOfWorkHeuristic() const {
-  static const size_t SIZE_BOUND = 1000;
-  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")
-{
-  smtStatisticsRegistry()->registerStat(&d_maxNonConstantsFolded);
-  smtStatisticsRegistry()->registerStat(&d_unexpected);
-  smtStatisticsRegistry()->registerStat(&d_unsimplified);
-  smtStatisticsRegistry()->registerStat(&d_exactMatchFold);
-  smtStatisticsRegistry()->registerStat(&d_binaryPredFold);
-  smtStatisticsRegistry()->registerStat(&d_specialEqualityFolds);
-  smtStatisticsRegistry()->registerStat(&d_simpITEVisits);
-  smtStatisticsRegistry()->registerStat(&d_inSmaller);
-}
-
-ITESimplifier::Statistics::~Statistics(){
-  smtStatisticsRegistry()->unregisterStat(&d_maxNonConstantsFolded);
-  smtStatisticsRegistry()->unregisterStat(&d_unexpected);
-  smtStatisticsRegistry()->unregisterStat(&d_unsimplified);
-  smtStatisticsRegistry()->unregisterStat(&d_exactMatchFold);
-  smtStatisticsRegistry()->unregisterStat(&d_binaryPredFold);
-  smtStatisticsRegistry()->unregisterStat(&d_specialEqualityFolds);
-  smtStatisticsRegistry()->unregisterStat(&d_simpITEVisits);
-  smtStatisticsRegistry()->unregisterStat(&d_inSmaller);
-}
-
-bool ITESimplifier::isConstantIte(TNode e){
-  if(e.isConst()){
-    return true;
-  }else if(ite::isTermITE(e)){
-    NodeVec* constants = computeConstantLeaves(e);
-    return constants != NULL;
-  }else{
-    return false;
-  }
-}
-
-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){
-    return (*it).second;
-  }
-  TNode thenB = ite[1];
-  TNode elseB = ite[2];
-
-  // special case 2 constant children
-  if(thenB.isConst() && elseB.isConst()){
-    NodeVec* pair = new NodeVec(2);
-    d_allocatedConstantLeaves.push_back(pair);
-
-    (*pair)[0] = std::min(thenB, elseB);
-    (*pair)[1] = std::max(thenB, elseB);
-    d_constantLeaves[ite] = pair;
-    return pair;
-  }
-  // At least 1 is an 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;
-  }
-
-  // At least 1 is not a constant
-  TNode definitelyITE = thenB.isConst() ? elseB : thenB;
-  TNode maybeITE = thenB.isConst() ? thenB : elseB;
-
-  NodeVec* defChildren = computeConstantLeaves(definitelyITE);
-  if(defChildren == NULL){
-    d_constantLeaves[ite] = NULL;
-    return NULL;
-  }
-
-  NodeVec scratch;
-  NodeVec* maybeChildren = NULL;
-  if(maybeITE.getKind() == kind::ITE){
-    maybeChildren = computeConstantLeaves(maybeITE);
-  }else{
-    scratch.push_back(maybeITE);
-    maybeChildren = &scratch;
-  }
-  if(maybeChildren == NULL){
-    d_constantLeaves[ite] = NULL;
-    return NULL;
-  }
-
-  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(),
-                          both->begin());
-  both->resize(newEnd - both->begin());
-  d_constantLeaves[ite] = both;
-  return both;
-}
-
-// This is uncached! Better for protoyping or getting limited size examples
-struct IteTreeSearchData{
-  set<Node> visited;
-  set<Node> constants;
-  set<Node> nonConstants;
-  int maxConstants;
-  int maxNonconstants;
-  int maxDepth;
-  bool failure;
-  IteTreeSearchData()
-    : maxConstants(-1), maxNonconstants(-1), maxDepth(-1), failure(false)
-  {}
-};
-void iteTreeSearch(Node e, int depth, IteTreeSearchData& search){
-  if(search.maxDepth >= 0 && depth > search.maxDepth){
-    search.failure = true;
-  }
-  if(search.failure){
-    return;
-  }
-  if(search.visited.find(e) != search.visited.end()){
-    return;
-  }else{
-    search.visited.insert(e);
-  }
-
-  if(e.isConst()){
-    search.constants.insert(e);
-    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{
-    search.nonConstants.insert(e);
-    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){
-    return replaceWith;
-  }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()){
-    return d_replaceOverCache[p];
-  }
-
-  NodeBuilder<> builder(n.getKind());
-  if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
-    builder << n.getOperator();
-  }
-  unsigned i = 0;
-  for (; i < n.getNumChildren(); ++ i) {
-    Node newChild = replaceOver(n[i], replaceWith, simpVar);
-    builder << newChild;
-  }
-  // Mark the substitution and continue
-  Node result = builder;
-  d_replaceOverCache[p] = result;
-  return result;
-}
-
-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()){
-      return d_replaceOverTermIteCache[p];
-    }
-    Assert(!e.getType().isBoolean());
-    Node cnd = e[0];
-    Node newThen = replaceOverTermIte(e[1], simpAtom, simpVar);
-    Node newElse = replaceOverTermIte(e[2], simpAtom, simpVar);
-    Node newIte = cnd.iteNode(newThen, newElse);
-    d_replaceOverTermIteCache[p] = newIte;
-    return newIte;
-  }else{
-    return replaceOver(simpAtom, e, simpVar);
-  }
-}
-
-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)){
-
-      // exactly 1 is an ite
-      TNode ite = left.getKind() == kind::ITE ? left :right;
-      TNode notIte = left.getKind() == kind::ITE ? right : left;
-
-      if(notIte == ite[1]){
-        ++(d_statistics.d_exactMatchFold);
-        return ite[0].iteNode(d_true, notIte.eqNode(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())){
-        ++(d_statistics.d_exactMatchFold);
-        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()){
-
-    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)){
-      // exactly 1 is an ite
-      bool leftIsIte = left.getKind() == kind::ITE;
-      Node ite = leftIsIte ? left :right;
-      Node notIte = leftIsIte ? right : left;
-
-      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;
-          NodeManager* nm = NodeManager::currentNM();
-          Node simpVar = getSimpVar(notIte.getType());
-          TNode newLeft = leftIsIte  ? simpVar : notIte;
-          TNode newRight = leftIsIte ? notIte : simpVar;
-          Node newAtom = nm->mkNode(atom.getKind(), newLeft, newRight);
-
-          ++(d_statistics.d_binaryPredFold);
-          return replaceOverTermIte(ite, newAtom, simpVar);
-        }
-      }
-    }
-  }
-
-  // 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()) ){
-    // expand all 4 cases
-
-    Node negOne = atom[1][0];
-
-    Node lite = atom[0];
-    Node lC = lite[0];
-    Node lT = lite[1];
-    Node lE = lite[2];
-
-    NodeManager* nm = NodeManager::currentNM();
-    Node negRite = atom[1][1];
-    Node rC = negRite[0];
-    Node rT = nm->mkNode(kind::MULT, negOne, negRite[1]);
-    Node rE = nm->mkNode(kind::MULT, negOne, negRite[2]);
-
-    // (ite lC lT lE) = (ite rC rT rE)
-    // (ite lc (= lT (ite rC rT rE) (= lE (ite rC rT rE))))
-    // (ite lc (ite rC (= lT rT) (= lT rE))
-    //         (ite rC (= lE rT) (= lE rE)))
-
-    Node eqTT = lT.eqNode(rT);
-    Node eqTE = lT.eqNode(rE);
-    Node eqET = lE.eqNode(rT);
-    Node eqEE = lE.eqNode(rE);
-    Node thenLC = rC.iteNode(eqTT, eqTE);
-    Node elseLC = rC.iteNode(eqET, eqEE);
-    Node newIte = lC.iteNode(thenLC, elseLC);
-
-    ++(d_statistics.d_specialEqualityFolds);
-    return newIte;
-  }
-  return Node::null();
-}
-
-// 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()){
-      // constant equality
-      return NodeManager::currentNM()->mkConst<bool>(atom[0] == atom[1]);
-    }
-    return Node::null();
-  }else{
-    Node acr = attemptConstantRemoval(atom);
-    if(!acr.isNull()){
-      return acr;
-    }
-    // Node ale = attemptLiftEquality(atom);
-    // if(!ale.isNull()){
-    //   //return ale;
-    // }
-    return Node::null();
-  }
-}
-
-static unsigned numBranches = 0;
-static unsigned numFalseBranches = 0;
-static unsigned itesMade = 0;
-
-Node ITESimplifier::constantIteEqualsConstant(TNode cite, TNode constant){
-  static int instance = 0;
-  ++instance;
-  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);
-
-  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;
-  }
-
-  ++d_citeEqConstApplications;
-
-  NodeVec* leaves = computeConstantLeaves(cite);
-  Assert(leaves != NULL);
-  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;
-      return d_true;
-    }else{
-      Assert(cite.getKind() == kind::ITE);
-      TNode cnd = cite[0];
-      TNode tB = cite[1];
-      TNode fB = cite[2];
-      Node tEqs = constantIteEqualsConstant(tB, constant);
-      Node fEqs = constantIteEqualsConstant(fB, constant);
-      Node boolIte = cnd.iteNode(tEqs, fEqs);
-      if(!(tEqs.isConst() || fEqs.isConst())){
-        ++numBranches;
-      }
-      if(!(tEqs == d_false || fEqs == d_false)){
-        ++numFalseBranches;
-      }
-      ++itesMade;
-      d_constantIteEqualsConstantCache[pair] = boolIte;
-      //Debug("ite::constantIteEqualsConstant") << instance << "->" << boolIte << endl;
-      return boolIte;
-    }
-  }else{
-    d_constantIteEqualsConstantCache[pair] = d_false;
-    Debug("ite::constantIteEqualsConstant") << instance << "->" << d_false << endl;
-    return d_false;
-  }
-}
-
-
-Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite){
-  // intersect the constant ite trees lcite and rcite
-
-  if(lcite.isConst() || rcite.isConst()){
-    bool lIsConst = lcite.isConst();
-    TNode constant = lIsConst ? lcite : rcite;
-    TNode cite = lIsConst ? rcite : lcite;
-
-    (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;
-    return bterm;
-  }
-  Assert(lcite.getKind() == kind::ITE);
-  Assert(rcite.getKind() == kind::ITE);
-
-  NodeVec* leftValues = computeConstantLeaves(lcite);
-  NodeVec* rightValues = computeConstantLeaves(rcite);
-
-  uint32_t smaller = std::min(leftValues->size(), rightValues->size());
-
-  (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(),
-                                 intersection.begin());
-  intersection.resize(newEnd - intersection.begin());
-  if(intersection.empty()){
-    return d_false;
-  }else{
-    NodeBuilder<> nb(kind::OR);
-    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);
-      Node bothHold = lefteq.andNode(righteq);
-      nb << bothHold;
-    }
-    Node result = (nb.getNumChildren() > 1) ? (Node)nb : nb[0];
-    return result;
-  }
-}
-
-
-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))){
-      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()){
-        Node ret = (*eq_pos).second;
-        if(ret.isConst()){
-          return ret;
-        }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);
-        d_constantIteEqualsConstantCache[pair] = d_false;
-        return d_false;
-      }
-    }
-  }
-  return Node::null();
-}
-
-Node ITESimplifier::attemptConstantRemoval(TNode atom){
-  if(atom.getKind() == kind::EQUAL){
-    TNode left = atom[0];
-    TNode right = atom[1];
-    if(isConstantIte(left) && isConstantIte(right)){
-      return intersectConstantIte(left, right);
-    }
-  }
-  return Node::null();
-}
-
-
-bool ITESimplifier::leavesAreConst(TNode e, TheoryId tid)
-{
-  Assert((e.getKind() == kind::ITE && !e.getType().isBoolean()) ||
-         Theory::theoryOf(e) != THEORY_BOOL);
-  if (e.isConst()) {
-    return true;
-  }
-
-  unordered_map<Node, bool, NodeHashFunction>::iterator it;
-  it = d_leavesConstCache.find(e);
-  if (it != d_leavesConstCache.end()) {
-    return (*it).second;
-  }
-
-  if (!containsTermITE(e) && Theory::isLeafOf(e, tid)) {
-    d_leavesConstCache[e] = false;
-    return false;
-  }
-
-  Assert(e.getNumChildren() > 0);
-  size_t k = 0, sz = e.getNumChildren();
-
-  if (e.getKind() == kind::ITE) {
-    k = 1;
-  }
-
-  for (; k < sz; ++k) {
-    if (!leavesAreConst(e[k], tid)) {
-      d_leavesConstCache[e] = false;
-      return false;
-    }
-  }
-  d_leavesConstCache[e] = true;
-  return true;
-}
-
-
-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()) {
-    return (*it).second;
-  }
-
-  if (iteNode.getKind() == kind::ITE) {
-    NodeBuilder<> builder(kind::ITE);
-    builder << iteNode[0];
-    unsigned i = 1;
-    for (; i < iteNode.getNumChildren(); ++ i) {
-      Node n = simpConstants(simpContext, iteNode[i], simpVar);
-      if (n.isNull()) {
-        return n;
-      }
-      builder << n;
-    }
-    // Mark the substitution and continue
-    Node result = builder;
-    result = Rewriter::rewrite(result);
-    d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = result;
-    return result;
-  }
-
-  if (!containsTermITE(iteNode)) {
-    Node n = Rewriter::rewrite(simpContext.substitute(simpVar, iteNode));
-    d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
-    return n;
-  }
-
-  Node iteNode2;
-  Node simpVar2;
-  d_simpContextCache.clear();
-  Node simpContext2 = createSimpContext(iteNode, iteNode2, simpVar2);
-  if (!simpContext2.isNull()) {
-    Assert(!iteNode2.isNull());
-    simpContext2 = simpContext.substitute(simpVar, simpContext2);
-    Node n = simpConstants(simpContext2, iteNode2, simpVar2);
-    if (n.isNull()) {
-      return n;
-    }
-    d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
-    return n;
-  }
-  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()) {
-    return (*it).second;
-  }
-  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()) {
-    return (*it).second;
-  }
-
-  if (!containsTermITE(c)) {
-    d_simpContextCache[c] = c;
-    return c;
-  }
-
-  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()) {
-      return Node();
-    }
-    simpVar = getSimpVar(c.getType());
-    if (simpVar.isNull()) {
-      return Node();
-    }
-    d_simpContextCache[c] = simpVar;
-    iteNode = c;
-    return simpVar;
-  }
-
-  NodeBuilder<> builder(c.getKind());
-  if (c.getMetaKind() == kind::metakind::PARAMETERIZED) {
-    builder << c.getOperator();
-  }
-  unsigned i = 0;
-  for (; i < c.getNumChildren(); ++ i) {
-    Node newChild = createSimpContext(c[i], iteNode, simpVar);
-    if (newChild.isNull()) {
-      return newChild;
-    }
-    builder << newChild;
-  }
-  // Mark the substitution and continue
-  Node result = builder;
-  d_simpContextCache[c] = result;
-  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()){
-    return;
-  }
-  visited.insert(x);
-  if(x.getKind() == k){
-    ++reached;
-  }
-  for(unsigned i =0, N=x.getNumChildren(); i < N; ++i){
-    countReachable_(x[i], k, visited, reached);
-  }
-}
-
-uint32_t countReachable(TNode x, Kind k){
-  NodeSet visited;
-  uint32_t reached = 0;
-  countReachable_(x, k, visited, reached);
-  return reached;
-}
-
-Node ITESimplifier::simpITEAtom(TNode atom)
-{
-  static int CVC4_UNUSED instance = 0;
-  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);
-    Debug("ite::print-success")
-      << 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)) {
-    Node iteNode;
-    Node simpVar;
-    d_simpContextCache.clear();
-    Node simpContext = createSimpContext(atom, iteNode, simpVar);
-    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);
-      }
-      Node n = simpConstants(simpContext, iteNode, simpVar);
-      if (!n.isNull()) {
-        ++(d_statistics.d_unexpected);
-        Debug("ite::simpite") << instance << " "
-                              << "here?" << atom << endl;
-        Debug("ite::simpite") << instance << " "
-                              << "\t" << n << endl;
-        return n;
-      }
-    }
-  }
-  if(Debug.isOn("ite::simpite")){
-    if(countReachable(atom, kind::ITE) > 0){
-      Debug("ite::simpite") << instance << " "
-                            << "remaining " << atom << endl;
-    }
-  }
-  ++(d_statistics.d_unsimplified);
-  return atom;
-}
-
-
-struct preprocess_stack_element {
-  TNode node;
-  bool children_added;
-  preprocess_stack_element(TNode node)
-  : node(node), children_added(false) {}
-};/* struct preprocess_stack_element */
-
-
-Node ITESimplifier::simpITE(TNode assertion)
-{
-  // Do a topological sort of the subexpressions and substitute them
-  vector<preprocess_stack_element> toVisit;
-  toVisit.push_back(assertion);
-
-  static int call = 0;
-  ++call;
-  int iteration = 0;
-
-  while (!toVisit.empty())
-  {
-    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;
-    }
-
-    NodeMap::iterator find = d_simpITECache.find(current);
-    if (find != d_simpITECache.end()) {
-      toVisit.pop_back();
-      continue;
-    }
-
-    // Not yet substituted, so process
-    if (stackHead.children_added) {
-      // Children have been processed, so substitute
-      NodeBuilder<> builder(current.getKind());
-      if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
-        builder << current.getOperator();
-      }
-      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]];
-        builder << childRes;
-      }
-      // Mark the substitution and continue
-      Node result = builder;
-
-      // If this is an atom, we process it
-      if (Theory::theoryOf(result) != THEORY_BOOL &&
-          result.getType().isBoolean()) {
-        result = simpITEAtom(result);
-      }
-
-      // if(current != result && result.isConst()){
-      //   static int instance = 0;
-      //   //cout << instance << " " << result << current << endl;
-      // }
-
-      result = Rewriter::rewrite(result);
-      d_simpITECache[current] = result;
-      ++(d_statistics.d_simpITEVisits);
-      toVisit.pop_back();
-    } else {
-      // Mark that we have added the children if any
-      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) {
-          TNode childNode = *child_it;
-          NodeMap::iterator childFind = d_simpITECache.find(childNode);
-          if (childFind == d_simpITECache.end()) {
-            toVisit.push_back(childNode);
-          }
-        }
-      } else {
-        // No children, so we're done
-        d_simpITECache[current] = current;
-        ++(d_statistics.d_simpITEVisits);
-        toVisit.pop_back();
-      }
-    }
-  }
-  return d_simpITECache[assertion];
-}
-
-ITECareSimplifier::ITECareSimplifier()
-    : d_careSetsOutstanding(0)
-    , d_usedSets()
-{
-  d_true = NodeManager::currentNM()->mkConst<bool>(true);
-  d_false = NodeManager::currentNM()->mkConst<bool>(false);
-}
-
-ITECareSimplifier::~ITECareSimplifier(){
-  Assert(d_usedSets.empty());
-  Assert(d_careSetsOutstanding == 0);
-}
-
-void ITECareSimplifier::clear(){
-  Assert(d_usedSets.empty());
-  Assert(d_careSetsOutstanding == 0);
-}
-
-ITECareSimplifier::CareSetPtr ITECareSimplifier::getNewSet()
-{
-  if (d_usedSets.empty()) {
-    d_careSetsOutstanding++;
-    return ITECareSimplifier::CareSetPtr::mkNew(*this);
-  }
-  else {
-    ITECareSimplifier::CareSetPtr cs =
-        ITECareSimplifier::CareSetPtr::recycle(d_usedSets.back());
-    cs.getCareSet().clear();
-    d_usedSets.pop_back();
-    return cs;
-  }
-}
-
-
-void ITECareSimplifier::updateQueue(CareMap& queue,
-                                    TNode e,
-                                    ITECareSimplifier::CareSetPtr& careSet)
-{
-  CareMap::iterator it = queue.find(e), iend = queue.end();
-  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(),
-                     inserter(csNew.getCareSet(), csNew.getCareSet().begin()));
-    (*it).second = csNew;
-  }
-  else {
-    queue[e] = careSet;
-  }
-}
-
-
-Node ITECareSimplifier::substitute(TNode e, TNodeMap& substTable, TNodeMap& cache)
-{
-  TNodeMap::iterator it = cache.find(e), iend = cache.end();
-  if (it != iend) {
-    return it->second;
-  }
-
-  // do substitution?
-  it = substTable.find(e);
-  iend = substTable.end();
-  if (it != iend) {
-    Node result = substitute(it->second, substTable, cache);
-    cache[e] = result;
-    return result;
-  }
-
-  size_t sz = e.getNumChildren();
-  if (sz == 0) {
-    cache[e] = e;
-    return e;
-  }
-
-  NodeBuilder<> builder(e.getKind());
-  if (e.getMetaKind() == kind::metakind::PARAMETERIZED) {
-    builder << e.getOperator();
-  }
-  for (unsigned i = 0; i < e.getNumChildren(); ++ i) {
-    builder << substitute(e[i], substTable, cache);
-  }
-
-  Node result = builder;
-  // it = substTable.find(result);
-  // if (it != iend) {
-  //   result = substitute(it->second, substTable, cache);
-  // }
-  cache[e] = result;
-  return result;
-}
-
-
-Node ITECareSimplifier::simplifyWithCare(TNode e)
-{
-  TNodeMap substTable;
-
-  /* This extra block is to trigger the destructors for cs and cs2
-   * before starting garbage collection.
-   */
-  {
-    CareMap queue;
-    CareMap::iterator it;
-    ITECareSimplifier::CareSetPtr cs = getNewSet();
-    ITECareSimplifier::CareSetPtr cs2;
-    queue[e] = cs;
-
-    TNode v;
-    bool done;
-    unsigned i;
-
-    while (!queue.empty()) {
-      it = queue.end();
-      --it;
-      v = it->first;
-      cs = it->second;
-      set<Node>& css = cs.getCareSet();
-      queue.erase(v);
-
-      done = false;
-      set<Node>::iterator iCare, iCareEnd = css.end();
-
-      switch (v.getKind()) {
-        case kind::ITE: {
-          iCare = css.find(v[0]);
-          if (iCare != iCareEnd) {
-            Assert(substTable.find(v) == substTable.end());
-            substTable[v] = v[1];
-            updateQueue(queue, v[1], cs);
-            done = true;
-            break;
-          }
-          else {
-            iCare = css.find(v[0].negate());
-            if (iCare != iCareEnd) {
-              Assert(substTable.find(v) == substTable.end());
-              substTable[v] = v[2];
-              updateQueue(queue, v[2], cs);
-              done = true;
-              break;
-            }
-          }
-          updateQueue(queue, v[0], cs);
-          cs2 = getNewSet();
-          cs2.getCareSet() = css;
-          cs2.getCareSet().insert(v[0]);
-          updateQueue(queue, v[1], cs2);
-          cs2 = getNewSet();
-          cs2.getCareSet() = css;
-          cs2.getCareSet().insert(v[0].negate());
-          updateQueue(queue, v[2], cs2);
-          done = true;
-          break;
-        }
-        case kind::AND: {
-          for (i = 0; i < v.getNumChildren(); ++i) {
-            iCare = css.find(v[i].negate());
-            if (iCare != iCareEnd) {
-              Assert(substTable.find(v) == substTable.end());
-              substTable[v] = d_false;
-              done = true;
-              break;
-            }
-          }
-          if (done) break;
-
-          Assert(v.getNumChildren() > 1);
-          updateQueue(queue, v[0], cs);
-          cs2 = getNewSet();
-          cs2.getCareSet() = css;
-          cs2.getCareSet().insert(v[0]);
-          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) {
-            iCare = css.find(v[i]);
-            if (iCare != iCareEnd) {
-              Assert(substTable.find(v) == substTable.end());
-              substTable[v] = d_true;
-              done = true;
-              break;
-            }
-          }
-          if (done) break;
-
-          Assert(v.getNumChildren() > 1);
-          updateQueue(queue, v[0], cs);
-          cs2 = getNewSet();
-          cs2.getCareSet() = css;
-          cs2.getCareSet().insert(v[0].negate());
-          for (i = 1; i < v.getNumChildren(); ++i) {
-            updateQueue(queue, v[i], cs2);
-          }
-          done = true;
-          break;
-        }
-        default:
-          break;
-      }
-
-      if (done) {
-        continue;
-      }
-
-      for (unsigned i = 0; i < v.getNumChildren(); ++i) {
-        updateQueue(queue, v[i], cs);
-      }
-    }
-  }
-  /* Perform garbage collection. */
-  while (!d_usedSets.empty()) {
-    CareSetPtrVal* used = d_usedSets.back();
-    d_usedSets.pop_back();
-    Assert(used->safeToGarbageCollect());
-    delete used;
-    Assert(d_careSetsOutstanding > 0);
-    d_careSetsOutstanding--;
-  }
-
-  TNodeMap cache;
-  return substitute(e, substTable, cache);
-}
-
-ITECareSimplifier::CareSetPtr ITECareSimplifier::CareSetPtr::mkNew(
-    ITECareSimplifier& simp) {
-  CareSetPtrVal* val = new CareSetPtrVal(simp);
-  return CareSetPtr(val);
-}
-
-
-
-} /* namespace theory */
-} /* namespace CVC4 */
diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h
deleted file mode 100644
index bfce390eb..000000000
--- a/src/theory/ite_utilities.h
+++ /dev/null
@@ -1,389 +0,0 @@
-/*********************                                                        */
-/*! \file ite_utilities.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Paul Meng, 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.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Simplifications for ITE expressions
- **
- ** 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
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__ITE_UTILITIES_H
-#define __CVC4__ITE_UTILITIES_H
-
-#include <unordered_map>
-#include <vector>
-
-#include "expr/node.h"
-#include "util/hash.h"
-#include "util/statistics_registry.h"
-
-namespace CVC4 {
-namespace theory {
-
-class IncomingArcCounter;
-class TermITEHeightCounter;
-class ITECompressor;
-class ITESimplifier;
-class ITECareSimplifier;
-
-/**
- * A caching visitor that computes whether a node contains a term ite.
- */
-class ContainsTermITEVisitor {
-public:
-  ContainsTermITEVisitor();
-  ~ContainsTermITEVisitor();
-
-  /** returns true if a node contains a term ite. */
-  bool containsTermITE(TNode n);
-
-  /** Garbage collects the cache. */
-  void garbageCollect();
-
-  /** returns the size of the cache. */
-  size_t cache_size() const { return d_cache.size(); }
-
-private:
-  typedef std::unordered_map<Node, bool, NodeHashFunction> NodeBoolMap;
-  NodeBoolMap d_cache;
-};
-
-class ITEUtilities
-{
- public:
-  ITEUtilities();
-  ~ITEUtilities();
-
-  Node simpITE(TNode assertion);
-
-  bool simpIteDidALotOfWorkHeuristic() const;
-
-  /* returns false if an assertion is discovered to be equal to false. */
-  bool compress(std::vector<Node>& assertions);
-
-  Node simplifyWithCare(TNode e);
-
-  void clear();
-
-  ContainsTermITEVisitor* getContainsVisitor()
-  {
-    return d_containsVisitor.get();
-  }
-
-  bool containsTermITE(TNode n)
-  {
-    return d_containsVisitor->containsTermITE(n);
-  }
-
- private:
-  std::unique_ptr<ContainsTermITEVisitor> d_containsVisitor;
-  ITECompressor* d_compressor;
-  ITESimplifier* d_simplifier;
-  ITECareSimplifier* d_careSimp;
-};
-
-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 {
-    NodeCountMap::const_iterator it = d_reachCount.find(n);
-    if(it == d_reachCount.end()){
-      return 0;
-    }else{
-      return (*it).second;
-    }
-  }
-  void clear();
-private:
-  typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
-  NodeCountMap d_reachCount;
-
-  bool d_skipVariables;
-  bool d_skipConstants;
-};
-
-class TermITEHeightCounter {
-public:
-  TermITEHeightCounter();
-  ~TermITEHeightCounter();
-
-  /**
-   * Compute and [potentially] cache the termITEHeight() of e.
-   * The term ite height equals the maximum number of term ites
-   * encountered on any path from e to a leaf.
-   * Inductively:
-   *  - 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))
-   */
-  uint32_t termITEHeight(TNode e);
-
-  /** Clear the cache. */
-  void clear();
-
-  /** Size of the cache. */
-  size_t cache_size() const;
-
-private:
-  typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
-  NodeCountMap d_termITEHeight;
-}; /* class TermITEHeightCounter */
-
-/**
- * A routine designed to undo the potentially large blow up
- * due to expansion caused by the ite simplifier.
- */
-class ITECompressor {
-public:
-  ITECompressor(ContainsTermITEVisitor* contains);
-  ~ITECompressor();
-
-  /* returns false if an assertion is discovered to be equal to false. */
-  bool compress(std::vector<Node>& assertions);
-
-  /* garbage Collects the compressor. */
-  void garbageCollect();
-
-private:
-
-  Node d_true; /* Copy of true. */
-  Node d_false; /* Copy of false. */
-  ContainsTermITEVisitor* d_contains;
-  std::vector<Node>* d_assertions;
-  IncomingArcCounter d_incoming;
-
-  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
-  NodeMap d_compressed;
-
-  void reset();
-
-  Node push_back_boolean(Node original, Node compressed);
-  bool multipleParents(TNode c);
-  Node compressBooleanITEs(Node toCompress);
-  Node compressTerm(Node toCompress);
-  Node compressBoolean(Node toCompress);
-
-  class Statistics {
-  public:
-    IntStat d_compressCalls;
-    IntStat d_skolemsAdded;
-    Statistics();
-    ~Statistics();
-  };
-  Statistics d_statistics;
-}; /* class ITECompressor */
-
-class ITESimplifier {
-public:
-  ITESimplifier(ContainsTermITEVisitor* d_containsVisitor);
-  ~ITESimplifier();
-
-  Node simpITE(TNode assertion);
-
-  bool doneALotOfWorkHeuristic() const;
-  void clearSimpITECaches();
-
-private:
-  Node d_true;
-  Node d_false;
-
-  ContainsTermITEVisitor* d_containsVisitor;
-  inline bool containsTermITE(TNode n) {
-    return d_containsVisitor->containsTermITE(n);
-  }
-  TermITEHeightCounter d_termITEHeight;
-  inline uint32_t termITEHeight(TNode e) {
-    return d_termITEHeight.termITEHeight(e);
-  }
-
-  // ConstantIte is a small inductive sublanguage:
-  //     constant
-  // or  termITE(cnd, ConstantIte, ConstantIte)
-  typedef std::vector<Node> NodeVec;
-  typedef std::unordered_map<Node, NodeVec*, NodeHashFunction > ConstantLeavesMap;
-  ConstantLeavesMap d_constantLeaves;
-
-  // d_constantLeaves satisfies the following invariants:
-  // not containsTermITE(x) then !isKey(x)
-  // 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
-  bool isConstantIte(TNode e);
-
-  /** If its not a constant and containsTermITE(ite),
-   * returns a sorted NodeVec of the leaves. */
-  NodeVec* computeConstantLeaves(TNode ite);
-
-  // 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);
-  Node attemptLiftEquality(TNode atom);
-  Node attemptEagerRemoval(TNode atom);
-
-  // Given ConstantIte trees lcite and rcite,
-  // return a boolean expression equivalent to (= lcite rcite)
-  Node intersectConstantIte(TNode lcite, TNode rcite);
-
-  // Given ConstantIte tree cite and a constant c,
-  // return a boolean expression equivalent to (= lcite c)
-  Node constantIteEqualsConstant(TNode cite, TNode c);
-  uint32_t d_citeEqConstApplications;
-
-  typedef std::pair<Node, Node> NodePair;
-  using NodePairHashFunction =
-      PairHashFunction<Node, Node, NodeHashFunction, NodeHashFunction>;
-  typedef std::unordered_map<NodePair, Node, NodePairHashFunction> NodePairMap;
-  NodePairMap d_constantIteEqualsConstantCache;
-  NodePairMap d_replaceOverCache;
-  NodePairMap d_replaceOverTermIteCache;
-  Node replaceOver(Node n, Node replaceWith, Node simpVar);
-  Node replaceOverTermIte(Node term, Node simpAtom, Node simpVar);
-
-  std::unordered_map<Node, bool, NodeHashFunction> d_leavesConstCache;
-  bool leavesAreConst(TNode e, theory::TheoryId tid);
-  bool leavesAreConst(TNode e);
-
-  NodePairMap d_simpConstCache;
-  Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar);
-  std::unordered_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars;
-  Node getSimpVar(TypeNode t);
-
-  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
-  NodeMap d_simpContextCache;
-  Node createSimpContext(TNode c, Node& iteNode, Node& simpVar);
-
-  NodeMap d_simpITECache;
-  Node simpITEAtom(TNode atom);
-
-
-private:
-  class Statistics {
-  public:
-    IntStat d_maxNonConstantsFolded;
-    IntStat d_unexpected;
-    IntStat d_unsimplified;
-    IntStat d_exactMatchFold;
-    IntStat d_binaryPredFold;
-    IntStat d_specialEqualityFolds;
-    IntStat d_simpITEVisits;
-
-    HistogramStat<uint32_t> d_inSmaller;
-
-    Statistics();
-    ~Statistics();
-  };
-
-  Statistics d_statistics;
-};
-
-class ITECareSimplifier {
-public:
-  ITECareSimplifier();
-  ~ITECareSimplifier();
-
-  Node simplifyWithCare(TNode e);
-
-  void clear();
-private:
-
-  /**
-   * This should always equal the number of care sets allocated by
-   * this object - the number of these that have been deleted. This is
-   * initially 0 and should always be 0 at the *start* of
-   * ~ITECareSimplifier().
-   */
-  unsigned d_careSetsOutstanding;
-
-  Node d_true;
-  Node d_false;
-
-  typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap;
-
-  class CareSetPtr;
-  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) {}
-  }; /* class ITECareSimplifier::CareSetPtrVal */
-
-  std::vector<CareSetPtrVal*> d_usedSets;
-  void careSetPtrGC(CareSetPtrVal* val) {
-    d_usedSets.push_back(val);
-  }
-
-  class CareSetPtr {
-    CareSetPtrVal* d_val;
-    CareSetPtr(CareSetPtrVal* val) : d_val(val) {}
-  public:
-    CareSetPtr() : d_val(NULL) {}
-    CareSetPtr(const CareSetPtr& cs) {
-      d_val = cs.d_val;
-      if (d_val != NULL) {
-        ++(d_val->d_refCount);
-      }
-    }
-    ~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)) {
-          d_val->d_iteSimplifier.careSetPtrGC(d_val);
-        }
-        d_val = cs.d_val;
-        if (d_val != NULL) {
-          ++(d_val->d_refCount);
-        }
-      }
-      return *this;
-    }
-    std::set<Node>& getCareSet() { return d_val->d_careSet; }
-
-    static CareSetPtr mkNew(ITECareSimplifier& simp);
-    static CareSetPtr recycle(CareSetPtrVal* val) {
-      Assert(val != NULL && val->d_refCount == 0);
-      val->d_refCount = 1;
-      return CareSetPtr(val);
-    }
-  }; /* class ITECareSimplifier::CareSetPtr */
-
-  CareSetPtr getNewSet();
-
-  typedef std::map<TNode, CareSetPtr> CareMap;
-  void updateQueue(CareMap& queue, TNode e, CareSetPtr& careSet);
-  Node substitute(TNode e, TNodeMap& substTable, TNodeMap& cache);
-};
-
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif
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;