- Removes arith_constants.h

- Adds ArithStaticLearner.  Consolidates and cleans up the code for static learning in arithmetic.  Static learning is now associated with a small amount of state between calls. This is used to track the data for the miplib trick.  The goal is to make this inference work without relying on the fact that all of the miplib problem is asserted under the same AND node.
- This commit contains miscellaneous other arithmetic cleanup.

11 files changed, 524 insertions, 441 deletions

diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 48be16f90..2c00f5d4d 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -9,10 +9,11 @@ libarith_la_SOURCES = \
 	theory_arith_type_rules.h \
 	arith_rewriter.h \
 	arith_rewriter.cpp \
+	arith_static_learner.h \
+	arith_static_learner.cpp \
 	normal_form.h\
 	normal_form.cpp \
 	arith_utilities.h \
-	arith_constants.h \
 	delta_rational.h \
 	delta_rational.cpp \
 	partial_model.h \
diff --git a/src/theory/arith/arith_constants.h b/src/theory/arith/arith_constants.h
deleted file mode 100644
index 98a202207..000000000
--- a/src/theory/arith/arith_constants.h
+++ /dev/null
@@ -1,67 +0,0 @@
-/*********************                                                        */
-/*! \file arith_constants.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_CONSTANTS_H
-#define __CVC4__THEORY__ARITH__ARITH_CONSTANTS_H
-
-#include "expr/node.h"
-#include "expr/node_manager.h"
-#include "util/rational.h"
-#include "theory/arith/delta_rational.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-class ArithConstants {
-public:
-  Rational d_ZERO;
-  Rational d_ONE;
-  Rational d_NEGATIVE_ONE;
-
-  DeltaRational d_ZERO_DELTA;
-
-  Node d_ZERO_NODE;
-  Node d_ONE_NODE;
-  Node d_NEGATIVE_ONE_NODE;
-
-  ArithConstants(NodeManager* nm) :
-    d_ZERO(0,1),
-    d_ONE(1,1),
-    d_NEGATIVE_ONE(-1,1),
-    d_ZERO_DELTA(d_ZERO),
-    d_ZERO_NODE(nm->mkConst(d_ZERO)),
-    d_ONE_NODE(nm->mkConst(d_ONE)),
-    d_NEGATIVE_ONE_NODE(nm->mkConst(d_NEGATIVE_ONE))
-  {}
-
-  ~ArithConstants() {
-    d_ZERO_NODE = Node::null();
-    d_ONE_NODE = Node::null();
-    d_NEGATIVE_ONE_NODE = Node::null();
-  }
-};/* class ArithConstants */
-
-}/* namespace CVC4::theory::arith */
-}/* namespace CVC4::theory */
-}/* namespace CVC4 */
-
-#endif /* __CVC4__THEORY__ARITH_ARITH_CONSTANTS_H */
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index cc80e2dd8..941394138 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -30,8 +30,6 @@ using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
 
-arith::ArithConstants* ArithRewriter::s_constants = NULL;
-
 bool isVariable(TNode t){
   return t.getMetaKind() == kind::metakind::VARIABLE;
 }
