Added some ITE rewrites,

Added ITE simplifier - on by default only for QF_LIA benchmarks
Fixed one bug in arrays
Added negate() to node.h - it returns kind == NOT ? kind[0] : kind.notNode()

13 files changed, 908 insertions, 33 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index 37499c3bf..4d39ec60f 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -848,6 +848,7 @@ public:
   NodeTemplate<true> eqNode(const NodeTemplate<ref_count2>& right) const;
 
   NodeTemplate<true> notNode() const;
+  NodeTemplate<true> negate() const;
   template <bool ref_count2>
   NodeTemplate<true> andNode(const NodeTemplate<ref_count2>& right) const;
   template <bool ref_count2>
@@ -1118,6 +1119,12 @@ NodeTemplate<true> NodeTemplate<ref_count>::notNode() const {
 }
 
 template <bool ref_count>
+NodeTemplate<true> NodeTemplate<ref_count>::negate() const {
+  assertTNodeNotExpired();
+  return (getKind() == kind::NOT) ? NodeTemplate<true>(d_nv->getChild(0)) : NodeManager::currentNM()->mkNode(kind::NOT, *this);
+}
+
+template <bool ref_count>
 template <bool ref_count2>
 NodeTemplate<true>
 NodeTemplate<ref_count>::andNode(const NodeTemplate<ref_count2>& right) const {
@@ -1235,6 +1242,9 @@ TypeNode NodeTemplate<ref_count>::getType(bool check) const
 template <bool ref_count>
 inline Node
 NodeTemplate<ref_count>::substitute(TNode node, TNode replacement) const {
+  if (node == *this) {
+    return replacement;
+  }
   std::hash_map<TNode, TNode, TNodeHashFunction> cache;
   return substitute(node, replacement, cache);
 }
@@ -1243,6 +1253,12 @@ template <bool ref_count>
 Node
 NodeTemplate<ref_count>::substitute(TNode node, TNode replacement,
                                     std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const {
+  Assert(node != *this);
+
+  if (getNumChildren() == 0) {
+    return *this;
+  }
+
   // in cache?
   typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
   if(i != cache.end()) {
@@ -1268,6 +1284,7 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement,
 
   // put in cache
   Node n = nb;
+  Assert(node != n);
   cache[*this] = n;
   return n;
 }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2759f5717..75b332314 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -156,6 +156,9 @@ class SmtEnginePrivate {
    */
   void removeITEs();
 
+  // Simplify ITE structure
+  void simpITE();
+
   /**
    * Any variable in a assertion that is declared as a subtype type
    * (predicate subtype or integer subrange type) must be constrained
@@ -251,6 +254,12 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
   d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
   d_staticLearningTime("smt::SmtEngine::staticLearningTime"),
+  d_simpITETime("smt::SmtEngine::simpITETime"),
+  d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"),
+  d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
+  d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
+  d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
+  d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
   d_statResultSource("smt::resultSource", "unknown") {
 
   NodeManagerScope nms(d_nodeManager);
@@ -258,6 +267,12 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   StatisticsRegistry::registerStat(&d_definitionExpansionTime);
   StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime);
   StatisticsRegistry::registerStat(&d_staticLearningTime);
+  StatisticsRegistry::registerStat(&d_simpITETime);
+  StatisticsRegistry::registerStat(&d_iteRemovalTime);
+  StatisticsRegistry::registerStat(&d_theoryPreprocessTime);
+  StatisticsRegistry::registerStat(&d_cnfConversionTime);
+  StatisticsRegistry::registerStat(&d_numAssertionsPre);
+  StatisticsRegistry::registerStat(&d_numAssertionsPost);
   StatisticsRegistry::registerStat(&d_statResultSource);
 
   // We have mutual dependency here, so we add the prop engine to the theory
@@ -347,9 +362,14 @@ SmtEngine::~SmtEngine() throw() {
     StatisticsRegistry::unregisterStat(&d_definitionExpansionTime);
     StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime);
     StatisticsRegistry::unregisterStat(&d_staticLearningTime);
+    StatisticsRegistry::unregisterStat(&d_simpITETime);
+    StatisticsRegistry::unregisterStat(&d_iteRemovalTime);
+    StatisticsRegistry::unregisterStat(&d_theoryPreprocessTime);
+    StatisticsRegistry::unregisterStat(&d_cnfConversionTime);
+    StatisticsRegistry::unregisterStat(&d_numAssertionsPre);
+    StatisticsRegistry::unregisterStat(&d_numAssertionsPost);
     StatisticsRegistry::unregisterStat(&d_statResultSource);
 
-
     delete d_private;
     delete d_userContext;
 
@@ -404,6 +424,13 @@ void SmtEngine::setLogicInternal(const LogicInfo& logic) throw() {
   } else {
     theory::Theory::setUninterpretedSortOwner(theory::THEORY_UF);
   }
+  // Turn on ite simplification only for QF_LIA
+  if(! Options::current()->doITESimpSetByUser) {
+    bool iteSimp = logic.isPure(theory::THEORY_ARITH) && logic.isLinear() && !logic.isDifferenceLogic() && !logic.isQuantified() && !logic.areRealsUsed();
+    Trace("smt") << "setting ite simplification to " << iteSimp << std::endl;
+    NodeManager::currentNM()->getOptions()->doITESimp = iteSimp;
+  }
+
 }
 
 void SmtEngine::setInfo(const std::string& key, const SExpr& value)
@@ -851,6 +878,18 @@ void SmtEnginePrivate::nonClausalSimplify() {
   d_assertionsToPreprocess.clear();
 }
 
+void SmtEnginePrivate::simpITE()
+{
+  TimerStat::CodeTimer simpITETimer(d_smt.d_simpITETime);
+
+  Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl;
+
+  for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
+
+    d_assertionsToCheck[i] = d_smt.d_theoryEngine->ppSimpITE(d_assertionsToCheck[i]);
+  }
+}
+
 void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertions)
   throw(AssertionException) {
 
@@ -934,6 +973,11 @@ void SmtEnginePrivate::simplifyAssertions()
       d_assertionsToCheck.swap(d_assertionsToPreprocess);
     }
 
+    if(Options::current()->doITESimp) {
+      // ite simplification
+      simpITE();
+    }
+
     if(Options::current()->doStaticLearning) {
       // Perform static learning
       Trace("simplify") << "SmtEnginePrivate::simplify(): "
@@ -1038,8 +1082,17 @@ void SmtEnginePrivate::processAssertions() {
   // removeITEs().
   int realAssertionsEnd = d_assertionsToCheck.size();
 
-  // Remove ITEs, updating d_iteSkolemMap
-  removeITEs();
+  {
+    TimerStat::CodeTimer codeTimer(d_smt.d_iteRemovalTime);
+    // Remove ITEs
+    d_smt.d_numAssertionsPre += d_assertionsToCheck.size();
+    // Remove ITEs, updating d_iteSkolemMap
+    removeITEs();
+    d_smt.d_numAssertionsPost += d_assertionsToCheck.size();
+    // This may need to be in a try-catch
+    // block. make regress is passing, so
+    // skipping for now --K
+  }
 
   // begin: INVARIANT to maintain: no reordering of assertions or
   // introducing new ones
@@ -1057,10 +1110,13 @@ void SmtEnginePrivate::processAssertions() {
     }
   }
 
-  // Call the theory preprocessors
-  d_smt.d_theoryEngine->preprocessStart();
-  for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
-    d_assertionsToCheck[i] = d_smt.d_theoryEngine->preprocess(d_assertionsToCheck[i]);
+  {
+    TimerStat::CodeTimer codeTimer(d_smt.d_theoryPreprocessTime);
+    // Call the theory preprocessors
+    d_smt.d_theoryEngine->preprocessStart();
+    for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
+      d_assertionsToCheck[i] = d_smt.d_theoryEngine->preprocess(d_assertionsToCheck[i]);
+    }
   }
 
   // Push the formula to decision engine
@@ -1072,9 +1128,13 @@ void SmtEnginePrivate::processAssertions() {
   // introducing new ones
 
   // Push the formula to SAT
-  for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
-    d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]);
+  {
+    TimerStat::CodeTimer codeTimer(d_smt.d_cnfConversionTime);
+    for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
+      d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]);
+    }
   }
+
   d_assertionsToCheck.clear();
   d_iteSkolemMap.clear();
 }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 43d3e1125..10a37b712 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -229,6 +229,19 @@ class CVC4_PUBLIC SmtEngine {
   TimerStat d_nonclausalSimplificationTime;
   /** time spent in static learning */
   TimerStat d_staticLearningTime;
+  /** time spent in simplifying ITEs */
+  TimerStat d_simpITETime;
+  /** time spent removing ITEs */
+  TimerStat d_iteRemovalTime;
+  /** time spent in theory preprocessing */
+  TimerStat d_theoryPreprocessTime;
+  /** time spent converting to CNF */
+  TimerStat d_cnfConversionTime;
+  /** Num of assertions before ite removal */
+  IntStat d_numAssertionsPre;
+  /** Num of assertions after ite removal */
+  IntStat d_numAssertionsPost;
+
   /** how the SMT engine got the answer -- SAT solver or DE */
   BackedStat<std::string> d_statResultSource;
 
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index 4a077450c..992796ebb 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -29,7 +29,9 @@ libtheory_la_SOURCES = \
 	shared_terms_database.h \
 	shared_terms_database.cpp \
 	term_registration_visitor.h \
-	term_registration_visitor.cpp
+	term_registration_visitor.cpp \
+	ite_simplifier.h \
+	ite_simplifier.cpp
 
 nodist_libtheory_la_SOURCES = \
 	rewriter_tables.h \
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 1dd74f060..f073e67d7 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1129,7 +1129,9 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
   if (d_propagateLemmas) {
     if (d_equalityEngine.areDisequal(i,j)) {
       Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating aj = bj ("<<aj<<", "<<bj<<")\n";
-      Node reason = nm->mkNode(kind::OR, aj.eqNode(bj), i.eqNode(j));
+      Node aj_eq_bj = aj.eqNode(bj);
+      Node i_eq_j = i.eqNode(j);
+      Node reason = nm->mkNode(kind::OR, aj_eq_bj, i_eq_j);
       d_permRef.push_back(reason);
       if (!ajExists) {
         preRegisterTerm(aj);
@@ -1137,15 +1139,17 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
       if (!bjExists) {
         preRegisterTerm(bj);
       }
-      d_equalityEngine.assertEquality(aj.eqNode(bj), true, reason);
+      d_equalityEngine.assertEquality(aj_eq_bj, true, reason);
       ++d_numProp;
       return;
     }
     if (bothExist && d_equalityEngine.areDisequal(aj,bj)) {
       Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<<i<<", "<<j<<")\n";
-      Node reason = nm->mkNode(kind::OR, i.eqNode(j), aj.eqNode(bj));
+      Node aj_eq_bj = aj.eqNode(bj);
+      Node i_eq_j = i.eqNode(j);
+      Node reason = nm->mkNode(kind::OR, i_eq_j, aj_eq_bj);
       d_permRef.push_back(reason);
-      d_equalityEngine.assertEquality(i.eqNode(j), true, reason);
+      d_equalityEngine.assertEquality(i_eq_j, true, reason);
       ++d_numProp;
       return;
     }
@@ -1168,9 +1172,25 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
   // TODO: maybe add triggers here
 
   if (d_eagerLemmas || bothExist) {
-    Node eq1 = nm->mkNode(kind::EQUAL, aj, bj);
-    Node eq2 = nm->mkNode(kind::EQUAL, i, j);
-    Node lemma = nm->mkNode(kind::OR, eq2, eq1);
+
+    Assert(aj == Rewriter::rewrite(aj));
+    Assert(bj == Rewriter::rewrite(bj));
+
+    // construct lemma
+    Node eq1 = aj.eqNode(bj);
+    Node eq1_r = Rewriter::rewrite(eq1);
+    if (eq1_r == d_true) {
+      d_equalityEngine.assertEquality(eq1, true, d_true);
+      return;
+    }
+
+    Node eq2 = i.eqNode(j);
+    Node eq2_r = Rewriter::rewrite(eq2);
+    if (eq2 == d_true) {
+      d_equalityEngine.assertEquality(eq2, true, d_true);
+      return;
+    }
+    Node lemma = nm->mkNode(kind::OR, eq2_r, eq1_r);
     Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lemma<<"\n";
     d_RowAlreadyAdded.insert(lem);
     d_out->lemma(lemma);
@@ -1211,10 +1231,37 @@ void TheoryArrays::dischargeLemmas()
       continue;
     }
 
+    Node aj2 = Rewriter::rewrite(aj);
+    if (aj != aj2) {
+      d_equalityEngine.assertEquality(aj.eqNode(aj2), true, d_true);
+    }
+    Node bj2 = Rewriter::rewrite(bj);
+    if (bj != bj2) {
+      d_equalityEngine.assertEquality(bj.eqNode(bj2), true, d_true);
+    }
+    if (aj2 == bj2) {
+      d_RowQueue.push(l);
+      continue;
+    }
+
     // construct lemma
-    Node eq1 = nm->mkNode(kind::EQUAL, aj, bj);
-    Node eq2 = nm->mkNode(kind::EQUAL, i, j);
-    Node lem = nm->mkNode(kind::OR, eq2, eq1);
+    Node eq1 = aj2.eqNode(bj2);
+    Node eq1_r = Rewriter::rewrite(eq1);
+    if (eq1_r == d_true) {
+      d_equalityEngine.assertEquality(eq1, true, d_true);
+      d_RowQueue.push(l);
+      continue;
+    }
+
+    Node eq2 = i.eqNode(j);
+    Node eq2_r = Rewriter::rewrite(eq2);
+    if (eq2_r == d_true) {
+      d_equalityEngine.assertEquality(eq2, true, d_true);
+      d_RowQueue.push(l);
+      continue;
+    }
+    
+    Node lem = nm->mkNode(kind::OR, eq2_r, eq1_r);
 
     Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lem<<"\n";
     d_RowAlreadyAdded.insert(l);
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index 4f41d2fa5..a6b02d784 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -153,15 +153,36 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
     // non-Boolean-valued ITEs should have been removed in place of
     // a variable
     // rewrite simple cases of ITE
-    if(n[0] == tt) {
-      // ITE true x y
-      return RewriteResponse(REWRITE_AGAIN, n[1]);
-    } else if(n[0] == ff) {
-      // ITE false x y
-      return RewriteResponse(REWRITE_AGAIN, n[2]);
-    } else if(n[1] == n[2]) {
-      // ITE c x x
+    if (n[0].isConst()) {
+      if (n[0] == tt) {
+        // ITE true x y
+        return RewriteResponse(REWRITE_AGAIN, n[1]);
+      } else {
+        Assert(n[0] == ff);
+        // ITE false x y
+        return RewriteResponse(REWRITE_AGAIN, n[2]);
+      }
+    } else if (n[1].isConst()) {
+      if (n[1] == tt && n[2] == ff) {
+        return RewriteResponse(REWRITE_AGAIN, n[0]);
+      }
+      else if (n[1] == ff && n[2] == tt) {
+        return RewriteResponse(REWRITE_AGAIN, n[0].notNode());
+      }
+    }
+    if (n[1] == n[2]) {
       return RewriteResponse(REWRITE_AGAIN, n[1]);
+    // 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));
     }
     break;
   }
diff --git a/src/theory/ite_simplifier.cpp b/src/theory/ite_simplifier.cpp
new file mode 100644
index 000000000..50881af82
--- /dev/null
+++ b/src/theory/ite_simplifier.cpp
@@ -0,0 +1,515 @@
+/*********************                                                        */
+/*! \file ite_simplifier.cpp
+ ** \verbatim
+ ** Original author: barrett
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** 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)
+{
+  NodeMap::iterator it;
+  it = d_simpConstCache.find(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[iteNode] = result;
+    return result;
+  }
+
+  if (!containsTermITE(iteNode)) {
+    Node n = Rewriter::rewrite(simpContext.substitute(simpVar, iteNode));
+    d_simpConstCache[iteNode] = n;
+    return n;
+  }
+
+  Node iteNode2;
+  Node simpVar2;
+  d_simpConstCache.clear();
+  Node simpContext2 = createSimpContext(iteNode, iteNode2, simpVar2);
+  if (!simpContext2.isNull()) {
+    Assert(!iteNode2.isNull());
+    simpContext2 = simpContext.substitute(simpVar, simpContext2);
+    d_simpConstCache.clear();
+    Node n = simpConstants(simpContext2, iteNode2, simpVar2);
+    if (n.isNull()) {
+      return n;
+    }
+    d_simpConstCache.clear();
+    d_simpConstCache[iteNode] = n;
+    return n;
+  }
+  return Node();
+}
+
+
+Node ITESimplifier::getSimpVar(TypeNode t)
+{
+  if (t.isInteger()) {
+    if (d_simpVarInt.isNull()) {
+      d_simpVarInt = NodeManager::currentNM()->mkVar(t);
+    }
+    return d_simpVarInt;
+  }
+  if (t.isReal()) {
+    if (d_simpVarReal.isNull()) {
+      d_simpVarReal = NodeManager::currentNM()->mkVar(t);
+    }
+    return d_simpVarReal;
+  }
+  return Node();
+}
+
+
+Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar)
+{
+  NodeMap::iterator it;
+  it = d_simpConstCache.find(c);
+  if (it != d_simpConstCache.end()) {
+    return (*it).second;
+  }
+
+  if (!containsTermITE(c)) {
+    d_simpConstCache[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_simpConstCache[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_simpConstCache[c] = result;
+  return result;
+}
+
+
+Node ITESimplifier::simpITEAtom(TNode atom)
+{
+  if (leavesAreConst(atom)) {
+    Node iteNode;
+    Node simpVar;
+    d_simpConstCache.clear();
+    Node simpContext = createSimpContext(atom, iteNode, simpVar);
+    if (!simpContext.isNull()) {
+      if (iteNode.isNull()) {
+        Assert(leavesAreConst(simpContext) && !containsTermITE(simpContext));
+        return Rewriter::rewrite(simpContext);
+      }
+      d_simpConstCache.clear();
+      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);
+        cs2 = getNewSet();
+        cs2.getCareSet() = css;
+        cs2.getCareSet().insert(v[1]);
+        updateQueue(queue, v[0], cs2);
+        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);
+        cs2 = getNewSet();
+        cs2.getCareSet() = css;
+        cs2.getCareSet().insert(v[1].negate());
+        updateQueue(queue, v[0], cs2);
+        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
new file mode 100644
index 000000000..8466c5444
--- /dev/null
+++ b/src/theory/ite_simplifier.h
@@ -0,0 +1,154 @@
+/*********************                                                        */
+/*! \file ite_simplifier.h
+ ** \verbatim
+ ** Original author: barrett
+ ** Major contributors: 
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** 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/substitutions.h"
+#include "theory/rewriter.h"
+#include "theory/substitutions.h"
+#include "theory/shared_terms_database.h"
+#include "theory/term_registration_visitor.h"
+#include "theory/valuation.h"
+#include "util/options.h"
+#include "util/stats.h"
+#include "util/hash.h"
+#include "util/cache.h"
+#include "util/ite_removal.h"
+
+namespace CVC4 {
+
+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;
+
+  NodeMap d_simpConstCache;
+  Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar);
+  Node d_simpVarInt;
+  Node d_simpVarReal;
+  Node getSimpVar(TypeNode t);
+  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() {}
+
+};
+
+}
+
+#endif
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index 403c90ced..6edeade8d 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -205,4 +205,3 @@ protected:
 };
 
 }
-
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index c19bdda91..77a768152 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -69,6 +69,8 @@ TheoryEngine::TheoryEngine(context::Context* context,
   }
   Rewriter::init();
   StatisticsRegistry::registerStat(&d_combineTheoriesTime);
+  d_true = NodeManager::currentNM()->mkConst<bool>(true);
+  d_false = NodeManager::currentNM()->mkConst<bool>(false);
 }
 
 TheoryEngine::~TheoryEngine() {
@@ -318,7 +320,7 @@ void TheoryEngine::combineTheories() {
 
     if (carePair.a.isConst() && carePair.b.isConst()) {
       // TODO: equality engine should auto-detect these as disequal
-      d_sharedTerms.processSharedLiteral(carePair.a.eqNode(carePair.b).notNode(), NodeManager::currentNM()->mkConst<bool>(true));
+      d_sharedTerms.processSharedLiteral(carePair.a.eqNode(carePair.b).notNode(), d_true);
       continue;
     }
 
@@ -332,7 +334,7 @@ void TheoryEngine::combineTheories() {
       
       if (isTrivial) {
         value = normalizedEquality.getConst<bool>();
-        normalizedEquality = NodeManager::currentNM()->mkConst<bool>(true);
+        normalizedEquality = d_true;
       }
       else {
         d_sharedLiteralsIn[normalizedEquality] = theory::THEORY_LAST;
@@ -875,7 +877,7 @@ Node TheoryEngine::explain(ExplainTask toExplain)
 #endif
 
   // No need to explain "true"
-  explained.insert(ExplainTask(NodeManager::currentNM()->mkConst<bool>(true), SHARED_DATABASE_EXPLANATION));
+  explained.insert(ExplainTask(d_true, SHARED_DATABASE_EXPLANATION));
 
   while (true) {
 
@@ -1011,3 +1013,12 @@ void TheoryEngine::sharedConflict(TNode conflict) {
   Debug("theory") << "TheoryEngine::sharedConflict(" << conflict << "): " << fullConflict << std::endl;
   lemma(fullConflict, true, false);
 }
+
+
+Node TheoryEngine::ppSimpITE(TNode assertion)
+{
+  Node result = d_iteSimplifier.simpITE(assertion);
+  result = d_iteSimplifier.simplifyWithCare(result);
+  result = Rewriter::rewrite(result);
+  return result;
+}
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 2871d5559..bb6c93bd6 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -41,7 +41,7 @@
 #include "util/stats.h"
 #include "util/hash.h"
 #include "util/cache.h"
-#include "util/ite_removal.h"
+#include "theory/ite_simplifier.h"
 
 namespace CVC4 {
 
@@ -123,6 +123,7 @@ class TheoryEngine {
   SharedTermsDatabase d_sharedTerms;
 
   typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap;
 
   /**
   * Cache for theory-preprocessing of assertions
@@ -477,6 +478,9 @@ class TheoryEngine {
   /** Time spent in theory combination */
   TimerStat d_combineTheoriesTime;
 
+  Node d_true;
+  Node d_false;
+
 public:
 
   /** Constructs a theory engine */
@@ -733,6 +737,12 @@ private:
   /** Prints the assertions to the debug stream */
   void printAssertions(const char* tag);
 
+  /** For preprocessing pass simplifying ITEs */
+  ITESimplifier d_iteSimplifier;
+
+public:
+  Node ppSimpITE(TNode assertion);
+
 };/* class TheoryEngine */
 
 }/* CVC4 namespace */
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 140850a28..7c8a07489 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -83,6 +83,8 @@ Options::Options() :
   decisionMode(DECISION_STRATEGY_INTERNAL),
   decisionModeSetByUser(false),
   doStaticLearning(true),
+  doITESimp(false),
+  doITESimpSetByUser(false),
   interactive(false),
   interactiveSetByUser(false),
   perCallResourceLimit(0),
@@ -178,6 +180,8 @@ Additional CVC4 options:\n\
    --simplification=MODE  choose simplification mode, see --simplification=help\n\
    --decision=MODE        choose decision mode, see --decision=help\n\
    --no-static-learning   turn off static learning (e.g. diamond-breaking)\n\
+   --ite-simp             turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\
+   --no-ite-simp          turn off ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\
    --replay=file          replay decisions from file\n\
    --replay-log=file      log decisions and propagations to file\n\
    --pivot-rule=RULE      change the pivot rule (see --pivot-rule help)\n\
@@ -359,6 +363,8 @@ enum OptionValue {
   SIMPLIFICATION_MODE,
   DECISION_MODE,
   NO_STATIC_LEARNING,
+  ITE_SIMP,
+  NO_ITE_SIMP,
   INTERACTIVE,
   NO_INTERACTIVE,
   PRODUCE_ASSIGNMENTS,
@@ -452,6 +458,8 @@ static struct option cmdlineOptions[] = {
   { "simplification", required_argument, NULL, SIMPLIFICATION_MODE },
   { "decision", required_argument, NULL, DECISION_MODE },
   { "no-static-learning", no_argument, NULL, NO_STATIC_LEARNING },
+  { "ite-simp", no_argument, NULL, ITE_SIMP },
+  { "no-ite-simp", no_argument, NULL, NO_ITE_SIMP },
   { "interactive", no_argument      , NULL, INTERACTIVE },
   { "no-interactive", no_argument   , NULL, NO_INTERACTIVE },
   { "produce-models", no_argument   , NULL, 'm' },
@@ -762,6 +770,16 @@ throw(OptionException) {
       doStaticLearning = false;
       break;
 
+    case ITE_SIMP:
+      doITESimp = true;
+      doITESimpSetByUser = true;
+      break;
+
+    case NO_ITE_SIMP:
+      doITESimp = false;
+      doITESimpSetByUser = true;
+      break;
+
     case INTERACTIVE:
       interactive = true;
       interactiveSetByUser = true;
diff --git a/src/util/options.h b/src/util/options.h
index eac09fabf..3b6584727 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -146,6 +146,9 @@ struct CVC4_PUBLIC Options {
   /** Whether to perform the static learning pass. */
   bool doStaticLearning;
 
+  /** Whether to do the ite-simplification pass */
+  bool doITESimp;
+
   /** Whether we're in interactive mode or not */
   bool interactive;
 
@@ -250,6 +253,11 @@ struct CVC4_PUBLIC Options {
   bool ufSymmetryBreakerSetByUser;
 
   /**
+   * Whether the user explicitly requested ite simplification
+   */
+  bool doITESimpSetByUser;
+
+  /**
    * Whether to do the linear diophantine equation solver
    * in Arith as described by Griggio JSAT 2012 (on by default).
    */