This commit merges the arith-prop-opt branch into the main trunk. This was done by way of the intermediate branch arith-prop-tmp. Both arith-prop-opt and arith-prop-tmp will now be phased out.

12 files changed, 586 insertions, 514 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index d89b8ec2f..f3caead8b 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -87,6 +87,13 @@ void PropEngine::assertLemma(TNode node) {
   d_cnfStream->convertAndAssert(node, true, false);
 }
 
+void PropEngine::assertSafeLemma(TNode node) {
+  if(d_inCheckSat){
+    assertLemma(node);
+  }else{
+    assertFormula(node);
+  }
+}
 
 void PropEngine::printSatisfyingAssignment(){
   const CnfStream::TranslationCache& transCache =
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index b43c2d859..c0483e943 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -103,6 +103,7 @@ public:
    * @param node the formula to assert
    */
   void assertLemma(TNode node);
+  void assertSafeLemma(TNode node);
 
   /**
    * Checks the current context for satisfiability.
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 7d78b1e6c..aa566b307 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -25,8 +25,8 @@ libarith_la_SOURCES = \
 	simplex.cpp \
 	row_vector.h \
 	row_vector.cpp \
-	arith_propagator.h \
-	arith_propagator.cpp \
+	unate_propagator.h \
+	unate_propagator.cpp \
 	theory_arith.h \
 	theory_arith.cpp
 
diff --git a/src/theory/arith/arith_propagator.cpp b/src/theory/arith/arith_propagator.cpp
deleted file mode 100644
index bf14e882e..000000000
--- a/src/theory/arith/arith_propagator.cpp
+++ /dev/null
@@ -1,366 +0,0 @@
-/*********************                                                        */
-/*! \file arith_propagator.cpp
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "theory/arith/arith_propagator.h"
-#include "theory/arith/arith_utilities.h"
-
-#include <list>
-
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arith;
-using namespace CVC4::theory::arith::propagator;
-
-using namespace CVC4::kind;
-
-using namespace std;
-
-ArithUnatePropagator::ArithUnatePropagator(context::Context* cxt) :
-  d_assertions(cxt), d_pendingAssertions(cxt,0)
-{ }
-
-
-bool acceptedKinds(Kind k){
-  switch(k){
-  case EQUAL:
-  case LEQ:
-  case GEQ:
-    return true;
-  default:
-    return false;
-  }
-}
-
-void ArithUnatePropagator::addAtom(TNode atom){
-  Assert(acceptedKinds(atom.getKind()));
-
-  TNode left  = atom[0];
-  TNode right = atom[1];
-
-  if(!leftIsSetup(left)){
-    setupLefthand(left);
-  }
-
-  switch(atom.getKind()){
-  case EQUAL:
-    {
-      OrderedBoundsList* eqList = left.getAttribute(propagator::PropagatorEqList());
-      Assert(!eqList->contains(atom));
-      eqList->append(atom);
-      break;
-    }
-  case LEQ:
-    {
-      OrderedBoundsList* leqList = left.getAttribute(propagator::PropagatorLeqList());
-      Assert(! leqList->contains(atom));
-      leqList->append(atom);
-      break;
-    }
-    break;
-  case GEQ:
-    {
-      OrderedBoundsList* geqList = left.getAttribute(propagator::PropagatorGeqList());
-      Assert(! geqList->contains(atom));
-      geqList->append(atom);
-      break;
-    }
-  default:
-    Unreachable();
-  }
-}
-bool ArithUnatePropagator::leftIsSetup(TNode left){
-  return left.hasAttribute(propagator::PropagatorEqList());
-}
-
-void ArithUnatePropagator::setupLefthand(TNode left){
-  Assert(!leftIsSetup(left));
-
-  OrderedBoundsList* eqList = new OrderedBoundsList();
-  OrderedBoundsList* geqList = new OrderedBoundsList();
-  OrderedBoundsList* leqList = new OrderedBoundsList();
-
-  left.setAttribute(propagator::PropagatorEqList(), eqList);
-  left.setAttribute(propagator::PropagatorLeqList(), leqList);
-  left.setAttribute(propagator::PropagatorGeqList(), geqList);
-}
-
-void ArithUnatePropagator::assertLiteral(TNode lit){
-
-  if(lit.getKind() == NOT){
-    Assert(!lit[0].getAttribute(propagator::PropagatorMarked()));
-    lit[0].setAttribute(propagator::PropagatorMarked(), true);
-  }else{
-    Assert(!lit.getAttribute(propagator::PropagatorMarked()));
-    lit.setAttribute(propagator::PropagatorMarked(), true);
-  }
-  d_assertions.push_back(lit);
-}
-
-std::vector<Node> ArithUnatePropagator::getImpliedLiterals(){
-  std::vector<Node> impliedButNotAsserted;
-
-  while(d_pendingAssertions < d_assertions.size()){
-    TNode assertion = d_assertions[d_pendingAssertions];
-    d_pendingAssertions = d_pendingAssertions + 1;
-
-    enqueueImpliedLiterals(assertion, impliedButNotAsserted);
-  }
-
-  if(Debug.isOn("arith::propagator")){
-    for(std::vector<Node>::iterator i = impliedButNotAsserted.begin(),
-          endIter = impliedButNotAsserted.end(); i != endIter; ++i){
-      Node imp = *i;
-      Debug("arith::propagator") << explain(imp) << " (prop)-> " << imp << endl;
-    }
-  }
-
-  return impliedButNotAsserted;
-}
-
-/** This function is effectively a case split. */
-void ArithUnatePropagator::enqueueImpliedLiterals(TNode lit, std::vector<Node>& buffer){
-  switch(lit.getKind()){
-  case EQUAL:
-    enqueueEqualityImplications(lit, buffer);
-    break;
-  case LEQ:
-    enqueueUpperBoundImplications(lit, lit, buffer);
-    break;
-  case GEQ:
-    enqueueLowerBoundImplications(lit, lit, buffer);
-    break;
-  case NOT:
-    {
-      TNode under = lit[0];
-      switch(under.getKind()){
-      case EQUAL:
-        //Do nothing
-        break;;
-      case LEQ:
-        enqueueLowerBoundImplications(under, lit, buffer);
-        break;
-      case GEQ:
-        enqueueUpperBoundImplications(under, lit, buffer);
-        break;
-      default:
-        Unreachable();
-      }
-      break;
-    }
-  default:
-    Unreachable();
-  }
-}
-
-/**
- * An equality (x = c) has been asserted.
- * In this case we can propagate everything by comparing against the other constants.
- */
-void ArithUnatePropagator::enqueueEqualityImplications(TNode orig, std::vector<Node>& buffer){
-  TNode left = orig[0];
-  TNode right = orig[1];
-  const Rational& c = right.getConst<Rational>();
-
-  OrderedBoundsList* eqList = left.getAttribute(propagator::PropagatorEqList());
-  OrderedBoundsList* leqList = left.getAttribute(propagator::PropagatorLeqList());
-  OrderedBoundsList* geqList = left.getAttribute(propagator::PropagatorGeqList());
-
-
-  /* (x = c) /\ (c !=d) => (x != d)  */
-  for(OrderedBoundsList::iterator i = eqList->begin(); i != eqList->end(); ++i){
-    TNode eq = *i;
-    Assert(eq.getKind() == EQUAL);
-    if(!eq.getAttribute(propagator::PropagatorMarked())){ //Note that (x = c) is marked
-      Assert(eq[1].getConst<Rational>() != c);
-
-      eq.setAttribute(propagator::PropagatorMarked(), true);
-
-      Node neq = NodeManager::currentNM()->mkNode(NOT, eq);
-      neq.setAttribute(propagator::PropagatorExplanation(), orig);
-      buffer.push_back(neq);
-    }
-  }
-  for(OrderedBoundsList::iterator i = leqList->begin(); i != leqList->end(); ++i){
-    TNode leq = *i;
-    Assert(leq.getKind() == LEQ);
-    if(!leq.getAttribute(propagator::PropagatorMarked())){
-      leq.setAttribute(propagator::PropagatorMarked(), true);
-      const Rational& d = leq[1].getConst<Rational>();
-      if(c <= d){
-        /* (x = c) /\ (c <= d) => (x <= d)  */
-        leq.setAttribute(propagator::PropagatorExplanation(), orig);
-        buffer.push_back(leq);
-      }else{
-        /* (x = c) /\ (c > d) => (x > d)  */
-        Node gt = NodeManager::currentNM()->mkNode(NOT, leq);
-        gt.setAttribute(propagator::PropagatorExplanation(), orig);
-        buffer.push_back(gt);
-      }
-    }
-  }
-
-  for(OrderedBoundsList::iterator i = geqList->begin(); i != geqList->end(); ++i){
-    TNode geq = *i;
-    Assert(geq.getKind() == GEQ);
-    if(!geq.getAttribute(propagator::PropagatorMarked())){
-      geq.setAttribute(propagator::PropagatorMarked(), true);
-      const Rational& d = geq[1].getConst<Rational>();
-      if(c >= d){
-        /* (x = c) /\ (c >= d) => (x >= d)  */
-        geq.setAttribute(propagator::PropagatorExplanation(), orig);
-        buffer.push_back(geq);
-      }else{
-        /* (x = c) /\ (c >= d) => (x >= d)  */
-        Node lt = NodeManager::currentNM()->mkNode(NOT, geq);
-        lt.setAttribute(propagator::PropagatorExplanation(), orig);
-        buffer.push_back(lt);
-      }
-    }
-  }
-}
-
-void ArithUnatePropagator::enqueueUpperBoundImplications(TNode atom, TNode orig, std::vector<Node>& buffer){
-
-  Assert(atom.getKind() == LEQ || (orig.getKind() == NOT && atom.getKind() == GEQ));
-
-  TNode left = atom[0];
-  TNode right = atom[1];
-  const Rational& c = right.getConst<Rational>();
-
-  OrderedBoundsList* eqList = left.getAttribute(propagator::PropagatorEqList());
-  OrderedBoundsList* leqList = left.getAttribute(propagator::PropagatorLeqList());
-  OrderedBoundsList* geqList = left.getAttribute(propagator::PropagatorGeqList());
-
-
-  //For every node (x <= d), we will restrict ourselves to look at the cases when (d >= c)
-  for(OrderedBoundsList::iterator i = leqList->lower_bound(atom); i != leqList->end(); ++i){
-    TNode leq = *i;
-    Assert(leq.getKind() == LEQ);
-    if(!leq.getAttribute(propagator::PropagatorMarked())){
-      leq.setAttribute(propagator::PropagatorMarked(), true);
-      const Rational& d = leq[1].getConst<Rational>();
-      Assert( c <= d );
-
-      leq.setAttribute(propagator::PropagatorExplanation(), orig);
-      buffer.push_back(leq); // (x<=c) /\ (c <= d) => (x <= d)
-      //Note that if c=d, that at the node is not marked this can only be reached when (x < c)
-      //So we do not have to worry about a circular dependency
-    }else if(leq != atom){
-      break; //No need to examine the rest, this atom implies the rest of the possible propagataions
-    }
-  }
-
-  for(OrderedBoundsList::iterator i = geqList->upper_bound(atom); i != geqList->end(); ++i){
-    TNode geq = *i;
-    Assert(geq.getKind() == GEQ);
-    if(!geq.getAttribute(propagator::PropagatorMarked())){
-      geq.setAttribute(propagator::PropagatorMarked(), true);
-      const Rational& d = geq[1].getConst<Rational>();
-      Assert( c < d );
-
-      Node lt = NodeManager::currentNM()->mkNode(NOT, geq);
-      lt.setAttribute(propagator::PropagatorExplanation(), orig);
-      buffer.push_back(lt); // x<=c /\ d > c => x < d
-    }else{
-      break; //No need to examine this atom implies the rest
-    }
-  }
-
-  for(OrderedBoundsList::iterator i = eqList->upper_bound(atom); i != eqList->end(); ++i){
-    TNode eq = *i;
-    Assert(eq.getKind() == EQUAL);
-    if(!eq.getAttribute(propagator::PropagatorMarked())){
-      eq.setAttribute(propagator::PropagatorMarked(), true);
-      const Rational& d = eq[1].getConst<Rational>();
-      Assert( c < d );
-
-      Node neq = NodeManager::currentNM()->mkNode(NOT, eq);
-      neq.setAttribute(propagator::PropagatorExplanation(), orig);
-      buffer.push_back(neq); // x<=c /\ c < d => x !=  d
-    }
-  }
-}
-
-void ArithUnatePropagator::enqueueLowerBoundImplications(TNode atom, TNode orig, std::vector<Node>& buffer){
-
-  Assert(atom.getKind() == GEQ || (orig.getKind() == NOT && atom.getKind() == LEQ));
-
-  TNode left = atom[0];
-  TNode right = atom[1];
-  const Rational& c = right.getConst<Rational>();
-
-  OrderedBoundsList* eqList = left.getAttribute(propagator::PropagatorEqList());
-  OrderedBoundsList* leqList = left.getAttribute(propagator::PropagatorLeqList());
-  OrderedBoundsList* geqList = left.getAttribute(propagator::PropagatorGeqList());
-
-
-  for(OrderedBoundsList::reverse_iterator i = geqList->reverse_lower_bound(atom);
-      i != geqList->rend(); i++){
-    TNode geq = *i;
-    Assert(geq.getKind() == GEQ);
-    if(!geq.getAttribute(propagator::PropagatorMarked())){
-      geq.setAttribute(propagator::PropagatorMarked(), true);
-      const Rational& d = geq[1].getConst<Rational>();
-      Assert( c >= d );
-
-      geq.setAttribute(propagator::PropagatorExplanation(), orig);
-      buffer.push_back(geq); // x>=c /\ c >= d => x >= d
-    }else if(geq != atom){
-      break; //No need to examine the rest, this atom implies the rest of the possible propagataions
-    }
-  }
-
-  for(OrderedBoundsList::reverse_iterator i = leqList->reverse_upper_bound(atom);
-      i != leqList->rend(); ++i){
-    TNode leq = *i;
-    Assert(leq.getKind() == LEQ);
-    if(!leq.getAttribute(propagator::PropagatorMarked())){
-      leq.setAttribute(propagator::PropagatorMarked(), true);
-      const Rational& d = leq[1].getConst<Rational>();
-      Assert( c > d );
-
-      Node gt = NodeManager::currentNM()->mkNode(NOT, leq);
-      gt.setAttribute(propagator::PropagatorExplanation(), orig);
-      buffer.push_back(gt); // x>=c /\ d < c => x > d
-    }else{
-      break; //No need to examine this atom implies the rest
-    }
-  }
-
-  for(OrderedBoundsList::reverse_iterator i = eqList->reverse_upper_bound(atom);
-      i != eqList->rend(); ++i){
-    TNode eq = *i;
-    Assert(eq.getKind() == EQUAL);
-    if(!eq.getAttribute(propagator::PropagatorMarked())){
-      eq.setAttribute(propagator::PropagatorMarked(), true);
-      const Rational& d = eq[1].getConst<Rational>();
-      Assert( c > d );
-
-      Node neq = NodeManager::currentNM()->mkNode(NOT, eq);
-      neq.setAttribute(propagator::PropagatorExplanation(), orig);
-      buffer.push_back(neq); // x>=c /\ c > d => x !=  d
-    }
-  }
-
-}
-
-Node ArithUnatePropagator::explain(TNode lit){
-  Assert(lit.hasAttribute(propagator::PropagatorExplanation()));
-  return lit.getAttribute(propagator::PropagatorExplanation());
-}
diff --git a/src/theory/arith/arith_propagator.h b/src/theory/arith/arith_propagator.h
deleted file mode 100644
index 8ea628f25..000000000
--- a/src/theory/arith/arith_propagator.h
+++ /dev/null
@@ -1,128 +0,0 @@
-/*********************                                                        */
-/*! \file arith_propagator.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__ARITH__ARITH_PROPAGATOR_H
-#define __CVC4__THEORY__ARITH__ARITH_PROPAGATOR_H
-
-#include "expr/node.h"
-#include "context/cdlist.h"
-#include "context/context.h"
-#include "context/cdo.h"
-#include "theory/arith/ordered_bounds_list.h"
-
-#include <algorithm>
-#include <vector>
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-class ArithUnatePropagator {
-private:
-  /** Index of assertions. */
-  context::CDList<Node> d_assertions;
-
-  /** Index of the last assertion in d_assertions to be asserted. */
-  context::CDO<unsigned int> d_pendingAssertions;
-
-public:
-  ArithUnatePropagator(context::Context* cxt);
-
-  /**
-   * Adds a new atom for the propagator to watch.
-   * Atom is assumed to have been rewritten by TheoryArith::rewrite().
-   */
-  void addAtom(TNode atom);
-
-  /**
-   * Informs the propagator that a literal has been asserted to the theory.
-   */
-  void assertLiteral(TNode lit);
-
-
-  /**
-   * returns a vector of literals that are 
-   */
-  std::vector<Node> getImpliedLiterals();
-
-  /** Explains a literal that was asserted in the current context. */
-  Node explain(TNode lit);
-
-private:
-  /** returns true if the left hand side side left has been setup. */
-  bool leftIsSetup(TNode left);
-
-  /**
-   * Sets up a left hand side.
-   * This initializes the attributes PropagatorEqList, PropagatorGeqList, and PropagatorLeqList for left.
-   */
-  void setupLefthand(TNode left);
-
-  /**
-   * Given that the literal lit is now asserted,
-   * enqueue additional entailed assertions in buffer.
-   */
-  void enqueueImpliedLiterals(TNode lit, std::vector<Node>& buffer);
-
-  void enqueueEqualityImplications(TNode original, std::vector<Node>& buffer);
-  void enqueueLowerBoundImplications(TNode atom, TNode original, std::vector<Node>& buffer);
-  /**
-   * Given that the literal original is now asserted, which is either (<= x c) or (not (>= x c)),
-   * enqueue additional entailed assertions in buffer.
-   */
-  void enqueueUpperBoundImplications(TNode atom, TNode original, std::vector<Node>& buffer);
-};
-
-
-
-namespace propagator {
-
-/** Basic memory management wrapper for deleting PropagatorEqList, PropagatorGeqList, and PropagatorLeqList.*/
-struct ListCleanupStrategy{
-  static void cleanup(OrderedBoundsList* l){
-    Debug("arithgc") << "cleaning up  " << l << "\n";
-    delete l;
-  }
-};
-
-
-struct PropagatorEqListID {};
-typedef expr::Attribute<PropagatorEqListID, OrderedBoundsList*, ListCleanupStrategy> PropagatorEqList;
-
-struct PropagatorGeqListID {};
-typedef expr::Attribute<PropagatorGeqListID, OrderedBoundsList*, ListCleanupStrategy> PropagatorGeqList;
-
-struct PropagatorLeqListID {};
-typedef expr::Attribute<PropagatorLeqListID, OrderedBoundsList*, ListCleanupStrategy> PropagatorLeqList;
-
-
-struct PropagatorMarkedID {};
-typedef expr::CDAttribute<PropagatorMarkedID, bool> PropagatorMarked;
-
-struct PropagatorExplanationID {};
-typedef expr::CDAttribute<PropagatorExplanationID, Node> PropagatorExplanation;
-}/* CVC4::theory::arith::propagator */
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_H */
diff --git a/src/theory/arith/ordered_set.h b/src/theory/arith/ordered_set.h
new file mode 100644
index 000000000..fa606188a
--- /dev/null
+++ b/src/theory/arith/ordered_set.h
@@ -0,0 +1,35 @@
+#include <set>
+#include "expr/kind.h"
+#include "expr/node.h"
+#include "util/Assert.h"
+
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+struct RightHandRationalLT
+{
+  bool operator()(TNode s1, TNode s2) const
+  {
+    TNode rh1 = s1[1];
+    TNode rh2 = s2[1];
+    const Rational& c1 = rh1.getConst<Rational>();
+    const Rational& c2 = rh2.getConst<Rational>();
+    int cmpRes = c1.cmp(c2);
+    return cmpRes < 0;
+  }
+};
+
+typedef std::set<Node, RightHandRationalLT> OrderedSet;
+
+struct SetCleanupStrategy{
+  static void cleanup(OrderedSet* l){
+    Debug("arithgc") << "cleaning up  " << l << "\n";
+    delete l;
+  }
+};
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 7cedbcd20..bf5f285a5 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -34,7 +34,7 @@
 #include "theory/arith/arithvar_dense_set.h"
 
 #include "theory/arith/arith_rewriter.h"
