Removed slack.h, and arith_activity.h. Replaced IsBasicManager with the more general ArithVarDenseSet. Renamed NextArithRewriter to ArithRewriter.

11 files changed, 113 insertions, 200 deletions

diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 665b9be4b..21ec99390 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -7,20 +7,18 @@ noinst_LTLIBRARIES = libarith.la
 
 libarith_la_SOURCES = \
 	theory_arith_type_rules.h \
-	next_arith_rewriter.h \
-	next_arith_rewriter.cpp \
+	arith_rewriter.h \
+	arith_rewriter.cpp \
 	normal_form.h\
 	normal_form.cpp \
 	arith_utilities.h \
 	arith_constants.h \
-	arith_activity.h \
 	delta_rational.h \
 	delta_rational.cpp \
 	partial_model.h \
 	partial_model.cpp \
 	ordered_bounds_list.h \
-	basic.h \
-	slack.h \
+	arithvar_dense_set.h \
 	tableau.h \
 	tableau.cpp \
 	arith_propagator.h \
diff --git a/src/theory/arith/arith_activity.h b/src/theory/arith/arith_activity.h
deleted file mode 100644
index 7db3d7d8f..000000000
--- a/src/theory/arith/arith_activity.h
+++ /dev/null
@@ -1,67 +0,0 @@
-/*********************                                                        */
-/*! \file arith_activity.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_ACTIVITY_H
-#define __CVC4__THEORY__ARITH__ARITH_ACTIVITY_H
-
-#include "expr/node.h"
-#include "expr/attribute.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-
-class ActivityMonitor {
-private:
-  std::vector<uint64_t> d_activities;
-
-public:
-  const static uint64_t ACTIVITY_THRESHOLD = 100;
-
-  ActivityMonitor() : d_activities() {}
-
-  void resetActivity(ArithVar var){
-    d_activities[var] = 0;
-  }
-
-  void initActivity(ArithVar var){
-    Assert(var == d_activities.size());
-    d_activities.push_back(0);
-  }
-
-  uint64_t getActivity(ArithVar var) const{
-    return d_activities[var];
-  }
-
-  inline void increaseActivity(ArithVar var, uint64_t x){
-    d_activities[var] += x;
-  }
-
-};
-
-
-}; /* namesapce arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
-
-
-#endif
diff --git a/src/theory/arith/next_arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 29fae233b..9f4388b54 100644
--- a/src/theory/arith/next_arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file next_arith_rewriter.cpp
+/*! \file arith_rewriter.cpp
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
@@ -20,7 +20,7 @@
 
 #include "theory/theory.h"
 #include "theory/arith/normal_form.h"
-#include "theory/arith/next_arith_rewriter.h"
+#include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_utilities.h"
 
 #include <vector>
@@ -36,20 +36,20 @@ bool isVariable(TNode t){
   return t.getMetaKind() == kind::metakind::VARIABLE;
 }
 
-RewriteResponse NextArithRewriter::rewriteConstant(TNode t){
+RewriteResponse ArithRewriter::rewriteConstant(TNode t){
   Assert(t.getMetaKind() == kind::metakind::CONSTANT);
   Node val = coerceToRationalNode(t);
 
   return RewriteComplete(val);
 }
 
-RewriteResponse NextArithRewriter::rewriteVariable(TNode t){
+RewriteResponse ArithRewriter::rewriteVariable(TNode t){
   Assert(isVariable(t));
 
   return RewriteComplete(t);
 }
 
-RewriteResponse NextArithRewriter::rewriteMinus(TNode t, bool pre){
+RewriteResponse ArithRewriter::rewriteMinus(TNode t, bool pre){
   Assert(t.getKind()== kind::MINUS);
 
   if(t[0] == t[1]) return RewriteComplete(d_constants->d_ZERO_NODE);
@@ -62,7 +62,7 @@ RewriteResponse NextArithRewriter::rewriteMinus(TNode t, bool pre){
   }
 }
 
-RewriteResponse NextArithRewriter::rewriteUMinus(TNode t, bool pre){
+RewriteResponse ArithRewriter::rewriteUMinus(TNode t, bool pre){
   Assert(t.getKind()== kind::UMINUS);
 
   Node noUminus = makeUnaryMinusNode(t[0]);
@@ -72,7 +72,7 @@ RewriteResponse NextArithRewriter::rewriteUMinus(TNode t, bool pre){
     return RewriteAgain(noUminus);
 }
 
-RewriteResponse NextArithRewriter::preRewriteTerm(TNode t){
+RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
   if(t.getMetaKind() == kind::metakind::CONSTANT){
     return rewriteConstant(t);
   }else if(isVariable(t)){
@@ -95,7 +95,7 @@ RewriteResponse NextArithRewriter::preRewriteTerm(TNode t){
     Unreachable();
   }
 }
-RewriteResponse NextArithRewriter::postRewriteTerm(TNode t){
+RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
   if(t.getMetaKind() == kind::metakind::CONSTANT){
     return rewriteConstant(t);
   }else if(isVariable(t)){
@@ -115,7 +115,7 @@ RewriteResponse NextArithRewriter::postRewriteTerm(TNode t){
   }
 }
 
-RewriteResponse NextArithRewriter::preRewriteMult(TNode t){
+RewriteResponse ArithRewriter::preRewriteMult(TNode t){
   Assert(t.getKind()== kind::MULT);
 
   // Rewrite multiplications with a 0 argument and to 0
@@ -138,13 +138,13 @@ RewriteResponse NextArithRewriter::preRewriteMult(TNode t){
   }
   return RewriteComplete(t);
 }
-RewriteResponse NextArithRewriter::preRewritePlus(TNode t){
+RewriteResponse ArithRewriter::preRewritePlus(TNode t){
   Assert(t.getKind()== kind::PLUS);
 
   return RewriteComplete(t);
 }
 
-RewriteResponse NextArithRewriter::postRewritePlus(TNode t){
+RewriteResponse ArithRewriter::postRewritePlus(TNode t){
   Assert(t.getKind()== kind::PLUS);
 
   Polynomial res = Polynomial::mkZero();
@@ -159,7 +159,7 @@ RewriteResponse NextArithRewriter::postRewritePlus(TNode t){
   return RewriteComplete(res.getNode());
 }
 
-RewriteResponse NextArithRewriter::postRewriteMult(TNode t){
+RewriteResponse ArithRewriter::postRewriteMult(TNode t){
   Assert(t.getKind()== kind::MULT);
 
   Polynomial res = Polynomial::mkOne();
@@ -174,7 +174,7 @@ RewriteResponse NextArithRewriter::postRewriteMult(TNode t){
   return RewriteComplete(res.getNode());
 }
 
-RewriteResponse NextArithRewriter::postRewriteAtomConstantRHS(TNode t){
+RewriteResponse ArithRewriter::postRewriteAtomConstantRHS(TNode t){
   TNode left  = t[0];
   TNode right = t[1];
 
@@ -212,7 +212,7 @@ RewriteResponse NextArithRewriter::postRewriteAtomConstantRHS(TNode t){
   return RewriteComplete(cmp.getNode());
 }
 
-RewriteResponse NextArithRewriter::postRewriteAtom(TNode atom){
+RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){
   // left |><| right
   TNode left = atom[0];
   TNode right = atom[1];
@@ -227,7 +227,7 @@ RewriteResponse NextArithRewriter::postRewriteAtom(TNode atom){
   }
 }
 
-RewriteResponse NextArithRewriter::preRewriteAtom(TNode atom){
+RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){
   Assert(isAtom(atom));
   NodeManager* currNM = NodeManager::currentNM();
 
@@ -260,7 +260,7 @@ RewriteResponse NextArithRewriter::preRewriteAtom(TNode atom){
   return RewriteComplete(reduction);
 }
 
-RewriteResponse NextArithRewriter::postRewrite(TNode t){
+RewriteResponse ArithRewriter::postRewrite(TNode t){
   if(isTerm(t)){
     RewriteResponse response = postRewriteTerm(t);
     if(Debug.isOn("arith::rewriter") && response.isDone()) {
@@ -279,7 +279,7 @@ RewriteResponse NextArithRewriter::postRewrite(TNode t){
   }
 }
 
-RewriteResponse NextArithRewriter::preRewrite(TNode t){
+RewriteResponse ArithRewriter::preRewrite(TNode t){
   if(isTerm(t)){
     return preRewriteTerm(t);
   }else if(isAtom(t)){
@@ -290,18 +290,18 @@ RewriteResponse NextArithRewriter::preRewrite(TNode t){
   }
 }
 
-Node NextArithRewriter::makeUnaryMinusNode(TNode n){
+Node ArithRewriter::makeUnaryMinusNode(TNode n){
   return NodeManager::currentNM()->mkNode(kind::MULT,d_constants->d_NEGATIVE_ONE_NODE,n);
 }
 
-Node NextArithRewriter::makeSubtractionNode(TNode l, TNode r){
+Node ArithRewriter::makeSubtractionNode(TNode l, TNode r){
   Node negR = makeUnaryMinusNode(r);
   Node diff = NodeManager::currentNM()->mkNode(kind::PLUS, l, negR);
 
   return diff;
 }
 
-RewriteResponse NextArithRewriter::rewriteDivByConstant(TNode t, bool pre){
+RewriteResponse ArithRewriter::rewriteDivByConstant(TNode t, bool pre){
   Assert(t.getKind()== kind::DIVISION);
 
   Node left = t[0];
diff --git a/src/theory/arith/next_arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 1fb743f71..f7ef8c0c7 100644
--- a/src/theory/arith/next_arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file next_arith_rewriter.h
+/*! \file arith_rewriter.h
  ** \verbatim
  ** Original author: taking
  ** Major contributors: mdeters
@@ -21,14 +21,14 @@
 #include "theory/theory.h"
 #include "theory/arith/normal_form.h"
 
-#ifndef __CVC4__THEORY__ARITH__REWRITER_NEXT_H
-#define __CVC4__THEORY__ARITH__REWRITER_NEXT_H
+#ifndef __CVC4__THEORY__ARITH__REWRITER_H
+#define __CVC4__THEORY__ARITH__REWRITER_H
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
-class NextArithRewriter{
+class ArithRewriter{
 private:
   ArithConstants* d_constants;
 
@@ -56,7 +56,7 @@ private:
   RewriteResponse postRewriteAtomConstantRHS(TNode t);
 
 public:
-  NextArithRewriter(ArithConstants* ac) : d_constants(ac) {}
+  ArithRewriter(ArithConstants* ac) : d_constants(ac) {}
 
   RewriteResponse preRewrite(TNode n);
   RewriteResponse postRewrite(TNode n);
@@ -71,4 +71,4 @@ private:
 }; /* namespace theory */
 }; /* namespace CVC4 */
 
