Merging the unate-propagator branch into the trunk. This is a big update so expect a little turbulence. This commit will not compile. There will be a second commit that fixes this in a moment. I am delaying a change to avoid svn whining about a conflict.

6 files changed, 757 insertions, 16 deletions

diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 83d44e285..37df73edd 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -15,10 +15,13 @@ libarith_la_SOURCES = \
 	delta_rational.cpp \
 	partial_model.h \
 	partial_model.cpp \
+	ordered_bounds_list.h \
 	basic.h \
 	normal.h \
 	slack.h \
 	tableau.h \
+	arith_propagator.h \
+	arith_propagator.cpp \
 	theory_arith.h \
 	theory_arith.cpp
 
diff --git a/src/theory/arith/arith_propagator.cpp b/src/theory/arith/arith_propagator.cpp
new file mode 100644
index 000000000..e40575054
--- /dev/null
+++ b/src/theory/arith/arith_propagator.cpp
@@ -0,0 +1,347 @@
+#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(debugTagIsOn("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
new file mode 100644
index 000000000..a623517fb
--- /dev/null
+++ b/src/theory/arith/arith_propagator.h
@@ -0,0 +1,111 @@
+
+
+#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_bounds_list.h b/src/theory/arith/ordered_bounds_list.h
new file mode 100644
index 000000000..d21283afa
--- /dev/null
+++ b/src/theory/arith/ordered_bounds_list.h
@@ -0,0 +1,212 @@
+
+
+#include "cvc4_private.h"
+
+
+#ifndef __CVC4__THEORY__ARITH__ORDERED_BOUNDS_LIST_H
+#define __CVC4__THEORY__ARITH__ORDERED_BOUNDS_LIST_H
+
+#include "expr/node.h"
+#include "util/rational.h"
+#include "expr/kind.h"
+
+#include <vector>
+#include <algorithm>
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+struct RightHandRationalLT
+{
+  bool operator()(TNode s1, TNode s2) const
+  {
+    Assert(s1.getNumChildren() >= 2);
+    Assert(s2.getNumChildren() >= 2);
+
+    Assert(s1[1].getKind() == kind::CONST_RATIONAL);
+    Assert(s2[1].getKind() == kind::CONST_RATIONAL);
+
+    TNode rh1 = s1[1];
+    TNode rh2 = s2[1];
+    const Rational& c1 = rh1.getConst<Rational>();
+    const Rational& c2 = rh2.getConst<Rational>();
+    return c1.cmp(c2) < 0;
+  }
+};
+
+struct RightHandRationalGT
+{
+  bool operator()(TNode s1, TNode s2) const
+  {
+    Assert(s1.getNumChildren() >= 2);
+    Assert(s2.getNumChildren() >= 2);
+
+    Assert(s1[1].getKind() == kind::CONST_RATIONAL);
+    Assert(s2[1].getKind() == kind::CONST_RATIONAL);
+
+    TNode rh1 = s1[1];
+    TNode rh2 = s2[1];
+    const Rational& c1 = rh1.getConst<Rational>();
+    const Rational& c2 = rh2.getConst<Rational>();
+    return c1.cmp(c2) > 0;
+  }
+};
+
+/**
+ * An OrderedBoundsList is a lazily sorted vector of Arithmetic constraints.
+ * The intended use is for a list of rewriting arithmetic atoms.
+ * An example of such a list would be [(<= x 5);(= y 78); (>= x 9)].
+ *
+ * Nodes are required to have a CONST_RATIONAL child as their second node.
+ * Nodes are sorted in increasing order according to RightHandRationalLT.
+ *
+ * The lists are lazily sorted in the sense that the list is not sorted until
+ * an operation to access the element is attempted.
+ *
+ * An append() may make the list no longer sorted.
+ * After an append() operation all iterators for the list become invalid.
+ */
+class OrderedBoundsList {
+private:
+  bool d_isSorted;
+  std::vector<Node> d_list;
+
+public:
+  typedef std::vector<Node>::const_iterator iterator;
+  typedef std::vector<Node>::const_reverse_iterator reverse_iterator;
+
+  /**
+   * Constucts a new and empty OrderBoundsList.
+   * The empty list is initially sorted.
+   */
+  OrderedBoundsList() : d_isSorted(true){}
+
+  /**
+   * Appends a node onto the back of the list.
+   * The list may no longer be sorted.
+   */
+  void append(TNode n){
+    Assert(n.getNumChildren() >= 2);
+    Assert(n[1].getKind() == kind::CONST_RATIONAL);
+    d_isSorted = false;
+    d_list.push_back(n);
+  }
+
+  /** returns the size of the list */
+  unsigned int size(){
+    return d_list.size();
+  }
+
+  /** returns the i'th element in the sort list. This may sort the list.*/
+  TNode at(unsigned int idx){
+    sortIfNeeded();
+    return d_list.at(idx);
+  }
+
+  /** returns true if the list is known to be sorted. */
+  bool isSorted() const{
+    return d_isSorted;
+  }
+
+  /** sorts the list. */
+  void sort(){
+    d_isSorted = true;
+    std::sort(d_list.begin(), d_list.end(), RightHandRationalLT());
+  }
+
+  /**
+   * returns an iterator to the list that iterates in ascending order.
+   * This may sort the list.
+   */
+  iterator begin(){
+    sortIfNeeded();
+    return d_list.begin();
+  }
+  /**
+   * returns an iterator to the end of the list when interating in ascending order.
+   */
+  iterator end() const{
+    return d_list.end();
+  }
+
+  /**
+   * returns an iterator to the list that iterates in descending order.
+   * This may sort the list.
+   */
+  reverse_iterator rbegin(){
+    sortIfNeeded();
+    return d_list.rend();
+  }
+  /**
+   * returns an iterator to the end of the list when interating in descending order.
+   */
+  reverse_iterator rend() const{
+    return d_list.rend();
+  }
+
+  /**
+   * returns an iterator to the least strict upper bound of value.
+   * if the list is [(<= x 2);(>= x 80);(< y 70)]
+   * then *upper_bound((< z 70)) == (>= x 80)
+   *
+   * This may sort the list.
+   * see stl::upper_bound for more information.
+   */
+  iterator upper_bound(TNode value){
+    sortIfNeeded();
+    return std::upper_bound(begin(), end(), value, RightHandRationalLT());
+  }
+  /**
+   * returns an iterator to the greatest lower bound of value.
+   * This is bound is not strict.
+   * if the list is [(<= x 2);(>= x 80);(< y 70)]
+   * then *lower_bound((< z 70)) == (< y 70)
+   *
+   * This may sort the list.
+   * see stl::upper_bound for more information.
+   */
+  iterator lower_bound(TNode value){
+    sortIfNeeded();
+    return std::lower_bound(begin(), end(), value, RightHandRationalLT());
+  }
+  /**
+   * see OrderedBoundsList::upper_bound for more information.
+   * The difference is that the iterator goes in descending order.
+   */
+  reverse_iterator reverse_upper_bound(TNode value){
+    sortIfNeeded();
+    return std::upper_bound(rbegin(), rend(), value, RightHandRationalGT());
+  }
+  /**
+   * see OrderedBoundsList::lower_bound for more information.
+   * The difference is that the iterator goes in descending order.
+   */
+  reverse_iterator reverse_lower_bound(TNode value){
+    sortIfNeeded();
+    return std::lower_bound(rbegin(), rend(), value, RightHandRationalGT());
+  }
+
+  /**
+   * This is an O(n) method for searching the array to check if it contains n.
+   */
+  bool contains(TNode n) const {
+    for(std::vector<Node>::const_iterator i = d_list.begin(); i != d_list.end(); ++i){
+      if(*i == n) return true;
+    }
+    return false;
+  }
+private:
+  /** Sorts the list if it is not already sorted.  */
+  void sortIfNeeded(){
+    if(!d_isSorted){
+      sort();
+    }
+  }
+};
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__ORDERED_BOUNDS_LIST_H */
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index b3b7f58be..bd35e0797 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -34,6 +34,7 @@
 #include "theory/arith/basic.h"
 
 #include "theory/arith/arith_rewriter.h"