-#include "theory/arith/arith_propagator.h"
+#include "theory/arith/unate_propagator.h"
 
 #include "theory/arith/theory_arith.h"
 #include "theory/arith/normal_form.h"
@@ -62,7 +62,7 @@ TheoryArith::TheoryArith(int id, context::Context* c, OutputChannel& out) :
   d_diseq(c),
   d_tableau(d_activityMonitor, d_basicManager),
   d_rewriter(&d_constants),
-  d_propagator(c),
+  d_propagator(c, out),
   d_simplex(d_constants, d_partialModel, d_basicManager,  d_out, d_activityMonitor, d_tableau),
   d_statistics()
 {}
@@ -71,15 +71,21 @@ TheoryArith::~TheoryArith(){}
 
 TheoryArith::Statistics::Statistics():
   d_statUserVariables("theory::arith::UserVariables", 0),
-  d_statSlackVariables("theory::arith::SlackVariables", 0)
+  d_statSlackVariables("theory::arith::SlackVariables", 0),
+  d_statDisequalitySplits("theory::arith::DisequalitySplits", 0),
+  d_statDisequalityConflicts("theory::arith::DisequalityConflicts", 0)
 {
   StatisticsRegistry::registerStat(&d_statUserVariables);
   StatisticsRegistry::registerStat(&d_statSlackVariables);
+  StatisticsRegistry::registerStat(&d_statDisequalitySplits);
+  StatisticsRegistry::registerStat(&d_statDisequalityConflicts);
 }
 
 TheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_statUserVariables);
   StatisticsRegistry::unregisterStat(&d_statSlackVariables);
