Substantial Changes:

-ITE Simplification -- Moved the utilities in src/theory/ite_simplifier.{h,cpp} to ite_utilities. -- Separated simpWithCare from simpITE. -- Disabled ite simplification on repeat simplification by default. Currently, ite simplification cannot help unless we internally make new constant leaf ites equal to constants. -- simplifyWithCare() is now only run on QF_AUFBV by default. Speeds up nec benchmarks dramatically. -- Added a new compress ites pass that is only run on QF_LIA by default. This targets the perverse structure of ites generated during ite simplification on nec benchmarks. -- After ite simplification, if the ite simplifier was used many times and the NodeManager's node pool is large enough, this garbage collects: zombies from the NodeManager repeatedly, the ite simplification caches, and the theory rewrite caches. - TheoryEngine -- Added TheoryEngine::donePPSimpITE() which orchestrates a number of ite simplifications above. -- Switched UnconstrainedSimplifier to a pointer. - RemoveITEs -- Added a heuristic for checking whether or not a node contains term ites and if not, not bothering to invoke the rest of RemoveITE::run(). This safely changes the type of the cache used on misses of run. This cache can be cleared in the future. Currently disabled pending additional testing. - TypeChecker -- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls. - Theory Bool Rewriter -- Added additional simplifications for boolean ites. Minor Changes: - TheoryModel -- Removed vestigial copy of the ITESimplifier. - AttributeManager -- Fixed a garbage collection bug when deleting the node table caused the NodeManager to reclaimZombies() which caused memory corruption by deleting from the attributeManager. - TypeChecker -- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls. -NodeManager -- Added additional functions for reclaiming zombies. -- Exposed the size of the node pool for heuristics that worry about memory consumption. - NaryBuilder -- Added convenience classes for constructing associative and commutative n-ary operators. -- Added a pass that turns associative and commutative n-ary operators into binary operators. (Mostly for printing expressions for strict parsers.)
author: Tim King <taking@cs.nyu.edu> 2013-11-25 18:36:06 -0500
committer: Tim King <taking@cs.nyu.edu> 2013-11-25 18:36:06 -0500
commit: 22df6e9e8618614e8c33700c55705266912500ae (patch)
tree: 20d78676c1e819517f371e8bc5e6363008fc9154 /src
parent: 91424455840a7365a328cbcc3d02ec453fe9d0ea (diff)
28 files changed, 2697 insertions, 744 deletions
diff --git a/src/Makefile.am b/src/Makefile.am
index 1858d4d32..d6a0ffe0a 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -142,8 +142,8 @@ libcvc4_la_SOURCES = \
 	theory/shared_terms_database.cpp \
 	theory/term_registration_visitor.h \
 	theory/term_registration_visitor.cpp \