@@ -52,7 +50,11 @@ RewriteResponse ArithRewriter::rewriteVariable(TNode t){
 RewriteResponse ArithRewriter::rewriteMinus(TNode t, bool pre){
   Assert(t.getKind()== kind::MINUS);
 
-  if(t[0] == t[1]) return RewriteResponse(REWRITE_DONE, s_constants->d_ZERO_NODE);
+  if(t[0] == t[1]){
+    Rational zero(0);
+    Node zeroNode  = mkRationalNode(zero);
+    return RewriteResponse(REWRITE_DONE, zeroNode);
+  }
 
   Node noMinus = makeSubtractionNode(t[0],t[1]);
   if(pre){
@@ -121,17 +123,19 @@ RewriteResponse ArithRewriter::preRewriteMult(TNode t){
   // Rewrite multiplications with a 0 argument and to 0
   Integer intZero;
 
+  Rational qZero(0);
+
   for(TNode::iterator i = t.begin(); i != t.end(); ++i) {
     if((*i).getKind() == kind::CONST_RATIONAL) {
-      if((*i).getConst<Rational>() == s_constants->d_ZERO) {
-        return RewriteResponse(REWRITE_DONE, s_constants->d_ZERO_NODE);
+      if((*i).getConst<Rational>() == qZero) {
+        return RewriteResponse(REWRITE_DONE, mkRationalNode(qZero));
       }
     } else if((*i).getKind() == kind::CONST_INTEGER) {
       if((*i).getConst<Integer>() == intZero) {
         if(t.getType().isInteger()) {
           return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(intZero));
         } else {
-          return RewriteResponse(REWRITE_DONE, s_constants->d_ZERO_NODE);
+          return RewriteResponse(REWRITE_DONE, mkRationalNode(qZero));
         }
       }
     }
@@ -222,7 +226,8 @@ RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){
   }else{
     //Transform this to: (left - right) |><| 0
     Node diff = makeSubtractionNode(left, right);
-    Node reduction = NodeManager::currentNM()->mkNode(atom.getKind(), diff, s_constants->d_ZERO_NODE);
+    Rational qZero(0);
+    Node reduction = NodeManager::currentNM()->mkNode(atom.getKind(), diff, mkRationalNode(qZero));
     return RewriteResponse(REWRITE_AGAIN_FULL, reduction);
   }
 }
@@ -246,7 +251,8 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){
 
     //Transform this to: (left - right) |><| 0
     Node diff = makeSubtractionNode(left, right);
-    reduction = currNM->mkNode(atom.getKind(), diff, s_constants->d_ZERO_NODE);
+    Rational qZero(0);
+    reduction = currNM->mkNode(atom.getKind(), diff, mkRationalNode(qZero));
   }
 
   if(reduction.getKind() == kind::GT){
@@ -291,7 +297,8 @@ RewriteResponse ArithRewriter::preRewrite(TNode t){
 }
 
 Node ArithRewriter::makeUnaryMinusNode(TNode n){
-  return NodeManager::currentNM()->mkNode(kind::MULT,s_constants->d_NEGATIVE_ONE_NODE,n);
+  Rational qNegOne(-1);
+  return NodeManager::currentNM()->mkNode(kind::MULT, mkRationalNode(qNegOne),n);
 }
 
 Node ArithRewriter::makeSubtractionNode(TNode l, TNode r){
@@ -311,7 +318,7 @@ RewriteResponse ArithRewriter::rewriteDivByConstant(TNode t, bool pre){
 
   const Rational& den = right.getConst<Rational>();
 
-  Assert(den != s_constants->d_ZERO);
+  Assert(den != Rational(0));
 
   Rational div = den.inverse();
 
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 3a8fc191a..d88a7ae92 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -23,7 +23,6 @@
 #define __CVC4__THEORY__ARITH__ARITH_REWRITER_H
 
 #include "theory/theory.h"
-#include "theory/arith/arith_constants.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/normal_form.h"
 
@@ -37,8 +36,6 @@ class ArithRewriter {
 
 private:
 
-  static arith::ArithConstants* s_constants;
-
   static Node makeSubtractionNode(TNode l, TNode r);
   static Node makeUnaryMinusNode(TNode n);
 
@@ -67,18 +64,9 @@ public:
   static RewriteResponse preRewrite(TNode n);
   static RewriteResponse postRewrite(TNode n);
 
-  static void init() {
-    if (s_constants == NULL) {
-      s_constants = new arith::ArithConstants(NodeManager::currentNM());
-    }
-  }
+  static void init() { }
 
-  static void shutdown() {
-    if (s_constants != NULL) {
-      delete s_constants;
-      s_constants = NULL;
-    }
-  }
+  static void shutdown() { }
 
 private:
 
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
new file mode 100644
index 000000000..6fb538fac
--- /dev/null
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -0,0 +1,298 @@
+/*********************                                                        */
+/*! \file arith_rewriter.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): mdeters
+ ** 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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "theory/rewriter.h"
+
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arith_static_learner.h"
+
+#include "util/propositional_query.h"
+
+#include <vector>
+
+using namespace std;
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::theory;
+using namespace CVC4::theory::arith;
+
+
+ArithStaticLearner::ArithStaticLearner():
+  d_miplibTrick(),
+  d_statistics()
+{}
+
+ArithStaticLearner::Statistics::Statistics():
+  d_iteMinMaxApplications("theory::arith::iteMinMaxApplications", 0),
+  d_iteConstantApplications("theory::arith::iteConstantApplications", 0),
+  d_miplibtrickApplications("theory::arith::miplibtrickApplications", 0),
+  d_avgNumMiplibtrickValues("theory::arith::avgNumMiplibtrickValues")
+{
+  StatisticsRegistry::registerStat(&d_iteMinMaxApplications);
+  StatisticsRegistry::registerStat(&d_iteConstantApplications);
+  StatisticsRegistry::registerStat(&d_miplibtrickApplications);
+  StatisticsRegistry::registerStat(&d_avgNumMiplibtrickValues);
+}
+
+ArithStaticLearner::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_iteMinMaxApplications);
+  StatisticsRegistry::unregisterStat(&d_iteConstantApplications);
+  StatisticsRegistry::unregisterStat(&d_miplibtrickApplications);
+  StatisticsRegistry::unregisterStat(&d_avgNumMiplibtrickValues);
+}
+
+void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){
+
+  vector<TNode> workList;
+  workList.push_back(n);
+  TNodeSet processed;
+
+  //Contains an underapproximation of nodes that must hold.
+  TNodeSet defTrue;
+
+  defTrue.insert(n);
+
+  while(!workList.empty()) {
+    n = workList.back();
+
+    bool unprocessedChildren = false;
+    for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
+      if(processed.find(*i) == processed.end()) {
+        // unprocessed child
+        workList.push_back(*i);
+        unprocessedChildren = true;
+      }
+    }
+    if(n.getKind() == AND && defTrue.find(n) != defTrue.end() ){
+      for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
+        defTrue.insert(*i);
+      }
+    }
+
+    if(unprocessedChildren) {
+      continue;
+    }
+
+    workList.pop_back();
+    // has node n been processed in the meantime ?
+    if(processed.find(n) != processed.end()) {
+      continue;
+    }
+    processed.insert(n);
+
+    process(n,learned, defTrue);
+
+  }
+
+  postProcess(learned);
+}
+
+void ArithStaticLearner::clear(){
+  d_miplibTrick.clear();
+}
+
+
+void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet& defTrue){
+  Debug("arith::static") << "===================== looking at" << n << endl;
+
+  switch(n.getKind()){
+  case ITE:
+    if(n[0].getKind() != EQUAL &&
+       isRelationOperator(n[0].getKind())  ){
+      iteMinMax(n, learned);
+    }
+
+    if((n[1].getKind() == CONST_RATIONAL || n[1].getKind() == CONST_INTEGER) &&
+       (n[2].getKind() == CONST_RATIONAL || n[2].getKind() == CONST_INTEGER)) {
+      iteConstant(n, learned);
+    }
+    break;
+  case IMPLIES:
+    // == 3-FINITE VALUE SET : Collect information ==
+    if(n[1].getKind() == EQUAL &&
+       n[1][0].getMetaKind() == metakind::VARIABLE &&
+       defTrue.find(n) != defTrue.end()){
+      Node eqTo = n[1][1];
+      Node rewriteEqTo = Rewriter::rewrite(eqTo);
+      if(rewriteEqTo.getKind() == CONST_RATIONAL){
+
+        TNode var = n[1][0];
+        if(d_miplibTrick.find(var)  == d_miplibTrick.end()){
+          d_miplibTrick.insert(make_pair(var, set<Node>()));
+        }
+        d_miplibTrick[var].insert(n);
+        Debug("arith::miplib") << "insert " << var  << " const " << n << endl;
+      }
+    }
+    break;
+  default: // Do nothing
+    break;
+  }
+}
+
+void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){
+  Assert(n.getKind() == kind::ITE);
+  Assert(n[0].getKind() != EQUAL);
+  Assert(isRelationOperator(n[0].getKind()));
+
+  TNode c = n[0];
+  Kind k = simplifiedKind(c);
+  TNode t = n[1];
+  TNode e = n[2];
+  TNode cleft = (c.getKind() == NOT) ? c[0][0] : c[0];
+  TNode cright = (c.getKind() == NOT) ? c[0][1] : c[1];
+
+  if((t == cright) && (e == cleft)){
+    TNode tmp = t;
+    t = e;
+    e = tmp;
+    k = reverseRelationKind(k);
+  }
+  if(t == cleft && e == cright){
+    // t == cleft && e == cright
+    Assert( t == cleft );
+    Assert( e == cright );
+    switch(k){
+    case LT:   // (ite (< x y) x y)
+    case LEQ: { // (ite (<= x y) x y)
+      Node nLeqX = NodeBuilder<2>(LEQ) << n << t;
+      Node nLeqY = NodeBuilder<2>(LEQ) << n << e;
+      Debug("arith::static") << n << "is a min =>"  << nLeqX << nLeqY << endl;
+      learned << nLeqX << nLeqY;
+      ++(d_statistics.d_iteMinMaxApplications);
+      break;
+    }
+    case GT: // (ite (> x y) x y)
+    case GEQ: { // (ite (>= x y) x y)
+      Node nGeqX = NodeBuilder<2>(GEQ) << n << t;
+      Node nGeqY = NodeBuilder<2>(GEQ) << n << e;
+      Debug("arith::static") << n << "is a max =>"  << nGeqX << nGeqY << endl;
+      learned << nGeqX << nGeqY;
+      ++(d_statistics.d_iteMinMaxApplications);
+      break;
+    }
+    default: Unreachable();
+    }
+  }
+}
+
+void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){
+  Assert(n.getKind() == ITE);
+  Assert(n[1].getKind() == CONST_RATIONAL || n[1].getKind() == CONST_INTEGER );
+  Assert(n[2].getKind() == CONST_RATIONAL || n[2].getKind() == CONST_INTEGER );
+
+  Rational t = coerceToRational(n[1]);
+  Rational e = coerceToRational(n[2]);
+  TNode min = (t <= e) ? n[1] : n[2];
+  TNode max = (t >= e) ? n[1] : n[2];
+
+  Node nGeqMin = NodeBuilder<2>(GEQ) << n << min;
+  Node nLeqMax = NodeBuilder<2>(LEQ) << n << max;
+  Debug("arith::static") << n << " iteConstant"  << nGeqMin << nLeqMax << endl;
+  learned << nGeqMin << nLeqMax;
+  ++(d_statistics.d_iteConstantApplications);
+}
+
+
+void ArithStaticLearner::postProcess(NodeBuilder<>& learned){
+
+  // == 3-FINITE VALUE SET ==
+  VarToNodeSetMap::iterator i = d_miplibTrick.begin();
+  VarToNodeSetMap::iterator endMipLibTrick = d_miplibTrick.end();
+  for(; i != endMipLibTrick; ++i){
+    TNode var = i->first;
+    const set<Node>& imps = i->second;
+
+    Assert(!imps.empty());
+    vector<Node> conditions;
+    set<Rational> values;
+    set<Node>::const_iterator j=imps.begin(), impsEnd=imps.end();
+    for(; j != impsEnd; ++j){
+      TNode imp = *j;
+      Assert(imp.getKind() == IMPLIES);
+      Assert(imp[1].getKind() == EQUAL);
+
+      Node eqTo = imp[1][1];
+      Node rewriteEqTo = Rewriter::rewrite(eqTo);
+      Assert(rewriteEqTo.getKind() == CONST_RATIONAL);
+
+      conditions.push_back(imp[0]);
+      values.insert(rewriteEqTo.getConst<Rational>());
+    }
+
+    Node possibleTaut = Node::null();
+    if(conditions.size() == 1){
+      possibleTaut = conditions.front();
+    }else{
+      NodeBuilder<> orBuilder(OR);
+      orBuilder.append(conditions);
+      possibleTaut = orBuilder;
+    }
+
+
+    Debug("arith::miplib") << "var: " << var << endl;
+    Debug("arith::miplib") << "possibleTaut: " << possibleTaut << endl;
+
+    Result isTaut = PropositionalQuery::isTautology(possibleTaut);
+    if(isTaut == Result(Result::VALID)){
+      miplibTrick(var, values, learned);
+    }
+  }
+}
+
+
+void ArithStaticLearner::miplibTrick(TNode var, set<Rational>& values, NodeBuilder<>& learned){
+
+  Debug("arith::miplib") << var << " found a tautology!"<< endl;
+
+  const Rational& min = *(values.begin());
+  const Rational& max = *(values.rbegin());
+
+  Debug("arith::miplib") << "min: " << min << endl;
+  Debug("arith::miplib") << "max: " << max << endl;
+
+  Assert(min <= max);
+  ++(d_statistics.d_miplibtrickApplications);
+  (d_statistics.d_avgNumMiplibtrickValues).addEntry(values.size());
+
+  Node nGeqMin = NodeBuilder<2>(GEQ) << var << mkRationalNode(min);
+  Node nLeqMax = NodeBuilder<2>(LEQ) << var << mkRationalNode(max);
+  Debug("arith::miplib") << nGeqMin << nLeqMax << endl;
+  learned << nGeqMin << nLeqMax;
+  set<Rational>::iterator valuesIter = values.begin();
+  set<Rational>::iterator valuesEnd = values.end();
+  set<Rational>::iterator valuesPrev = valuesIter;
+  ++valuesIter;
+  for(; valuesIter != valuesEnd; valuesPrev = valuesIter, ++valuesIter){
+    const Rational& prev = *valuesPrev;
+    const Rational& curr = *valuesIter;
+    Assert(prev < curr);
+
+    //The interval (last,curr) can be excluded:
+    //(not (and (> var prev) (< var curr))
+    //<=> (or (not (> var prev)) (not (< var curr)))
+    //<=> (or (<= var prev) (>= var curr))
+    Node leqPrev = NodeBuilder<2>(LEQ) << var << mkRationalNode(prev);
+    Node geqCurr = NodeBuilder<2>(GEQ) << var << mkRationalNode(curr);
+    Node excludedMiddle =  NodeBuilder<2>(OR) << leqPrev << geqCurr;
+    Debug("arith::miplib") << excludedMiddle << endl;
+    learned << excludedMiddle;
+  }
+}
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
new file mode 100644
index 000000000..02274318f
--- /dev/null
+++ b/src/theory/arith/arith_static_learner.h
@@ -0,0 +1,63 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
+#define __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
+
+
+#include "util/stats.h"
+#include "theory/arith/arith_utilities.h"
+#include <set>
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class ArithStaticLearner {
+private:
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+
+  /* Maps a variable, x, to the set of defTrue nodes of the form
+   *  (=> _ (= x c))
+   * where c is a constant.
+   */
+  typedef __gnu_cxx::hash_map<Node, std::set<Node>, NodeHashFunction> VarToNodeSetMap;
+  VarToNodeSetMap d_miplibTrick;
+
+public:
+  ArithStaticLearner();
+  void staticLearning(TNode n, NodeBuilder<>& learned);
+
+  void clear();
+
+private:
+  void process(TNode n, NodeBuilder<>& learned, const TNodeSet& defTrue);
+
+  void postProcess(NodeBuilder<>& learned);
+
+  void iteMinMax(TNode n, NodeBuilder<>& learned);
+  void iteConstant(TNode n, NodeBuilder<>& learned);
+
+  void miplibTrick(TNode var, std::set<Rational>& values, NodeBuilder<>& learned);
+
+  /** These fields are designed to be accessable to ArithStaticLearner methods. */
+  class Statistics {
+  public:
+    IntStat d_iteMinMaxApplications;
+    IntStat d_iteConstantApplications;
+
+    IntStat d_miplibtrickApplications;
+    AverageStat d_avgNumMiplibtrickValues;
+
+    Statistics();
+    ~Statistics();
+  };
+
+  Statistics d_statistics;
+
+};/* class ArithStaticLearner */
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H */
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index aa4e8bc13..5d6ca27e9 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -26,7 +26,6 @@
 #include "expr/node_self_iterator.h"
 #include "util/rational.h"
 #include "theory/theory.h"
-#include "theory/arith/arith_constants.h"
 #include "theory/arith/arith_utilities.h"
 
 #include <list>
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index dc451288b..1e7b5c028 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -618,7 +618,7 @@ Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){
     if(nonbasic == conflictVar) continue;
 
     const Rational& a_ij = (*nbi).getCoefficient();
-    Assert(a_ij != d_constants.d_ZERO);
+    Assert(a_ij != d_ZERO);
 
     int sgn = a_ij.sgn();
     Assert(sgn != 0);
@@ -662,7 +662,7 @@ Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){
     const Rational& a_ij = (*nbi).getCoefficient();
 
     int sgn = a_ij.sgn();
-    Assert(a_ij != d_constants.d_ZERO);
+    Assert(a_ij != d_ZERO);
     Assert(sgn != 0);
 
     if(sgn < 0){
@@ -691,7 +691,7 @@ Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){
  */
 DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe){
   Assert(d_tableau.isBasic(x));
-  DeltaRational sum = d_constants.d_ZERO_DELTA;
+  DeltaRational sum(0);
 
   ReducedRowVector& row = d_tableau.lookup(x);
   for(ReducedRowVector::const_iterator i = row.begin(), end = row.end();
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index c6bc3c434..6f3ff073f 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -25,9 +25,6 @@ namespace arith {
 class SimplexDecisionProcedure {
 private:
 
-  /** Stores system wide constants to avoid unnessecary reconstruction. */
-  const ArithConstants& d_constants;
-
   /**
    * Manages information about the assignment and upper and lower bounds on
    * variables.
@@ -44,23 +41,22 @@ private:
   std::vector<Node> d_delayedLemmas;
   uint32_t d_delayedLemmasPos;
 
+  Rational d_ZERO;
+
 public:
-  SimplexDecisionProcedure(const ArithConstants& constants,
-                           ArithPartialModel& pm,
+  SimplexDecisionProcedure(ArithPartialModel& pm,
                            OutputChannel* out,
                            Tableau& tableau) :
-    d_constants(constants),
     d_partialModel(pm),
     d_out(out),
     d_tableau(tableau),
     d_queue(pm, tableau),
     d_numVariables(0),
     d_delayedLemmas(),
-    d_delayedLemmasPos(0)
+    d_delayedLemmasPos(0),
+    d_ZERO(0)
   {}
 
-
-public:
   /**
    * Assert*(n, orig) takes an bound n that is implied by orig.
    * and asserts that as a new bound if it is tighter than the current bound
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index c0e7057c2..726bfc210 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -57,7 +57,6 @@ typedef expr::Attribute<SlackAttrID, Node> Slack;
 
 TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
   Theory(THEORY_ARITH, c, out),
-  d_constants(NodeManager::currentNM()),
   d_partialModel(c),
   d_userVariables(),
   d_diseq(c),
@@ -67,7 +66,8 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
   d_tableauResetDensity(2.0),
   d_tableauResetPeriod(10),
   d_propagator(c, out),
-  d_simplex(d_constants, d_partialModel, d_out, d_tableau),
+  d_simplex(d_partialModel, d_out, d_tableau),
+  d_DELTA_ZERO(0),
   d_statistics()
 {}
 
@@ -81,8 +81,6 @@ TheoryArith::Statistics::Statistics():
   d_staticLearningTimer("theory::arith::staticLearningTimer"),
   d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0),
   d_presolveTime("theory::arith::presolveTime"),
-  d_miplibtrickApplications("theory::arith::miplibtrickApplications", 0),
-  d_avgNumMiplibtrickValues("theory::arith::avgNumMiplibtrickValues"),
   d_initialTableauDensity("theory::arith::initialTableauDensity", 0.0),
   d_avgTableauDensityAtRestart("theory::arith::avgTableauDensityAtRestarts"),
   d_tableauResets("theory::arith::tableauResets", 0),
@@ -97,8 +95,6 @@ TheoryArith::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_permanentlyRemovedVariables);
   StatisticsRegistry::registerStat(&d_presolveTime);
 
-  StatisticsRegistry::registerStat(&d_miplibtrickApplications);
-  StatisticsRegistry::registerStat(&d_avgNumMiplibtrickValues);
 
   StatisticsRegistry::registerStat(&d_initialTableauDensity);
   StatisticsRegistry::registerStat(&d_avgTableauDensityAtRestart);
@@ -116,8 +112,6 @@ TheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_permanentlyRemovedVariables);
   StatisticsRegistry::unregisterStat(&d_presolveTime);
 
-  StatisticsRegistry::unregisterStat(&d_miplibtrickApplications);
-  StatisticsRegistry::unregisterStat(&d_avgNumMiplibtrickValues);
 
   StatisticsRegistry::unregisterStat(&d_initialTableauDensity);
   StatisticsRegistry::unregisterStat(&d_avgTableauDensityAtRestart);
@@ -125,228 +119,29 @@ TheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_restartTimer);
 }
 
-#include "util/propositional_query.h"
 void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
   TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer);
 
-  vector<TNode> workList;
-  workList.push_back(n);
-  __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed;
-
-  //Contains an underapproximation of nodes that must hold.
-  __gnu_cxx::hash_set<TNode, TNodeHashFunction> defTrue;
-
-  /* Maps a variable, x, to the set of defTrue nodes of the form
-   *  (=> _ (= x c))
-   * where c is a constant.
-   */
-  typedef __gnu_cxx::hash_map<TNode, set<TNode>, TNodeHashFunction> VarToNodeSetMap;
-  VarToNodeSetMap miplibTrick;
-
-  defTrue.insert(n);
-
-  while(!workList.empty()) {
-    n = workList.back();
-
-    bool unprocessedChildren = false;
-    for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
-      if(processed.find(*i) == processed.end()) {
-        // unprocessed child
-        workList.push_back(*i);
-        unprocessedChildren = true;
-      }
-    }
-    if(n.getKind() == AND && defTrue.find(n) != defTrue.end() ){
-      for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
-        defTrue.insert(*i);
-      }
-    }
-
-    if(unprocessedChildren) {
-      continue;
-    }
-
-    workList.pop_back();
-    // has node n been processed in the meantime ?
-    if(processed.find(n) != processed.end()) {
-      continue;
-    }
-    processed.insert(n);
-
-    // == MINS ==
-
-    Debug("mins") << "===================== looking at" << endl << n << endl;
-    if(n.getKind() == kind::ITE && n[0].getKind() != EQUAL && isRelationOperator(n[0].getKind())  ){
-      TNode c = n[0];
-      Kind k = simplifiedKind(c);
-      TNode t = n[1];
-      TNode e = n[2];
-      TNode cleft = (c.getKind() == NOT) ? c[0][0] : c[0];
-      TNode cright = (c.getKind() == NOT) ? c[0][1] : c[1];
-
-      if((t == cright) && (e == cleft)){
-        TNode tmp = t;
-        t = e;
-        e = tmp;
-        k = reverseRelationKind(k);
-      }
-      if(t == cleft && e == cright){
-        // t == cleft && e == cright
-        Assert( t == cleft );
-        Assert( e == cright );
-        switch(k){
-        case LT:   // (ite (< x y) x y)
-        case LEQ: { // (ite (<= x y) x y)
-          Node nLeqX = NodeBuilder<2>(LEQ) << n << t;
-          Node nLeqY = NodeBuilder<2>(LEQ) << n << e;
-          Debug("arith::mins") << n << "is a min =>"  << nLeqX << nLeqY << endl;
-          learned << nLeqX << nLeqY;
-          break;
-        }
-        case GT: // (ite (> x y) x y)
-        case GEQ: { // (ite (>= x y) x y)
-          Node nGeqX = NodeBuilder<2>(GEQ) << n << t;
-          Node nGeqY = NodeBuilder<2>(GEQ) << n << e;
-          Debug("arith::mins") << n << "is a max =>"  << nGeqX << nGeqY << endl;
-          learned << nGeqX << nGeqY;
-          break;
-        }
-        default: Unreachable();
-        }
-      }
-    }
-    // == 2-CONSTANTS ==
-
-    if(n.getKind() == ITE &&
-       (n[1].getKind() == CONST_RATIONAL || n[1].getKind() == CONST_INTEGER) &&
-       (n[2].getKind() == CONST_RATIONAL || n[2].getKind() == CONST_INTEGER)) {
-      Rational t = coerceToRational(n[1]);
-      Rational e = coerceToRational(n[2]);
-      TNode min = (t <= e) ? n[1] : n[2];
-      TNode max = (t >= e) ? n[1] : n[2];
-
-      Node nGeqMin = NodeBuilder<2>(GEQ) << n << min;
-      Node nLeqMax = NodeBuilder<2>(LEQ) << n << max;
-      Debug("arith::mins") << n << " is a constant sandwich"  << nGeqMin << nLeqMax << endl;
-      learned << nGeqMin << nLeqMax;
-    }
-    // == 3-FINITE VALUE SET : Collect information ==
-    if(n.getKind() == IMPLIES &&
-       n[1].getKind() == EQUAL &&
-       n[1][0].getMetaKind() == metakind::VARIABLE &&
-       defTrue.find(n) != defTrue.end()){
-      Node eqTo = n[1][1];
-      Node rewriteEqTo = Rewriter::rewrite(eqTo);
-      if(rewriteEqTo.getKind() == CONST_RATIONAL){
-
-        TNode var = n[1][0];
-        if(miplibTrick.find(var)  == miplibTrick.end()){
-          miplibTrick.insert(make_pair(var, set<TNode>()));
-        }
-        miplibTrick[var].insert(n);
-        Debug("arith::miplib") << "insert " << var  << " const " << n << endl;
-      }
-    }
-  }
-
-  // == 3-FINITE VALUE SET ==
-  VarToNodeSetMap::iterator i = miplibTrick.begin(), endMipLibTrick = miplibTrick.end();
-  for(; i != endMipLibTrick; ++i){
-    TNode var = i->first;
-    const set<TNode>& imps = i->second;
-
-    Assert(!imps.empty());
-    vector<Node> conditions;
-    vector<Rational> valueCollection;
-    set<TNode>::const_iterator j=imps.begin(), impsEnd=imps.end();
-    for(; j != impsEnd; ++j){
-      TNode imp = *j;
-      Assert(imp.getKind() == IMPLIES);
-      Assert(defTrue.find(imp) != defTrue.end());
-      Assert(imp[1].getKind() == EQUAL);
-
-
-      Node eqTo = imp[1][1];
-      Node rewriteEqTo = Rewriter::rewrite(eqTo);
-      Assert(rewriteEqTo.getKind() == CONST_RATIONAL);
-
-      conditions.push_back(imp[0]);
-      valueCollection.push_back(rewriteEqTo.getConst<Rational>());
-    }
-
-    Node possibleTaut = Node::null();
-    if(conditions.size() == 1){
-      possibleTaut = conditions.front();
-    }else{
-      NodeBuilder<> orBuilder(OR);
-      orBuilder.append(conditions);
-      possibleTaut = orBuilder;
-    }
-
-
-    Debug("arith::miplib") << "var: " << var << endl;
-    Debug("arith::miplib") << "possibleTaut: " << possibleTaut << endl;
-
-    Result isTaut = PropositionalQuery::isTautology(possibleTaut);
-    if(isTaut == Result(Result::VALID)){
-      Debug("arith::miplib") << var << " found a tautology!"<< endl;
-
-      set<Rational> values(valueCollection.begin(), valueCollection.end());
-      const Rational& min = *(values.begin());
-      const Rational& max = *(values.rbegin());
-
-      Debug("arith::miplib") << "min: " << min << endl;
-      Debug("arith::miplib") << "max: " << max << endl;
-
-      Assert(min <= max);
-      ++(d_statistics.d_miplibtrickApplications);
-      (d_statistics.d_avgNumMiplibtrickValues).addEntry(values.size());
-
-      Node nGeqMin = NodeBuilder<2>(GEQ) << var << mkRationalNode(min);
-      Node nLeqMax = NodeBuilder<2>(LEQ) << var << mkRationalNode(max);
-      Debug("arith::miplib") << nGeqMin << nLeqMax << endl;
-      learned << nGeqMin << nLeqMax;
-      set<Rational>::iterator valuesIter = values.begin();
-      set<Rational>::iterator valuesEnd = values.end();
-      set<Rational>::iterator valuesPrev = valuesIter;
-      ++valuesIter;
-      for(; valuesIter != valuesEnd; valuesPrev = valuesIter, ++valuesIter){
-        const Rational& prev = *valuesPrev;
-        const Rational& curr = *valuesIter;
-        Assert(prev < curr);
-
-        //The interval (last,curr) can be excluded:
-        //(not (and (> var prev) (< var curr))
-        //<=> (or (not (> var prev)) (not (< var curr)))
-        //<=> (or (<= var prev) (>= var curr))
-        Node leqPrev = NodeBuilder<2>(LEQ) << var << mkRationalNode(prev);
-        Node geqCurr = NodeBuilder<2>(GEQ) << var << mkRationalNode(curr);
-        Node excludedMiddle =  NodeBuilder<2>(OR) << leqPrev << geqCurr;
-        Debug("arith::miplib") << excludedMiddle << endl;
-        learned << excludedMiddle;
-      }
-    }
-  }
+  learner.staticLearning(n, learned);
 }
 
 
 
 ArithVar TheoryArith::findShortestBasicRow(ArithVar variable){
   ArithVar bestBasic = ARITHVAR_SENTINEL;
-  unsigned rowLength = 0;
+  uint64_t rowLength = std::numeric_limits<uint64_t>::max();
 
-  for(ArithVarSet::iterator basicIter = d_tableau.begin();
-      basicIter != d_tableau.end();
-      ++basicIter){
+  Column::iterator basicIter = d_tableau.beginColumn(variable);
+  Column::iterator end = d_tableau.endColumn(variable);
+  for(; basicIter != end; ++basicIter){
     ArithVar x_j = *basicIter;
     ReducedRowVector& row_j = d_tableau.lookup(x_j);
 
-    if(row_j.has(variable)){
-      if((bestBasic == ARITHVAR_SENTINEL) ||
-         (bestBasic != ARITHVAR_SENTINEL && row_j.size() < rowLength)){
-        bestBasic = x_j;
-        rowLength = row_j.size();
-      }
+    Assert(row_j.has(variable));
+    if((row_j.size() < rowLength) ||
+       (row_j.size() == rowLength && x_j < bestBasic)){
+      bestBasic = x_j;
+      rowLength = row_j.size();
     }
   }
   return bestBasic;
@@ -369,8 +164,6 @@ void TheoryArith::preRegisterTerm(TNode n) {
     setupInitialValue(varN);
   }
 
-
-  //TODO is an atom
   if(isRelationOperator(k)){
     Assert(Comparison::isNormalAtom(n));
 
@@ -402,7 +195,6 @@ ArithVar TheoryArith::requestArithVar(TNode x, bool basic){
 
   setArithVar(x,varX);
 
-  //d_basicManager.init(varX,basic);
   d_userVariables.init(varX, !basic);
   d_tableau.increaseSize();
 
@@ -458,7 +250,7 @@ void TheoryArith::setupSlack(TNode left){
 void TheoryArith::setupInitialValue(ArithVar x){
 
   if(!d_tableau.isBasic(x)){
-    d_partialModel.initialize(x,d_constants.d_ZERO_DELTA);
+    d_partialModel.initialize(x, d_DELTA_ZERO);
   }else{
     //If the variable is basic, assertions may have already happened and updates
     //may have occured before setting this variable up.
@@ -469,15 +261,6 @@ void TheoryArith::setupInitialValue(ArithVar x){
     DeltaRational assignment = d_simplex.computeRowValue(x, false);
     d_partialModel.initialize(x,safeAssignment);
     d_partialModel.setAssignment(x,assignment);
-
-
-    //d_simplex.checkBasicVariable(x);
-    //Conciously violating unneeded check
-
-    //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;
 };
@@ -525,6 +308,15 @@ DeltaRational determineRightConstant(TNode assertion, Kind simpleKind){
   return DeltaRational(noninf, inf);
 }
 
+void TheoryArith::disequalityConflict(TNode eq, TNode lb, TNode ub){
+
+  NodeBuilder<3> conflict(kind::AND);
+  conflict << eq << lb << ub;
+  ++(d_statistics.d_statDisequalityConflicts);
+  d_out->conflict((TNode)conflict);
+
+}
+
 bool TheoryArith::assertionCases(TNode assertion){
   Kind simpKind = simplifiedKind(assertion);
   Assert(simpKind != UNDEFINED_KIND);
@@ -539,10 +331,7 @@ bool TheoryArith::assertionCases(TNode assertion){
     if (d_partialModel.hasLowerBound(x_i) && d_partialModel.getLowerBound(x_i) == c_i) {
       Node diseq = assertion[0].eqNode(assertion[1]).notNode();
       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);
+        disequalityConflict(diseq, d_partialModel.getLowerConstraint(x_i) , assertion);
         return true;
       }
     }
@@ -552,10 +341,7 @@ bool TheoryArith::assertionCases(TNode assertion){
     if (d_partialModel.hasUpperBound(x_i) && d_partialModel.getUpperBound(x_i) == c_i) {
       Node diseq = assertion[0].eqNode(assertion[1]).notNode();
       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);
+        disequalityConflict(diseq, assertion, d_partialModel.getUpperConstraint(x_i));
         return true;
       }
     }
@@ -574,11 +360,14 @@ bool TheoryArith::assertionCases(TNode assertion){
       Assert(rhs.getKind() == CONST_RATIONAL);
       ArithVar lhsVar = determineLeftVariable(eq, kind::EQUAL);
       DeltaRational rhsValue = determineRightConstant(eq, kind::EQUAL);
-      if (d_partialModel.hasLowerBound(lhsVar) && d_partialModel.hasUpperBound(lhsVar) &&
-          d_partialModel.getLowerBound(lhsVar) == rhsValue && d_partialModel.getUpperBound(lhsVar) == rhsValue) {
-        NodeBuilder<3> conflict(kind::AND);
-        conflict << assertion << d_partialModel.getLowerConstraint(lhsVar) << d_partialModel.getUpperConstraint(lhsVar);
-        d_out->conflict((TNode)conflict);
+      if (d_partialModel.hasLowerBound(lhsVar) &&
+          d_partialModel.hasUpperBound(lhsVar) &&
+          d_partialModel.getLowerBound(lhsVar) == rhsValue &&
+          d_partialModel.getUpperBound(lhsVar) == rhsValue) {
+        Node lb = d_partialModel.getLowerConstraint(lhsVar);
+        Node ub = d_partialModel.getUpperConstraint(lhsVar);
+        disequalityConflict(assertion, lb, ub);
+        return true;
       }
     }
     return false;
@@ -588,14 +377,14 @@ bool TheoryArith::assertionCases(TNode assertion){
   }
 }
 
+
+
 void TheoryArith::check(Effort effortLevel){
   Debug("arith") << "TheoryArith::check begun" << std::endl;
 
   while(!done()){
 
     Node assertion = get();
-
-    //d_propagator.assertLiteral(assertion);
     bool conflictDuringAnAssert = assertionCases(assertion);
 
     if(conflictDuringAnAssert){
@@ -605,23 +394,7 @@ void TheoryArith::check(Effort effortLevel){
   }
 
   if(Debug.isOn("arith::print_assertions") && fullEffort(effortLevel)) {
-    Debug("arith::print_assertions") << "Assertions:" << endl;
-    for (ArithVar i = 0; i < d_variables.size(); ++ i) {
-      if (d_partialModel.hasLowerBound(i)) {
-        Node lConstr = d_partialModel.getLowerConstraint(i);
-        Debug("arith::print_assertions") << lConstr.toString() << endl;
-      }
-
-      if (d_partialModel.hasUpperBound(i)) {
-        Node uConstr = d_partialModel.getUpperConstraint(i);
-        Debug("arith::print_assertions") << uConstr.toString() << endl;
-      }
-    }
-    context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin();
-    context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end();
-    for(; it != it_end; ++ it) {
-      Debug("arith::print_assertions") << *it << endl;
-    }
+    debugPrintAssertions();
   }
 
   Node possibleConflict = d_simplex.updateInconsistentVars();
@@ -629,72 +402,92 @@ void TheoryArith::check(Effort effortLevel){
 
     d_partialModel.revertAssignmentChanges();
 
-    if(Debug.isOn("arith::print-conflict"))
-      Debug("arith_conflict") << (possibleConflict) << std::endl;
-
     d_out->conflict(possibleConflict);
-
-    Debug("arith_conflict") <<"Found a conflict "<< possibleConflict << endl;
   }else{
     d_partialModel.commitAssignmentChanges();
 
     if (fullEffort(effortLevel)) {
-      context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin();
-      context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end();
-      for(; it != it_end; ++ it) {
-        TNode eq = (*it)[0];
-        Assert(eq.getKind() == kind::EQUAL);
-        TNode lhs = eq[0];
-        TNode rhs = eq[1];
-        Assert(rhs.getKind() == CONST_RATIONAL);
-        ArithVar lhsVar = determineLeftVariable(eq, kind::EQUAL);
-        DeltaRational lhsValue = d_partialModel.getAssignment(lhsVar);
-        DeltaRational rhsValue = determineRightConstant(eq, kind::EQUAL);
-        if (lhsValue == rhsValue) {
-          Debug("arith_lemma") << "Splitting on " << eq << endl;
-          Debug("arith_lemma") << "LHS value = " << lhsValue << endl;
-          Debug("arith_lemma") << "RHS value = " << rhsValue << endl;
-          Node ltNode = NodeBuilder<2>(kind::LT) << lhs << rhs;
-          Node gtNode = NodeBuilder<2>(kind::GT) << lhs << rhs;
-          Node lemma = NodeBuilder<3>(OR) << eq << ltNode << gtNode;
-
-          // < => !>
-          Node imp1 = NodeBuilder<2>(kind::IMPLIES) << ltNode << gtNode.notNode();
-          // < => !=
-          Node imp2 = NodeBuilder<2>(kind::IMPLIES) << ltNode << eq.notNode();
-          // > => !=
-          Node imp3 = NodeBuilder<2>(kind::IMPLIES) << gtNode << eq.notNode();
-          // All the implication
-          Node impClosure = NodeBuilder<3>(kind::AND) << imp1 << imp2 << imp3;
-
-          ++(d_statistics.d_statDisequalitySplits);
-          d_out->lemma(lemma.andNode(impClosure));
-        }
-      }
+      splitDisequalities();
     }
   }
-  if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); }
 
+  if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); }
+  if(Debug.isOn("arith::print_model")) { debugPrintModel(); }
   Debug("arith") << "TheoryArith::check end" << std::endl;
+}
 
-  if(Debug.isOn("arith::print_model")) {
-    Debug("arith::print_model") << "Model:" << endl;
+void TheoryArith::splitDisequalities(){
+  context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin();
+  context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end();
+  for(; it != it_end; ++ it) {
+    TNode eq = (*it)[0];
+    Assert(eq.getKind() == kind::EQUAL);
+    TNode lhs = eq[0];
+    TNode rhs = eq[1];
+    Assert(rhs.getKind() == CONST_RATIONAL);
+    ArithVar lhsVar = determineLeftVariable(eq, kind::EQUAL);
+    DeltaRational lhsValue = d_partialModel.getAssignment(lhsVar);
+    DeltaRational rhsValue = determineRightConstant(eq, kind::EQUAL);
+    if (lhsValue == rhsValue) {
+      Debug("arith_lemma") << "Splitting on " << eq << endl;
+      Debug("arith_lemma") << "LHS value = " << lhsValue << endl;
+      Debug("arith_lemma") << "RHS value = " << rhsValue << endl;
+      Node ltNode = NodeBuilder<2>(kind::LT) << lhs << rhs;
+      Node gtNode = NodeBuilder<2>(kind::GT) << lhs << rhs;
+      Node lemma = NodeBuilder<3>(OR) << eq << ltNode << gtNode;
+
+      // // < => !>
+      // Node imp1 = NodeBuilder<2>(kind::IMPLIES) << ltNode << gtNode.notNode();
+      // // < => !=
+      // Node imp2 = NodeBuilder<2>(kind::IMPLIES) << ltNode << eq.notNode();
+      // // > => !=
+      // Node imp3 = NodeBuilder<2>(kind::IMPLIES) << gtNode << eq.notNode();
+      // // All the implication
+      // Node impClosure = NodeBuilder<3>(kind::AND) << imp1 << imp2 << imp3;
+
+      ++(d_statistics.d_statDisequalitySplits);
+      d_out->lemma(lemma);
+    }
+  }
+}
 
-    for (ArithVar i = 0; i < d_variables.size(); ++ i) {
-      Debug("arith::print_model") << d_variables[i] << " : " <<
-        d_partialModel.getAssignment(i);
-      if(d_tableau.isBasic(i))
-        Debug("arith::print_model") << " (basic)";
-      Debug("arith::print_model") << endl;
+/**
+ * Should be guarded by at least Debug.isOn("arith::print_assertions").
+ * Prints to Debug("arith::print_assertions")
+ */
+void TheoryArith::debugPrintAssertions() {
+  Debug("arith::print_assertions") << "Assertions:" << endl;
+  for (ArithVar i = 0; i < d_variables.size(); ++ i) {
+    if (d_partialModel.hasLowerBound(i)) {
+      Node lConstr = d_partialModel.getLowerConstraint(i);
+      Debug("arith::print_assertions") << lConstr.toString() << endl;
     }
+
+    if (d_partialModel.hasUpperBound(i)) {
+      Node uConstr = d_partialModel.getUpperConstraint(i);
+      Debug("arith::print_assertions") << uConstr.toString() << endl;
+    }
+  }
+  context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin();
+  context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end();
+  for(; it != it_end; ++ it) {
+    Debug("arith::print_assertions") << *it << endl;
+  }
+}
+
+void TheoryArith::debugPrintModel(){
+  Debug("arith::print_model") << "Model:" << endl;
+
+  for (ArithVar i = 0; i < d_variables.size(); ++ i) {
+    Debug("arith::print_model") << d_variables[i] << " : " <<
+      d_partialModel.getAssignment(i);
+    if(d_tableau.isBasic(i))
+      Debug("arith::print_model") << " (basic)";
+    Debug("arith::print_model") << endl;
   }
 }
 
 void TheoryArith::explain(TNode n) {
-  // Node explanation = d_propagator.explain(n);
-  // Debug("arith") << "arith::explain("<<explanation<<")->"
-  //                << explanation << endl;
-  // d_out->explanation(explanation, true);
 }
 
 void TheoryArith::propagate(Effort e) {
@@ -704,14 +497,6 @@ void TheoryArith::propagate(Effort e) {
       d_out->lemma(lemma);
     }
   }
-  // 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, Valuation* valuation) {
@@ -741,7 +526,7 @@ Node TheoryArith::getValue(TNode n, Valuation* valuation) {
       mkConst( valuation->getValue(n[0]) == valuation->getValue(n[1]) );
 
   case kind::PLUS: { // 2+ args
-    Rational value = d_constants.d_ZERO;
+    Rational value(0);
     for(TNode::iterator i = n.begin(),
             iend = n.end();
           i != iend;
@@ -752,7 +537,7 @@ Node TheoryArith::getValue(TNode n, Valuation* valuation) {
   }
 
   case kind::MULT: { // 2+ args
-    Rational value = d_constants.d_ONE;
+    Rational value(1);
     for(TNode::iterator i = n.begin(),
             iend = n.end();
           i != iend;
@@ -897,5 +682,7 @@ void TheoryArith::presolve(){
   static int callCount = 0;
   Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl;
 
+  learner.clear();
+
   check(FULL_EFFORT);
 }
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 1dcdceab0..ef93b7d64 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -35,6 +35,7 @@
 #include "theory/arith/partial_model.h"
 #include "theory/arith/unate_propagator.h"
 #include "theory/arith/simplex.h"
+#include "theory/arith/arith_static_learner.h"
 
 #include "util/stats.h"
 
@@ -54,26 +55,22 @@ namespace arith {
 class TheoryArith : public Theory {
 private:
 
-  /* TODO Everything in the chopping block needs to be killed. */
-  /* Chopping block begins */
-
-  std::vector<Node> d_splits;
-  //This stores the eager splits sent out of the theory.
-
-  /* Chopping block ends */
+  /** Static learner. */
+  ArithStaticLearner learner;
 
+  /**
+   * List of the variables in the system.
+   * This is needed to keep a positive ref count on slack variables.
+   */
   std::vector<Node> d_variables;
 
   /**
    * If ArithVar v maps to the node n in d_removednode,
    * then n = (= asNode(v) rhs) where rhs is a term that
-   * can be used to determine the value of n uysing getValue().
+   * can be used to determine the value of n using getValue().
    */
   std::map<ArithVar, Node> d_removedRows;
 
-  /** Stores system wide constants to avoid unnessecary reconstruction. */
-  ArithConstants d_constants;
-
   /**
    * Manages information about the assignment and upper and lower bounds on
    * variables.
@@ -178,9 +175,17 @@ public:
     d_simplex.notifyOptions(opt);
   }
 private:
+  /** The constant zero. */
+  DeltaRational d_DELTA_ZERO;
 
+  /**
+   * Using the simpleKind return the ArithVar associated with the
+   * left hand side of assertion.
+   */
   ArithVar determineLeftVariable(TNode assertion, Kind simpleKind);
 
+  /** Splits the disequalities in d_diseq that are violated using lemmas on demand. */
+  void splitDisequalities();
 
   /**
    * This requests a new unique ArithVar value for x.
@@ -203,6 +208,11 @@ private:
   bool assertionCases(TNode assertion);
 
   /**
+   * This is used for reporting conflicts caused by disequalities during assertionCases.
+   */
+  void disequalityConflict(TNode eq, TNode lb, TNode ub);
+
+  /**
    * Returns the basic variable with the shorted row containg a non-basic variable.
    * If no such row exists, return ARITHVAR_SENTINEL.
    */
@@ -225,6 +235,10 @@ private:
                  std::vector<Rational>& coeffs,
                  std::vector<ArithVar>& variables) const;
 
+  /** Routine for debugging. Print the assertions the theory is aware of. */
+  void debugPrintAssertions();
+  /** Debugging only routine. Prints the model. */
+  void debugPrintModel();
 
   /** These fields are designed to be accessable to TheoryArith methods. */
   class Statistics {
@@ -237,9 +251,6 @@ private:
     IntStat d_permanentlyRemovedVariables;
     TimerStat d_presolveTime;
 
-    IntStat d_miplibtrickApplications;
-    AverageStat d_avgNumMiplibtrickValues;
-
     BackedStat<double> d_initialTableauDensity;
     AverageStat d_avgTableauDensityAtRestart;
     IntStat d_tableauResets;