+  StatisticsRegistry::unregisterStat(&d_statDisequalitySplits);
+  StatisticsRegistry::unregisterStat(&d_statDisequalityConflicts);
 }
 
 
@@ -299,6 +305,7 @@ bool TheoryArith::assertionCases(TNode assertion){
       if (d_diseq.find(diseq) != d_diseq.end()) {
         NodeBuilder<3> conflict(kind::AND);
         conflict << diseq << assertion << d_partialModel.getLowerConstraint(x_i);
+        ++(d_statistics.d_statDisequalityConflicts);
         d_out->conflict((TNode)conflict);
         return true;
       }
@@ -311,6 +318,7 @@ bool TheoryArith::assertionCases(TNode assertion){
       if (d_diseq.find(diseq) != d_diseq.end()) {
         NodeBuilder<3> conflict(kind::AND);
         conflict << diseq << assertion << d_partialModel.getUpperConstraint(x_i);
+        ++(d_statistics.d_statDisequalityConflicts);
         d_out->conflict((TNode)conflict);
         return true;
       }
@@ -351,7 +359,7 @@ void TheoryArith::check(Effort effortLevel){
 
     Node assertion = get();
 
-    d_propagator.assertLiteral(assertion);
+    //d_propagator.assertLiteral(assertion);
     bool conflictDuringAnAssert = assertionCases(assertion);
 
     if(conflictDuringAnAssert){
@@ -426,6 +434,7 @@ void TheoryArith::check(Effort effortLevel){
           // All the implication
           Node impClosure = NodeBuilder<3>(kind::AND) << imp1 << imp2 << imp3;
 
+          ++(d_statistics.d_statDisequalitySplits);
           d_out->lemma(lemma.andNode(impClosure));
         }
       }
@@ -449,22 +458,22 @@ void TheoryArith::check(Effort effortLevel){
 }
 
 void TheoryArith::explain(TNode n, Effort e) {
-  Node explanation = d_propagator.explain(n);
-  Debug("arith") << "arith::explain("<<explanation<<")->"
-                 << explanation << endl;
-  d_out->explanation(explanation, true);
+  // Node explanation = d_propagator.explain(n);
+  // Debug("arith") << "arith::explain("<<explanation<<")->"
+  //                << explanation << endl;
+  // d_out->explanation(explanation, true);
 }
 
 void TheoryArith::propagate(Effort e) {
 
-  if(quickCheckOrMore(e)){
-    std::vector<Node> implied = d_propagator.getImpliedLiterals();
-    for(std::vector<Node>::iterator i = implied.begin();
-        i != implied.end();
-        ++i){
-      d_out->propagate(*i);
-    }
-  }
+  // if(quickCheckOrMore(e)){
+  //   std::vector<Node> implied = d_propagator.getImpliedLiterals();
+  //   for(std::vector<Node>::iterator i = implied.begin();
+  //       i != implied.end();
+  //       ++i){
+  //     d_out->propagate(*i);
+  //   }
+  // }
 }
 
 Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 5c65b993d..81711a101 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -33,7 +33,7 @@
 #include "theory/arith/tableau.h"
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/partial_model.h"
-#include "theory/arith/arith_propagator.h"
+#include "theory/arith/unate_propagator.h"
 #include "theory/arith/simplex.h"
 
 #include "util/stats.h"
@@ -176,6 +176,8 @@ private:
   class Statistics {
   public:
     IntStat d_statUserVariables, d_statSlackVariables;
+    IntStat d_statDisequalitySplits;
+    IntStat d_statDisequalityConflicts;
 
     Statistics();
     ~Statistics();
diff --git a/src/theory/arith/unate_propagator.cpp b/src/theory/arith/unate_propagator.cpp
new file mode 100644
index 000000000..38bc06555
--- /dev/null
+++ b/src/theory/arith/unate_propagator.cpp
@@ -0,0 +1,381 @@
+/*********************                                                        */
+/*! \file arith_propagator.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "theory/arith/unate_propagator.h"
+#include "theory/arith/arith_utilities.h"
+
+#include <list>
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::arith;
+
+using namespace CVC4::kind;
+
+using namespace std;
+
+struct PropagatorLeqSetID {};
+typedef expr::Attribute<PropagatorLeqSetID, OrderedSet*, SetCleanupStrategy> PropagatorLeqSet;
+
+struct PropagatorEqSetID {};
+typedef expr::Attribute<PropagatorEqSetID, OrderedSet*, SetCleanupStrategy> PropagatorEqSet;
+
+struct PropagatorGeqSetID {};
+typedef expr::Attribute<PropagatorGeqSetID, OrderedSet*, SetCleanupStrategy> PropagatorGeqSet;
+
+ArithUnatePropagator::ArithUnatePropagator(context::Context* cxt, OutputChannel& out) :
+  d_arithOut(out)
+{ }
+
+bool ArithUnatePropagator::leftIsSetup(TNode left){
+  return left.hasAttribute(PropagatorEqSet());
+}
+
+void ArithUnatePropagator::setupLefthand(TNode left){
+  Assert(!leftIsSetup(left));
+
+  OrderedSet* eqList = new OrderedSet();
+  OrderedSet* leqList = new OrderedSet();
+  OrderedSet* geqList = new OrderedSet();
+
+  left.setAttribute(PropagatorEqSet(), eqList);
+  left.setAttribute(PropagatorLeqSet(), geqList);
+  left.setAttribute(PropagatorGeqSet(), leqList);
+}
+
+void ArithUnatePropagator::addAtom(TNode atom){
+  TNode left  = atom[0];
+  TNode right = atom[1];
+
+  if(!leftIsSetup(left)){
+    setupLefthand(left);
+  }
+
+  OrderedSet* eqSet = left.getAttribute(PropagatorEqSet());
+  OrderedSet* leqSet = left.getAttribute(PropagatorLeqSet());
+  OrderedSet* geqSet = left.getAttribute(PropagatorGeqSet());
+
+  switch(atom.getKind()){
+  case EQUAL:
+    {
+      pair<OrderedSet::iterator, bool> res = eqSet->insert(atom);
+      Assert(res.second);
+      addEqualityToEqualities(atom, eqSet, res.first);
+      addEqualityToLeqs(atom, leqSet);
+      addEqualityToGeqs(atom, geqSet);
+      break;
+    }
+  case LEQ:
+    {
+      pair<OrderedSet::iterator, bool> res = leqSet->insert(atom);
+      Assert(res.second);
+
+      addLeqToLeqs(atom, leqSet, res.first);
+      addLeqToEqualities(atom, eqSet);
+      addLeqToGeqs(atom, geqSet);
+      break;
+    }
+  case GEQ:
+    {
+      pair<OrderedSet::iterator, bool> res = geqSet->insert(atom);
+      Assert(res.second);
+
+      addGeqToGeqs(atom, geqSet, res.first);
+      addGeqToEqualities(atom, eqSet);
+      addGeqToLeqs(atom, leqSet);
+
+      break;
+    }
+  default:
+    Unreachable();
+  }
+}
+
+bool rightHandRationalIsEqual(TNode a, TNode b){
+  TNode secondA = a[1];
+  TNode secondB = b[1];
+
+  const Rational& qA = secondA.getConst<Rational>();
+  const Rational& qB = secondB.getConst<Rational>();
+
+  return qA == qB;
+}
+bool rightHandRationalIsLT(TNode a, TNode b){
+  TNode secondA = a[1];
+  TNode secondB = b[1];
+
+  const Rational& qA = secondA.getConst<Rational>();
+  const Rational& qB = secondB.getConst<Rational>();
+
+  return qA < qB;
+}
+
+void ArithUnatePropagator::addEqualityToEqualities(TNode atom,
+                                                   OrderedSet* eqSet,
+                                                   OrderedSet::iterator eqPos){
+  Assert(atom.getKind() == EQUAL);
+  Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
+  for(OrderedSet::iterator eqIter = eqSet->begin();
+      eqIter != eqSet->end(); ++eqIter){
+    if(eqIter == eqPos) continue;
+    TNode eq = *eqIter;
+    Assert(!rightHandRationalIsEqual(eq, atom));
+    addImplication(eq, negation);
+  }
+}
+
+void ArithUnatePropagator::addEqualityToLeqs(TNode atom, OrderedSet* leqSet)
+{
+  Assert(atom.getKind() == EQUAL);
+  Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
+
+  OrderedSet::iterator leqIter = leqSet->lower_bound(atom);
+  if(leqIter != leqSet->end()){
+    TNode lowerBound = *leqIter;
+    if(rightHandRationalIsEqual(atom, lowerBound)){
+      addImplication(atom, lowerBound);  // x=b /\ b = b' => x <= b'
+      if(leqIter != leqSet->begin()){
+        --leqIter;
+        Assert(rightHandRationalIsLT(*leqIter, atom));
+        addImplication(*leqIter, negation); // x=b /\ b > b' => x > b'
+      }
+    }else{
+      //probably wrong
+      Assert(rightHandRationalIsLT(atom, lowerBound));
+      addImplication(atom, lowerBound);// x=b /\ b < b' => x <= b'
+
+      if(leqIter != leqSet->begin()){
+        --leqIter;
+        Assert(rightHandRationalIsLT(*leqIter, atom));
+        addImplication(*leqIter, negation);// x=b /\ b > b' => x > b'
+      }
+    }
+  }else if(leqIter != leqSet->begin()){
+    --leqIter;
+    TNode strictlyLessThan = *leqIter;
+    Assert(rightHandRationalIsLT(strictlyLessThan, atom));
+    addImplication(*leqIter, negation); // x=b /\ b < b' => x <= b'
+  }else{
+    Assert(leqSet->empty());
+  }
+}
+
+void ArithUnatePropagator::addEqualityToGeqs(TNode atom, OrderedSet* geqSet){
+
+  Assert(atom.getKind() == EQUAL);
+  Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
+
+  OrderedSet::iterator geqIter = geqSet->lower_bound(atom);
+  if(geqIter != geqSet->end()){
+    TNode lowerBound = *geqIter;
+    if(rightHandRationalIsEqual(atom, lowerBound)){
+      addImplication(atom, lowerBound);  // x=b /\ b = b' => x >= b'
+      ++geqIter;
+      if(geqIter != geqSet->end()){ // x=b /\ b < b' => x < b'
+        TNode strictlyGt = *geqIter;
+        Assert(rightHandRationalIsLT( atom, strictlyGt ));
+        addImplication(strictlyGt, negation);
+      }
+    }else{
+      Assert(rightHandRationalIsLT(atom, lowerBound));
+      addImplication(lowerBound, negation);// x=b /\ b < b' => x < b'
+      if(geqIter != geqSet->begin()){
+        --geqIter;
+        TNode strictlyLessThan = *geqIter;
+        Assert(rightHandRationalIsLT(strictlyLessThan, atom));
+        addImplication(atom, strictlyLessThan);// x=b /\ b > b' => x >= b'
+      }
+    }
+  }else if(geqIter != geqSet->begin()){
+    --geqIter;
+    TNode strictlyLT = *geqIter;
+    Assert(rightHandRationalIsLT(strictlyLT, atom));
+    addImplication(atom, strictlyLT);// x=b /\ b > b' => x >= b'
+  }else{
+    Assert(geqSet->empty());
+  }
+}
+
+void ArithUnatePropagator::addLeqToLeqs
+(TNode atom,
+ OrderedSet* leqSet,
+ OrderedSet::iterator atomPos)
+{
+  Assert(atom.getKind() == LEQ);
+  Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
+
+  if(atomPos != leqSet->begin()){
+    --atomPos;
+    TNode beforeLeq = *atomPos;
+    Assert(rightHandRationalIsLT(beforeLeq, atom));
+    addImplication(beforeLeq, atom);// x<=b' /\ b' < b => x <= b
+    ++atomPos;
+  }
+  ++atomPos;
+  if(atomPos != leqSet->end()){
+    TNode afterLeq = *atomPos;
+    Assert(rightHandRationalIsLT(atom, afterLeq));
+    addImplication(atom, afterLeq);// x<=b /\ b < b' => x <= b'
+  }
+}
+void ArithUnatePropagator::addLeqToGeqs(TNode atom, OrderedSet* geqSet) {
+
+  Assert(atom.getKind() == LEQ);
+  Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
+
+  OrderedSet::iterator geqIter = geqSet->lower_bound(atom);
+  if(geqIter != geqSet->end()){
+    TNode lowerBound = *geqIter;
+    if(rightHandRationalIsEqual(atom, lowerBound)){
+      Assert(rightHandRationalIsEqual(atom, lowerBound));
+      addImplication(negation, lowerBound);// (x > b) => (x >= b)
+      ++geqIter;
+      if(geqIter != geqSet->end()){
+        TNode next = *geqIter;
+        Assert(rightHandRationalIsLT(atom, next));
+        addImplication(next, negation);// x>=b' /\ b' > b => x > b
+      }
+    }else{
+      Assert(rightHandRationalIsLT(atom, lowerBound));
+      addImplication(lowerBound, negation);// x>=b' /\ b' > b => x > b
+      if(geqIter != geqSet->begin()){
+        --geqIter;
+        TNode prev = *geqIter;
+        Assert(rightHandRationalIsLT(prev, atom));
+        addImplication(negation, prev);// (x>b /\ b > b') => x >= b'
+      }
+    }
+  }else if(geqIter != geqSet->begin()){
+    --geqIter;
+    TNode strictlyLT = *geqIter;
+    Assert(rightHandRationalIsLT(strictlyLT, atom));
+    addImplication(negation, strictlyLT);// (x>b /\ b > b') => x >= b'
+  }else{
+    Assert(geqSet->empty());
+  }
+}
+
+void ArithUnatePropagator::addLeqToEqualities(TNode atom, OrderedSet* eqSet) {
+  Assert(atom.getKind() == LEQ);
+  Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
+
+  //TODO Improve this later
+  for(OrderedSet::iterator eqIter = eqSet->begin(); eqIter != eqSet->end(); ++eqIter){
+    TNode eq = *eqIter;
+    if(rightHandRationalIsEqual(atom, eq)){
+      // (x = b' /\ b = b') =>  x <= b
+      addImplication(eq, atom);
+    }else if(rightHandRationalIsLT(atom, eq)){
+      // (x = b' /\ b' > b) =>  x > b
+      addImplication(eq, negation);
+    }else{
+      // (x = b' /\ b' < b) =>  x <= b
+      addImplication(eq, atom);
+    }
+  }
+}
+
+
+void ArithUnatePropagator::addGeqToGeqs
+(TNode atom, OrderedSet* geqSet, OrderedSet::iterator atomPos)
+{
+  Assert(atom.getKind() == GEQ);
+  Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
+
+  if(atomPos != geqSet->begin()){
+    --atomPos;
+    TNode beforeGeq = *atomPos;
+    Assert(rightHandRationalIsLT(beforeGeq, atom));
+    addImplication(atom, beforeGeq);// x>=b /\ b > b' => x >= b'
+    ++atomPos;
+  }
+  ++atomPos;
+  if(atomPos != geqSet->end()){
+    TNode afterGeq = *atomPos;
+    Assert(rightHandRationalIsLT(atom, afterGeq));
+    addImplication(afterGeq, atom);// x>=b' /\ b' > b => x >= b
+  }
+}
+
+void ArithUnatePropagator::addGeqToLeqs(TNode atom, OrderedSet* leqSet){
+
+  Assert(atom.getKind() == GEQ);
+  Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
+
+  OrderedSet::iterator leqIter = leqSet->lower_bound(atom);
+  if(leqIter != leqSet->end()){
+    TNode lowerBound = *leqIter;
+    if(rightHandRationalIsEqual(atom, lowerBound)){
+      Assert(rightHandRationalIsEqual(atom, lowerBound));
+      addImplication(negation, lowerBound);// (x < b) => (x <= b)
+
+      if(leqIter != leqSet->begin()){
+        --leqIter;
+        TNode prev = *leqIter;
+        Assert(rightHandRationalIsLT(prev, atom));
+        addImplication(prev, negation);// x<=b' /\ b' < b => x < b
+      }
+    }else{
+      Assert(rightHandRationalIsLT(atom, lowerBound));
+      addImplication(negation, lowerBound);// (x < b /\ b < b') => x <= b'
+      ++leqIter;
+      if(leqIter != leqSet->end()){
+        TNode next = *leqIter;
+        Assert(rightHandRationalIsLT(atom, next));
+        addImplication(negation, next);// (x < b /\ b < b') => x <= b'
+      }
+    }
+  }else if(leqIter != leqSet->begin()){
+    --leqIter;
+    TNode strictlyLT = *leqIter;
+    Assert(rightHandRationalIsLT(strictlyLT, atom));
+    addImplication(strictlyLT, negation);// (x <= b' /\ b' < b) => x < b
+  }else{
+    Assert(leqSet->empty());
+  }
+}
+void ArithUnatePropagator::addGeqToEqualities(TNode atom, OrderedSet* eqSet){
+
+  Assert(atom.getKind() == GEQ);
+  Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
+
+  //TODO Improve this later
+  for(OrderedSet::iterator eqIter = eqSet->begin(); eqIter != eqSet->end(); ++eqIter){
+    TNode eq = *eqIter;
+    if(rightHandRationalIsEqual(atom, eq)){
+      // (x = b' /\ b = b') =>  x >= b
+      addImplication(eq, atom);
+    }else if(rightHandRationalIsLT(eq, atom)){
+      // (x = b' /\ b' < b) =>  x < b
+      addImplication(eq, negation);
+    }else{
+      // (x = b' /\ b' > b) =>  x >= b
+      addImplication(eq, atom);
+    }
+  }
+}
+
+void ArithUnatePropagator::addImplication(TNode a, TNode b){
+  Node imp = NodeBuilder<2>(IMPLIES) << a << b;
+
+  Debug("arith-propagate") << "ArithUnatePropagator::addImplication";
+  Debug("arith-propagate") << "(" << a << ", " << b <<")" << endl;
+
+  d_arithOut.lemma(imp);
+}
diff --git a/src/theory/arith/unate_propagator.h b/src/theory/arith/unate_propagator.h
new file mode 100644
index 000000000..88020b52b
--- /dev/null
+++ b/src/theory/arith/unate_propagator.h
@@ -0,0 +1,125 @@
+/*********************                                                        */
+/*! \file arith_propagator.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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 ArithUnatePropagator constructs implications of the form
+ ** "if x < c and c < b, then x < b" (where c and b are constants).
+ **
+ ** ArithUnatePropagator detects unate implications amongst the atoms
+ ** associated with the theory of arithmetic and informs the SAT solver of the
+ ** implication. A unate implication is an implication of the form:
+ **   "if x < c and c < b, then x < b" (where c and b are constants).
+ ** Unate implications are always 2-SAT clauses.
+ ** ArithUnatePropagator sends the implications to the SAT solver in an
+ ** online fashion.
+ ** This means that atoms may be added during solving or before.
+ **
+ ** ArithUnatePropagator maintains sorted lists containing all atoms associated
+ ** for each unique left hand side, the "x" in the inequality "x < c".
+ ** The lists are sorted by the value of the right hand side which must be a
+ ** rational constant.
+ **
+ ** ArithUnatePropagator tries to send out a minimal number of additional
+ ** lemmas per atom added.  Let (x < a), (x < b), (x < c) be arithmetic atoms s.t.
+ ** a < b < c.
+ ** If the the order of adding the atoms is (x < a), (x < b), and (x < c), then
+ ** then set of all lemmas added is:
+ **   {(=> (x<a) (x < b)), (=> (x<b) (x < c))}
+ ** If the order is changed to (x < a), (x < c), and (x < b), then
+ ** the final set of implications emitted is:
+ **   {(=> (x<a) (x < c)), (=> (x<a) (x < b)), (=> (x<b) (x < c))}
+ **
+ ** \todo document this file
+ **/
+
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__ARITH_PROPAGATOR_H
+#define __CVC4__THEORY__ARITH__ARITH_PROPAGATOR_H
+
+#include "expr/node.h"
+#include "context/cdlist.h"
+#include "context/context.h"
+#include "context/cdo.h"
+
+#include "theory/output_channel.h"
+#include "theory/arith/ordered_set.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class ArithUnatePropagator {
+private:
+  /**
+   * OutputChannel for the theory of arithmetic.
+   * The propagator uses this to pass implications back to the SAT solver.
+   */
+  OutputChannel& d_arithOut;
+
+public:
+  ArithUnatePropagator(context::Context* cxt, OutputChannel& arith);
+
+  /**
+   * Adds an atom to the propagator.
+   * Any resulting lemmas will be output via d_arithOut.
+   */
+  void addAtom(TNode atom);
+
+private:
+  /** Sends an implication (=> a b) to the PropEngine via d_arithOut. */
+  void addImplication(TNode a, TNode b);
+
+  /** Check to make sure an lhs has been properly set-up. */
+  bool leftIsSetup(TNode left);
+
+  /** Initializes the lists associated with a unique lhs. */
+  void setupLefthand(TNode left);
+
+
+  /**
+   * The addKtoJs(...) functions are the work horses of ArithUnatePropagator.
+   * These take an atom of the kind K that has just been added
+   * to its associated list, and the list of Js associated with the lhs,
+   * and uses these to deduce unate implications.
+   * (K and J vary over EQUAL, LEQ, and GEQ.)
+   *
+   * Input:
+   * atom - the atom being inserted
+   * Kset - the list of atoms of kind K associated with the lhs.
+   * atomPos - the atoms Position in its own list after being inserted.
+   *
+   * Unfortunately, these tend to be an absolute bear to read because
+   * of all of the special casing and C++ iterator manipulation required.
+   */
+
+  void addEqualityToEqualities(TNode eq, OrderedSet* eqSet, OrderedSet::iterator eqPos);
+  void addEqualityToLeqs(TNode eq, OrderedSet* leqSet);
+  void addEqualityToGeqs(TNode eq, OrderedSet* geqSet);
+
+  void addLeqToLeqs(TNode leq, OrderedSet* leqSet, OrderedSet::iterator leqPos);
+  void addLeqToGeqs(TNode leq, OrderedSet* geqSet);
+  void addLeqToEqualities(TNode leq, OrderedSet* eqSet);
+
+  void addGeqToGeqs(TNode geq, OrderedSet* geqSet, OrderedSet::iterator geqPos);
+  void addGeqToLeqs(TNode geq, OrderedSet* leqSet);
+  void addGeqToEqualities(TNode geq, OrderedSet* eqSet);
+
+};
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_H */
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 7958d977e..813b38d93 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -318,7 +318,7 @@ public:
   }
 
   inline void newLemma(TNode node) {
-    d_propEngine->assertLemma(preprocess(node));
+    d_propEngine->assertSafeLemma(preprocess(node));
   }
 
   /**
diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index 7d147f6a5..8c34370d7 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -114,6 +114,12 @@ public:
     return d_callHistory.size();
   }
 
+  void printIth(std::ostream& os, int i){
+    os << "[TestOutputChannel " << i;
+    os << " " << getIthCallType(i);
+    os << " " << getIthNode(i) << "]";
+  }
+
 private:
   void push(OutputChannelCallType call, TNode n) {
     d_callHistory.push_back(std::make_pair(call,n));