-	theory/ite_simplifier.h \
-	theory/ite_simplifier.cpp \
+	theory/ite_utilities.h \
+	theory/ite_utilities.cpp \
 	theory/unconstrained_simplifier.h \
 	theory/unconstrained_simplifier.cpp \
 	theory/quantifiers_engine.h \
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 92a21546c..056e68c69 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -26,6 +26,19 @@ namespace CVC4 {
 namespace expr {
 namespace attr {
 
+AttributeManager::AttributeManager(context::Context* ctxt) :
+  d_cdbools(ctxt),
+  d_cdints(ctxt),
+  d_cdtnodes(ctxt),
+  d_cdnodes(ctxt),
+  d_cdstrings(ctxt),
+  d_cdptrs(ctxt),
+  d_inGarbageCollection(false)
+{}
+
+bool AttributeManager::inGarbageCollection() const {
+  return d_inGarbageCollection;
+}
 
 void AttributeManager::debugHook(int debugFlag) {
   /* DO NOT CHECK IN ANY CODE INTO THE DEBUG HOOKS!
@@ -36,6 +49,7 @@ void AttributeManager::debugHook(int debugFlag) {
 }
 
 void AttributeManager::deleteAllAttributes(NodeValue* nv) {
+  Assert(!inGarbageCollection());
   d_bools.erase(nv);
   deleteFromTable(d_ints, nv);
   deleteFromTable(d_tnodes, nv);
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 605427190..1e3f25461 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -101,17 +101,14 @@ class AttributeManager {
   template <class T, bool context_dep>
   friend struct getTable;
 
+  bool d_inGarbageCollection;
+
+  void clearDeleteAllAttributesBuffer();
+
 public:
 
   /** Construct an attribute manager. */
-  AttributeManager(context::Context* ctxt) :
-    d_cdbools(ctxt),
-    d_cdints(ctxt),
-    d_cdtnodes(ctxt),
-    d_cdnodes(ctxt),
-    d_cdstrings(ctxt),
-    d_cdptrs(ctxt) {
-  }
+  AttributeManager(context::Context* ctxt);
 
   /**
    * Get a particular attribute on a particular node.
@@ -177,6 +174,10 @@ public:
    */
   void deleteAllAttributes();
 
+  /**
+   * Returns true if a table is currently being deleted.
+   */
+  bool inGarbageCollection() const ;
 
   /**
    * Determines the AttrTableId of an attribute.
@@ -563,6 +564,8 @@ AttributeManager::setAttribute(NodeValue* nv,
 /**
  * Search for the NodeValue in all attribute tables and remove it,
  * calling the cleanup function if one is defined.
+ *
+ * This cannot use nv as anything other than a pointer!
  */
 template <class T>
 inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
@@ -600,6 +603,9 @@ inline void AttributeManager::deleteFromTable(CDAttrHash<T>& table,
  */
 template <class T>
 inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
+  Assert(!d_inGarbageCollection);
+  d_inGarbageCollection = true;
+
   bool anyRequireClearing = false;
   typedef AttributeTraits<T, false> traits_t;
   typedef AttrHash<T> hash_t;
@@ -627,6 +633,8 @@ inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
     }
   }
   table.clear();
+  d_inGarbageCollection = false;
+  Assert(!d_inGarbageCollection);
 }
 
 template <class AttrKind>
@@ -639,6 +647,7 @@ AttributeUniqueId AttributeManager::getAttributeId(const AttrKind& attr){
 
 template <class T>
 void AttributeManager::deleteAttributesFromTable(AttrHash<T>& table, const std::vector<uint64_t>& ids){
+  d_inGarbageCollection = true;
   typedef AttributeTraits<T, false> traits_t;
   typedef AttrHash<T> hash_t;
 
@@ -664,6 +673,7 @@ void AttributeManager::deleteAttributesFromTable(AttrHash<T>& table, const std::
       ++it;
     }
   }
+  d_inGarbageCollection = false;
   static const size_t ReconstructShrinkRatio = 8;
   if(initialSize/ReconstructShrinkRatio > table.size()){
     reconstructTable(table);
@@ -672,10 +682,12 @@ void AttributeManager::deleteAttributesFromTable(AttrHash<T>& table, const std::
 
 template <class T>
 void AttributeManager::reconstructTable(AttrHash<T>& table){
+  d_inGarbageCollection = true;
   typedef AttrHash<T> hash_t;
   hash_t cpy;
   cpy.insert(table.begin(), table.end());
   cpy.swap(table);
+  d_inGarbageCollection = false;
 }
 
 
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 8c94db3cc..9e7a2596f 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -65,6 +65,7 @@ exportConstant_cases=
 
 typerules=
 construles=
+neverconstrules=
 
 seen_theory=false
 seen_theory_builtin=false
@@ -168,6 +169,12 @@ function construle {
 #line $lineno \"$kf\"
     return $2::computeIsConst(nodeManager, n);
 "
+  neverconstrules="${neverconstrules}
+#line $lineno \"$kf\"
+  case kind::$1:
+#line $lineno \"$kf\"
+    return false;
+"
 }
 
 function sort {
@@ -294,6 +301,7 @@ for var in \
     typechecker_includes \
     typerules \
     construles \
+    neverconstrules \
     ; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 done
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index b1614f31b..39bbfbc2e 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -73,6 +73,10 @@ bool NodeTemplate<ref_count>::isConst() const {
     Debug("isConst") << "Node::isConst() returning false, it's a VARIABLE" << std::endl;
     return false;
   default:
+    if(expr::TypeChecker::neverIsConst(NodeManager::currentNM(), *this)){
+      Debug("isConst") << "Node::isConst() returning false, the kind is never const" << std::endl;
+      return false;
+    }
     if(getAttribute(IsConstComputedAttr())) {
       bool bval = getAttribute(IsConstAttr());
       Debug("isConst") << "Node::isConst() returning cached value " << (bval ? "true" : "false") << " for: " << *this << std::endl;
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index cede6ff1f..9c76a41f3 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -134,6 +134,7 @@ NodeManager::~NodeManager() {
     d_operators[i] = Node::null();
   }
 
+  Assert(!d_attrManager->inGarbageCollection() );
   while(!d_zombies.empty()) {
     reclaimZombies();
   }
@@ -161,6 +162,7 @@ NodeManager::~NodeManager() {
 
 void NodeManager::reclaimZombies() {
   // FIXME multithreading
+  Assert(!d_attrManager->inGarbageCollection());
 
   Debug("gc") << "reclaiming " << d_zombies.size() << " zombie(s)!\n";
 
@@ -435,6 +437,23 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
   return dtt;
 }
 
+void NodeManager::reclaimAllZombies(){
+  reclaimZombiesUntil(0u);
+}
+
+/** Reclaim zombies while there are more than k nodes in the pool (if possible).*/
+void NodeManager::reclaimZombiesUntil(uint32_t k){
+  if(safeToReclaimZombies()){
+    while(poolSize() >= k && !d_zombies.empty()){
+      reclaimZombies();
+    }
+  }
+}
+
+size_t NodeManager::poolSize() const{
+  return d_nodeValuePool.size();
+}
+
 TypeNode NodeManager::mkSort(uint32_t flags) {
   NodeBuilder<1> nb(this, kind::SORT_TYPE);
   Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
@@ -586,6 +605,11 @@ Node NodeManager::mkAbstractValue(const TypeNode& type) {
   return n;
 }
 
+bool NodeManager::safeToReclaimZombies() const{
+  // FIXME multithreading
+  return !d_inReclaimZombies && !d_attrManager->inGarbageCollection();
+}
+
 void NodeManager::deleteAttributes(const std::vector<const expr::attr::AttributeUniqueId*>& ids){
   d_attrManager->deleteAttributes(ids);
 }
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 32c492003..af771bd89 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -229,8 +229,7 @@ class NodeManager {
     }
     d_zombies.insert(nv);// FIXME multithreading
 
-    if(!d_inReclaimZombies) {// FIXME multithreading
-      // for now, collect eagerly.  can add heuristic here later..
+    if(safeToReclaimZombies()) {
       if(d_zombies.size() > 5000) {
         reclaimZombies();
       }
@@ -243,6 +242,11 @@ class NodeManager {
   void reclaimZombies();
 
   /**
+   * It is safe to collect zombies.
+   */
+  bool safeToReclaimZombies() const;
+
+  /**
    * This template gives a mechanism to stack-allocate a NodeValue
    * with enough space for N children (where N is a compile-time
    * constant).  You use it like this:
@@ -860,6 +864,15 @@ public:
    */
   static inline TypeNode fromType(Type t);
 
+  /** Reclaim zombies while there are more than k nodes in the pool (if possible).*/
+  void reclaimZombiesUntil(uint32_t k);
+
+  /** Reclaims all zombies (if possible).*/
+  void reclaimAllZombies();
+
+  /** Size of the node pool. */
+  size_t poolSize() const;
+
   /** Deletes a list of attributes from the NM's AttributeManager.*/
   void deleteAttributes(const std::vector< const expr::attr::AttributeUniqueId* >& ids);
 
@@ -871,7 +884,6 @@ public:
    * any published code!
    */
   void debugHook(int debugFlag);
-
 };/* class NodeManager */
 
 /**
diff --git a/src/expr/options b/src/expr/options
index 223189d1b..cf893a7a5 100644
--- a/src/expr/options
+++ b/src/expr/options
@@ -21,5 +21,8 @@ option earlyTypeChecking --eager-type-checking/--lazy-type-checking bool :defaul
 option typeChecking /--no-type-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--lazy-type-checking
  never type check expressions
 
+option biasedITERemoval --biased-ites bool :default false
+ try the new remove ite pass that is biased against term ites appearing
+
 endmodule
 
diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h
index ac461bb7b..d34a7c7d6 100644
--- a/src/expr/type_checker.h
+++ b/src/expr/type_checker.h
@@ -34,6 +34,9 @@ public:
   static bool computeIsConst(NodeManager* nodeManager, TNode n)
     throw (AssertionException);
 
+  static bool neverIsConst(NodeManager* nodeManager, TNode n)
+    throw (AssertionException);
+
 };/* class TypeChecker */
 
 }/* CVC4::expr namespace */
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index b2138c9a1..4e476f4d9 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -78,5 +78,22 @@ ${construles}
 
 }/* TypeChecker::computeIsConst */
 
+bool TypeChecker::neverIsConst(NodeManager* nodeManager, TNode n)
+  throw (AssertionException) {
+
+  Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED);
+
+  switch(n.getKind()) {
+${neverconstrules}
+
+#line 90 "${template}"
+
+  default:;
+  }
+
+  return true;
+
+}/* TypeChecker::neverIsConst */
+
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */
diff --git a/src/smt/options b/src/smt/options
index d2455b520..6b9944cdd 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -42,18 +42,31 @@ common-option interactive interactive-mode --interactive bool :read-write
 option doITESimp --ite-simp bool :read-write
  turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)
 
+option doITESimpOnRepeat --on-repeat-ite-simp bool :read-write :default false
+ do the ite simplification pass again if repeating simplification
+
+option simplifyWithCareEnabled --simp-with-care bool :default false :read-write
+ enables simplifyWithCare in ite simplificiation
+
+option compressItes --simp-ite-compress bool :default false :read-write
+ enables compressing ites after ite simplification
+
 option unconstrainedSimp --unconstrained-simp bool :default false :read-write
  turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)
 
 option repeatSimp --repeat-simp bool :read-write
  make multiple passes with nonclausal simplifier
 
+option zombieHuntThreshold --simp-ite-hunt-zombies uint32_t :default 524288
+ post ite compression enables zombie removal while the number of nodes is above this threshold
+
 option sortInference --sort-inference bool :read-write :default false
  calculate sort inference of input problem, convert the input based on monotonic sorts
 
 common-option incrementalSolving incremental -i --incremental bool
  enable incremental solving
 
+
 option abstractValues abstract-values --abstract-values bool :default false
  in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard
 option modelUninterpDtEnum --model-u-dt-enum bool :default false
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 21f2d9209..2cc606fa9 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -52,6 +52,7 @@
 #include "util/node_visitor.h"
 #include "util/configuration.h"
 #include "util/exception.h"
+#include "util/nary_builder.h"
 #include "smt/command_list.h"
 #include "smt/boolean_terms.h"
 #include "smt/options.h"
@@ -90,6 +91,19 @@ namespace CVC4 {
 
 namespace smt {
 
+/** Useful for counting the number of recursive calls. */
+class ScopeCounter {
+private:
+  unsigned& d_depth;
+public:
+  ScopeCounter(unsigned& d) : d_depth(d) {
+    ++d_depth;
+  }
+  ~ScopeCounter(){
+    --d_depth;
+  }
+};
+
 /**
  * Representation of a defined function.  We keep these around in
  * SmtEngine to permit expanding definitions late (and lazily), to
@@ -150,6 +164,9 @@ struct SmtEngineStatistics {
   /** time spent in processAssertions() */
   TimerStat d_processAssertionsTime;
 
+  /** Has something simplified to false? */
+  IntStat d_simplifiedToFalse;
+
   SmtEngineStatistics() :
     d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
     d_rewriteBooleanTermsTime("smt::SmtEngine::rewriteBooleanTermsTime"),
@@ -168,7 +185,10 @@ struct SmtEngineStatistics {
     d_checkModelTime("smt::SmtEngine::checkModelTime"),
     d_solveTime("smt::SmtEngine::solveTime"),
     d_pushPopTime("smt::SmtEngine::pushPopTime"),
-    d_processAssertionsTime("smt::SmtEngine::processAssertionsTime") {
+    d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
+    d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0)
+
+ {
 
     StatisticsRegistry::registerStat(&d_definitionExpansionTime);
     StatisticsRegistry::registerStat(&d_rewriteBooleanTermsTime);
@@ -188,6 +208,7 @@ struct SmtEngineStatistics {
     StatisticsRegistry::registerStat(&d_solveTime);
     StatisticsRegistry::registerStat(&d_pushPopTime);
     StatisticsRegistry::registerStat(&d_processAssertionsTime);
+    StatisticsRegistry::registerStat(&d_simplifiedToFalse);
   }
 
   ~SmtEngineStatistics() {
@@ -209,6 +230,7 @@ struct SmtEngineStatistics {
     StatisticsRegistry::unregisterStat(&d_solveTime);
     StatisticsRegistry::unregisterStat(&d_pushPopTime);
     StatisticsRegistry::unregisterStat(&d_processAssertionsTime);
+    StatisticsRegistry::unregisterStat(&d_simplifiedToFalse);
   }
 };/* struct SmtEngineStatistics */
 
@@ -305,6 +327,10 @@ class SmtEnginePrivate : public NodeManagerListener {
    */
   Node d_modZero;
 
+  /** Number of calls of simplify assertions active.
+   */
+  unsigned d_simplifyAssertionsDepth;
+
 public:
   /**
    * Map from skolem variables to index in d_assertionsToCheck containing
@@ -353,11 +379,15 @@ private:
   void bvToBool();
 
   // Simplify ITE structure
-  void simpITE();
+  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);
+
   /**
    * Any variable in an assertion that is declared as a subtype type
    * (predicate subtype or integer subrange type) must be constrained
@@ -402,6 +432,7 @@ public:
     d_divByZero(),
     d_intDivByZero(),
     d_modZero(),
+    d_simplifyAssertionsDepth(0),
     d_iteSkolemMap(),
     d_iteRemover(smt.d_userContext),
     d_topLevelSubstitutions(smt.d_userContext)
@@ -869,12 +900,41 @@ void SmtEngine::setLogicInternal() throw() {
   }
   // Turn on ite simplification for QF_LIA and QF_AUFBV
   if(! options::doITESimp.wasSetByUser()) {
-    bool iteSimp = !d_logic.isQuantified() &&
-      ((d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areRealsUsed()) ||
-       (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_UF) && d_logic.isTheoryEnabled(THEORY_BV)));
+    bool qf_aufbv = !d_logic.isQuantified() &&
+      d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+      d_logic.isTheoryEnabled(THEORY_UF) &&
+      d_logic.isTheoryEnabled(THEORY_BV);
+    bool qf_lia = !d_logic.isQuantified() &&
+      d_logic.isPure(THEORY_ARITH) &&
+      d_logic.isLinear() &&
+      !d_logic.isDifferenceLogic() &&
+      !d_logic.areRealsUsed();
+
+    bool iteSimp = (qf_aufbv || qf_lia);
     Trace("smt") << "setting ite simplification to " << iteSimp << endl;
     options::doITESimp.set(iteSimp);
   }
+  if(! options::compressItes.wasSetByUser() ){
+    bool qf_lia = !d_logic.isQuantified() &&
+      d_logic.isPure(THEORY_ARITH) &&
+      d_logic.isLinear() &&
+      !d_logic.isDifferenceLogic() &&
+      !d_logic.areRealsUsed();
+
+    bool compressIte = qf_lia;
+    Trace("smt") << "setting ite compression to " << compressIte << endl;
+    options::compressItes.set(compressIte);
+  }
+  if(! options::simplifyWithCareEnabled.wasSetByUser() ){
+    bool qf_aufbv = !d_logic.isQuantified() &&
+      d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+      d_logic.isTheoryEnabled(THEORY_UF) &&
+      d_logic.isTheoryEnabled(THEORY_BV);
+
+    bool withCare = qf_aufbv;
+    Trace("smt") << "setting ite simplify with care to " << withCare << endl;
+    options::simplifyWithCareEnabled.set(withCare);
+  }
   // Turn off array eager index splitting for QF_AUFLIA
   if(! options::arraysEagerIndexSplitting.wasSetByUser()) {
     if (not d_logic.isQuantified() &&
@@ -2031,16 +2091,56 @@ void SmtEnginePrivate::bvToBool() {
   }
 }
 
-void SmtEnginePrivate::simpITE() {
+bool SmtEnginePrivate::simpITE() {
   TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime);
 
   Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl;
 
+  unsigned numAssertionOnEntry = d_assertionsToCheck.size();
   for (unsigned i = 0; i < d_assertionsToCheck.size(); ++i) {
-    d_assertionsToCheck[i] = d_smt.d_theoryEngine->ppSimpITE(d_assertionsToCheck[i]);
+    Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertionsToCheck[i]);
+    d_assertionsToCheck[i] = result;
+    if(result.isConst() && !result.getConst<bool>()){
+      return false;
+    }
   }
+  bool result = d_smt.d_theoryEngine->donePPSimpITE(d_assertionsToCheck);
+  if(numAssertionOnEntry < d_assertionsToCheck.size()){
+    compressBeforeRealAssertions(numAssertionOnEntry);
+  }
+  return result;
 }
 
+void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){
+  size_t curr = d_assertionsToCheck.size();
+  if(before >= curr ||
+     d_realAssertionsEnd <= 0 ||
+     d_realAssertionsEnd >= curr){
+    return;
+  }
+
+  // assertions
+  // original: [0 ... d_realAssertionsEnd)
+  //  can be modified
+  // ites skolems [d_realAssertionsEnd, before)
+  //  cannot be moved
+  // added [before, curr)
+  //  can be modified
+  Assert(0 < d_realAssertionsEnd);
+  Assert(d_realAssertionsEnd <= before);
+  Assert(before < curr);
+
+  std::vector<Node> intoConjunction;
+  for(size_t i = before; i<curr; ++i){
+    intoConjunction.push_back(d_assertionsToCheck[i]);
+  }
+  d_assertionsToCheck.resize(before);
+  size_t lastBeforeItes = d_realAssertionsEnd - 1;
+  intoConjunction.push_back(d_assertionsToCheck[lastBeforeItes]);
+  Node newLast = util::NaryBuilder::mkAssoc(kind::AND, intoConjunction);
+  d_assertionsToCheck[lastBeforeItes] = newLast;
+  Assert(d_assertionsToCheck.size() == before);
+}
 
 void SmtEnginePrivate::unconstrainedSimp() {
   TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime);
@@ -2490,11 +2590,13 @@ void SmtEnginePrivate::doMiplibTrick() {
   d_realAssertionsEnd = d_assertionsToCheck.size();
 }
 
+
 // returns false if simplification led to "false"
 bool SmtEnginePrivate::simplifyAssertions()
   throw(TypeCheckingException, LogicException) {
   Assert(d_smt.d_pendingPops == 0);
   try {
+    ScopeCounter depth(d_simplifyAssertionsDepth);
 
     Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
 
@@ -2560,9 +2662,14 @@ bool SmtEnginePrivate::simplifyAssertions()
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
     // ITE simplification
-    if(options::doITESimp()) {
+    if(options::doITESimp() &&
+       (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat())) {
       Chat() << "...doing ITE simplification..." << endl;
-      simpITE();
+      bool noConflict = simpITE();
+      if(!noConflict){
+        Chat() << "...ITE simplification found unsat..." << endl;
+        return false;
+      }
     }
 
     dumpAssertions("post-itesimp", d_assertionsToCheck);
@@ -2916,6 +3023,9 @@ void SmtEnginePrivate::processAssertions() {
   dumpAssertions("pre-simplify", d_assertionsToPreprocess);
   Chat() << "simplifying assertions..." << endl;
   bool noConflict = simplifyAssertions();
+  if(!noConflict){
+    ++(d_smt.d_stats->d_simplifiedToFalse);
+  }
   dumpAssertions("post-simplify", d_assertionsToCheck);
 
   dumpAssertions("pre-static-learning", d_assertionsToCheck);
@@ -2954,6 +3064,7 @@ void SmtEnginePrivate::processAssertions() {
   if(options::repeatSimp()) {
     d_assertionsToCheck.swap(d_assertionsToPreprocess);
     Chat() << "re-simplifying assertions..." << endl;
+    ScopeCounter depth(d_simplifyAssertionsDepth);
     noConflict &= simplifyAssertions();
     if (noConflict) {
       // Need to fix up assertion list to maintain invariants:
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index 9867ccd4e..1caa4b429 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -22,6 +22,10 @@ namespace CVC4 {
 namespace theory {
 namespace booleans {
 
+RewriteResponse TheoryBoolRewriter::postRewrite(TNode node) {
+  return preRewrite(node);
+}
+
 /**
  * flattenNode looks for children of same kind, and if found merges
  * them into the parent.
@@ -88,6 +92,40 @@ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode)
   }
 }
 
+// Equality parity returns
+// * 0 if no relation between a and b is found
+// * 1 if a == b
+// * 2 if a == not(b)
+// * 3 or b == not(a)
+inline int equalityParity(TNode a, TNode b){
+  if(a == b){
+    return 1;
+  }else if(a.getKind() == kind::NOT && a[0] == b){
+    return 2;
+  }else if(b.getKind() == kind::NOT && b[0] == a){
+    return 3;
+  }else{
+    return 0;
+  }
+}
+
+inline Node makeNegation(TNode n){
+  bool even = false;
+  while(n.getKind() == kind::NOT){
+    n = n[0];
+    even = !even;
+  }
+  if(even){
+    return n;
+  } else {
+    if(n.isConst()){
+      return NodeManager::currentNM()->mkConst(!n.getConst<bool>());
+    }else{
+      return n.notNode();
+    }
+  }
+}
+
 RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
   NodeManager* nodeManager = NodeManager::currentNM();
   Node tt = nodeManager->mkConst(true);
@@ -132,7 +170,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
     if (n[0] == ff || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt);
     if (n[0] == tt && n[0] == ff) return RewriteResponse(REWRITE_DONE, ff);
     if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]);
-    if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, n[0].notNode());
+    if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
     break;
   }
   case kind::IFF:
@@ -146,10 +184,10 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
       return RewriteResponse(REWRITE_AGAIN, n[0]);
     } else if(n[0] == ff) {
       // IFF false x
-      return RewriteResponse(REWRITE_AGAIN, n[1].notNode());
+      return RewriteResponse(REWRITE_AGAIN, makeNegation(n[1]));
     } else if(n[1] == ff) {
       // IFF x false
-      return RewriteResponse(REWRITE_AGAIN, n[0].notNode());
+      return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
     } else if(n[0] == n[1]) {
       // IFF x x
       return RewriteResponse(REWRITE_DONE, tt);
@@ -207,7 +245,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
           if(kappa.knownLessThanOrEqual(two)){
             return RewriteResponse(REWRITE_DONE, ff);
           }else{
-            Node neitherEquality = (n[0].notNode()).andNode(n[1].notNode());
+            Node neitherEquality = (makeNegation(n[0])).andNode(makeNegation(n[1]));
             return RewriteResponse(REWRITE_AGAIN, neitherEquality);
           }
         }
@@ -219,10 +257,10 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
     // rewrite simple cases of XOR
     if(n[0] == tt) {
       // XOR true x
-      return RewriteResponse(REWRITE_AGAIN, n[1].notNode());
+      return RewriteResponse(REWRITE_AGAIN, makeNegation(n[1]));
     } else if(n[1] == tt) {
       // XCR x true
-      return RewriteResponse(REWRITE_AGAIN, n[0].notNode());
+      return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
     } else if(n[0] == ff) {
       // XOR false x
       return RewriteResponse(REWRITE_AGAIN, n[1]);
@@ -248,33 +286,79 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
     if (n[0].isConst()) {
       if (n[0] == tt) {
         // ITE true x y
+
+        Debug("bool-ite") << "n[0] ==tt " << n << ": " << n[1] << std::endl;
         return RewriteResponse(REWRITE_AGAIN, n[1]);
       } else {
         Assert(n[0] == ff);
         // ITE false x y
+        Debug("bool-ite") << "n[0] ==ff " << n << ": " << n[1] << std::endl;
         return RewriteResponse(REWRITE_AGAIN, n[2]);
       }
     } else if (n[1].isConst()) {
       if (n[1] == tt && n[2] == ff) {
+        Debug("bool-ite") << "n[1] ==tt && n[2] == ff " << n << ": " << n[0] << std::endl;
         return RewriteResponse(REWRITE_AGAIN, n[0]);
       }
       else if (n[1] == ff && n[2] == tt) {
-        return RewriteResponse(REWRITE_AGAIN, n[0].notNode());
+        Debug("bool-ite") << "n[1] ==ff && n[2] == tt " << n << ": " << n[0].notNode() << std::endl;
+        return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
       }
+      // else if(n[1] == ff){
+      //   Node resp = (n[0].notNode()).andNode(n[2]);
+      //   return RewriteResponse(REWRITE_AGAIN, resp);
+      // }
     }
-    if (n[1] == n[2]) {
-      return RewriteResponse(REWRITE_AGAIN, n[1]);
+    // else if (n[2].isConst()) {
+    //   if(n[2] == ff){
+    //     Node resp = (n[0]).andNode(n[1]);
+    //     return RewriteResponse(REWRITE_AGAIN, resp);
+    //   }
+    // }
+
+    int parityTmp;
+    if ((parityTmp = equalityParity(n[1], n[2])) != 0) {
+      Node resp = (parityTmp == 1) ? (Node)n[1] : n[0].iffNode(n[1]);
+      Debug("bool-ite") << "equalityParity n[1], n[2] " << parityTmp
+                        << " " << n << ": " << resp << std::endl;
+      return RewriteResponse(REWRITE_AGAIN, resp);
     // Curiously, this rewrite affects several benchmarks dramatically, including copy_array and some simple_startup - disable for now
     // } else if (n[0].getKind() == kind::NOT) {
     //   return RewriteResponse(REWRITE_AGAIN, n[0][0].iteNode(n[2], n[1]));
-    } else if (n[0] == n[1]) {
-      return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(tt, n[2]));
-    } else if (n[0] == n[2]) {
-      return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(n[1], ff));
-    } else if (n[1].getKind() == kind::NOT && n[1][0] == n[0]) {
-      return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(ff, n[2]));
-    } else if (n[2].getKind() == kind::NOT && n[2][0] == n[0]) {
-      return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(n[1], tt));
+    } else if(!n[1].isConst() && (parityTmp = equalityParity(n[0], n[1])) != 0){
+      // (parityTmp == 1) if n[0] == n[1]
+      // otherwise, n[0] == not(n[1]) or not(n[0]) == n[1]
+
+      // if n[1] is constant this can loop, this is possible in prewrite
+      Node resp = n[0].iteNode( (parityTmp == 1) ? tt : ff, n[2]);
+      Debug("bool-ite") << "equalityParity n[0], n[1] " << parityTmp
+                        << " " << n << ": " << resp << std::endl;
+      return RewriteResponse(REWRITE_AGAIN, resp);
+    } else if(!n[2].isConst() && (parityTmp = equalityParity(n[0], n[2])) != 0){
+      // (parityTmp == 1) if n[0] == n[2]
+      // otherwise, n[0] == not(n[2]) or not(n[0]) == n[2]
+      Node resp = n[0].iteNode(n[1], (parityTmp == 1) ? ff : tt);
+      Debug("bool-ite") << "equalityParity n[0], n[2] " << parityTmp
+                        << " " << n << ": " << resp << std::endl;
+      return RewriteResponse(REWRITE_AGAIN, resp);
+    } else if(n[1].getKind() == kind::ITE &&
+              (parityTmp = equalityParity(n[0], n[1][0])) != 0){
+      // (parityTmp == 1) then n : (ite c (ite c x y) z)
+      // (parityTmp > 1)  then n : (ite c (ite (not c) x y) z) or
+      // n: (ite (not c) (ite c x y) z)
+      Node resp = n[0].iteNode((parityTmp == 1) ? n[1][1] : n[1][2], n[2]);
+      Debug("bool-ite") << "equalityParity n[0], n[1][0] " << parityTmp
+                        << " " << n << ": " << resp << std::endl;
+      return RewriteResponse(REWRITE_AGAIN, resp);
+    } else if(n[2].getKind() == kind::ITE &&
+              (parityTmp = equalityParity(n[0], n[2][0])) != 0){
+      // (parityTmp == 1) then n : (ite c x (ite c y z))
+      // (parityTmp > 1)  then n : (ite c x (ite (not c) y z)) or
+      // n: (ite (not c) x (ite c y z))
+      Node resp = n[0].iteNode(n[1], (parityTmp == 1) ? n[2][2] : n[2][1]);
+      Debug("bool-ite") << "equalityParity n[0], n[2][0] " << parityTmp
+                        << " " << n << ": " << resp << std::endl;
+      return RewriteResponse(REWRITE_AGAIN, resp);
     }
     break;
   }
diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h
index 96bd2ae29..ac9469980 100644
--- a/src/theory/booleans/theory_bool_rewriter.h
+++ b/src/theory/booleans/theory_bool_rewriter.h
@@ -31,9 +31,7 @@ class TheoryBoolRewriter {
 public:
 
   static RewriteResponse preRewrite(TNode node);
-  static RewriteResponse postRewrite(TNode node) {
-    return preRewrite(node);
-  }
+  static RewriteResponse postRewrite(TNode node);
 
   static void init() {}
   static void shutdown() {}
diff --git a/src/theory/ite_simplifier.cpp b/src/theory/ite_simplifier.cpp
deleted file mode 100644
index 463a9c41a..000000000
--- a/src/theory/ite_simplifier.cpp
+++ /dev/null
@@ -1,501 +0,0 @@
-/*********************                                                        */
-/*! \file ite_simplifier.cpp
- ** \verbatim
- ** Original author: Clark Barrett
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** 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_simplifier.h"
-
-
-using namespace std;
-using namespace CVC4;
-using namespace theory;
-
-
-bool ITESimplifier::containsTermITE(TNode e)
-{
-  if (e.getKind() == kind::ITE && !e.getType().isBoolean()) {
-    return true;
-  }
-
-  hash_map<Node, bool, NodeHashFunction>::iterator it;
-  it = d_containsTermITECache.find(e);
-  if (it != d_containsTermITECache.end()) {
-    return (*it).second;
-  }
-
-  size_t k = 0, sz = e.getNumChildren();
-  for (; k < sz; ++k) {
-    if (containsTermITE(e[k])) {
-      d_containsTermITECache[e] = true;
-      return true;
-    }
-  }
-
-  d_containsTermITECache[e] = false;
-  return false;
-}
-
-
-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;
-  }
-
-  hash_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::hash_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;
-}
-
-
-Node ITESimplifier::simpITEAtom(TNode atom)
-{
-  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));
-        return Rewriter::rewrite(simpContext);
-      }
-      Node n = simpConstants(simpContext, iteNode, simpVar);
-      if (!n.isNull()) {
-        return n;
-      }
-    }
-  }
-  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);
-
-  while (!toVisit.empty())
-  {
-    // 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;
-       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());
-        builder << d_simpITECache[current[i]];
-      }
-      // 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);
-      }
-
-      result = Rewriter::rewrite(result);
-      d_simpITECache[current] = result;
-      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;
-        toVisit.pop_back();
-      }
-    }
-  }
-  return d_simpITECache[assertion];
-}
-
-
-ITESimplifier::CareSetPtr ITESimplifier::getNewSet()
-{
-  if (d_usedSets.empty()) {
-    return ITESimplifier::CareSetPtr::mkNew(*this);
-  }
-  else {
-    ITESimplifier::CareSetPtr cs = ITESimplifier::CareSetPtr::recycle(d_usedSets.back());
-    cs.getCareSet().clear();
-    d_usedSets.pop_back();
-    return cs;
-  }
-}
-
-
-void ITESimplifier::updateQueue(CareMap& queue,
-                               TNode e,
-                               ITESimplifier::CareSetPtr& careSet)
-{
-  CareMap::iterator it = queue.find(e), iend = queue.end();
-  if (it != iend) {
-    set<Node>& cs2 = (*it).second.getCareSet();
-    ITESimplifier::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 ITESimplifier::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 ITESimplifier::simplifyWithCare(TNode e)
-{
-  TNodeMap substTable;
-  CareMap queue;
-  CareMap::iterator it;
-  ITESimplifier::CareSetPtr cs = getNewSet();
-  ITESimplifier::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);
-    }
-  }
-  while (!d_usedSets.empty()) {
-    delete d_usedSets.back();
-    d_usedSets.pop_back();
-  }
-
-  TNodeMap cache;
-  return substitute(e, substTable, cache);
-}
-
diff --git a/src/theory/ite_simplifier.h b/src/theory/ite_simplifier.h
deleted file mode 100644
index 07fa0dedb..000000000
--- a/src/theory/ite_simplifier.h
+++ /dev/null
@@ -1,165 +0,0 @@
-/*********************                                                        */
-/*! \file ite_simplifier.h
- ** \verbatim
- ** Original author: Clark Barrett
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** 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_SIMPLIFIER_H
-#define __CVC4__ITE_SIMPLIFIER_H
-
-#include <deque>
-#include <vector>
-#include <utility>
-
-#include "expr/node.h"
-#include "expr/command.h"
-#include "prop/prop_engine.h"
-#include "context/cdhashset.h"
-#include "theory/theory.h"
-#include "theory/rewriter.h"
-#include "theory/shared_terms_database.h"
-#include "theory/term_registration_visitor.h"
-#include "theory/valuation.h"
-#include "util/statistics_registry.h"
-#include "util/hash.h"
-#include "util/cache.h"
-#include "util/ite_removal.h"
-
-namespace CVC4 {
-namespace theory {
-
-class ITESimplifier {
-  Node d_true;
-  Node d_false;
-
-  std::hash_map<Node, bool, NodeHashFunction> d_containsTermITECache;
-  bool containsTermITE(TNode e);
-
-  std::hash_map<Node, bool, NodeHashFunction> d_leavesConstCache;
-  bool leavesAreConst(TNode e, theory::TheoryId tid);
-  bool leavesAreConst(TNode e)
-    { return leavesAreConst(e, theory::Theory::theoryOf(e)); }
-
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
-  typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap;
-
-  typedef std::pair<Node, Node> NodePair;
-  struct NodePairHashFunction {
-    size_t operator () (const NodePair& pair) const {
-      size_t hash = 0;
-      hash = 0x9e3779b9 + NodeHashFunction().operator()(pair.first);
-      hash ^= 0x9e3779b9 + NodeHashFunction().operator()(pair.second) + (hash << 6) + (hash >> 2);
-      return hash;
-    }
-  };/* struct ITESimplifier::NodePairHashFunction */
-
-  typedef std::hash_map<NodePair, Node, NodePairHashFunction> NodePairMap;
-
-
-  NodePairMap d_simpConstCache;
-  Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar);
-  std::hash_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars;
-  Node getSimpVar(TypeNode t);
-
-  NodeMap d_simpContextCache;
-  Node createSimpContext(TNode c, Node& iteNode, Node& simpVar);
-
-  Node simpITEAtom(TNode atom);
-
-  NodeMap d_simpITECache;
-
-public:
-  Node simpITE(TNode assertion);
-
-private:
-
-  class CareSetPtr;
-  class CareSetPtrVal {
-    friend class ITESimplifier::CareSetPtr;
-    ITESimplifier& d_iteSimplifier;
-    unsigned d_refCount;
-    std::set<Node> d_careSet;
-    CareSetPtrVal(ITESimplifier& simp) : d_iteSimplifier(simp), d_refCount(1) {}
-  };
-
-  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(ITESimplifier& simp) {
-      CareSetPtrVal* val = new CareSetPtrVal(simp);
-      return CareSetPtr(val);
-    }
-    static CareSetPtr recycle(CareSetPtrVal* val) {
-      Assert(val != NULL && val->d_refCount == 0);
-      val->d_refCount = 1;
-      return CareSetPtr(val);
-    }
-  };
-
-  CareSetPtr getNewSet();
-
-  typedef std::map<TNode, CareSetPtr> CareMap;
-  void updateQueue(CareMap& queue, TNode e, CareSetPtr& careSet);
-  Node substitute(TNode e, TNodeMap& substTable, TNodeMap& cache);
-
-public:
-  Node simplifyWithCare(TNode e);
-
-  ITESimplifier() {
-    d_true = NodeManager::currentNM()->mkConst<bool>(true);
-    d_false = NodeManager::currentNM()->mkConst<bool>(false);
-  }
-  ~ITESimplifier() {}
-
-};
-
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif
diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp
new file mode 100644
index 000000000..facd5f4f0
--- /dev/null
+++ b/src/theory/ite_utilities.cpp
@@ -0,0 +1,1613 @@
+/*********************                                                        */
+/*! \file ite_simplifier.cpp
+ ** \verbatim
+ ** Original author: Clark Barrett
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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 "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(){}
+  CTIVStackElement(TNode c) : curr(c), pos(0){ }
+};/* CTIVStackElement */
+
+} /* CVC4::theory::ite */
+
+
+
+ITEUtilities::ITEUtilities(ContainsTermITEVistor* containsVisitor)
+  : d_containsVisitor(containsVisitor)
+  , 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);
+  }
+  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);
+  }
+  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();
+  }
+}
+
+/*********************                                                        */
+/* ContainsTermITEVistor
+ */
+ContainsTermITEVistor::ContainsTermITEVistor(): d_cache() {}
+ContainsTermITEVistor::~ContainsTermITEVistor(){}
+bool ContainsTermITEVistor::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 ContainsTermITEVistor::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(ContainsTermITEVistor* 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)
+{
+  StatisticsRegistry::registerStat(&d_compressCalls);
+  StatisticsRegistry::registerStat(&d_skolemsAdded);
+
+}
+ITECompressor::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_compressCalls);
+  StatisticsRegistry::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.iffNode(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(){}
+  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(ContainsTermITEVistor* 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")
+{
+  StatisticsRegistry::registerStat(&d_maxNonConstantsFolded);
+  StatisticsRegistry::registerStat(&d_unexpected);
+  StatisticsRegistry::registerStat(&d_unsimplified);
+  StatisticsRegistry::registerStat(&d_exactMatchFold);
+  StatisticsRegistry::registerStat(&d_binaryPredFold);
+  StatisticsRegistry::registerStat(&d_specialEqualityFolds);
+  StatisticsRegistry::registerStat(&d_simpITEVisits);
+  StatisticsRegistry::registerStat(&d_inSmaller);
+}
+
+ITESimplifier::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_maxNonConstantsFolded);
+  StatisticsRegistry::unregisterStat(&d_unexpected);
+  StatisticsRegistry::unregisterStat(&d_unsimplified);
+  StatisticsRegistry::unregisterStat(&d_exactMatchFold);
+  StatisticsRegistry::unregisterStat(&d_binaryPredFold);
+  StatisticsRegistry::unregisterStat(&d_specialEqualityFolds);
+  StatisticsRegistry::unregisterStat(&d_simpITEVisits);
+  StatisticsRegistry::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);
+    (*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());
+  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;
+  }
+
+  hash_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::hash_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::hash_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_usedSets()
+{
+  d_true = NodeManager::currentNM()->mkConst<bool>(true);
+  d_false = NodeManager::currentNM()->mkConst<bool>(false);
+}
+
+ITECareSimplifier::~ITECareSimplifier(){}
+
+void ITECareSimplifier::clear(){
+  d_usedSets.clear();
+}
+
+ITECareSimplifier::CareSetPtr ITECareSimplifier::getNewSet()
+{
+  if (d_usedSets.empty()) {
+    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;
+  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);
+    }
+  }
+  while (!d_usedSets.empty()) {
+    delete d_usedSets.back();
+    d_usedSets.pop_back();
+  }
+
+  TNodeMap cache;
+  return substitute(e, substTable, cache);
+}
+
+
+} /* namespace theory */
+} /* namespace CVC4 */
diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h
new file mode 100644
index 000000000..73f0386d2
--- /dev/null
+++ b/src/theory/ite_utilities.h
@@ -0,0 +1,373 @@
+/*********************                                                        */
+/*! \file ite_simplifier.h
+ ** \verbatim
+ ** Original author: Clark Barrett
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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 <vector>
+#include <ext/hash_map>
+#include <ext/hash_set>
+#include "expr/node.h"
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+
+class ContainsTermITEVistor;
+class IncomingArcCounter;
+class TermITEHeightCounter;
+class ITECompressor;
+class ITESimplifier;
+class ITECareSimplifier;
+
+class ITEUtilities {
+public:
+  ITEUtilities(ContainsTermITEVistor* containsVisitor);
+  ~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();
+
+private:
+  ContainsTermITEVistor* d_containsVisitor;
+  ITECompressor* d_compressor;
+  ITESimplifier* d_simplifier;
+  ITECareSimplifier* d_careSimp;
+};
+
+/**
+ * A caching visitor that computes whether a node contains a term ite.
+ */
+class ContainsTermITEVistor {
+public:
+  ContainsTermITEVistor();
+  ~ContainsTermITEVistor();
+
+  /** 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::hash_map<Node, bool, NodeHashFunction> NodeBoolMap;
+  NodeBoolMap d_cache;
+};
+
+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::hash_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::hash_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
+  NodeCountMap d_termITEHeight;
+};
+
+/**
+ * A routine designed to undo the potentially large blow up
+ * due to expansion caused by the ite simplifier.
+ */
+class ITECompressor {
+public:
+  ITECompressor(ContainsTermITEVistor* 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. */
+  ContainsTermITEVistor* d_contains;
+  std::vector<Node>* d_assertions;
+  IncomingArcCounter d_incoming;
+
+  typedef std::hash_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 ITESimplifier {
+public:
+  ITESimplifier(ContainsTermITEVistor* d_containsVisitor);
+  ~ITESimplifier();
+
+  Node simpITE(TNode assertion);
+
+  bool doneALotOfWorkHeuristic() const;
+  void clearSimpITECaches();
+
+private:
+  Node d_true;
+  Node d_false;
+
+  ContainsTermITEVistor* 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::hash_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;
+  struct NodePairHashFunction {
+    size_t operator () (const NodePair& pair) const {
+      size_t hash = 0;
+      hash = 0x9e3779b9 + NodeHashFunction().operator()(pair.first);
+      hash ^= 0x9e3779b9 + NodeHashFunction().operator()(pair.second) + (hash << 6) + (hash >> 2);
+      return hash;
+    }
+  };/* struct ITESimplifier::NodePairHashFunction */
+  typedef std::hash_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::hash_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::hash_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars;
+  Node getSimpVar(TypeNode t);
+
+  typedef std::hash_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:
+  Node d_true;
+  Node d_false;
+
+  typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap;
+
+  class CareSetPtr;
+  class CareSetPtrVal {
+    friend class ITECareSimplifier::CareSetPtr;
+    ITECareSimplifier& d_iteSimplifier;
+    unsigned d_refCount;
+    std::set<Node> d_careSet;
+    CareSetPtrVal(ITECareSimplifier& simp) : d_iteSimplifier(simp), d_refCount(1) {}
+  };
+
+  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) {
+      CareSetPtrVal* val = new CareSetPtrVal(simp);
+      return CareSetPtr(val);
+    }
+    static CareSetPtr recycle(CareSetPtrVal* val) {
+      Assert(val != NULL && val->d_refCount == 0);
+      val->d_refCount = 1;
+      return CareSetPtr(val);
+    }
+  };
+
+  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/model.h b/src/theory/model.h
index a18d66ab0..8192274b5 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -22,7 +22,6 @@
 #include "theory/rep_set.h"
 #include "theory/substitutions.h"
 #include "theory/type_enumerator.h"
-#include "theory/ite_simplifier.h"
 
 namespace CVC4 {
 
@@ -38,7 +37,6 @@ class TheoryModel : public Model
 protected:
   /** substitution map for this model */
   SubstitutionMap d_substitutions;
-  ITESimplifier d_iteSimp;
 public:
   TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
   virtual ~TheoryModel(){}
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 84bbbc179..93b3f0d7e 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -35,6 +35,11 @@
 #include "util/node_visitor.h"
 #include "util/ite_removal.h"
 
+//#include "theory/ite_simplifier.h"
+//#include "theory/ite_compressor.h"
+#include "theory/ite_utilities.h"
+#include "theory/unconstrained_simplifier.h"
+
 #include "theory/model.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/theory_quantifiers.h"
@@ -122,7 +127,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_factsAsserted(context, false),
   d_preRegistrationVisitor(this, context),
   d_sharedTermsVisitor(d_sharedTerms),
-  d_unconstrainedSimp(context, logicInfo),
+  d_unconstrainedSimp(new UnconstrainedSimplifier(context, logicInfo)),
   d_bvToBoolPreprocessor()
 {
   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
@@ -140,7 +145,9 @@ TheoryEngine::TheoryEngine(context::Context* context,
   StatisticsRegistry::registerStat(&d_combineTheoriesTime);
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
-  PROOF (ProofManager::currentPM()->initTheoryProof(); ); 
+  PROOF (ProofManager::currentPM()->initTheoryProof(); );
+
+  d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor());
 }
 
 TheoryEngine::~TheoryEngine() {
@@ -161,6 +168,10 @@ TheoryEngine::~TheoryEngine() {
   delete d_masterEqualityEngine;
 
   StatisticsRegistry::unregisterStat(&d_combineTheoriesTime);
+
+  delete d_unconstrainedSimp;
+
+  delete d_iteUtilities;
 }
 
 void TheoryEngine::interrupt() throw(ModalException) {
@@ -1401,9 +1412,48 @@ void TheoryEngine::ppBvToBool(const std::vector<Node>& assertions, std::vector<N
 
 Node TheoryEngine::ppSimpITE(TNode assertion)
 {
-  Node result = d_iteSimplifier.simpITE(assertion);
-  result = d_iteSimplifier.simplifyWithCare(Rewriter::rewrite(result));
-  result = Rewriter::rewrite(result);
+  if(!d_iteRemover.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){
+  bool result = true;
+  if(d_iteUtilities->simpIteDidALotOfWorkHeuristic()){
+    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::garbageCollect();
+        d_iteRemover.garbageCollect();
+        nm->reclaimZombiesUntil(options::zombieHuntThreshold());
+        Chat() << "....node manager contains " << nm->poolSize() << " nodes after cleanup" << endl;
+      }
+    }
+  }
   return result;
 }
 
@@ -1481,7 +1531,7 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
 
 void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions)
 {
-  d_unconstrainedSimp.processAssertions(assertions);
+  d_unconstrainedSimp->processAssertions(assertions);
 }
 
 
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 53ff4d167..e5b2ad8d2 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -37,12 +37,8 @@
 #include "options/options.h"
 #include "smt/options.h"
 #include "util/statistics_registry.h"
-#include "util/hash.h"
-#include "util/cache.h"
 #include "util/cvc4_assert.h"
 #include "util/sort_inference.h"
-#include "theory/ite_simplifier.h"
-#include "theory/unconstrained_simplifier.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/bv/bv_to_bool.h"
 #include "theory/atom_requests.h"
@@ -77,18 +73,19 @@ struct NodeTheoryPairHashFunction {
 
 
 
-
+/* Forward Declarations Block */
 namespace theory {
   class TheoryModel;
   class TheoryEngineModelBuilder;
+  class ITEUtilities;
 
   namespace eq {
     class EqualityEngine;
   }
 }/* CVC4::theory namespace */
-
-
 class DecisionEngine;
+class RemoveITE;
+class UnconstrainedSimplifier;
 
 /**
  * This is essentially an abstraction for a collection of theories.  A
@@ -771,11 +768,14 @@ private:
   /** Dump the assertions to the dump */
   void dumpAssertions(const char* tag);
 
-  /** For preprocessing pass simplifying ITEs */
-  theory::ITESimplifier d_iteSimplifier;
+  /**
+   * A collection of ite preprocessing passes.
+   */
+  theory::ITEUtilities* d_iteUtilities;
+
 
   /** For preprocessing pass simplifying unconstrained expressions */
-  UnconstrainedSimplifier d_unconstrainedSimp;
+  UnconstrainedSimplifier* d_unconstrainedSimp;
 
   /** For preprocessing pass lifting bit-vectors of size 1 to booleans */
   theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor; 
@@ -783,6 +783,9 @@ public:
 
   void ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); 
   Node ppSimpITE(TNode assertion);
+  /** Returns false if an assertion simplified to false. */
+  bool donePPSimpITE(std::vector<Node>& assertions);
+
   void ppUnconstrainedSimp(std::vector<Node>& assertions);
 
   SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; }
diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index 9b172a561..8bbdded3e 100644
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -18,6 +18,7 @@
 
 #include "theory/unconstrained_simplifier.h"
 #include "theory/rewriter.h"
+#include "theory/logic_info.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/theory/unconstrained_simplifier.h b/src/theory/unconstrained_simplifier.h
index 7d8e85036..0ee754256 100644
--- a/src/theory/unconstrained_simplifier.h
+++ b/src/theory/unconstrained_simplifier.h
@@ -24,11 +24,14 @@
 #include <utility>
 
 #include "expr/node.h"
-#include "theory/theory.h"
 #include "theory/substitutions.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 
+/* Forward Declarations */
+class LogicInfo;
+
 class UnconstrainedSimplifier {
 
   /** number of expressions eliminated due to unconstrained simplification */
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 156288600..5647a2057 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -76,6 +76,8 @@ libutil_la_SOURCES = \
 	boolean_simplification.cpp \
 	ite_removal.h \
 	ite_removal.cpp \
+	nary_builder.h \
+	nary_builder.cpp \
 	node_visitor.h \
 	chain.h \
 	index.h \
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index 7d4948251..5231e05c2 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -17,15 +17,37 @@
 #include <vector>
 
 #include "util/ite_removal.h"
-#include "theory/rewriter.h"
 #include "expr/command.h"
 #include "theory/quantifiers/options.h"
+#include "theory/ite_utilities.h"
 
 using namespace CVC4;
 using namespace std;
 
 namespace CVC4 {
 
+RemoveITE::RemoveITE(context::UserContext* u)
+  : d_iteCache(u)
+{
+  d_containsVisitor = new theory::ContainsTermITEVistor();
+}
+
+RemoveITE::~RemoveITE(){
+  delete d_containsVisitor;
+}
+
+void RemoveITE::garbageCollect(){
+  d_containsVisitor->garbageCollect();
+}
+
+theory::ContainsTermITEVistor*  RemoveITE::getContainsVisitor(){
+  return d_containsVisitor;
+}
+
+size_t RemoveITE::collectedCacheSizes() const{
+  return d_containsVisitor->cache_size() + d_iteCache.size();
+}
+
 void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap)
 {
   for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
@@ -38,18 +60,28 @@ void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap)
   }
 }
 
+bool RemoveITE::containsTermITE(TNode e){
+  return d_containsVisitor->containsTermITE(e);
+}
+
 Node RemoveITE::run(TNode node, std::vector<Node>& output,
-                    IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar) {
+                    IteSkolemMap& iteSkolemMap,
+                    std::vector<Node>& quantVar) {
   // Current node
   Debug("ite") << "removeITEs(" << node << ")" << endl;
 
+  if(node.isVar() || node.isConst() ||
+     (options::biasedITERemoval() && !containsTermITE(node))){
+    return Node(node);
+  }
+
   // The result may be cached already
   NodeManager *nodeManager = NodeManager::currentNM();
-  ITECache::iterator i = d_iteCache.find(node);
+  ITECache::const_iterator i = d_iteCache.find(node);
   if(i != d_iteCache.end()) {
-    Node cachedRewrite = (*i).second;
-    Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl;
-    return cachedRewrite.isNull() ? Node(node) : cachedRewrite;
+    Node cached = (*i).second;
+    Debug("ite") << "removeITEs: in-cache: " << cached << endl;
+    return cached.isNull() ? Node(node) : cached;
   }
 
   // If an ITE replace it
@@ -81,7 +113,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
       Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
 
       // Attach the skolem
-      d_iteCache[node] = skolem;
+      d_iteCache.insert(node, skolem);
 
       // Remove ITEs from the new assertion, rewrite it and push it to the output
       newAssertion = run(newAssertion, output, iteSkolemMap, quantVar);
@@ -127,17 +159,18 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
 
     // If changes, we rewrite
     if(somethingChanged) {
-      Node cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren);
-      d_iteCache[node] = cachedRewrite;
-      return cachedRewrite;
+      Node cached = nodeManager->mkNode(node.getKind(), newChildren);
+      d_iteCache.insert(node, cached);
+      return cached;
     } else {
-      d_iteCache[node] = Node::null();
+      d_iteCache.insert(node, Node::null());
       return node;
     }
   } else {
-    d_iteCache[node] = Node::null();
+    d_iteCache.insert(node, Node::null());
     return node;
   }
 }
 
