FCSimplex branch merge

1 files changed, 26 insertions, 2504 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index bc7b4b278..c0442da90 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file theory_arith.cpp
  ** \verbatim
- ** Original author: Tim King
+ ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds, Morgan Deters, Dejan Jovanovic
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Minor contributors (to current version): kshitij, ajreynol, mdeters, dejan
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -15,35 +15,8 @@
  ** \todo document this file
  **/
 
-#include "expr/node.h"
-#include "expr/kind.h"
-#include "expr/metakind.h"
-#include "expr/node_builder.h"
-
-#include "theory/valuation.h"
-#include "theory/rewriter.h"
-
-#include "util/rational.h"
-#include "util/integer.h"
-#include "util/boolean_simplification.h"
-#include "util/dense_map.h"
-
-#include "smt/logic_exception.h"
-
-#include "theory/arith/arith_utilities.h"
-#include "theory/arith/delta_rational.h"
-#include "theory/arith/partial_model.h"
-#include "theory/arith/matrix.h"
-
-#include "theory/arith/arith_rewriter.h"
-#include "theory/arith/constraint.h"
 #include "theory/arith/theory_arith.h"
-#include "theory/arith/normal_form.h"
-#include "theory/model.h"
-
-#include "theory/arith/options.h"
-
-#include <stdint.h>
+#include "theory/arith/theory_arith_private.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -52,2516 +25,65 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-const uint32_t RESET_START = 2;
-
-
-TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
-  Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe),
-  d_nlIncomplete( false),
-  d_qflraStatus(Result::SAT_UNKNOWN),
-  d_unknownsInARow(0),
-  d_hasDoneWorkSinceCut(false),
-  d_learner(u),
-  d_numberOfVariables(0),
-  d_pool(),
-  d_setupLiteralCallback(this),
-  d_assertionsThatDoNotMatchTheirLiterals(c),
-  d_nextIntegerCheckVar(0),
-  d_constantIntegerVariables(c),
-  d_diseqQueue(c, false),
-  d_currentPropagationList(),
-  d_learnedBounds(c),
-  d_partialModel(c, d_deltaComputeCallback),
-  d_tableau(),
-  d_linEq(d_partialModel, d_tableau, d_basicVarModelUpdateCallBack),
-  d_diosolver(c),
-  d_restartsCounter(0),
-  d_tableauSizeHasBeenModified(false),
-  d_tableauResetDensity(1.6),
-  d_tableauResetPeriod(10),
-  d_conflicts(c),
-  d_raiseConflict(d_conflicts),
-  d_tempVarMalloc(*this),
-  d_congruenceManager(c, d_constraintDatabase, d_setupLiteralCallback, d_arithvarNodeMap, d_raiseConflict),
-  d_simplex(d_linEq, d_raiseConflict),
-  d_constraintDatabase(c, u, d_arithvarNodeMap, d_congruenceManager, d_raiseConflict),
-  d_deltaComputeCallback(this),
-  d_basicVarModelUpdateCallBack(d_simplex),
-  d_DELTA_ZERO(0),
-  d_fullCheckCounter(0),
-  d_cutsInContext(c,0),
-  d_statistics()
-{
-}
-
-TheoryArith::~TheoryArith(){}
-
-void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  d_congruenceManager.setMasterEqualityEngine(eq);
-}
-
-Node skolemFunction(const std::string& name, TypeNode dom, TypeNode range){
-  NodeManager* currNM = NodeManager::currentNM();
-  TypeNode functionType = currNM->mkFunctionType(dom, range);
-  return currNM->mkSkolem(name, functionType);
-}
-
-Node TheoryArith::getRealDivideBy0Func(){
-  Assert(!getLogicInfo().isLinear());
-  Assert(getLogicInfo().areRealsUsed());
-
-  if(d_realDivideBy0Func.isNull()){
-    TypeNode realType = NodeManager::currentNM()->realType();
-    d_realDivideBy0Func = skolemFunction("/by0_$$", realType, realType);
-  }
-  return d_realDivideBy0Func;
-}
-
-Node TheoryArith::getIntDivideBy0Func(){
-  Assert(!getLogicInfo().isLinear());
-  Assert(getLogicInfo().areIntegersUsed());
-
-  if(d_intDivideBy0Func.isNull()){
-    TypeNode intType = NodeManager::currentNM()->integerType();
-    d_intDivideBy0Func = skolemFunction("divby0_$$", intType, intType);
-  }
-  return d_intDivideBy0Func;
-}
-
-Node TheoryArith::getIntModulusBy0Func(){
-  Assert(!getLogicInfo().isLinear());
-  Assert(getLogicInfo().areIntegersUsed());
-
-  if(d_intModulusBy0Func.isNull()){
-    TypeNode intType = NodeManager::currentNM()->integerType();
-    d_intModulusBy0Func = skolemFunction("modby0_$$", intType, intType);
-  }
-  return d_intModulusBy0Func;
-}
-
-TheoryArith::ModelException::ModelException(TNode n, const char* msg) throw (){
-  stringstream ss;
-  ss << "Cannot construct a model for " << n << " as " << endl << msg;
-  setMessage(ss.str());
-}
-TheoryArith::ModelException::~ModelException() throw (){ }
-
-
-TheoryArith::Statistics::Statistics():
-  d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0),
-  d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0),
-  d_statUserVariables("theory::arith::UserVariables", 0),
-  d_statSlackVariables("theory::arith::SlackVariables", 0),
-  d_statDisequalitySplits("theory::arith::DisequalitySplits", 0),
-  d_statDisequalityConflicts("theory::arith::DisequalityConflicts", 0),
-  d_simplifyTimer("theory::arith::simplifyTimer"),
-  d_staticLearningTimer("theory::arith::staticLearningTimer"),
-  d_presolveTime("theory::arith::presolveTime"),
-  d_newPropTime("theory::arith::newPropTimer"),
-  d_externalBranchAndBounds("theory::arith::externalBranchAndBounds",0),
-  d_initialTableauSize("theory::arith::initialTableauSize", 0),
-  d_currSetToSmaller("theory::arith::currSetToSmaller", 0),
-  d_smallerSetToCurr("theory::arith::smallerSetToCurr", 0),
-  d_restartTimer("theory::arith::restartTimer"),
-  d_boundComputationTime("theory::arith::bound::time"),
-  d_boundComputations("theory::arith::bound::boundComputations",0),
-  d_boundPropagations("theory::arith::bound::boundPropagations",0),
-  d_unknownChecks("theory::arith::status::unknowns", 0),
-  d_maxUnknownsInARow("theory::arith::status::maxUnknownsInARow", 0),
-  d_avgUnknownsInARow("theory::arith::status::avgUnknownsInARow"),
-  d_revertsOnConflicts("theory::arith::status::revertsOnConflicts",0),
-  d_commitsOnConflicts("theory::arith::status::commitsOnConflicts",0),
-  d_nontrivialSatChecks("theory::arith::status::nontrivialSatChecks",0)
-{
-  StatisticsRegistry::registerStat(&d_statAssertUpperConflicts);
-  StatisticsRegistry::registerStat(&d_statAssertLowerConflicts);
-
-  StatisticsRegistry::registerStat(&d_statUserVariables);
-  StatisticsRegistry::registerStat(&d_statSlackVariables);
-  StatisticsRegistry::registerStat(&d_statDisequalitySplits);
-  StatisticsRegistry::registerStat(&d_statDisequalityConflicts);
-  StatisticsRegistry::registerStat(&d_simplifyTimer);
-  StatisticsRegistry::registerStat(&d_staticLearningTimer);
-
-  StatisticsRegistry::registerStat(&d_presolveTime);
-  StatisticsRegistry::registerStat(&d_newPropTime);
-
-  StatisticsRegistry::registerStat(&d_externalBranchAndBounds);
-
-  StatisticsRegistry::registerStat(&d_initialTableauSize);
-  StatisticsRegistry::registerStat(&d_currSetToSmaller);
-  StatisticsRegistry::registerStat(&d_smallerSetToCurr);
-  StatisticsRegistry::registerStat(&d_restartTimer);
-
-  StatisticsRegistry::registerStat(&d_boundComputationTime);
-  StatisticsRegistry::registerStat(&d_boundComputations);
-  StatisticsRegistry::registerStat(&d_boundPropagations);
-
-  StatisticsRegistry::registerStat(&d_unknownChecks);
-  StatisticsRegistry::registerStat(&d_maxUnknownsInARow);
-  StatisticsRegistry::registerStat(&d_avgUnknownsInARow);
-  StatisticsRegistry::registerStat(&d_revertsOnConflicts);
-  StatisticsRegistry::registerStat(&d_commitsOnConflicts);
-  StatisticsRegistry::registerStat(&d_nontrivialSatChecks);
-}
-
-TheoryArith::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts);
-  StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts);
-
-  StatisticsRegistry::unregisterStat(&d_statUserVariables);
-  StatisticsRegistry::unregisterStat(&d_statSlackVariables);
-  StatisticsRegistry::unregisterStat(&d_statDisequalitySplits);
-  StatisticsRegistry::unregisterStat(&d_statDisequalityConflicts);
-  StatisticsRegistry::unregisterStat(&d_simplifyTimer);
-  StatisticsRegistry::unregisterStat(&d_staticLearningTimer);
-
-  StatisticsRegistry::unregisterStat(&d_presolveTime);
-  StatisticsRegistry::unregisterStat(&d_newPropTime);
-
-  StatisticsRegistry::unregisterStat(&d_externalBranchAndBounds);
-
-  StatisticsRegistry::unregisterStat(&d_initialTableauSize);
-  StatisticsRegistry::unregisterStat(&d_currSetToSmaller);
-  StatisticsRegistry::unregisterStat(&d_smallerSetToCurr);
-  StatisticsRegistry::unregisterStat(&d_restartTimer);
-
-  StatisticsRegistry::unregisterStat(&d_boundComputationTime);
-  StatisticsRegistry::unregisterStat(&d_boundComputations);
-  StatisticsRegistry::unregisterStat(&d_boundPropagations);
-
-  StatisticsRegistry::unregisterStat(&d_unknownChecks);
-  StatisticsRegistry::unregisterStat(&d_maxUnknownsInARow);
-  StatisticsRegistry::unregisterStat(&d_avgUnknownsInARow);
-  StatisticsRegistry::unregisterStat(&d_revertsOnConflicts);
-  StatisticsRegistry::unregisterStat(&d_commitsOnConflicts);
-  StatisticsRegistry::unregisterStat(&d_nontrivialSatChecks);
-}
-
-void TheoryArith::revertOutOfConflict(){
-  d_partialModel.revertAssignmentChanges();
-  clearUpdates();
-  d_currentPropagationList.clear();
-}
-
-void TheoryArith::clearUpdates(){
-  d_updatedBounds.purge();
-}
-
-void TheoryArith::zeroDifferenceDetected(ArithVar x){
-  Assert(d_congruenceManager.isWatchedVariable(x));
-  Assert(d_partialModel.upperBoundIsZero(x));
-  Assert(d_partialModel.lowerBoundIsZero(x));
-
-  Constraint lb = d_partialModel.getLowerBoundConstraint(x);
-  Constraint ub = d_partialModel.getUpperBoundConstraint(x);
-
-  if(lb->isEquality()){
-    d_congruenceManager.watchedVariableIsZero(lb);
-  }else if(ub->isEquality()){
-    d_congruenceManager.watchedVariableIsZero(ub);
-  }else{
-    d_congruenceManager.watchedVariableIsZero(lb, ub);
-  }
-}
-
-/* procedure AssertLower( x_i >= c_i ) */
-bool TheoryArith::AssertLower(Constraint constraint){
-  Assert(constraint != NullConstraint);
-  Assert(constraint->isLowerBound());
-
-  ArithVar x_i = constraint->getVariable();
-  const DeltaRational& c_i = constraint->getValue();
-
-  Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
-
-  Assert(!isInteger(x_i) || c_i.isIntegral());
+TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe)
+  : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe)
+  , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, qe))
+{}
 