-#endif /* __CVC4__THEORY__ARITH__REWRITER_NEXT_H */
+#endif /* __CVC4__THEORY__ARITH__REWRITER_H */
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index c764d0d2e..d50c48552 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -25,6 +25,7 @@
 #include "util/rational.h"
 #include "expr/node.h"
 #include "expr/attribute.h"
+#include <vector>
 #include <stdint.h>
 #include <limits>
 
@@ -55,6 +56,9 @@ inline void setArithVar(TNode x, ArithVar a){
   return x.setAttribute(ArithVarAttr(), (uint64_t)a);
 }
 
+typedef std::vector<uint64_t> ActivityMonitor;
+
+
 inline Node mkRationalNode(const Rational& q){
   return NodeManager::currentNM()->mkConst<Rational>(q);
 }
diff --git a/src/theory/arith/basic.h b/src/theory/arith/arithvar_dense_set.h
index c52e0881d..274246fbe 100644
--- a/src/theory/arith/basic.h
+++ b/src/theory/arith/arithvar_dense_set.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file basic.h
+/*! \file arithvar_dense_set.h
  ** \verbatim
  ** Original author: taking
  ** Major contributors: mdeters
@@ -17,42 +17,51 @@
  ** \todo document this file
  **/
 
+#include <vector>
+#include "theory/arith/arith_utilities.h"
 