+
 }/* CVC4 namespace */
diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h
index 03197be89..9d79687f4 100644
--- a/src/util/ite_removal.h
+++ b/src/util/ite_removal.h
@@ -22,21 +22,25 @@
 #include "expr/node.h"
 #include "util/dump.h"
 #include "context/context.h"
-#include "context/cdhashmap.h"
+#include "context/cdinsert_hashmap.h"
 
 namespace CVC4 {
 
+namespace theory {
+class ContainsTermITEVistor;
+}
+
 typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
 
 class RemoveITE {
-  typedef context::CDHashMap<Node, Node, NodeHashFunction> ITECache;
+  typedef context::CDInsertHashMap<Node, Node, NodeHashFunction> ITECache;
   ITECache d_iteCache;
 
+
 public:
 
-  RemoveITE(context::UserContext* u) :
-    d_iteCache(u) {
-  }
+  RemoveITE(context::UserContext* u);
+  ~RemoveITE();
 
   /**
    * Removes the ITE nodes by introducing skolem variables. All
@@ -57,6 +61,21 @@ public:
   Node run(TNode node, std::vector<Node>& additionalAssertions,
            IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar);
 
+  /** Returns true if e contains a term ite.*/
+  bool containsTermITE(TNode e);
+
+  /** Returns the collected size of the caches.*/
+  size_t collectedCacheSizes() const;
+
+  /** Garbage collects non-context dependent data-structures.*/
+  void garbageCollect();
+
+  /** Return the RemoveITE's containsVisitor.*/
+  theory::ContainsTermITEVistor* getContainsVisitor();
+
+private:
+  theory::ContainsTermITEVistor* d_containsVisitor;
+
 };/* class RemoveTTE */
 
 }/* CVC4 namespace */