-  //TODO Relax to less than?
-  if(d_partialModel.lessThanLowerBound(x_i, c_i)){
-    return false; //sat
-  }
-
-  int cmpToUB = d_partialModel.cmpToUpperBound(x_i, c_i);
-  if(cmpToUB > 0){ //  c_i < \lowerbound(x_i)
-    Constraint ubc = d_partialModel.getUpperBoundConstraint(x_i);
-    Node conflict = ConstraintValue::explainConflict(ubc, constraint);
-    Debug("arith") << "AssertLower conflict " << conflict << endl;
-    ++(d_statistics.d_statAssertLowerConflicts);
-    d_raiseConflict(conflict);
-    return true;
-  }else if(cmpToUB == 0){
-    if(isInteger(x_i)){
-      d_constantIntegerVariables.push_back(x_i);
-      Debug("dio::push") << x_i << endl;
-    }
-    Constraint ub = d_partialModel.getUpperBoundConstraint(x_i);
-
-    if(!d_congruenceManager.isWatchedVariable(x_i) || c_i.sgn() != 0){
-      // if it is not a watched variable report it
-      // if it is is a watched variable and c_i == 0,
-      // let zeroDifferenceDetected(x_i) catch this
-      d_congruenceManager.equalsConstant(constraint, ub);
-    }
-
-    const ValueCollection& vc = constraint->getValueCollection();
-    if(vc.hasDisequality()){
-      Assert(vc.hasEquality());
-      const Constraint eq = vc.getEquality();
-      const Constraint diseq = vc.getDisequality();
-      if(diseq->isTrue()){
-        //const Constraint ub = vc.getUpperBound();
-        Node conflict = ConstraintValue::explainConflict(diseq, ub, constraint);
-
-        ++(d_statistics.d_statDisequalityConflicts);
-        Debug("eq") << " assert lower conflict " << conflict << endl;
-        d_raiseConflict(conflict);
-        return true;
-      }else if(!eq->isTrue()){
-        Debug("eq") << "lb == ub, propagate eq" << eq << endl;
-        eq->impliedBy(constraint, d_partialModel.getUpperBoundConstraint(x_i));
-        // do not need to add to d_learnedBounds
-      }
-    }
-  }else{
-    Assert(cmpToUB < 0);
-    const ValueCollection& vc = constraint->getValueCollection();
-
-    if(vc.hasDisequality()){
-      const Constraint diseq = vc.getDisequality();
-      if(diseq->isTrue()){
-        const Constraint ub = d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), UpperBound);
-
-        if(ub->hasProof()){
-          Node conflict = ConstraintValue::explainConflict(diseq, ub, constraint);
-          Debug("eq") << " assert upper conflict " << conflict << endl;
-          d_raiseConflict(conflict);
-          return true;
-        }else if(!ub->negationHasProof()){
-          Constraint negUb = ub->getNegation();
-          negUb->impliedBy(constraint, diseq);
-          d_learnedBounds.push_back(negUb);
-        }
-      }
-    }
-  }
-
-  d_currentPropagationList.push_back(constraint);
-  d_currentPropagationList.push_back(d_partialModel.getLowerBoundConstraint(x_i));
-
-  d_partialModel.setLowerBoundConstraint(constraint);
-
-  if(d_congruenceManager.isWatchedVariable(x_i)){
-    int sgn = c_i.sgn();
-    if(sgn > 0){
-      d_congruenceManager.watchedVariableCannotBeZero(constraint);
-    }else if(sgn == 0 && d_partialModel.upperBoundIsZero(x_i)){
-      zeroDifferenceDetected(x_i);
-    }
-  }
-
-  d_updatedBounds.softAdd(x_i);
-
-  if(Debug.isOn("model")) {
-    Debug("model") << "before" << endl;
-    d_partialModel.printModel(x_i);
-    d_tableau.debugPrintIsBasic(x_i);
-  }
-
-  if(!d_tableau.isBasic(x_i)){
-    if(d_partialModel.getAssignment(x_i) < c_i){
-      d_linEq.update(x_i, c_i);
-    }
-  }else{
-    d_simplex.updateBasic(x_i);
-  }
-
-  if(Debug.isOn("model")) {
-    Debug("model") << "after" << endl;
-    d_partialModel.printModel(x_i);
-    d_tableau.debugPrintIsBasic(x_i);
- }
-
-  return false; //sat
-}
-
-/* procedure AssertUpper( x_i <= c_i) */
-bool TheoryArith::AssertUpper(Constraint constraint){
-  ArithVar x_i = constraint->getVariable();
-  const DeltaRational& c_i = constraint->getValue();
-
-  Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
-  AssertArgument(constraint != NullConstraint,
-                 "AssertUpper() called on a NullConstraint.");
-  Assert(constraint->isUpperBound());
-
-  //Too strong because of rounding with integers
-  //Assert(!constraint->hasLiteral() || original == constraint->getLiteral());
-  Assert(!isInteger(x_i) || c_i.isIntegral());
-
-  Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
-
-  if(d_partialModel.greaterThanUpperBound(x_i, c_i) ){ // \upperbound(x_i) <= c_i
-    return false; //sat
-  }
-
-  // cmpToLb =  \lowerbound(x_i).cmp(c_i)
-  int cmpToLB = d_partialModel.cmpToLowerBound(x_i, c_i);
-  if( cmpToLB < 0 ){ //  \upperbound(x_i) < \lowerbound(x_i)
-    Constraint lbc = d_partialModel.getLowerBoundConstraint(x_i);
-    Node conflict =  ConstraintValue::explainConflict(lbc, constraint);
-    Debug("arith") << "AssertUpper conflict " << conflict << endl;
-    ++(d_statistics.d_statAssertUpperConflicts);
-    d_raiseConflict(conflict);
-    return true;
-  }else if(cmpToLB == 0){ // \lowerBound(x_i) == \upperbound(x_i)
-    if(isInteger(x_i)){
-      d_constantIntegerVariables.push_back(x_i);
-      Debug("dio::push") << x_i << endl;
-    }
-    Constraint lb = d_partialModel.getLowerBoundConstraint(x_i);
-    if(!d_congruenceManager.isWatchedVariable(x_i) || c_i.sgn() != 0){
-      // if it is not a watched variable report it
-      // if it is is a watched variable and c_i == 0,
-      // let zeroDifferenceDetected(x_i) catch this
-      d_congruenceManager.equalsConstant(lb, constraint);
-    }
-
-    const ValueCollection& vc = constraint->getValueCollection();
-    if(vc.hasDisequality()){
-      Assert(vc.hasEquality());
-      const Constraint diseq = vc.getDisequality();
-      const Constraint eq = vc.getEquality();
-      if(diseq->isTrue()){
-        Node conflict = ConstraintValue::explainConflict(diseq, lb, constraint);
-        Debug("eq") << " assert upper conflict " << conflict << endl;
-        d_raiseConflict(conflict);
-        return true;
-      }else if(!eq->isTrue()){
-        Debug("eq") << "lb == ub, propagate eq" << eq << endl;
-        eq->impliedBy(constraint, d_partialModel.getLowerBoundConstraint(x_i));
-        //do not bother to add to d_learnedBounds
-      }
-    }
-  }else if(cmpToLB > 0){
-    const ValueCollection& vc = constraint->getValueCollection();
-    if(vc.hasDisequality()){
-      const Constraint diseq = vc.getDisequality();
-      if(diseq->isTrue()){
-        const Constraint lb =
-          d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), LowerBound);
-        if(lb->hasProof()){
-          Node conflict = ConstraintValue::explainConflict(diseq, lb, constraint);
-          Debug("eq") << " assert upper conflict " << conflict << endl;
-          d_raiseConflict(conflict);
-          return true;
-        }else if(!lb->negationHasProof()){
-          Constraint negLb = lb->getNegation();
-          negLb->impliedBy(constraint, diseq);
-          //if(!negLb->canBePropagated()){
-          d_learnedBounds.push_back(negLb);
-          //}//otherwise let this be propagated/asserted later
-        }
-      }
-    }
-  }
-
-  d_currentPropagationList.push_back(constraint);
-  d_currentPropagationList.push_back(d_partialModel.getUpperBoundConstraint(x_i));
-  //It is fine if this is NullConstraint
-
-  d_partialModel.setUpperBoundConstraint(constraint);
-
-  if(d_congruenceManager.isWatchedVariable(x_i)){
-    int sgn = c_i.sgn();
-     if(sgn < 0){
-       d_congruenceManager.watchedVariableCannotBeZero(constraint);
-     }else if(sgn == 0 && d_partialModel.lowerBoundIsZero(x_i)){
-       zeroDifferenceDetected(x_i);
-     }
-  }
-
-  d_updatedBounds.softAdd(x_i);
-
-  if(Debug.isOn("model")) {
-    Debug("model") << "before" << endl;
-    d_partialModel.printModel(x_i);
-    d_tableau.debugPrintIsBasic(x_i);
-  }
-
-  if(!d_tableau.isBasic(x_i)){
-    if(d_partialModel.getAssignment(x_i) > c_i){
-      d_linEq.update(x_i, c_i);
-    }
-  }else{
-    d_simplex.updateBasic(x_i);
-  }
-
-  if(Debug.isOn("model")) {
-    Debug("model") << "after" << endl;
-    d_partialModel.printModel(x_i);
-    d_tableau.debugPrintIsBasic(x_i);
-  }
-
-  return false; //sat
+TheoryArith::~TheoryArith(){
+  delete d_internal;
 }
 
-
-/* procedure AssertEquality( x_i == c_i ) */
-bool TheoryArith::AssertEquality(Constraint constraint){
-  AssertArgument(constraint != NullConstraint,
-                 "AssertUpper() called on a NullConstraint.");
-
-  ArithVar x_i = constraint->getVariable();
-  const DeltaRational& c_i = constraint->getValue();
-
-  Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl;
-
-  //Should be fine in integers
-  Assert(!isInteger(x_i) || c_i.isIntegral());
-
-  int cmpToLB = d_partialModel.cmpToLowerBound(x_i, c_i);
-  int cmpToUB = d_partialModel.cmpToUpperBound(x_i, c_i);
-
-  // u_i <= c_i <= l_i
-  // This can happen if both c_i <= x_i and x_i <= c_i are in the system.
-  if(cmpToUB >= 0 && cmpToLB <= 0){
-    return false; //sat
-  }
-
-  if(cmpToUB > 0){
-    Constraint ubc = d_partialModel.getUpperBoundConstraint(x_i);
-    Node conflict = ConstraintValue::explainConflict(ubc, constraint);
-    Debug("arith") << "AssertEquality conflicts with upper bound " << conflict << endl;
-    d_raiseConflict(conflict);
-    return true;
-  }
-
-  if(cmpToLB < 0){
-    Constraint lbc = d_partialModel.getLowerBoundConstraint(x_i);
-    Node conflict = ConstraintValue::explainConflict(lbc, constraint);
-    Debug("arith") << "AssertEquality conflicts with lower bound" << conflict << endl;
-    d_raiseConflict(conflict);
-    return true;
-  }
-
-  Assert(cmpToUB <= 0);
-  Assert(cmpToLB >= 0);
-  Assert(cmpToUB < 0 || cmpToLB > 0);
-
-
-  if(isInteger(x_i)){
-    d_constantIntegerVariables.push_back(x_i);
-    Debug("dio::push") << x_i << endl;
-  }
-
-  // Don't bother to check whether x_i != c_i is in d_diseq
-  // The a and (not a) should never be on the fact queue
-  d_currentPropagationList.push_back(constraint);
-  d_currentPropagationList.push_back(d_partialModel.getLowerBoundConstraint(x_i));
-  d_currentPropagationList.push_back(d_partialModel.getUpperBoundConstraint(x_i));
-
-  d_partialModel.setUpperBoundConstraint(constraint);
-  d_partialModel.setLowerBoundConstraint(constraint);
-
-  if(d_congruenceManager.isWatchedVariable(x_i)){
-    int sgn = c_i.sgn();
-    if(sgn == 0){
-      zeroDifferenceDetected(x_i);
-    }else{
-      d_congruenceManager.watchedVariableCannotBeZero(constraint);
-      d_congruenceManager.equalsConstant(constraint);
-    }
-  }else{
-    d_congruenceManager.equalsConstant(constraint);
-  }
-
-  d_updatedBounds.softAdd(x_i);
-
-  if(Debug.isOn("model")) {
-    Debug("model") << "before" << endl;
-    d_partialModel.printModel(x_i);
-    d_tableau.debugPrintIsBasic(x_i);
-  }
-
-  if(!d_tableau.isBasic(x_i)){
-    if(!(d_partialModel.getAssignment(x_i) == c_i)){
-      d_linEq.update(x_i, c_i);
-    }
-  }else{
-    d_simplex.updateBasic(x_i);
-  }
-
-  if(Debug.isOn("model")) {
-    Debug("model") << "after" << endl;
-    d_partialModel.printModel(x_i);
-    d_tableau.debugPrintIsBasic(x_i);
-  }
-
-  return false;
+void TheoryArith::preRegisterTerm(TNode n){
+  d_internal->preRegisterTerm(n);
 }
 
-
-/* procedure AssertDisequality( x_i != c_i ) */
-bool TheoryArith::AssertDisequality(Constraint constraint){
-
-  AssertArgument(constraint != NullConstraint,
-                 "AssertUpper() called on a NullConstraint.");
-  ArithVar x_i = constraint->getVariable();
-  const DeltaRational& c_i = constraint->getValue();
-
-  Debug("arith") << "AssertDisequality(" << x_i << " " << c_i << ")"<< std::endl;
-
-  //Should be fine in integers
-  Assert(!isInteger(x_i) || c_i.isIntegral());
-
-  if(d_congruenceManager.isWatchedVariable(x_i)){
-    int sgn = c_i.sgn();
-    if(sgn == 0){
-      d_congruenceManager.watchedVariableCannotBeZero(constraint);
-    }
-  }
-
-  const ValueCollection& vc = constraint->getValueCollection();
-  if(vc.hasLowerBound() && vc.hasUpperBound()){
-    const Constraint lb = vc.getLowerBound();
-    const Constraint ub = vc.getUpperBound();
-    if(lb->isTrue() && ub->isTrue()){
-      //in conflict
-      Debug("eq") << "explaining" << endl;
-      ++(d_statistics.d_statDisequalityConflicts);
-      Node conflict = ConstraintValue::explainConflict(constraint, lb, ub);
-      d_raiseConflict(conflict);
-      return true;
-    }
-  }
-  if(vc.hasLowerBound() ){
-    const Constraint lb = vc.getLowerBound();
-    if(lb->isTrue()){
-      const Constraint ub = d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), UpperBound);
-      Debug("eq") << "propagate UpperBound " << constraint << lb << ub << endl;
-      const Constraint negUb = ub->getNegation();
-      if(!negUb->isTrue()){
-        negUb->impliedBy(constraint, lb);
-        d_learnedBounds.push_back(negUb);
-      }
-    }
-  }
-  if(vc.hasUpperBound()){
-    const Constraint ub = vc.getUpperBound();
-    if(ub->isTrue()){
-      const Constraint lb = d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), LowerBound);
-
-      Debug("eq") << "propagate LowerBound " << constraint << lb << ub << endl;
-      const Constraint negLb = lb->getNegation();
-      if(!negLb->isTrue()){
-        negLb->impliedBy(constraint, ub);
-        d_learnedBounds.push_back(negLb);
-      }
-    }
-  }
-
-  bool split = constraint->isSplit();
-
-  if(!split && c_i == d_partialModel.getAssignment(x_i)){
-    Debug("eq") << "lemma now! " << constraint << endl;
-    d_out->lemma(constraint->split());
-    return false;
-  }else if(d_partialModel.strictlyLessThanLowerBound(x_i, c_i)){
-    Debug("eq") << "can drop as less than lb" << constraint << endl;
-  }else if(d_partialModel.strictlyGreaterThanUpperBound(x_i, c_i)){
-    Debug("eq") << "can drop as less than ub" << constraint << endl;
-  }else if(!split){
-    Debug("eq") << "push back" << constraint << endl;
-    d_diseqQueue.push(constraint);
-    d_partialModel.invalidateDelta();
-  }else{
-    Debug("eq") << "skipping already split " << constraint << endl;
-  }
-  return false;
+void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_internal->setMasterEqualityEngine(eq);
 }
 
 void TheoryArith::addSharedTerm(TNode n){
-  Debug("arith::addSharedTerm") << "addSharedTerm: " << n << endl;
-  if(n.isConst()){
-    d_partialModel.invalidateDelta();
-  }
-
-  d_congruenceManager.addSharedTerm(n);
-  if(!n.isConst() && !isSetup(n)){
-    Polynomial poly = Polynomial::parsePolynomial(n);
-    Polynomial::iterator it = poly.begin();
-    Polynomial::iterator it_end = poly.end();
-    for (; it != it_end; ++ it) {
-      Monomial m = *it;
-      if (!m.isConstant() && !isSetup(m.getVarList().getNode())) {
-        setupVariableList(m.getVarList());
-      }
-    }
-  }
+  d_internal->addSharedTerm(n);
 }
 
 Node TheoryArith::ppRewrite(TNode atom) {
-  Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
-
-
-  if (atom.getKind() == kind::EQUAL  && options::arithRewriteEq()) {
-    Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
-    Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
-    Node rewritten = Rewriter::rewrite(leq.andNode(geq));
-    Debug("arith::preprocess") << "arith::preprocess() : returning "
-                               << rewritten << endl;
-    return rewritten;
-  } else {
-    return atom;
-  }
+  return d_internal->ppRewrite(atom);
 }
 
 Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