+#include "theory/arith/arith_propagator.h"
 
 #include "theory/arith/theory_arith.h"
 #include <map>
@@ -55,6 +56,7 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
   d_partialModel(c),
   d_diseq(c),
   d_rewriter(&d_constants),
+  d_propagator(c),
   d_statistics()
 {
   uint64_t ass_id = partial_model::Assignment::getId();
@@ -81,6 +83,15 @@ TheoryArith::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_statUpdateConflicts);
 }
 
+TheoryArith::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_statPivots);
+  StatisticsRegistry::unregisterStat(&d_statUpdates);
+  StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts);
+  StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts);
+  StatisticsRegistry::unregisterStat(&d_statUpdateConflicts);
+}
+
+
 bool isBasicSum(TNode n){
   if(n.getKind() != kind::PLUS) return false;
 
@@ -143,6 +154,8 @@ void TheoryArith::preRegisterTerm(TNode n) {
     Assert(isNormalAtom(n));
 
 
+    d_propagator.addAtom(n);
+
     TNode left  = n[0];
     TNode right = n[1];
     if(left.getKind() == PLUS){
@@ -206,6 +219,10 @@ void TheoryArith::setupVariable(TNode x){
     //lower bound. This is done to strongly enforce the notion that basic
     //variables should not be changed without begin checked.
 
+    //Strictly speaking checking x is unnessecary as it cannot have an upper or
+    //lower bound. This is done to strongly enforce the notion that basic
+    //variables should not be changed without begin checked.
+
   }
   Debug("arithgc") << "setupVariable("<<x<<")"<<std::endl;
 };
@@ -682,41 +699,69 @@ void TheoryArith::check(Effort level){
   Debug("arith") << "TheoryArith::check begun" << std::endl;
 
   while(!done()){
+
     Node original = get();
     Node assertion = simulatePreprocessing(original);
     Debug("arith_assertions") << "arith assertion(" << original
                               << " \\-> " << assertion << ")" << std::endl;
 
+    d_propagator.assertLiteral(original);
     bool conflictDuringAnAssert = assertionCases(original, assertion);
 
+
     if(conflictDuringAnAssert){
-      if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
       d_partialModel.revertAssignmentChanges();
-      if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
-
       return;
     }
   }
 
-  if(fullEffort(level)){
-    if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
+  //TODO This must be done everytime for the time being
+  if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
 
-    Node possibleConflict = updateInconsistentVars();
-    if(possibleConflict != Node::null()){
+  Node possibleConflict = updateInconsistentVars();
+  if(possibleConflict != Node::null()){
 
-      d_partialModel.revertAssignmentChanges();
+    d_partialModel.revertAssignmentChanges();
 
-      d_out->conflict(possibleConflict, true);
+    if(debugTagIsOn("arith::print-conflict"))
+      Debug("arith_conflict") << (possibleConflict) << std::endl;
 
-      Debug("arith_conflict") <<"Found a conflict "<< possibleConflict << endl;
-    }else{
-      d_partialModel.commitAssignmentChanges();
-    }
-    if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
+    d_out->conflict(possibleConflict);
+
+    Debug("arith_conflict") <<"Found a conflict "<< possibleConflict << endl;
+  }else{
+    d_partialModel.commitAssignmentChanges();
   }
+  if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
+
 
   Debug("arith") << "TheoryArith::check end" << std::endl;
 
+  if(debugTagIsOn("arith::print_model")) {
+    Debug("arith::print_model") << "Model:" << endl;
+
+    for (unsigned i = 0; i < d_variables.size(); ++ i) {
+      Debug("arith::print_model") << d_variables[i] << " : " <<
+        d_partialModel.getAssignment(d_variables[i]);
+      if(isBasic(d_variables[i]))
+        Debug("arith::print_model") << " (basic)";
+      Debug("arith::print_model") << endl;
+    }
+  }
+  if(debugTagIsOn("arith::print_assertions")) {
+    Debug("arith::print_assertions") << "Assertions:" << endl;
+    for (unsigned i = 0; i < d_variables.size(); ++ i) {
+      Node x = d_variables[i];
+      if (x.hasAttribute(partial_model::LowerConstraint())) {
+        Node constr = d_partialModel.getLowerConstraint(x);
+        Debug("arith::print_assertions") << constr.toString() << endl;
+      }
+      if (x.hasAttribute(partial_model::UpperConstraint())) {
+        Node constr = d_partialModel.getUpperConstraint(x);
+        Debug("arith::print_assertions") << constr.toString() << endl;
+      }
+    }
+  }
 }
 
 /**
@@ -750,3 +795,23 @@ void TheoryArith::checkTableau(){
     Assert(sum == shouldBe);
   }
 }
+
+
+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);
+}
+
+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);
+    }
+  }
+}
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index aff60f651..c76923bee 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -30,6 +30,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 "util/stats.h"
 
@@ -96,6 +97,7 @@ private:
    */
   ArithRewriter d_rewriter;
 
+  ArithUnatePropagator d_propagator;
 
 public:
   TheoryArith(context::Context* c, OutputChannel& out);
@@ -115,8 +117,8 @@ public:
   void registerTerm(TNode n);
 
   void check(Effort e);
-  void propagate(Effort e) { Unimplemented(); }
-  void explain(TNode n, Effort e) { Unimplemented(); }
+  void propagate(Effort e);
+  void explain(TNode n, Effort e);
 
   void shutdown(){ }
 
@@ -242,6 +244,7 @@ private:
     IntStat d_statAssertLowerConflicts, d_statUpdateConflicts;
 
     Statistics();
+    ~Statistics();
   };
 
   Statistics d_statistics;