diff --git a/src/util/nary_builder.cpp b/src/util/nary_builder.cpp
new file mode 100644
index 000000000..004dd3382
--- /dev/null
+++ b/src/util/nary_builder.cpp
@@ -0,0 +1,183 @@
+
+#include "util/nary_builder.h"
+#include "expr/metakind.h"
+using namespace std;
+
+namespace CVC4 {
+namespace util {
+
+Node NaryBuilder::mkAssoc(Kind kind, const std::vector<Node>& children){
+  if(children.size() == 0){
+    return zeroArity(kind);
+  }else if(children.size() == 1){
+    return children[0];
+  }else{
+    const unsigned int max = kind::metakind::getUpperBoundForKind(kind);
+    const unsigned int min = kind::metakind::getLowerBoundForKind(kind);
+
+    Assert(min <= children.size());
+
+    unsigned int numChildren = children.size();
+    NodeManager* nm = NodeManager::currentNM();
+    if( numChildren <= max ) {
+      return nm->mkNode(kind,children);
+    }
+
+    typedef std::vector<Node>::const_iterator const_iterator;
+    const_iterator it = children.begin() ;
+    const_iterator end = children.end() ;
+
+    /* The new top-level children and the children of each sub node */
+    std::vector<Node> newChildren;
+    std::vector<Node> subChildren;
+
+    while( it != end && numChildren > max ) {
+      /* Grab the next max children and make a node for them. */
+      for(const_iterator next = it + max; it != next; ++it, --numChildren ) {
+        subChildren.push_back(*it);
+      }
+      Node subNode = nm->mkNode(kind,subChildren);
+      newChildren.push_back(subNode);
+      subChildren.clear();
+    }
+
+    /* If there's children left, "top off" the Expr. */
+    if(numChildren > 0) {
+      /* If the leftovers are too few, just copy them into newChildren;
+       * otherwise make a new sub-node  */
+      if(numChildren < min) {
+        for(; it != end; ++it) {
+          newChildren.push_back(*it);
+        }
+      } else {
+        for(; it != end; ++it) {
+          subChildren.push_back(*it);
+        }
+        Node subNode = nm->mkNode(kind, subChildren);
+        newChildren.push_back(subNode);
+      }
+    }
+
+    /* It's inconceivable we could have enough children for this to fail
+     * (more than 2^32, in most cases?). */
+    AlwaysAssert( newChildren.size() <= max,
+                  "Too many new children in mkAssociative" );
+
+    /* It would be really weird if this happened (it would require
+     * min > 2, for one thing), but let's make sure. */
+    AlwaysAssert( newChildren.size() >= min,
+                  "Too few new children in mkAssociative" );
+
+    return nm->mkNode(kind,newChildren);
+  }
+}
+
+Node NaryBuilder::zeroArity(Kind k){
+  using namespace kind;
+  NodeManager* nm = NodeManager::currentNM();
+  switch(k){
+  case AND:
+    return nm->mkConst(true);
+  case OR:
+    return nm->mkConst(false);
+  case PLUS:
+    return nm->mkConst(Rational(0));
+  case MULT:
+    return nm->mkConst(Rational(1));
+  default:
+    return Node::null();
+  }
+}
+
+
+RePairAssocCommutativeOperators::RePairAssocCommutativeOperators()
+  : d_cache()
+{}
+RePairAssocCommutativeOperators::~RePairAssocCommutativeOperators(){}
+size_t RePairAssocCommutativeOperators::size() const{ return d_cache.size(); }
+void RePairAssocCommutativeOperators::clear(){ d_cache.clear(); }
+
+bool RePairAssocCommutativeOperators::isAssociateCommutative(Kind k){
+  using namespace kind;
+  switch(k){
+  case BITVECTOR_CONCAT:
+  case BITVECTOR_AND:
+  case BITVECTOR_OR:
+  case BITVECTOR_XOR:
+  case BITVECTOR_MULT:
+  case BITVECTOR_PLUS:
+  case DISTINCT:
+  case PLUS:
+  case MULT:
+  case AND:
+  case OR:
+    return true;
+  default:
+    return false;
+  }
+}
+
+Node RePairAssocCommutativeOperators::rePairAssocCommutativeOperators(TNode n){
+  if(d_cache.find(n) != d_cache.end()){
+    return d_cache[n];
+  }
+  Node result =
+    isAssociateCommutative(n.getKind()) ?
+    case_assoccomm(n) : case_other(n);
+
+  d_cache[n] = result;
+  return result;
+}
+
+Node RePairAssocCommutativeOperators::case_assoccomm(TNode n){
+  Kind k = n.getKind();
+  Assert(isAssociateCommutative(k));
+  Assert(n.getMetaKind() != kind::metakind::PARAMETERIZED);
+  unsigned N = n.getNumChildren();
+  Assert(N >= 2);
+
+
+  Node last = rePairAssocCommutativeOperators( n[N-1]);
+  Node nextToLast = rePairAssocCommutativeOperators(n[N-2]);
+
+  NodeManager* nm = NodeManager::currentNM();
+  Node last2 = nm->mkNode(k, nextToLast, last);
+
+  if(N <= 2){
+    return last2;
+  } else{
+    Assert(N > 2);
+    Node prevRound = last2;
+    for(unsigned prevPos = N-2; prevPos > 0; --prevPos){
+      unsigned currPos = prevPos-1;
+      Node curr = rePairAssocCommutativeOperators(n[currPos]);
+      Node round = nm->mkNode(k, curr, prevRound);
+      prevRound = round;
+    }
+    return prevRound;
+  }
+}
+
+Node RePairAssocCommutativeOperators::case_other(TNode n){
+  if(n.isConst() || n.isVar()){
+    return n;
+  }
+
+  NodeBuilder<> nb(n.getKind());
+
+  if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+    nb << n.getOperator();
+  }
+
+  // Remove the ITEs from the children
+  for(TNode::const_iterator i = n.begin(), end = n.end(); i != end; ++i) {
+    Node newChild = rePairAssocCommutativeOperators(*i);
+    nb << newChild;
+  }
+
+  Node result = (Node)nb;
+  return result;
+}
+
+}/* util namespace */
+}/* CVC4 namespace */
diff --git a/src/util/nary_builder.h b/src/util/nary_builder.h
new file mode 100644
index 000000000..ceaa44e77
--- /dev/null
+++ b/src/util/nary_builder.h
@@ -0,0 +1,38 @@
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include <vector>
+#include "expr/node.h"
+
+namespace CVC4{
+namespace util {
+
+class NaryBuilder {
+public:
+  static Node mkAssoc(Kind k, const std::vector<Node>& children);
+  static Node zeroArity(Kind k);
+};/* class NaryBuilder */
+
+class RePairAssocCommutativeOperators {
+public:
+  RePairAssocCommutativeOperators();
+  ~RePairAssocCommutativeOperators();
+
+  Node rePairAssocCommutativeOperators(TNode n);
+
+  static bool isAssociateCommutative(Kind k);
+
+  size_t size() const;
+  void clear();
+private:
+  Node case_assoccomm(TNode n);
+  Node case_other(TNode n);
+
+  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  NodeMap d_cache;
+};/* class RePairAssocCommutativeOperators */
+
+}/* util namespace */
+}/* CVC4 namespace */
author	Tim King <taking@cs.nyu.edu>	2013-11-25 18:36:06 -0500
committer	Tim King <taking@cs.nyu.edu>	2013-11-25 18:36:06 -0500
commit	22df6e9e8618614e8c33700c55705266912500ae (patch)
tree	20d78676c1e819517f371e8bc5e6363008fc9154 /src
parent	91424455840a7365a328cbcc3d02ec453fe9d0ea (diff)