-  TimerStat::CodeTimer codeTimer(d_statistics.d_simplifyTimer);
-  Debug("simplify") << "TheoryArith::solve(" << in << ")" << endl;
-
-
-  // Solve equalities
-  Rational minConstant = 0;
-  Node minMonomial;
-  Node minVar;
-  if (in.getKind() == kind::EQUAL) {
-    Comparison cmp = Comparison::parseNormalForm(in);
-
-    Polynomial left = cmp.getLeft();
-    Polynomial right = cmp.getRight();
-
-    Monomial m = left.getHead();
-    if (m.getVarList().singleton()){
-      VarList vl = m.getVarList();
-      Node var = vl.getNode();
-      if (var.getKind() == kind::VARIABLE){
-        // if vl.isIntegral then m.getConstant().isOne()
-        if(!vl.isIntegral() || m.getConstant().isOne()){
-          minVar = var;
-        }
-      }
-    }
-
-    // Solve for variable
-    if (!minVar.isNull()) {
-      Polynomial right = cmp.getRight();
-      Node elim = right.getNode();
-      // ax + p = c -> (ax + p) -ax - c = -ax
-      // x = (p - ax - c) * -1/a
-      // Add the substitution if not recursive
-      Assert(elim == Rewriter::rewrite(elim));
-
-
-      static const unsigned MAX_SUB_SIZE = 2;
-      if(right.size() > MAX_SUB_SIZE){
-        Debug("simplify") << "TheoryArith::solve(): did not substitute due to the right hand side containing too many terms: " << minVar << ":" << elim << endl;
-        Debug("simplify") << right.size() << endl;
-      }else if(elim.hasSubterm(minVar)){
-        Debug("simplify") << "TheoryArith::solve(): can't substitute due to recursive pattern with sharing: " << minVar << ":" << elim << endl;
-      }else if (!minVar.getType().isInteger() || right.isIntegral()) {
-        Assert(!elim.hasSubterm(minVar));
-        // cannot eliminate integers here unless we know the resulting
-        // substitution is integral
-        Debug("simplify") << "TheoryArith::solve(): substitution " << minVar << " |-> " << elim << endl;
-
-        outSubstitutions.addSubstitution(minVar, elim);
-        return PP_ASSERT_STATUS_SOLVED;
-      } else {
-        Debug("simplify") << "TheoryArith::solve(): can't substitute b/c it's integer: " << minVar << ":" << minVar.getType() << " |-> " << elim << ":" << elim.getType() << endl;
-      }
-    }
-  }
-
-  // If a relation, remember the bound
-  switch(in.getKind()) {
-  case kind::LEQ:
-  case kind::LT:
-  case kind::GEQ:
-  case kind::GT:
-    if (in[0].isVar()) {
-      d_learner.addBound(in);
-    }
-    break;
-  default:
-    // Do nothing
-    break;
-  }
-
-  return PP_ASSERT_STATUS_UNSOLVED;
+  return d_internal->ppAssert(in, outSubstitutions);
 }
 
 void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
