Changes:

- The Tableau is now in charge of managing what variables are basic in a unified manner. Specifically, TheoryArith::d_basicManager was merged into Tableau::d_basicVariables.

6 files changed, 44 insertions, 52 deletions

diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 4d417659e..0f4f27a76 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -72,7 +72,7 @@ bool SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_
   d_partialModel.setLowerConstraint(x_i,original);
   d_partialModel.setLowerBound(x_i, c_i);
 
-  if(!d_basicManager.isMember(x_i)){
+  if(!d_tableau.isBasic(x_i)){
     if(d_partialModel.getAssignment(x_i) < c_i){
       update(x_i, c_i);
     }
@@ -103,7 +103,7 @@ bool SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_
   d_partialModel.setUpperConstraint(x_i,original);
   d_partialModel.setUpperBound(x_i, c_i);
 
-  if(!d_basicManager.isMember(x_i)){
+  if(!d_tableau.isBasic(x_i)){
     if(d_partialModel.getAssignment(x_i) > c_i){
       update(x_i, c_i);
     }
@@ -149,7 +149,7 @@ bool SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational&
   d_partialModel.setUpperConstraint(x_i,original);
   d_partialModel.setUpperBound(x_i, c_i);
 
-  if(!d_basicManager.isMember(x_i)){
+  if(!d_tableau.isBasic(x_i)){
     if(!(d_partialModel.getAssignment(x_i) == c_i)){
       update(x_i, c_i);
     }
@@ -161,7 +161,7 @@ bool SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational&
 }
 
 void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){
-  Assert(!d_basicManager.isMember(x_i));
+  Assert(!d_tableau.isBasic(x_i));
   DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i);
   ++(d_statistics.d_statUpdates);
 
@@ -294,7 +294,7 @@ ArithVar SimplexDecisionProcedure::selectSmallestInconsistentVar(){
     while(!d_griggioRuleQueue.empty()){
       ArithVar var = d_griggioRuleQueue.top().first;
       Debug("arith_update") << "possiblyInconsistentGriggio var" << var << endl;
-      if(d_basicManager.isMember(var)){
+      if(d_tableau.isBasic(var)){
         if(!d_partialModel.assignmentIsConsistent(var)){
           return var;
         }
@@ -305,7 +305,7 @@ ArithVar SimplexDecisionProcedure::selectSmallestInconsistentVar(){
     while(!d_possiblyInconsistent.empty()){
       ArithVar var = d_possiblyInconsistent.top();
       Debug("arith_update") << "possiblyInconsistent var" << var << endl;
-      if(d_basicManager.isMember(var)){
+      if(d_tableau.isBasic(var)){
         if(!d_partialModel.assignmentIsConsistent(var)){
           return var;
         }
@@ -392,7 +392,7 @@ Node SimplexDecisionProcedure::selectInitialConflict() {
 
   while( !d_griggioRuleQueue.empty()){
     ArithVar var = d_griggioRuleQueue.top().first;
-    if(d_basicManager.isMember(var)){
+    if(d_tableau.isBasic(var)){
       if(!d_partialModel.assignmentIsConsistent(var)){
         init.push_back( d_griggioRuleQueue.top());
       }
@@ -451,7 +451,7 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){
 
 Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){
 
-  Assert(d_basicManager.isMember(basic));
+  Assert(d_tableau.isBasic(basic));
   const DeltaRational& beta = d_partialModel.getAssignment(basic);
 
   if(d_partialModel.belowLowerBound(basic, beta, true)){
@@ -520,7 +520,7 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){
   if(d_pivotStage && iteratationNum >= d_numVariables){
     while(!d_griggioRuleQueue.empty()){
       ArithVar var = d_griggioRuleQueue.top().first;
-      if(d_basicManager.isMember(var)){
+      if(d_tableau.isBasic(var)){
         d_possiblyInconsistent.push(var);
       }
       d_griggioRuleQueue.pop();
@@ -623,7 +623,7 @@ Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){
  * Computes the value of a basic variable using the current assignment.
  */
 DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe){
-  Assert(d_basicManager.isMember(x));
+  Assert(d_tableau.isBasic(x));
   DeltaRational sum = d_constants.d_ZERO_DELTA;
 
   ReducedRowVector& row = d_tableau.lookup(x);
@@ -641,7 +641,7 @@ DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe
 
 
 void SimplexDecisionProcedure::checkBasicVariable(ArithVar basic){
-  Assert(d_basicManager.isMember(basic));
+  Assert(d_tableau.isBasic(basic));
   if(!d_partialModel.assignmentIsConsistent(basic)){
     if(d_pivotStage){
       const DeltaRational& beta = d_partialModel.getAssignment(basic);
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index abd5cb5e6..84d7cdcbb 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -55,8 +55,6 @@ private:
    */
   ArithPartialModel& d_partialModel;
 
-  ArithVarSet& d_basicManager;
-
   OutputChannel* d_out;
 
   Tableau& d_tableau;
@@ -68,13 +66,11 @@ private:
 public:
   SimplexDecisionProcedure(const ArithConstants& constants,
                            ArithPartialModel& pm,
-                           ArithVarSet& bm,
                            OutputChannel* out,
                            Tableau& tableau) :
     d_possiblyInconsistent(),
     d_constants(constants),
     d_partialModel(pm),
-    d_basicManager(bm),
     d_out(out),
     d_tableau(tableau),
     d_numVariables(0),
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index 5ba173eb6..d318a70e6 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -25,8 +25,8 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
 
 Tableau::~Tableau(){
-  while(!d_activeBasicVars.empty()){
-    ArithVar curr = *(d_activeBasicVars.begin());
+  while(!d_basicVariables.empty()){
+    ArithVar curr = *(d_basicVariables.begin());
     ReducedRowVector* vec = removeRow(curr);
     delete vec;
   }
@@ -37,11 +37,10 @@ void Tableau::addRow(ArithVar basicVar,
                      const std::vector<ArithVar>& variables){
 
   Assert(coeffs.size() == variables.size());
-  Assert(d_basicManager.isMember(basicVar));
 
   //The new basic variable cannot already be a basic variable
-  Assert(!d_activeBasicVars.isMember(basicVar));
-  d_activeBasicVars.add(basicVar);
+  Assert(!d_basicVariables.isMember(basicVar));
+  d_basicVariables.add(basicVar);
   ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount);
   d_rowsTable[basicVar] = row_current;
 
@@ -53,9 +52,7 @@ void Tableau::addRow(ArithVar basicVar,
   for( ; varsIter != varsEnd; ++varsIter){
     ArithVar var = *varsIter;
 
-    if(d_basicManager.isMember(var)){
-      Assert(d_activeBasicVars.isMember(var));
-
+    if(d_basicVariables.isMember(var)){
       ReducedRowVector& row_var = lookup(var);
       row_current->substitute(row_var);
     }
@@ -63,20 +60,19 @@ void Tableau::addRow(ArithVar basicVar,
 }
 
 ReducedRowVector* Tableau::removeRow(ArithVar basic){
-  Assert(d_basicManager.isMember(basic));
-  Assert(d_activeBasicVars.isMember(basic));
+  Assert(d_basicVariables.isMember(basic));
 
   ReducedRowVector* row = d_rowsTable[basic];
 
-  d_activeBasicVars.remove(basic);
+  d_basicVariables.remove(basic);
   d_rowsTable[basic] = NULL;
 
   return row;
 }
 
 void Tableau::pivot(ArithVar x_r, ArithVar x_s){
-  Assert(d_basicManager.isMember(x_r));
-  Assert(!d_basicManager.isMember(x_s));
+  Assert(d_basicVariables.isMember(x_r));
+  Assert(!d_basicVariables.isMember(x_s));
 
   Debug("tableau") << "Tableau::pivot(" <<  x_r <<", " <<x_s <<")"  << endl;
 
@@ -88,11 +84,9 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){
   d_rowsTable[x_s] = row_s;
   d_rowsTable[x_r] = NULL;
 
-  d_activeBasicVars.remove(x_r);
-  d_basicManager.remove(x_r);
+  d_basicVariables.remove(x_r);
 
-  d_activeBasicVars.add(x_s);
-  d_basicManager.add(x_s);
+  d_basicVariables.add(x_s);
 
   row_s->pivot(x_s);
 
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 433f6472f..32c2986e3 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -42,10 +42,9 @@ private:
 
   typedef std::vector< ReducedRowVector* > RowsTable;
 
-  ArithVarSet d_activeBasicVars;
   RowsTable d_rowsTable;
 
-  ArithVarSet& d_basicManager;
+  ArithVarSet d_basicVariables;
 
   std::vector<uint32_t> d_rowCount;
 
@@ -53,29 +52,33 @@ public:
   /**
    * Constructs an empty tableau.
    */
-  Tableau(ArithVarSet& bm) :
-    d_activeBasicVars(),
+  Tableau() :
     d_rowsTable(),
-    d_basicManager(bm)
+    d_basicVariables(),
+    d_rowCount()
   {}
   ~Tableau();
 
   void increaseSize(){
-    d_activeBasicVars.increaseSize();
+    d_basicVariables.increaseSize();
     d_rowsTable.push_back(NULL);
     d_rowCount.push_back(0);
   }
 
+  bool isBasic(ArithVar v) const {
+    return d_basicVariables.isMember(v);
+  }
+
   ArithVarSet::iterator begin(){
-    return d_activeBasicVars.begin();
+    return d_basicVariables.begin();
   }
 
   ArithVarSet::iterator end(){
-    return d_activeBasicVars.end();
+    return d_basicVariables.end();
   }
 
   ReducedRowVector& lookup(ArithVar var){
-    Assert(d_activeBasicVars.isMember(var));
+    Assert(d_basicVariables.isMember(var));
     Assert(d_rowsTable[var] != NULL);
     return *(d_rowsTable[var]);
   }
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 9fbec23ac..4e84c85db 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -57,12 +57,11 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
   Theory(THEORY_ARITH, c, out),
   d_constants(NodeManager::currentNM()),
   d_partialModel(c),
-  d_basicManager(),
   d_userVariables(),
   d_diseq(c),
-  d_tableau(d_basicManager),
+  d_tableau(),
   d_propagator(c, out),
-  d_simplex(d_constants, d_partialModel, d_basicManager,  d_out, d_tableau),
+  d_simplex(d_constants, d_partialModel, d_out, d_tableau),
   d_statistics()
 {}
 
@@ -261,7 +260,7 @@ ArithVar TheoryArith::requestArithVar(TNode x, bool basic){
 
   setArithVar(x,varX);
 
-  d_basicManager.init(varX,basic);
+  //d_basicManager.init(varX,basic);
   d_userVariables.init(varX, !basic);
   d_tableau.increaseSize();
 
@@ -316,7 +315,7 @@ void TheoryArith::setupSlack(TNode left){
  */
 void TheoryArith::setupInitialValue(ArithVar x){
 
-  if(!d_basicManager.isMember(x)){
+  if(!d_tableau.isBasic(x)){
     d_partialModel.initialize(x,d_constants.d_ZERO_DELTA);
   }else{
     //If the variable is basic, assertions may have already happened and updates
@@ -542,7 +541,7 @@ void TheoryArith::check(Effort effortLevel){
     for (ArithVar i = 0; i < d_variables.size(); ++ i) {
       Debug("arith::print_model") << d_variables[i] << " : " <<
         d_partialModel.getAssignment(i);
-      if(d_basicManager.isMember(i))
+      if(d_tableau.isBasic(i))
         Debug("arith::print_model") << " (basic)";
       Debug("arith::print_model") << endl;
     }
@@ -676,7 +675,7 @@ void TheoryArith::permanentlyRemoveVariable(ArithVar v){
 
   bool noRow = false;
 
-  if(!d_basicManager.isMember(v)){
+  if(!d_tableau.isBasic(v)){
     ArithVar basic = findShortestBasicRow(v);
 
     if(basic == ARITHVAR_SENTINEL){
@@ -687,9 +686,8 @@ void TheoryArith::permanentlyRemoveVariable(ArithVar v){
     }
   }
 
-  if(d_basicManager.isMember(v)){
+  if(d_tableau.isBasic(v)){
     Assert(!noRow);
-    Assert(d_basicManager.isMember(v));
 
     //remove the row from the tableau
     ReducedRowVector* row  = d_tableau.removeRow(v);
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index efd1adde4..60d24708c 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -89,7 +89,9 @@ private:
    */
   ArithPartialModel d_partialModel;
 
-  ArithVarSet d_basicManager;
+  /**
+   * Set of ArithVars that were introduced via preregisteration.
+   */
   ArithVarSet d_userVariables;
 
   /**
@@ -100,7 +102,6 @@ private:
 
   inline bool hasArithVar(TNode x) const {
     return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end();
-    //return x.hasAttribute(ArithVarAttr());
   }
 
   inline ArithVar asArithVar(TNode x) const{