-#include "expr/node.h"
-#include "expr/attribute.h"
 
-
-#ifndef __CVC4__THEORY__ARITH__BASIC_H
-#define __CVC4__THEORY__ARITH__BASIC_H
+#ifndef __CVC4__THEORY__ARITH__ARTIHVAR_DENSE_SET_H
+#define __CVC4__THEORY__ARITH__ARTIHVAR_DENSE_SET_H
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
-class IsBasicManager {
+class ArithVarDenseSet {
 private:
-  std::vector<bool> d_basic;
+  std::vector<bool> d_set;
 
 public:
-  IsBasicManager() : d_basic() {}
+  ArithVarDenseSet() : d_set() {}
+
+  size_t size() const {
+    return d_set.size();
+  }
+
+  void increaseSize(ArithVar max){
+    Assert(max >= size());
+    d_set.resize(max+1, false);
+  }
 
-  void init(ArithVar var, bool value){
-    Assert(var == d_basic.size());
-    d_basic.push_back(value);
+  bool isMember(ArithVar x) const{
+    return d_set[x];
   }
 
-  bool isBasic(ArithVar x) const{
-    return d_basic[x];
+  void init(ArithVar x, bool val) {
+    Assert(x >= size());
+    increaseSize(x);
+    d_set[x] = val;
   }
 
-  void makeBasic(ArithVar x){
-    Assert(!isBasic(x));
-    d_basic[x] = true;
+  void add(ArithVar x){
+    Assert(!isMember(x));
+    d_set[x] = true;
   }
 
-  void makeNonbasic(ArithVar x){
-    Assert(isBasic(x));
-    d_basic[x] = false;
+  void remove(ArithVar x){
+    Assert(isMember(x));
+    d_set[x] = false;
   }
 };
 
@@ -60,4 +69,4 @@ public:
 }; /* namespace theory */
 }; /* namespace CVC4 */
 
-#endif /* __CVC4__THEORY__ARITH__BASIC_H */
+#endif /* __CVC4__THEORY__ARITH__ARTIHVAR_DENSE_SET_H */
diff --git a/src/theory/arith/slack.h b/src/theory/arith/slack.h
deleted file mode 100644
index 87bf83e32..000000000
--- a/src/theory/arith/slack.h
+++ /dev/null
@@ -1,33 +0,0 @@
-/*********************                                                        */
-/*! \file slack.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
- **/
-
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-struct SlackAttrID;
-
-typedef expr::Attribute<SlackAttrID, Node> Slack;
-
-
-}; /* namespace arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
-
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index d6a30ac91..2490ed51b 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -108,7 +108,7 @@ void Tableau::addRow(ArithVar basicVar,
                      const std::vector<ArithVar>& variables){
 
   Assert(coeffs.size() == variables.size());
-  Assert(d_basicManager.isBasic(basicVar));
+  Assert(d_basicManager.isMember(basicVar));
 
   //The new basic variable cannot already be a basic variable
   Assert(!isActiveBasicVariable(basicVar));
@@ -126,7 +126,7 @@ void Tableau::addRow(ArithVar basicVar,
   for( ; coeffsIter != coeffsEnd; ++coeffsIter, ++ varsIter){
     ArithVar var = *varsIter;
 
-    if(d_basicManager.isBasic(var)){
+    if(d_basicManager.isMember(var)){
       if(!isActiveBasicVariable(var)){
         reinjectBasic(var);
       }
@@ -139,8 +139,8 @@ void Tableau::addRow(ArithVar basicVar,
 }
 
 void Tableau::pivot(ArithVar x_r, ArithVar x_s){
-  Assert(d_basicManager.isBasic(x_r));
-  Assert(!d_basicManager.isBasic(x_s));
+  Assert(d_basicManager.isMember(x_r));
+  Assert(!d_basicManager.isMember(x_s));
 
   Row* row_s = lookup(x_r);
   Assert(row_s->has(x_s));
@@ -150,10 +150,10 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){
   d_rowsTable[x_r] = NULL;
 
   d_activeBasicVars.erase(x_r);
-  d_basicManager.makeNonbasic(x_r);
+  d_basicManager.remove(x_r);
 
   d_activeBasicVars.insert(x_s);
-  d_basicManager.makeBasic(x_s);
+  d_basicManager.add(x_s);
 
   row_s->pivot(x_s);
 
@@ -162,7 +162,7 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){
     ArithVar basic = *basicIter;
     Row* row_k = lookup(basic);
     if(row_k->has(x_s)){
-      d_activityMonitor.increaseActivity(basic, 30);
+      d_activityMonitor[basic] += 30;
       row_k->substitute(*row_s);
     }
   }
@@ -185,7 +185,7 @@ void Tableau::updateRow(Row* row){
   for(Row::iterator i=row->begin(), endIter = row->end(); i != endIter; ){
     ArithVar var = i->first;
     ++i;
-    if(d_basicManager.isBasic(var)){
+    if(d_basicManager.isMember(var)){
       Row* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var);
 
       Assert(row_var != row);
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 88a5c2317..588b521b1 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -22,8 +22,7 @@
 #include "expr/attribute.h"
 
 #include "theory/arith/arith_utilities.h"
-#include "theory/arith/arith_activity.h"
-#include "theory/arith/basic.h"
+#include "theory/arith/arithvar_dense_set.h"
 #include "theory/arith/normal_form.h"
 
 #include <ext/hash_map>
@@ -144,14 +143,15 @@ private:
   ArithVarSet d_activeBasicVars;
   RowsTable d_rowsTable;
 
+
   ActivityMonitor& d_activityMonitor;
-  IsBasicManager& d_basicManager;
+  ArithVarDenseSet& d_basicManager;
 
 public:
   /**
    * Constructs an empty tableau.
    */
-  Tableau(ActivityMonitor &am, IsBasicManager& bm) :
+  Tableau(ActivityMonitor &am, ArithVarDenseSet& bm) :
     d_activeBasicVars(),
     d_rowsTable(),
     d_activityMonitor(am),
@@ -196,18 +196,18 @@ public:
   void printTableau();
 
   bool isEjected(ArithVar var){
-    return d_basicManager.isBasic(var) && !isActiveBasicVariable(var);
+    return d_basicManager.isMember(var) && !isActiveBasicVariable(var);
   }
 
   void ejectBasic(ArithVar basic){
-    Assert(d_basicManager.isBasic(basic));
+    Assert(d_basicManager.isMember(basic));
     Assert(isActiveBasicVariable(basic));
 
     d_activeBasicVars.erase(basic);
   }
 
   void reinjectBasic(ArithVar basic){
-    Assert(d_basicManager.isBasic(basic));
+    Assert(d_basicManager.isMember(basic));
     Assert(isEjected(basic));
 
     Row* row = lookupEjected(basic);
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index f913eda93..bd686737a 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -31,11 +31,9 @@
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/tableau.h"
-#include "theory/arith/slack.h"
-#include "theory/arith/basic.h"
-#include "theory/arith/arith_activity.h"
+#include "theory/arith/arithvar_dense_set.h"
 
-#include "theory/arith/next_arith_rewriter.h"
+#include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_propagator.h"
 
 #include "theory/arith/theory_arith.h"
@@ -52,7 +50,10 @@ using namespace CVC4::kind;
 using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
 
+struct SlackAttrID;
+typedef expr::Attribute<SlackAttrID, Node> Slack;
 
+const static uint64_t ACTIVITY_THRESHOLD = 100;
 
 TheoryArith::TheoryArith(int id, context::Context* c, OutputChannel& out) :
   Theory(id, c, out),
@@ -62,7 +63,7 @@ TheoryArith::TheoryArith(int id, context::Context* c, OutputChannel& out) :
   d_activityMonitor(),
   d_diseq(c),
   d_tableau(d_activityMonitor, d_basicManager),
-  d_nextRewriter(&d_constants),
+  d_rewriter(&d_constants),
   d_propagator(c),
   d_statistics()
 {}
@@ -133,7 +134,7 @@ bool TheoryArith::shouldEject(ArithVar var){
     return false;
   }else if(!d_partialModel.hasEverHadABound(var)){
     return true;
-  }else if(d_activityMonitor.getActivity(var) >= ActivityMonitor::ACTIVITY_THRESHOLD){
+  }else if(d_activityMonitor[var] >= ACTIVITY_THRESHOLD){
     return true;
   }
   return false;
@@ -159,7 +160,7 @@ void TheoryArith::ejectInactiveVariables(){
     //TNode var = *i;
     //ArithVar variable = asArithVar(var);
     if(shouldEject(variable)){
-      if(d_basicManager.isBasic(variable)){
+      if(d_basicManager.isMember(variable)){
         Debug("decay") << "ejecting basic " << variable << endl;;
         d_tableau.ejectBasic(variable);
       }
@@ -228,7 +229,7 @@ void TheoryArith::preRegisterTerm(TNode n) {
 
 
 void TheoryArith::checkBasicVariable(ArithVar basic){
-  Assert(d_basicManager.isBasic(basic));
+  Assert(d_basicManager.isMember(basic));
   if(!d_partialModel.assignmentIsConsistent(basic)){
     d_possiblyInconsistent.push(basic);
   }
@@ -247,8 +248,10 @@ ArithVar TheoryArith::requestArithVar(TNode x, bool basic){
 
   setArithVar(x,varX);
 
-  d_activityMonitor.initActivity(varX);
-  d_basicManager.init(varX, basic);
+  Assert(varX == d_activityMonitor.size());
+  d_activityMonitor.push_back(0);
+
+  d_basicManager.init(varX,basic);
   d_tableau.increaseSize();
 
   Debug("arith::arithvar") << x << " |-> " << varX << endl;
@@ -299,7 +302,7 @@ void TheoryArith::setupSlack(TNode left){
  */
 void TheoryArith::setupInitialValue(ArithVar x){
 
-  if(!d_basicManager.isBasic(x)){
+  if(!d_basicManager.isMember(x)){
     d_partialModel.initialize(x,d_constants.d_ZERO_DELTA);
   }else{
     //If the variable is basic, assertions may have already happened and updates
@@ -325,7 +328,7 @@ void TheoryArith::setupInitialValue(ArithVar x){
  * Computes the value of a basic variable using the current assignment.
  */
 DeltaRational TheoryArith::computeRowValue(ArithVar x, bool useSafe){
-  Assert(d_basicManager.isBasic(x));
+  Assert(d_basicManager.isMember(x));
   DeltaRational sum = d_constants.d_ZERO_DELTA;
 
   Row* row = d_tableau.lookup(x);
@@ -341,7 +344,7 @@ DeltaRational TheoryArith::computeRowValue(ArithVar x, bool useSafe){
 
 
 RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) {
-  return d_nextRewriter.preRewrite(n);
+  return d_rewriter.preRewrite(n);
 }
 
 void TheoryArith::registerTerm(TNode tn){
@@ -352,7 +355,7 @@ void TheoryArith::registerTerm(TNode tn){
 bool TheoryArith::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode original){
 
   Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
-  if(d_basicManager.isBasic(x_i) && d_tableau.isEjected(x_i)){
+  if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){
     reinjectVariable(x_i);
   }
 
@@ -371,9 +374,9 @@ bool TheoryArith::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode orig
   d_partialModel.setUpperConstraint(x_i,original);
   d_partialModel.setUpperBound(x_i, c_i);
 
-  d_activityMonitor.resetActivity(x_i);
+  d_activityMonitor[x_i] = 0;
 
-  if(!d_basicManager.isBasic(x_i)){
+  if(!d_basicManager.isMember(x_i)){
     if(d_partialModel.getAssignment(x_i) > c_i){
       update(x_i, c_i);
     }
@@ -388,7 +391,7 @@ bool TheoryArith::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode orig
 bool TheoryArith::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){
   Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
 
-  if(d_basicManager.isBasic(x_i) && d_tableau.isEjected(x_i)){
+  if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){
     reinjectVariable(x_i);
   }
 
@@ -406,9 +409,9 @@ bool TheoryArith::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode orig
 
   d_partialModel.setLowerConstraint(x_i,original);
   d_partialModel.setLowerBound(x_i, c_i);
-  d_activityMonitor.resetActivity(x_i);
+  d_activityMonitor[x_i] = 0;
 
-  if(!d_basicManager.isBasic(x_i)){
+  if(!d_basicManager.isMember(x_i)){
     if(d_partialModel.getAssignment(x_i) < c_i){
       update(x_i, c_i);
     }
@@ -424,7 +427,7 @@ bool TheoryArith::AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode o
 
   Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl;
 
-  if(d_basicManager.isBasic(x_i) && d_tableau.isEjected(x_i)){
+  if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){
     reinjectVariable(x_i);
   }
 
@@ -456,9 +459,9 @@ bool TheoryArith::AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode o
 
   d_partialModel.setUpperConstraint(x_i,original);
   d_partialModel.setUpperBound(x_i, c_i);
-  d_activityMonitor.resetActivity(x_i);
+  d_activityMonitor[x_i] = 0;
 
-  if(!d_basicManager.isBasic(x_i)){
+  if(!d_basicManager.isMember(x_i)){
     if(!(d_partialModel.getAssignment(x_i) == c_i)){
       update(x_i, c_i);
     }
@@ -469,7 +472,7 @@ bool TheoryArith::AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode o
   return false;
 }
 void TheoryArith::update(ArithVar x_i, const DeltaRational& v){
-  Assert(!d_basicManager.isBasic(x_i));
+  Assert(!d_basicManager.isMember(x_i));
   DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i);
   ++(d_statistics.d_statUpdates);
 
@@ -490,7 +493,7 @@ void TheoryArith::update(ArithVar x_i, const DeltaRational& v){
       DeltaRational  nAssignment = assignment+(diff * a_ji);
       d_partialModel.setAssignment(x_j, nAssignment);
 
-      d_activityMonitor.increaseActivity(x_j, 1);
+      d_activityMonitor[x_j] += 1;
 
       checkBasicVariable(x_j);
     }
@@ -532,7 +535,7 @@ void TheoryArith::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){
       DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj);
       d_partialModel.setAssignment(x_k, nextAssignment);
 
-      d_activityMonitor.increaseActivity(x_j, 1);
+      d_activityMonitor[x_j] += 1;
 
       checkBasicVariable(x_k);
     }
@@ -556,7 +559,7 @@ ArithVar TheoryArith::selectSmallestInconsistentVar(){
   while(!d_possiblyInconsistent.empty()){
     ArithVar var = d_possiblyInconsistent.top();
     Debug("arith_update") << "possiblyInconsistent var" << var << endl;
-    if(d_basicManager.isBasic(var)){
+    if(d_basicManager.isMember(var)){
       if(!d_partialModel.assignmentIsConsistent(var)){
         return var;
       }
@@ -834,7 +837,7 @@ void TheoryArith::check(Effort level){
     for (ArithVar i = 0; i < d_variables.size(); ++ i) {
       Debug("arith::print_model") << d_variables[i] << " : " <<
         d_partialModel.getAssignment(i);
-      if(d_basicManager.isBasic(i))
+      if(d_basicManager.isMember(i))
         Debug("arith::print_model") << " (basic)";
       Debug("arith::print_model") << endl;
     }
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 5d00c4cc8..5395327c0 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -27,11 +27,10 @@
 #include "expr/node.h"
 
 #include "theory/arith/arith_utilities.h"
-#include "theory/arith/basic.h"
-#include "theory/arith/arith_activity.h"
+#include "theory/arith/arithvar_dense_set.h"
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/tableau.h"
-#include "theory/arith/next_arith_rewriter.h"
+#include "theory/arith/arith_rewriter.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/arith_propagator.h"
 
@@ -80,7 +79,7 @@ private:
    */
   ArithPartialModel d_partialModel;
 
-  IsBasicManager d_basicManager;
+  ArithVarDenseSet d_basicManager;
   ActivityMonitor d_activityMonitor;
 
   /**
@@ -96,7 +95,7 @@ private:
   /**
    * The rewriter module for arithmetic.
    */
-  NextArithRewriter d_nextRewriter;
+  ArithRewriter d_rewriter;
 
   ArithUnatePropagator d_propagator;
 
@@ -113,7 +112,7 @@ public:
    * Plug in old rewrite to the new (pre,post)rewrite interface.
    */
   RewriteResponse postRewrite(TNode n, bool topLevel) {
-    return d_nextRewriter.postRewrite(n);
+    return d_rewriter.postRewrite(n);
   }
 
   /**