-  TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer);
-
-  d_learner.staticLearning(n, learned);
-}
-
-
-
-ArithVar TheoryArith::findShortestBasicRow(ArithVar variable){
-  ArithVar bestBasic = ARITHVAR_SENTINEL;
-  uint64_t bestRowLength = std::numeric_limits<uint64_t>::max();
-
-  Tableau::ColIterator basicIter = d_tableau.colIterator(variable);
-  for(; !basicIter.atEnd(); ++basicIter){
-    const Tableau::Entry& entry = *basicIter;
-    Assert(entry.getColVar() == variable);
-    RowIndex ridx = entry.getRowIndex();
-    ArithVar basic = d_tableau.rowIndexToBasic(ridx);
-    uint32_t rowLength = d_tableau.getRowLength(ridx);
-    if((rowLength < bestRowLength) ||
-       (rowLength == bestRowLength && basic < bestBasic)){
-      bestBasic = basic;
-      bestRowLength = rowLength;
-    }
-  }
-  Assert(bestBasic == ARITHVAR_SENTINEL || bestRowLength < std::numeric_limits<uint32_t>::max());
-  return bestBasic;
-}
-
-void TheoryArith::setupVariable(const Variable& x){
-  Node n = x.getNode();
-
-  Assert(!isSetup(n));
-
-  ++(d_statistics.d_statUserVariables);
-  requestArithVar(n,false);
-  //ArithVar varN = requestArithVar(n,false);
-  //setupInitialValue(varN);
-
-  markSetup(n);
-
-
-  if(x.isDivLike()){
-    setupDivLike(x);
-  }
-
-}
-
-void TheoryArith::setupVariableList(const VarList& vl){
-  Assert(!vl.empty());
-
-  TNode vlNode = vl.getNode();
-  Assert(!isSetup(vlNode));
-  Assert(!d_arithvarNodeMap.hasArithVar(vlNode));
-
-  for(VarList::iterator i = vl.begin(), end = vl.end(); i != end; ++i){
-    Variable var = *i;
-
-    if(!isSetup(var.getNode())){
-      setupVariable(var);
-    }
-  }
-
-  if(!vl.singleton()){
-    // vl is the product of at least 2 variables
-    // vl : (* v1 v2 ...)
-    if(getLogicInfo().isLinear()){
-      throw LogicException("Non-linear term was asserted to arithmetic in a linear logic.");
-    }
-
-    d_out->setIncomplete();
-    d_nlIncomplete = true;
-
-    ++(d_statistics.d_statUserVariables);
-    requestArithVar(vlNode, false);
-    //ArithVar av = requestArithVar(vlNode, false);
-    //setupInitialValue(av);
-
-    markSetup(vlNode);
-  }
-
-  /* Note:
-   * Only call markSetup if the VarList is not a singleton.
-   * See the comment in setupPolynomail for more.
-   */
-}
-
-void TheoryArith::cautiousSetupPolynomial(const Polynomial& p){
-  if(p.containsConstant()){
-    if(!p.isConstant()){
-      Polynomial noConstant = p.getTail();
-      if(!isSetup(noConstant.getNode())){
-        setupPolynomial(noConstant);
-      }
-    }
-  }else if(!isSetup(p.getNode())){
-    setupPolynomial(p);
-  }
-}
-
-void TheoryArith::setupDivLike(const Variable& v){
-  Assert(v.isDivLike());
-
-  if(getLogicInfo().isLinear()){
-    throw LogicException("Non-linear term was asserted to arithmetic in a linear logic.");
-  }
-
-  Node vnode = v.getNode();
-  Assert(isSetup(vnode)); // Otherwise there is some invariant breaking recursion
-  Polynomial m = Polynomial::parsePolynomial(vnode[0]);
-  Polynomial n = Polynomial::parsePolynomial(vnode[1]);
-
-  cautiousSetupPolynomial(m);
-  cautiousSetupPolynomial(n);
-
-  Node lem;
-  switch(vnode.getKind()){
-  case DIVISION:
-  case INTS_DIVISION:
-  case INTS_MODULUS:
-    lem = definingIteForDivLike(vnode);
-    break;
-  case DIVISION_TOTAL:
-    lem = axiomIteForTotalDivision(vnode);
-    break;
-  case INTS_DIVISION_TOTAL:
-  case INTS_MODULUS_TOTAL:
-    lem = axiomIteForTotalIntDivision(vnode);
-    break;
-  default:
-    /* intentionally blank */
-    break;
-  }
-
-  if(!lem.isNull()){
-    Debug("arith::div") << lem << endl;
-    d_out->lemma(lem);
-  }
-}
-
-Node TheoryArith::definingIteForDivLike(Node divLike){
-  Kind k = divLike.getKind();
-  Assert(k == DIVISION || k == INTS_DIVISION || k == INTS_MODULUS);
-  // (for all ((n Real) (d Real))
-  //  (=
-  //   (DIVISION n d)
-  //   (ite (= d 0)
-  //    (APPLY [div_0_skolem_function] n)
-  //    (DIVISION_TOTAL x y))))
-
-  Polynomial n = Polynomial::parsePolynomial(divLike[0]);
-  Polynomial d = Polynomial::parsePolynomial(divLike[1]);
-
-  NodeManager* currNM = NodeManager::currentNM();
-  Node dEq0 = currNM->mkNode(EQUAL, d.getNode(), mkRationalNode(0));
-
-  Kind kTotal = (k == DIVISION) ? DIVISION_TOTAL :
-    (k == INTS_DIVISION) ? INTS_DIVISION_TOTAL : INTS_MODULUS_TOTAL;
-
-  Node by0Func = (k == DIVISION) ?  getRealDivideBy0Func():
-    (k == INTS_DIVISION) ? getIntDivideBy0Func() : getIntModulusBy0Func();
-
-
-  Debug("arith::div") << divLike << endl;
-  Debug("arith::div") << by0Func << endl;
-
-  Node divTotal = currNM->mkNode(kTotal, n.getNode(), d.getNode());
-  Node divZero = currNM->mkNode(APPLY_UF, by0Func, n.getNode());
-
-  Node defining = divLike.eqNode(dEq0.iteNode( divZero, divTotal));
-
-  return defining;
-}
-
-Node TheoryArith::axiomIteForTotalDivision(Node div_tot){
-  Assert(div_tot.getKind() == DIVISION_TOTAL);
-
-  // Inverse of multiplication axiom:
-  //   (for all ((n Real) (d Real))
-  //    (ite (= d 0)
-  //     (= (DIVISION_TOTAL n d) 0)
-  //     (= (* d (DIVISION_TOTAL n d)) n)))
-
-
-  Polynomial n = Polynomial::parsePolynomial(div_tot[0]);
-  Polynomial d = Polynomial::parsePolynomial(div_tot[1]);
-  Polynomial div_tot_p = Polynomial::parsePolynomial(div_tot);
-
-  Comparison invEq = Comparison::mkComparison(EQUAL, n, d * div_tot_p);
-  Comparison zeroEq = Comparison::mkComparison(EQUAL, div_tot_p, Polynomial::mkZero());
-  Node dEq0 = (d.getNode()).eqNode(mkRationalNode(0));
-  Node ite = dEq0.iteNode(zeroEq.getNode(), invEq.getNode());
-
-  return ite;
-}
-
-Node TheoryArith::axiomIteForTotalIntDivision(Node int_div_like){
-  Kind k = int_div_like.getKind();
-  Assert(k == INTS_DIVISION_TOTAL || k == INTS_MODULUS_TOTAL);
-
-  // (for all ((m Int) (n Int))
-  //   (=> (distinct n 0)
-  //       (let ((q (div m n)) (r (mod m n)))
-  //         (and (= m (+ (* n q) r))
-  //              (<= 0 r (- (abs n) 1))))))
-
-  // Updated for div 0 functions
-  // (for all ((m Int) (n Int))
-  //   (let ((q (div m n)) (r (mod m n)))
-  //     (ite (= n 0)
-  //          (and (= q (div_0_func m)) (= r (mod_0_func m)))
-  //          (and (= m (+ (* n q) r))
-  //               (<= 0 r (- (abs n) 1)))))))
-
-  Polynomial n = Polynomial::parsePolynomial(int_div_like[0]);
-  Polynomial d = Polynomial::parsePolynomial(int_div_like[1]);
-
-  NodeManager* currNM = NodeManager::currentNM();
-  Node zero = mkRationalNode(0);
-
-  Node q = (k == INTS_DIVISION_TOTAL) ? int_div_like : currNM->mkNode(INTS_DIVISION_TOTAL, n.getNode(), d.getNode());
-  Node r = (k == INTS_MODULUS_TOTAL) ? int_div_like : currNM->mkNode(INTS_MODULUS_TOTAL, n.getNode(), d.getNode());
-
-  Node dEq0 = (d.getNode()).eqNode(zero);
-  Node qEq0 = q.eqNode(zero);
-  Node rEq0 = r.eqNode(zero);
-
-  Polynomial rp = Polynomial::parsePolynomial(r);
-  Polynomial qp = Polynomial::parsePolynomial(q);
-
-  Node abs_d = (n.isConstant()) ?
-    d.getHead().getConstant().abs().getNode() : mkIntSkolem("abs_$$");
-
-  Node eq = Comparison::mkComparison(EQUAL, n, d * qp + rp).getNode();
-  Node leq0 = currNM->mkNode(LEQ, zero, r);
-  Node leq1 = currNM->mkNode(LT, r, abs_d);
-
-  Node andE = currNM->mkNode(AND, eq, leq0, leq1);
-  Node defDivMode = dEq0.iteNode(qEq0.andNode(rEq0), andE);
-  Node lem = abs_d.getMetaKind () == metakind::VARIABLE ?
-    defDivMode.andNode(d.makeAbsCondition(Variable(abs_d))) : defDivMode;
-
-  return lem;
-}
-
-
-void TheoryArith::setupPolynomial(const Polynomial& poly) {
-  Assert(!poly.containsConstant());
-  TNode polyNode = poly.getNode();
-  Assert(!isSetup(polyNode));
-  Assert(!d_arithvarNodeMap.hasArithVar(polyNode));
-
-  for(Polynomial::iterator i = poly.begin(), end = poly.end(); i != end; ++i){
-    Monomial mono = *i;
-    const VarList& vl = mono.getVarList();
-    if(!isSetup(vl.getNode())){
-      setupVariableList(vl);
-    }
-  }
-
-  if(polyNode.getKind() == PLUS){
-    d_tableauSizeHasBeenModified = true;
-
-    vector<ArithVar> variables;
-    vector<Rational> coefficients;
-    asVectors(poly, coefficients, variables);
-
-    ArithVar varSlack = requestArithVar(polyNode, true);
-    d_tableau.addRow(varSlack, coefficients, variables);
-    setupBasicValue(varSlack);
-
-    //Add differences to the difference manager
-    Polynomial::iterator i = poly.begin(), end = poly.end();
-    if(i != end){
-      Monomial first = *i;
-      ++i;
-      if(i != end){
-        Monomial second = *i;
-        ++i;
-        if(i == end){
-          if(first.getConstant().isOne() && second.getConstant().getValue() == -1){
-            VarList vl0 = first.getVarList();
-            VarList vl1 = second.getVarList();
-            if(vl0.singleton() && vl1.singleton()){
-              d_congruenceManager.addWatchedPair(varSlack, vl0.getNode(), vl1.getNode());
-            }
-          }
-        }
-      }
-    }
-
-    ++(d_statistics.d_statSlackVariables);
-    markSetup(polyNode);
-  }
-
-  /* Note:
-   * It is worth documenting that polyNode should only be marked as
-   * being setup by this function if it has kind PLUS.
-   * Other kinds will be marked as being setup by lower levels of setup
-   * specifically setupVariableList.
-   */
-}
-
-void TheoryArith::setupAtom(TNode atom) {
-  Assert(isRelationOperator(atom.getKind()));
-  Assert(Comparison::isNormalAtom(atom));
-  Assert(!isSetup(atom));
-  Assert(!d_constraintDatabase.hasLiteral(atom));
-
-  Comparison cmp = Comparison::parseNormalForm(atom);
-  Polynomial nvp = cmp.normalizedVariablePart();
-  Assert(!nvp.isZero());
-
-  if(!isSetup(nvp.getNode())){
-    setupPolynomial(nvp);
-  }
-
-  d_constraintDatabase.addLiteral(atom);
-
-  markSetup(atom);
-}
-
-void TheoryArith::preRegisterTerm(TNode n) {
-  Debug("arith::preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl;
-
-  if(isRelationOperator(n.getKind())){
-    if(!isSetup(n)){
-      setupAtom(n);
-    }
-    Constraint c = d_constraintDatabase.lookup(n);
-    Assert(c != NullConstraint);
-
-    Debug("arith::preregister") << "setup constraint" << c << endl;
-    Assert(!c->canBePropagated());
-    c->setPreregistered();
-  }
-
-  Debug("arith::preregister") << "end arith::preRegisterTerm("<< n <<")" << endl;
-}
-
-void TheoryArith::releaseArithVar(ArithVar v){
-  Assert(d_arithvarNodeMap.hasNode(v));
-  
-  d_constraintDatabase.removeVariable(v);
-  d_arithvarNodeMap.remove(v);
-
-  d_pool.push_back(v);
-}
-
-ArithVar TheoryArith::requestArithVar(TNode x, bool slack){
-  //TODO : The VarList trick is good enough?
-  Assert(isLeaf(x) || VarList::isMember(x) || x.getKind() == PLUS);
-  if(getLogicInfo().isLinear() && Variable::isDivMember(x)){
-    throw LogicException("Non-linear term was asserted to arithmetic in a linear logic.");
-  }
-  Assert(!d_arithvarNodeMap.hasArithVar(x));
-  Assert(x.getType().isReal());// real or integer
-
-  // ArithVar varX = d_variables.size();
-  // d_variables.push_back(Node(x));
-
-  bool reclaim = !d_pool.empty();
-  ArithVar varX;
-
-  if(reclaim){
-    varX = d_pool.back();
-    d_pool.pop_back();
-
-    d_partialModel.setAssignment(varX, d_DELTA_ZERO, d_DELTA_ZERO);
-  }else{
-    varX = d_numberOfVariables;
-    ++d_numberOfVariables;
-
-    d_slackVars.push_back(true);
-    d_variableTypes.push_back(ATReal);
-
-    d_simplex.increaseMax();
-
-    d_tableau.increaseSize();
-    d_tableauSizeHasBeenModified = true;
-
-    d_partialModel.initialize(varX, d_DELTA_ZERO);
-  }
-
-  ArithType type;
-  if(slack){
-    //The type computation is not quite accurate for Rationals that are integral.
-    //We'll use the isIntegral check from the polynomial package instead.
-    Polynomial p = Polynomial::parsePolynomial(x);
-    type = p.isIntegral() ? ATInteger : ATReal;
-  }else{
-    type = nodeToArithType(x);
-  }
-  d_variableTypes[varX] = type;
-  d_slackVars[varX] = slack;
-
-  d_constraintDatabase.addVariable(varX);
-
-  d_arithvarNodeMap.setArithVar(x,varX);
-
-  // Debug("integers") << "isInteger[[" << x << "]]: " << x.getType().isInteger() << endl;
-
-  // if(slack){
-  //   //The type computation is not quite accurate for Rationals that are integral.
-  //   //We'll use the isIntegral check from the polynomial package instead.
-  //   Polynomial p = Polynomial::parsePolynomial(x);
-  //   d_variableTypes.push_back(p.isIntegral() ? ATInteger : ATReal);
-  // }else{
-  //   d_variableTypes.push_back(nodeToArithType(x));
-  // }
-
-  // d_slackVars.push_back(slack);
-
-  // d_simplex.increaseMax();
-
-  // d_tableau.increaseSize();
-  // d_tableauSizeHasBeenModified = true;
-
-  // d_constraintDatabase.addVariable(varX);
-
-  Debug("arith::arithvar") << x << " |-> " << varX << endl;
-
-  Assert(!d_partialModel.hasUpperBound(varX));
-  Assert(!d_partialModel.hasLowerBound(varX));
-
-  return varX;
-}
-
-void TheoryArith::asVectors(const Polynomial& p, std::vector<Rational>& coeffs, std::vector<ArithVar>& variables) {
-  for(Polynomial::iterator i = p.begin(), end = p.end(); i != end; ++i){
-    const Monomial& mono = *i;
-    const Constant& constant = mono.getConstant();
-    const VarList& variable = mono.getVarList();
-
-    Node n = variable.getNode();
-
-    Debug("rewriter") << "should be var: " << n << endl;
-
-    // TODO: This VarList::isMember(n) can be stronger
-    Assert(isLeaf(n) || VarList::isMember(n));
-    Assert(theoryOf(n) != THEORY_ARITH || d_arithvarNodeMap.hasArithVar(n));
-
-    Assert(d_arithvarNodeMap.hasArithVar(n));
-    ArithVar av = d_arithvarNodeMap.asArithVar(n);
-
-    coeffs.push_back(constant.getValue());
-    variables.push_back(av);
-  }
-}
-
-/* Requirements:
- * For basic variables the row must have been added to the tableau.
- */
-void TheoryArith::setupBasicValue(ArithVar x){
-  Assert(d_tableau.isBasic(x));
-
-  // if(!d_tableau.isBasic(x)){
-  //   d_partialModel.setAssignment(x, d_DELTA_ZERO, d_DELTA_ZERO);
-  // }else{
-    //If the variable is basic, assertions may have already happened and updates
-    //may have occured before setting this variable up.
-
-    //This can go away if the tableau creation is done at preregister
-    //time instead of register
-    DeltaRational safeAssignment = d_linEq.computeRowValue(x, true);
-    DeltaRational assignment = d_linEq.computeRowValue(x, false);
-    //d_partialModel.initialize(x,safeAssignment);
-    //d_partialModel.setAssignment(x,assignment);
-    d_partialModel.setAssignment(x,safeAssignment,assignment);
-
-    //  }
-  Debug("arith") << "setupVariable("<<x<<")"<<std::endl;
-}
-
-ArithVar TheoryArith::determineArithVar(const Polynomial& p) const{
-  Assert(!p.containsConstant());
-  Assert(p.getHead().constantIsPositive());
-  TNode n = p.getNode();
-  Debug("determineArithVar") << "determineArithVar(" << n << ")" << endl;
-  return d_arithvarNodeMap.asArithVar(n);
-}
-
-ArithVar TheoryArith::determineArithVar(TNode assertion) const{
-  Debug("determineArithVar") << "determineArithVar " << assertion << endl;
-  Comparison cmp = Comparison::parseNormalForm(assertion);
-  Polynomial variablePart = cmp.normalizedVariablePart();
-  return determineArithVar(variablePart);
-}
-
-
-bool TheoryArith::canSafelyAvoidEqualitySetup(TNode equality){
-  Assert(equality.getKind() == EQUAL);
-  return d_arithvarNodeMap.hasArithVar(equality[0]);
-}
-
-Comparison TheoryArith::mkIntegerEqualityFromAssignment(ArithVar v){
-  const DeltaRational& beta = d_partialModel.getAssignment(v);
-
-  Assert(beta.isIntegral());
-  Polynomial betaAsPolynomial( Constant::mkConstant(beta.floor()) );
-
-  TNode var = d_arithvarNodeMap.asNode(v);
-  Polynomial varAsPolynomial = Polynomial::parsePolynomial(var);
-  return Comparison::mkComparison(EQUAL, varAsPolynomial, betaAsPolynomial);
-}
-
-Node TheoryArith::dioCutting(){
-  context::Context::ScopedPush speculativePush(getSatContext());
-  //DO NOT TOUCH THE OUTPUTSTREAM
-
-  for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
-    ArithVar v = *vi;
-    if(isInteger(v)){
-      const DeltaRational& dr = d_partialModel.getAssignment(v);
-      if(d_partialModel.equalsUpperBound(v, dr) || d_partialModel.equalsLowerBound(v, dr)){
-        if(!d_partialModel.boundsAreEqual(v)){
-          // If the bounds are equal this is already in the dioSolver
-          //Add v = dr as a speculation.
-          Comparison eq = mkIntegerEqualityFromAssignment(v);
-          Debug("dio::push") <<v << " " <<  eq.getNode() << endl;
-          Assert(!eq.isBoolean());
-          d_diosolver.pushInputConstraint(eq, eq.getNode());
-          // It does not matter what the explanation of eq is.
-          // It cannot be used in a conflict
-        }
-      }
-    }
-  }
-
-  SumPair plane = d_diosolver.processEquationsForCut();
-  if(plane.isZero()){
-    return Node::null();
-  }else{
-    Polynomial p = plane.getPolynomial();
-    Polynomial c(plane.getConstant() * Constant::mkConstant(-1));
-    Integer gcd = p.gcd();
-    Assert(p.isIntegral());
-    Assert(c.isIntegral());
-    Assert(gcd > 1);
-    Assert(!gcd.divides(c.asConstant().getNumerator()));
-    Comparison leq = Comparison::mkComparison(LEQ, p, c);
-    Comparison geq = Comparison::mkComparison(GEQ, p, c);
-    Node lemma = NodeManager::currentNM()->mkNode(OR, leq.getNode(), geq.getNode());
-    Node rewrittenLemma = Rewriter::rewrite(lemma);
-    Debug("arith::dio") << "dioCutting found the plane: " << plane.getNode() << endl;
-    Debug("arith::dio") << "resulting in the cut: " << lemma << endl;
-    Debug("arith::dio") << "rewritten " << rewrittenLemma << endl;
-    return rewrittenLemma;
-  }
-}
-
-Node TheoryArith::callDioSolver(){
-  while(!d_constantIntegerVariables.empty()){
-    ArithVar v = d_constantIntegerVariables.front();
-    d_constantIntegerVariables.pop();
-
-    Debug("arith::dio")  << v << endl;
-
-    Assert(isInteger(v));
-    Assert(d_partialModel.boundsAreEqual(v));
-
-
-    Constraint lb = d_partialModel.getLowerBoundConstraint(v);
-    Constraint ub = d_partialModel.getUpperBoundConstraint(v);
-
-    Node orig = Node::null();
-    if(lb->isEquality()){
-      orig = lb->explainForConflict();
-    }else if(ub->isEquality()){
-      orig = ub->explainForConflict();
-    }else {
-      orig = ConstraintValue::explainConflict(ub, lb);
-    }
-
-    Assert(d_partialModel.assignmentIsConsistent(v));
-
-    Comparison eq = mkIntegerEqualityFromAssignment(v);
-
-    if(eq.isBoolean()){
-      //This can only be a conflict
-      Assert(!eq.getNode().getConst<bool>());
-
-      //This should be handled by the normal form earlier in the case of equality
-      Assert(orig.getKind() != EQUAL);
-      return orig;
-    }else{
-      Debug("dio::push") << v << " " << eq.getNode() << " with reason " << orig << endl;
-      d_diosolver.pushInputConstraint(eq, orig);
-    }
-  }
-
-  return d_diosolver.processEquationsForConflict();
-}
-
-Constraint TheoryArith::constraintFromFactQueue(){
-  Assert(!done());
-  TNode assertion = get();
-
-  Kind simpleKind = Comparison::comparisonKind(assertion);
-  Constraint constraint = d_constraintDatabase.lookup(assertion);
-  if(constraint == NullConstraint){
-    Assert(simpleKind == EQUAL || simpleKind == DISTINCT );
-    bool isDistinct = simpleKind == DISTINCT;
-    Node eq = (simpleKind == DISTINCT) ? assertion[0] : assertion;
-    Assert(!isSetup(eq));
-    Node reEq = Rewriter::rewrite(eq);
-    if(reEq.getKind() == CONST_BOOLEAN){
-      if(reEq.getConst<bool>() == isDistinct){
-        // if is (not true), or false
-        Assert((reEq.getConst<bool>() && isDistinct) ||
-               (!reEq.getConst<bool>() && !isDistinct));
-        d_raiseConflict(assertion);
-      }
-      return NullConstraint;
-    }
-    Assert(reEq.getKind() != CONST_BOOLEAN);
-    if(!isSetup(reEq)){
-      setupAtom(reEq);
-    }
-    Node reAssertion = isDistinct ? reEq.notNode() : reEq;
-    constraint = d_constraintDatabase.lookup(reAssertion);
-
-    if(assertion != reAssertion){
-      Debug("arith::nf") << "getting non-nf assertion " << assertion << " |-> " <<  reAssertion << endl;
-      Assert(constraint != NullConstraint);
-      d_assertionsThatDoNotMatchTheirLiterals.insert(assertion, constraint);
-    }
-  }
-
-  // Kind simpleKind = Comparison::comparisonKind(assertion);
-  // Assert(simpleKind != UNDEFINED_KIND);
-  // Assert(constraint != NullConstraint ||
-  //        simpleKind == EQUAL ||
-  //        simpleKind == DISTINCT );
-  // if(simpleKind == EQUAL || simpleKind == DISTINCT){
-  //   Node eq = (simpleKind == DISTINCT) ? assertion[0] : assertion;
-
-  //   if(!isSetup(eq)){
-  //     //The previous code was equivalent to:
-  //     setupAtom(eq);
-  //     constraint = d_constraintDatabase.lookup(assertion);
-  //   }
-  // }
-  Assert(constraint != NullConstraint);
-
-  if(constraint->negationHasProof()){
-    Constraint negation = constraint->getNegation();
-    if(negation->isSelfExplaining()){
-      if(Debug.isOn("whytheoryenginewhy")){
-        debugPrintFacts();
-      }
-    }
-    Debug("arith::eq") << constraint << endl;
-    Debug("arith::eq") << negation << endl;
-
-    NodeBuilder<> nb(kind::AND);
-    nb << assertion;
-    negation->explainForConflict(nb);
-    Node conflict = nb;
-    Debug("arith::eq") << "conflict" << conflict << endl;
-    d_raiseConflict(conflict);
-    return NullConstraint;
-  }
-  Assert(!constraint->negationHasProof());
-
-  if(constraint->assertedToTheTheory()){
-    //Do nothing
-    return NullConstraint;
-  }else{
-    Debug("arith::constraint") << "arith constraint " << constraint << std::endl;
-    constraint->setAssertedToTheTheory(assertion);
-
-    if(!constraint->hasProof()){
-      Debug("arith::constraint") << "marking as constraint as self explaining " << endl;
-      constraint->selfExplaining();
-    }else{
-      Debug("arith::constraint") << "already has proof: " << constraint->explainForConflict() << endl;
-    }
-
-    return constraint;
-  }
-}
-
-bool TheoryArith::assertionCases(Constraint constraint){
-  Assert(constraint->hasProof());
-  Assert(!constraint->negationHasProof());
-
-  ArithVar x_i = constraint->getVariable();
-
-  switch(constraint->getType()){
-  case UpperBound:
-    if(isInteger(x_i) && constraint->isStrictUpperBound()){
-      Constraint floorConstraint = constraint->getFloor();
-      if(!floorConstraint->isTrue()){
-        if(floorConstraint->negationHasProof()){
-          Node conf = ConstraintValue::explainConflict(constraint, floorConstraint->getNegation());
-          d_raiseConflict(conf);
-          return true;
-        }else{
-          floorConstraint->impliedBy(constraint);
-          // Do not need to add to d_learnedBounds
-        }
-      }
-      return AssertUpper(floorConstraint);
-    }else{
-      return AssertUpper(constraint);
-    }
-  case LowerBound:
-    if(isInteger(x_i) && constraint->isStrictLowerBound()){
-      Constraint ceilingConstraint = constraint->getCeiling();
-      if(!ceilingConstraint->isTrue()){
-        if(ceilingConstraint->negationHasProof()){
-          Node conf = ConstraintValue::explainConflict(constraint, ceilingConstraint->getNegation());
-          d_raiseConflict(conf);
-          return true;
-        }
-        ceilingConstraint->impliedBy(constraint);
-        // Do not need to add to learnedBounds
-      }
-      return AssertLower(ceilingConstraint);
-    }else{
-      return AssertLower(constraint);
-    }
-  case Equality:
-    return AssertEquality(constraint);
-  case Disequality:
-    return AssertDisequality(constraint);
-  default:
-    Unreachable();
-    return false;
-  }
-}
-
-/**
- * Looks for the next integer variable without an integer assignment in a round robin fashion.
- * Changes the value of d_nextIntegerCheckVar.
- *
- * If this returns false, d_nextIntegerCheckVar does not have an integer assignment.
- * If this returns true, all integer variables have an integer assignment.
- */
-bool TheoryArith::hasIntegerModel(){
-  //if(d_variables.size() > 0){
-  if(getNumberOfVariables()){
-    const ArithVar rrEnd = d_nextIntegerCheckVar;
-    do {
-      //Do not include slack variables
-      if(isInteger(d_nextIntegerCheckVar) && !isSlackVariable(d_nextIntegerCheckVar)) { // integer
-        const DeltaRational& d = d_partialModel.getAssignment(d_nextIntegerCheckVar);
-        if(!d.isIntegral()){
-          return false;
-        }
-      }
-    } while((d_nextIntegerCheckVar = (1 + d_nextIntegerCheckVar == getNumberOfVariables() ? 0 : 1 + d_nextIntegerCheckVar)) != rrEnd);
-  }
-  return true;
-}
-
-/** Outputs conflicts to the output channel. */
-void TheoryArith::outputConflicts(){
-  Assert(!d_conflicts.empty());
-  for(size_t i = 0, i_end = d_conflicts.size(); i < i_end; ++i){
-    Node conflict = d_conflicts[i];
-    Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict << endl;
-    d_out->conflict(conflict);
-  }
+  d_internal->ppStaticLearn(n, learned);
 }
 
 void TheoryArith::check(Effort effortLevel){
-  Assert(d_currentPropagationList.empty());
-  Debug("effortlevel") << "TheoryArith::check " << effortLevel << std::endl;
-  Debug("arith") << "TheoryArith::check begun " << effortLevel << std::endl;
-
-  if(Debug.isOn("arith::consistency")){
-    Assert(unenqueuedVariablesAreConsistent());
-  }
-
-  bool newFacts = !done();
-  //If previous == SAT, then reverts on conflicts are safe
-  //Otherwise, they are not and must be committed.
-  Result::Sat previous = d_qflraStatus;
-  if(newFacts){
-    d_qflraStatus = Result::SAT_UNKNOWN;
-    d_hasDoneWorkSinceCut = true;
-  }
-
-  while(!done()){
-    Constraint curr = constraintFromFactQueue();
-    if(curr != NullConstraint){
-      bool res CVC4_UNUSED = assertionCases(curr);
-      Assert(!res || inConflict());
-    }
-    if(inConflict()){ break; }
-  }
-  if(!inConflict()){
-    while(!d_learnedBounds.empty()){
-      // we may attempt some constraints twice.  this is okay!
-      Constraint curr = d_learnedBounds.front();
-      d_learnedBounds.pop();
-      Debug("arith::learned") << curr << endl;
-
-      bool res CVC4_UNUSED = assertionCases(curr);
-      Assert(!res || inConflict());
-
-      if(inConflict()){ break; }
-    }
-  }
-
-  if(inConflict()){
-    d_qflraStatus = Result::UNSAT;
-    if(previous == Result::SAT){
-      ++d_statistics.d_revertsOnConflicts;
-      Debug("arith::bt") << "clearing here " << " " << newFacts << " " << previous << " " << d_qflraStatus  << endl;
-      revertOutOfConflict();
-      d_simplex.clearQueue();
-    }else{
-      ++d_statistics.d_commitsOnConflicts;
-      Debug("arith::bt") << "committing here " << " " << newFacts << " " << previous << " " << d_qflraStatus  << endl;
-      d_partialModel.commitAssignmentChanges();
-      revertOutOfConflict();
-    }
-    outputConflicts();
-    return;
-  }
-
-
-  if(Debug.isOn("arith::print_assertions")) {
-    debugPrintAssertions();
-  }
-
-  bool emmittedConflictOrSplit = false;
-  Assert(d_conflicts.empty());
-
-  d_qflraStatus = d_simplex.findModel(fullEffort(effortLevel));
-
-  switch(d_qflraStatus){
-  case Result::SAT:
-    if(newFacts){
-      ++d_statistics.d_nontrivialSatChecks;
-    }
-
-    Debug("arith::bt") << "committing sap inConflit"  << " " << newFacts << " " << previous << " " << d_qflraStatus  << endl;
-    d_partialModel.commitAssignmentChanges();
-    d_unknownsInARow = 0;
-    if(Debug.isOn("arith::consistency")){
-      Assert(entireStateIsConsistent("sat comit"));
-    }
-    break;
-  case Result::SAT_UNKNOWN:
-    ++d_unknownsInARow;
-    ++(d_statistics.d_unknownChecks);
-    Assert(!fullEffort(effortLevel));
-    Debug("arith::bt") << "committing unknown"  << " " << newFacts << " " << previous << " " << d_qflraStatus  << endl;
-    d_partialModel.commitAssignmentChanges();
-    d_statistics.d_maxUnknownsInARow.maxAssign(d_unknownsInARow);
-    break;
-  case Result::UNSAT:
-    d_unknownsInARow = 0;
-    if(options::revertArithModels() && previous == Result::SAT){
-      ++d_statistics.d_revertsOnConflicts;
-      Debug("arith::bt") << "clearing on conflict" << " " << newFacts << " " << previous << " " << d_qflraStatus  << endl;
-      revertOutOfConflict();
-      d_simplex.clearQueue();
-    }else{
-      ++d_statistics.d_commitsOnConflicts;
-
-      Debug("arith::bt") << "committing on conflict" << " " << newFacts << " " << previous << " " << d_qflraStatus  << endl;
-      d_partialModel.commitAssignmentChanges();
-      revertOutOfConflict();
-
-      if(Debug.isOn("arith::consistency::comitonconflict")){
-        entireStateIsConsistent("commit on conflict");
-      }
-    }
-    outputConflicts();
-    emmittedConflictOrSplit = true;
-    break;
-  default:
-    Unimplemented();
-  }
-  d_statistics.d_avgUnknownsInARow.addEntry(d_unknownsInARow);
-
-  // This should be fine if sat or unknown
-  if(!emmittedConflictOrSplit &&
-     (options::arithPropagationMode() == UNATE_PROP ||
-      options::arithPropagationMode() == BOTH_PROP)){
-    TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime);
-    Assert(d_qflraStatus != Result::UNSAT);
-
-    while(!d_currentPropagationList.empty()  && !inConflict()){
-      Constraint curr = d_currentPropagationList.front();
-      d_currentPropagationList.pop_front();
-
-      ConstraintType t = curr->getType();
-      Assert(t != Disequality, "Disequalities are not allowed in d_currentPropagation");
-
-
-      switch(t){
-      case LowerBound:
-        {
-          Constraint prev = d_currentPropagationList.front();
-          d_currentPropagationList.pop_front();
-          d_constraintDatabase.unatePropLowerBound(curr, prev);
-          break;
-        }
-      case UpperBound:
-        {
-          Constraint prev = d_currentPropagationList.front();
-          d_currentPropagationList.pop_front();
-          d_constraintDatabase.unatePropUpperBound(curr, prev);
-          break;
-        }
-      case Equality:
-        {
-          Constraint prevLB = d_currentPropagationList.front();
-          d_currentPropagationList.pop_front();
-          Constraint prevUB = d_currentPropagationList.front();
-          d_currentPropagationList.pop_front();
-          d_constraintDatabase.unatePropEquality(curr, prevLB, prevUB);
-          break;
-        }
-      default:
-        Unhandled(curr->getType());
-      }
-    }
-
-    if(inConflict()){
-      Debug("arith::unate") << "unate conflict" << endl;
-      revertOutOfConflict();
-      d_qflraStatus = Result::UNSAT;
-      outputConflicts();
-      emmittedConflictOrSplit = true;
-      Debug("arith::bt") << "committing on unate conflict" << " " << newFacts << " " << previous << " " << d_qflraStatus  << endl;
-
-    }
-  }else{
-    TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime);
-    d_currentPropagationList.clear();
-  }
-  Assert( d_currentPropagationList.empty());
-
-  if(!emmittedConflictOrSplit && fullEffort(effortLevel)){
-    ++d_fullCheckCounter;
-  }
-  static const int CUT_ALL_BOUNDED_PERIOD = 10;
-  if(!emmittedConflictOrSplit && fullEffort(effortLevel) &&
-     d_fullCheckCounter % CUT_ALL_BOUNDED_PERIOD == 1){
-
-    Debug("arith::demand-restart") << options::maxCutsInContext() << " " << d_cutsInContext << "cut all" << endl;
-
-    vector<Node> lemmas = cutAllBounded();
-    //output the lemmas
-    for(vector<Node>::const_iterator i = lemmas.begin(); i != lemmas.end(); ++i){
-      d_out->lemma(*i);
-      Debug("arith::demand-restart") << options::maxCutsInContext() << " " << d_cutsInContext << "cut all " << *i << endl;
-      ++(d_statistics.d_externalBranchAndBounds);
-      d_cutsInContext = d_cutsInContext + 1;
-      emmittedConflictOrSplit = lemmas.size() > 0;
-    }
-    if(options::maxCutsInContext() <= d_cutsInContext){
-      d_out->demandRestart();
-    }
-  }
-
-  if(!emmittedConflictOrSplit && fullEffort(effortLevel)){
-    emmittedConflictOrSplit = splitDisequalities();
-  }
-
-  if(!emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()){
-    Node possibleConflict = Node::null();
-    if(!emmittedConflictOrSplit && options::arithDioSolver()){
-      possibleConflict = callDioSolver();
-      if(possibleConflict != Node::null()){
-        revertOutOfConflict();
-        Debug("arith::conflict") << "dio conflict   " << possibleConflict << endl;
-        d_out->conflict(possibleConflict);
-        emmittedConflictOrSplit = true;
-      }
-    }
-
-    if(!emmittedConflictOrSplit && d_hasDoneWorkSinceCut && options::arithDioSolver()){
-      Node possibleLemma = dioCutting();
-      if(!possibleLemma.isNull()){
-        Debug("arith") << "dio cut   " << possibleLemma << endl;
-        emmittedConflictOrSplit = true;
-        d_hasDoneWorkSinceCut = false;
-        d_out->lemma(possibleLemma);
-
-        d_cutsInContext = d_cutsInContext + 1;
-        Debug("arith::demand-restart") << options::maxCutsInContext() << " " << d_cutsInContext << " dio cut" << endl;
-        if(options::maxCutsInContext() <= d_cutsInContext){
-          d_out->demandRestart();
-        }
-      }
-    }
-
-    if(!emmittedConflictOrSplit) {
-      Node possibleLemma = roundRobinBranch();
-      if(!possibleLemma.isNull()){
-
-        d_cutsInContext = d_cutsInContext + 1;
-
-        Debug("arith::demand-restart") << options::maxCutsInContext() << " " << d_cutsInContext << " branch" << endl;
-
-        ++(d_statistics.d_externalBranchAndBounds);
-        emmittedConflictOrSplit = true;
-        d_out->lemma(possibleLemma);
-        d_cutsInContext = d_cutsInContext + 1;
-        if(options::maxCutsInContext() <= d_cutsInContext){
-          d_out->demandRestart();
-        }
-      }
-    }
-  }//if !emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()
-  if(fullEffort(effortLevel) && d_nlIncomplete){
-    // TODO this is total paranoia
-    d_out->setIncomplete();
-  }
-
-  if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
-  if(Debug.isOn("arith::print_model")) { debugPrintModel(); }
-  Debug("arith") << "TheoryArith::check end" << std::endl;
-}
-
-Node TheoryArith::branchIntegerVariable(ArithVar x) const {
-  const DeltaRational& d = d_partialModel.getAssignment(x);
-  Assert(!d.isIntegral());
-  const Rational& r = d.getNoninfinitesimalPart();
-  const Rational& i = d.getInfinitesimalPart();
-  Trace("integers") << "integers: assignment to [[" << d_arithvarNodeMap.asNode(x) << "]] is " << r << "[" << i << "]" << endl;
-
-  Assert(! (r.getDenominator() == 1 && i.getNumerator() == 0));
-  Assert(!d.isIntegral());
-  TNode var = d_arithvarNodeMap.asNode(x);
-  Integer floor_d = d.floor();
-
-  Node ub = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, mkRationalNode(floor_d)));
-  Node lb = ub.notNode();
-
-
-  Node lem = NodeManager::currentNM()->mkNode(kind::OR, ub, lb);
-  Trace("integers") << "integers: branch & bound: " << lem << endl;
-  if(d_valuation.isSatLiteral(lem[0])) {
-    Debug("integers") << "    " << lem[0] << " == " << d_valuation.getSatValue(lem[0]) << endl;
-  } else {
-    Debug("integers") << "    " << lem[0] << " is not assigned a SAT literal" << endl;
-  }
-  if(d_valuation.isSatLiteral(lem[1])) {
-    Debug("integers") << "    " << lem[1] << " == " << d_valuation.getSatValue(lem[1]) << endl;
-    } else {
-    Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
-  }
-  return lem;
+  d_internal->check(effortLevel);
 }
 
-std::vector<Node> TheoryArith::cutAllBounded() const{
-  vector<Node> lemmas;
-  if(options::doCutAllBounded() && getNumberOfVariables() > 0){
-    for(ArithVar iter = 0; iter != getNumberOfVariables(); ++iter){
-    //Do not include slack variables
-      const DeltaRational& d = d_partialModel.getAssignment(iter);
-      if(isInteger(iter) && !isSlackVariable(iter) &&
-         d_partialModel.hasUpperBound(iter) &&
-         d_partialModel.hasLowerBound(iter) &&
-         !d.isIntegral()){
-        Node lem = branchIntegerVariable(iter);
-        lemmas.push_back(lem);
-      }
-    }
-  }
-  return lemmas;
-}
-
-/** Returns true if the roundRobinBranching() issues a lemma. */
-Node TheoryArith::roundRobinBranch(){
-  if(hasIntegerModel()){
-    return Node::null();
-  }else{
-    ArithVar v = d_nextIntegerCheckVar;
-
-    Assert(isInteger(v));
-    Assert(!isSlackVariable(v));
-    return branchIntegerVariable(v);
-
-    // Assert(isInteger(v));
-    // Assert(!isSlackVariable(v));
-
-    // const DeltaRational& d = d_partialModel.getAssignment(v);
-    // const Rational& r = d.getNoninfinitesimalPart();
-    // const Rational& i = d.getInfinitesimalPart();
-    // Trace("integers") << "integers: assignment to [[" << d_arithvarNodeMap.asNode(v) << "]] is " << r << "[" << i << "]" << endl;
-
-    // Assert(! (r.getDenominator() == 1 && i.getNumerator() == 0));
-    // Assert(!d.isIntegral());
-
-    // TNode var = d_arithvarNodeMap.asNode(v);
-    // Integer floor_d = d.floor();
-    // Integer ceil_d = d.ceiling();
-
-    // Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, mkRationalNode(floor_d)));
-    // Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, mkRationalNode(ceil_d)));
-
-
-    // Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq);
-    // Trace("integers") << "integers: branch & bound: " << lem << endl;
-    // if(d_valuation.isSatLiteral(lem[0])) {
-    //   Debug("integers") << "    " << lem[0] << " == " << d_valuation.getSatValue(lem[0]) << endl;
-    // } else {
-    //   Debug("integers") << "    " << lem[0] << " is not assigned a SAT literal" << endl;
-    // }
-    // if(d_valuation.isSatLiteral(lem[1])) {
-    //   Debug("integers") << "    " << lem[1] << " == " << d_valuation.getSatValue(lem[1]) << endl;
-    // } else {
-    //   Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
-    // }
-    // return lem;
-  }
-}
-
-bool TheoryArith::splitDisequalities(){
-  bool splitSomething = false;
-
-  vector<Constraint> save;
-
-  while(!d_diseqQueue.empty()){
-    Constraint front = d_diseqQueue.front();
-    d_diseqQueue.pop();
-
-    if(front->isSplit()){
-      Debug("eq") << "split already" << endl;
-    }else{
-      Debug("eq") << "not split already" << endl;
-
-      ArithVar lhsVar = front->getVariable();
-
-      const DeltaRational& lhsValue = d_partialModel.getAssignment(lhsVar);
-      const DeltaRational& rhsValue = front->getValue();
-      if(lhsValue == rhsValue){
-        Debug("arith::lemma") << "Splitting on " << front << endl;
-        Debug("arith::lemma") << "LHS value = " << lhsValue << endl;
-        Debug("arith::lemma") << "RHS value = " << rhsValue << endl;
-        Node lemma = front->split();
-        ++(d_statistics.d_statDisequalitySplits);
-        Node relem = Rewriter::rewrite(lemma);
-
-        Debug("arith::lemma") << "Now " << relem << endl;
-        d_out->lemma(lemma);
-        splitSomething = true;
-      }else if(d_partialModel.strictlyLessThanLowerBound(lhsVar, rhsValue)){
-        Debug("eq") << "can drop as less than lb" << front << endl;
-      }else if(d_partialModel.strictlyGreaterThanUpperBound(lhsVar, rhsValue)){
-        Debug("eq") << "can drop as greater than ub" << front << endl;
-      }else{
-        Debug("eq") << "save" << front << ": " <<lhsValue << " != " << rhsValue << endl;
-        save.push_back(front);
-      }
-    }
-  }
-  vector<Constraint>::const_iterator i=save.begin(), i_end = save.end();
-  for(; i != i_end; ++i){
-    d_diseqQueue.push(*i);
-  }
-  return splitSomething;
-}
-
-/**
- * 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 (var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
-    ArithVar i = *vi;
-    if (d_partialModel.hasLowerBound(i)) {
-      Constraint lConstr = d_partialModel.getLowerBoundConstraint(i);
-      Debug("arith::print_assertions") << lConstr << endl;
-    }
-
-    if (d_partialModel.hasUpperBound(i)) {
-      Constraint uConstr = d_partialModel.getUpperBoundConstraint(i);
-      Debug("arith::print_assertions") << uConstr << endl;
-    }
-  }
-  context::CDQueue<Constraint>::const_iterator it = d_diseqQueue.begin();
-  context::CDQueue<Constraint>::const_iterator it_end = d_diseqQueue.end();
-  for(; it != it_end; ++ it) {
-    Debug("arith::print_assertions") << *it << endl;
-  }
-}
-
-void TheoryArith::debugPrintModel(){
-  Debug("arith::print_model") << "Model:" << endl;
-  for (var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
-    ArithVar i = *vi;
-    if(d_arithvarNodeMap.hasNode(i)){
-      Debug("arith::print_model") << d_arithvarNodeMap.asNode(i) << " : " <<
-        d_partialModel.getAssignment(i);
-      if(d_tableau.isBasic(i))
-        Debug("arith::print_model") << " (basic)";
-      Debug("arith::print_model") << endl;
-    }
-  }
-}
-
-
-
 Node TheoryArith::explain(TNode n) {
-
-  Debug("arith::explain") << "explain @" << getSatContext()->getLevel() << ": " << n << endl;
-
-  Constraint c = d_constraintDatabase.lookup(n);
-  if(c != NullConstraint){
-    Assert(!c->isSelfExplaining());
-    Node exp = c->explainForPropagation();
-    Debug("arith::explain") << "constraint explanation" << n << ":" << exp << endl;
-    return exp;
-  }else if(d_assertionsThatDoNotMatchTheirLiterals.find(n) != d_assertionsThatDoNotMatchTheirLiterals.end()){
-    c = d_assertionsThatDoNotMatchTheirLiterals[n];
-    if(!c->isSelfExplaining()){
-      Node exp = c->explainForPropagation();
-      Debug("arith::explain") << "assertions explanation" << n << ":" << exp << endl;
-      return exp;
-    }else{
-      Debug("arith::explain") << "this is a strange mismatch" << n << endl;
-      Assert(d_congruenceManager.canExplain(n));
-      Debug("arith::explain") << "this is a strange mismatch" << n << endl;
-      return d_congruenceManager.explain(n);
-    }
-  }else{
-    Assert(d_congruenceManager.canExplain(n));
-    Debug("arith::explain") << "dm explanation" << n << endl;
-    return d_congruenceManager.explain(n);
-  }
+  return d_internal->explain(n);
 }
 
-
 void TheoryArith::propagate(Effort e) {
-  // This uses model values for safety. Disable for now.
-  if(d_qflraStatus == Result::SAT &&
-     (options::arithPropagationMode() == BOUND_INFERENCE_PROP ||
-      options::arithPropagationMode() == BOTH_PROP)
-     && hasAnyUpdates()){
-    propagateCandidates();
-  }else{
-    clearUpdates();
-  }
-
-  while(d_constraintDatabase.hasMorePropagations()){
-    Constraint c = d_constraintDatabase.nextPropagation();
-    Debug("arith::prop") << "next prop" << getSatContext()->getLevel() << ": " << c << endl;
-
-    if(c->negationHasProof()){
-      Debug("arith::prop") << "negation has proof " << c->getNegation() << endl
-                           << c->getNegation()->explainForConflict() << endl;
-    }
-    Assert(!c->negationHasProof(), "A constraint has been propagated on the constraint propagation queue, but the negation has been set to true.  Contact Tim now!");
-
-    if(!c->assertedToTheTheory()){
-      Node literal = c->getLiteral();
-      Debug("arith::prop") << "propagating @" << getSatContext()->getLevel() << " " << literal << endl;
-
-      d_out->propagate(literal);
-    }else{
-      Debug("arith::prop") << "already asserted to the theory " <<  c->getLiteral() << endl;
-    }
-  }
-
-  while(d_congruenceManager.hasMorePropagations()){
-    TNode toProp = d_congruenceManager.getNextPropagation();
-
-    //Currently if the flag is set this came from an equality detected by the
-    //equality engine in the the difference manager.
-    Node normalized = Rewriter::rewrite(toProp);
-
-    Constraint constraint = d_constraintDatabase.lookup(normalized);
-    if(constraint == NullConstraint){
-      Debug("arith::prop") << "propagating on non-constraint? "  << toProp << endl;
-      d_out->propagate(toProp);
-    }else if(constraint->negationHasProof()){
-      Node exp = d_congruenceManager.explain(toProp);
-      Node notNormalized = normalized.getKind() == NOT ?
-        normalized[0] : normalized.notNode();
-      Node lp = flattenAnd(exp.andNode(notNormalized));
-      Debug("arith::prop") << "propagate conflict" <<  lp << endl;
-      d_out->conflict(lp);
-      return;
-    }else{
-      Debug("arith::prop") << "propagating still?" <<  toProp << endl;
-
-      d_out->propagate(toProp);
-    }
-  }
-}
-
-DeltaRational TheoryArith::getDeltaValue(TNode n) const throw (DeltaRationalException, ModelException) {
-  AlwaysAssert(d_qflraStatus != Result::SAT_UNKNOWN);
-  Debug("arith::value") << n << std::endl;
-
-  switch(n.getKind()) {
-
-  case kind::CONST_RATIONAL:
-    return n.getConst<Rational>();
-
-  case kind::PLUS: { // 2+ args
-    DeltaRational value(0);
-    for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
-      value = value + getDeltaValue(*i);
-    }
-    return value;
-  }
-
-  case kind::MULT: { // 2+ args
-    DeltaRational value(1);
-    unsigned variableParts = 0;
-    for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
-      TNode curr = *i;
-      value = value * getDeltaValue(curr);
-      if(!curr.isConst()){
-        ++variableParts;
-      }
-    }
-    // TODO: This is a bit of a weak check
-    if(isSetup(n)){
-      ArithVar var = d_arithvarNodeMap.asArithVar(n);
-      const DeltaRational& assign = d_partialModel.getAssignment(var);
-      if(assign != value){
-        throw ModelException(n, "Model disagrees on non-linear term.");
-      }
-    }
-    return value;
-  }
-  case kind::MINUS:{ // 2 args
-    return getDeltaValue(n[0]) - getDeltaValue(n[1]);
-  }
-
-  case kind::UMINUS:{ // 1 arg
-    return (- getDeltaValue(n[0]));
-  }
-
-  case kind::DIVISION:{ // 2 args
-    DeltaRational res = getDeltaValue(n[0]) / getDeltaValue(n[1]);
-    if(isSetup(n)){
-      ArithVar var = d_arithvarNodeMap.asArithVar(n);
-      if(d_partialModel.getAssignment(var) != res){
-        throw ModelException(n, "Model disagrees on non-linear term.");
-      }
-    }
-    return res;
-  }
-  case kind::DIVISION_TOTAL:
-  case kind::INTS_DIVISION_TOTAL:
-  case kind::INTS_MODULUS_TOTAL: { // 2 args
-    DeltaRational denom = getDeltaValue(n[1]);
-    if(denom.isZero()){
-      return DeltaRational(0,0);
-    }else{
-      DeltaRational numer = getDeltaValue(n[0]);
-      DeltaRational res;
-      if(n.getKind() == kind::DIVISION_TOTAL){
-        res = numer / denom;
-      }else if(n.getKind() == kind::INTS_DIVISION_TOTAL){
-        res = Rational(numer.euclidianDivideQuotient(denom));
-      }else{
-        Assert(n.getKind() == kind::INTS_MODULUS_TOTAL);
-        res = Rational(numer.euclidianDivideRemainder(denom));
-      }
-      if(isSetup(n)){
-        ArithVar var = d_arithvarNodeMap.asArithVar(n);
-        if(d_partialModel.getAssignment(var) != res){
-          throw ModelException(n, "Model disagrees on non-linear term.");
-        }
-      }
-      return res;
-    }
-  }
-
-  default:
-    if(isSetup(n)){
-      ArithVar var = d_arithvarNodeMap.asArithVar(n);
-      return d_partialModel.getAssignment(var);
-    }else{
-      throw ModelException(n, "Expected a setup node.");
-    }
-  }
-}
-
-Rational TheoryArith::deltaValueForTotalOrder() const{
-  Rational min(2);
-  std::set<DeltaRational> relevantDeltaValues;
-  context::CDQueue<Constraint>::const_iterator qiter = d_diseqQueue.begin();
-  context::CDQueue<Constraint>::const_iterator qiter_end = d_diseqQueue.end();
-
-  for(; qiter != qiter_end; ++qiter){
-    Constraint curr = *qiter;
-
-    const DeltaRational& rhsValue = curr->getValue();
-    relevantDeltaValues.insert(rhsValue);
-  }
-
-  for(shared_terms_iterator shared_iter = shared_terms_begin(),
-        shared_end = shared_terms_end(); shared_iter != shared_end; ++shared_iter){
-    Node sharedCurr = *shared_iter;
-
-    // ModelException is fatal as this point. Don't catch!
-    // DeltaRationalException is fatal as this point. Don't catch!
-    DeltaRational val = getDeltaValue(sharedCurr);
-    relevantDeltaValues.insert(val);
-  }
-
-  for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
-    ArithVar v = *vi;
-    const DeltaRational& value = d_partialModel.getAssignment(v);
-    relevantDeltaValues.insert(value);
-    if( d_partialModel.hasLowerBound(v)){
-      const DeltaRational& lb = d_partialModel.getLowerBound(v);
-      relevantDeltaValues.insert(lb);
-    }
-    if( d_partialModel.hasUpperBound(v)){
-      const DeltaRational& ub = d_partialModel.getUpperBound(v);
-      relevantDeltaValues.insert(ub);
-    }
-  }
-
-  if(relevantDeltaValues.size() >= 2){
-    std::set<DeltaRational>::const_iterator iter = relevantDeltaValues.begin();
-    std::set<DeltaRational>::const_iterator iter_end = relevantDeltaValues.end();
-    DeltaRational prev = *iter;
-    ++iter;
-    for(; iter != iter_end; ++iter){
-      const DeltaRational& curr = *iter;
-
-      Assert(prev < curr);
-
-      DeltaRational::seperatingDelta(min, prev, curr);
-      prev = curr;
-    }
-  }
-
-  Assert(min.sgn() > 0);
-  Rational belowMin = min/Rational(2);
-  return belowMin;
+  d_internal->propagate(e);
 }
 
 void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){
-  AlwaysAssert(d_qflraStatus ==  Result::SAT);
-  //AlwaysAssert(!d_nlIncomplete, "Arithmetic solver cannot currently produce models for input with nonlinear arithmetic constraints");
-
-  if(Debug.isOn("arith::collectModelInfo")){
-    debugPrintFacts();
-  }
-
-  Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl;
-
-
-  // Delta lasts at least the duration of the function call
-  const Rational& delta = d_partialModel.getDelta();
-  std::hash_set<TNode, TNodeHashFunction> shared = currentlySharedTerms();
-
-  // TODO:
-  // This is not very good for user push/pop....
-  // Revisit when implementing push/pop
-  for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
-    ArithVar v = *vi;
-    if(!isSlackVariable(v)){
-      Node term = d_arithvarNodeMap.asNode(v);
-
-      if(theoryOf(term) == THEORY_ARITH || shared.find(term) != shared.end()){
-        const DeltaRational& mod = d_partialModel.getAssignment(v);
-        Rational qmodel = mod.substituteDelta(delta);
-
-        Node qNode = mkRationalNode(qmodel);
-        Debug("arith::collectModelInfo") << "m->assertEquality(" << term << ", " << qmodel << ", true)" << endl;
-
-        m->assertEquality(term, qNode, true);
-      }else{
-        Debug("arith::collectModelInfo") << "Skipping m->assertEquality(" << term << ", true)" << endl;
-
-      }
-    }
-  }
-
-  // Iterate over equivalence classes in LinearEqualityModule
-  // const eq::EqualityEngine& ee = d_congruenceManager.getEqualityEngine();
-  // m->assertEqualityEngine(&ee);
-
-  Debug("arith::collectModelInfo") << "collectModelInfo() end " << endl;
-}
-
-bool TheoryArith::safeToReset() const {
-  Assert(!d_tableauSizeHasBeenModified);
-
-  ArithPriorityQueue::const_iterator conf_iter = d_simplex.queueBegin();
-  ArithPriorityQueue::const_iterator conf_end = d_simplex.queueEnd();
-  for(; conf_iter != conf_end; ++conf_iter){
-    ArithVar basic = *conf_iter;
-    if(!d_smallTableauCopy.isBasic(basic)){
-      return false;
-    }
-  }
-
-  return true;
+  d_internal->collectModelInfo(m, fullModel);
 }
 
 void TheoryArith::notifyRestart(){
-  TimerStat::CodeTimer codeTimer(d_statistics.d_restartTimer);
-
-  if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
-
-  ++d_restartsCounter;
-
-  uint32_t currSize = d_tableau.size();
-  uint32_t copySize = d_smallTableauCopy.size();
-
-  Debug("arith::reset") << "resetting" << d_restartsCounter << endl;
-  Debug("arith::reset") << "curr " << currSize << " copy " << copySize << endl;
-  Debug("arith::reset") << "tableauSizeHasBeenModified " << d_tableauSizeHasBeenModified << endl;
-
-  if(d_tableauSizeHasBeenModified){
-    Debug("arith::reset") << "row has been added must copy " << d_restartsCounter << endl;
-    d_smallTableauCopy = d_tableau;
-    d_tableauSizeHasBeenModified = false;
-  }else if( d_restartsCounter >= RESET_START){
-    if(copySize >= currSize * 1.1 ){
-      Debug("arith::reset") << "size has shrunk " << d_restartsCounter << endl;
-      ++d_statistics.d_smallerSetToCurr;
-      d_smallTableauCopy = d_tableau;
-    }else if(d_tableauResetDensity * copySize <=  currSize){
-      d_simplex.reduceQueue();
-      if(safeToReset()){
-        Debug("arith::reset") << "resetting " << d_restartsCounter << endl;
-        ++d_statistics.d_currSetToSmaller;
-        d_tableau = d_smallTableauCopy;
-      }else{
-        Debug("arith::reset") << "not safe to reset at the moment " << d_restartsCounter << endl;
-      }
-    }
-  }
-  Assert(unenqueuedVariablesAreConsistent());
-}
-
-bool TheoryArith::entireStateIsConsistent(const string& s){
-  bool result = true;
-  for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
-    ArithVar var = *vi;
-    //ArithVar var = d_arithvarNodeMap.asArithVar(*i);
-    if(!d_partialModel.assignmentIsConsistent(var)){
-      d_partialModel.printModel(var);
-      Warning() << s << ":" << "Assignment is not consistent for " << var << d_arithvarNodeMap.asNode(var);
-      if(d_tableau.isBasic(var)){
-        Warning() << " (basic)";
-      }
-      Warning() << endl;
-      result = false;
-    }
-  }
-  return result;
-}
-
-bool TheoryArith::unenqueuedVariablesAreConsistent(){
-  bool result = true;
-  for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
-    ArithVar var = *vi;
-    if(!d_partialModel.assignmentIsConsistent(var)){
-      if(!d_simplex.debugIsInCollectionQueue(var)){
-
-        d_partialModel.printModel(var);
-        Warning() << "Unenqueued var is not consistent for " << var <<  d_arithvarNodeMap.asNode(var);
-        if(d_tableau.isBasic(var)){
-          Warning() << " (basic)";
-        }
-        Warning() << endl;
-        result = false;
-      } else if(Debug.isOn("arith::consistency::initial")){
-        d_partialModel.printModel(var);
-        Warning() << "Initial var is not consistent for " << var <<  d_arithvarNodeMap.asNode(var);
-        if(d_tableau.isBasic(var)){
-          Warning() << " (basic)";
-        }
-        Warning() << endl;
-      }
-     }
-  }
-  return result;
+  d_internal->notifyRestart();
 }
 
 void TheoryArith::presolve(){
-  TimerStat::CodeTimer codeTimer(d_statistics.d_presolveTime);
-
-  d_statistics.d_initialTableauSize.setData(d_tableau.size());
-
-  if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
-
-  static CVC4_THREADLOCAL(unsigned) callCount = 0;
-  if(Debug.isOn("arith::presolve")) {
-    Debug("arith::presolve") << "TheoryArith::presolve #" << callCount << endl;
-    callCount = callCount + 1;
-  }
-
-  vector<Node> lemmas;
-  switch(options::arithUnateLemmaMode()){
-  case NO_PRESOLVE_LEMMAS:
-    break;
-  case INEQUALITY_PRESOLVE_LEMMAS:
-    d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
-    break;
-  case EQUALITY_PRESOLVE_LEMMAS:
-    d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
-    break;
-  case ALL_PRESOLVE_LEMMAS:
-    d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
-    d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
-    break;
-  default:
-    Unhandled(options::arithUnateLemmaMode());
-  }
-
-  vector<Node>::const_iterator i = lemmas.begin(), i_end = lemmas.end();
-  for(; i != i_end; ++i){
-    Node lem = *i;
-    Debug("arith::oldprop") << " lemma lemma duck " <<lem << endl;
-    d_out->lemma(lem);
-  }
-
-  // if(options::arithUnateLemmaMode() == Options::ALL_UNATE){
-  //   vector<Node> lemmas;
-  //   d_constraintDatabase.outputAllUnateLemmas(lemmas);
-  //   vector<Node>::const_iterator i = lemmas.begin(), i_end = lemmas.end();
-  //   for(; i != i_end; ++i){
-  //     Node lem = *i;
-  //     Debug("arith::oldprop") << " lemma lemma duck " <<lem << endl;
-  //     d_out->lemma(lem);
-  //   }
-  // }
+  d_internal->presolve();
 }
 
 EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
-  if(d_qflraStatus == Result::SAT_UNKNOWN){
-    return EQUALITY_UNKNOWN;
-  }else{
-    try {
-      if (getDeltaValue(a) == getDeltaValue(b)) {
-        return EQUALITY_TRUE_IN_MODEL;
-      } else {
-        return EQUALITY_FALSE_IN_MODEL;
-      }
-    } catch (DeltaRationalException& dr) {
-      return EQUALITY_UNKNOWN;
-    } catch (ModelException& me) {
-      return EQUALITY_UNKNOWN;
-    }
-  }
-}
-
-bool TheoryArith::propagateCandidateBound(ArithVar basic, bool upperBound){
-  ++d_statistics.d_boundComputations;
-
-  DeltaRational bound = upperBound ?
-    d_linEq.computeUpperBound(basic):
-    d_linEq.computeLowerBound(basic);
-
-  if((upperBound && d_partialModel.strictlyLessThanUpperBound(basic, bound)) ||
-     (!upperBound && d_partialModel.strictlyGreaterThanLowerBound(basic, bound))){
-
-    // TODO: "Policy point"
-    //We are only going to recreate the functionality for now.
-    //In the future this can be improved to generate a temporary constraint
-    //if none exists.
-    //Experiment with doing this everytime or only when the new constraint
-    //implies an unknown fact.
-
-    ConstraintType t = upperBound ? UpperBound : LowerBound;
-    Constraint bestImplied = d_constraintDatabase.getBestImpliedBound(basic, t, bound);
-
-    // Node bestImplied = upperBound ?
-    //   d_apm.getBestImpliedUpperBound(basic, bound):
-    //   d_apm.getBestImpliedLowerBound(basic, bound);
-
-    if(bestImplied != NullConstraint){
-      //This should be stronger
-      Assert(!upperBound || bound <= bestImplied->getValue());
-      Assert(!upperBound || d_partialModel.lessThanUpperBound(basic, bestImplied->getValue()));
-
-      Assert( upperBound || bound >= bestImplied->getValue());
-      Assert( upperBound || d_partialModel.greaterThanLowerBound(basic, bestImplied->getValue()));
-      //slightly changed
-
-      // Constraint c = d_constraintDatabase.lookup(bestImplied);
-      // Assert(c != NullConstraint);
-
-      bool assertedToTheTheory = bestImplied->assertedToTheTheory();
-      bool canBePropagated = bestImplied->canBePropagated();
-      bool hasProof = bestImplied->hasProof();
-
-      Debug("arith::prop") << "arith::prop" << basic
-                           << " " << assertedToTheTheory
-                           << " " << canBePropagated
-                           << " " << hasProof
-                           << endl;
-
-      if(bestImplied->negationHasProof()){
-        Warning() << "the negation of " <<  bestImplied << " : " << endl
-                  << "has proof " << bestImplied->getNegation() << endl
-                  << bestImplied->getNegation()->explainForConflict() << endl;
-      }
-
-      if(!assertedToTheTheory && canBePropagated && !hasProof ){
-        if(upperBound){
-          Assert(bestImplied != d_partialModel.getUpperBoundConstraint(basic));
-          d_linEq.propagateNonbasicsUpperBound(basic, bestImplied);
-        }else{
-          Assert(bestImplied != d_partialModel.getLowerBoundConstraint(basic));
-          d_linEq.propagateNonbasicsLowerBound(basic, bestImplied);
-        }
-        // I think this can be skipped if canBePropagated is true
-        //d_learnedBounds.push(bestImplied);
-        return true;
-      }
-    }
-  }
-  return false;
-}
-
-void TheoryArith::propagateCandidate(ArithVar basic){
-  bool success = false;
-  if(d_partialModel.strictlyAboveLowerBound(basic) && d_linEq.hasLowerBounds(basic)){
-    success |= propagateCandidateLowerBound(basic);
-  }
-  if(d_partialModel.strictlyBelowUpperBound(basic) && d_linEq.hasUpperBounds(basic)){
-    success |= propagateCandidateUpperBound(basic);
-  }
-  if(success){
-    ++d_statistics.d_boundPropagations;
-  }
-}
-
-void TheoryArith::propagateCandidates(){
-  TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime);
-
-  Assert(d_candidateBasics.empty());
-
-  if(d_updatedBounds.empty()){ return; }
-
-  DenseSet::const_iterator i = d_updatedBounds.begin();
-  DenseSet::const_iterator end = d_updatedBounds.end();
-  for(; i != end; ++i){
-    ArithVar var = *i;
-    if(d_tableau.isBasic(var) &&
-       d_tableau.getRowLength(d_tableau.basicToRowIndex(var)) <= options::arithPropagateMaxLength()){
-      d_candidateBasics.softAdd(var);
-    }else{
-      Tableau::ColIterator basicIter = d_tableau.colIterator(var);
-      for(; !basicIter.atEnd(); ++basicIter){
-        const Tableau::Entry& entry = *basicIter;
-        RowIndex ridx = entry.getRowIndex();
-        ArithVar rowVar = d_tableau.rowIndexToBasic(ridx);
-        Assert(entry.getColVar() == var);
-        Assert(d_tableau.isBasic(rowVar));
-        if(d_tableau.getRowLength(ridx) <= options::arithPropagateMaxLength()){
-          d_candidateBasics.softAdd(rowVar);
-        }
-      }
-    }
-  }
-  d_updatedBounds.purge();
-
-  while(!d_candidateBasics.empty()){
-    ArithVar candidate = d_candidateBasics.back();
-    d_candidateBasics.pop_back();
-    Assert(d_tableau.isBasic(candidate));
-    propagateCandidate(candidate);
-  }
+  return d_internal->getEqualityStatus(a,b);
 }
 
 }/* CVC4::theory::arith namespace */