This commit is the promised clean up after removing row ejection.

5 files changed, 20 insertions, 170 deletions

diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 6e7685570..4d417659e 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -17,8 +17,6 @@ SimplexDecisionProcedure::Statistics::Statistics():
   d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0),
   d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0),
   d_statUpdateConflicts("theory::arith::UpdateConflicts", 0),
-  d_statEjections("theory::arith::Ejections", 0),
-  d_statUnEjections("theory::arith::UnEjections", 0),
   d_statEarlyConflicts("theory::arith::EarlyConflicts", 0),
   d_statEarlyConflictImprovements("theory::arith::EarlyConflictImprovements", 0),
   d_selectInitialConflictTime("theory::arith::selectInitialConflictTime"),
@@ -31,8 +29,6 @@ SimplexDecisionProcedure::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_statAssertUpperConflicts);
   StatisticsRegistry::registerStat(&d_statAssertLowerConflicts);
   StatisticsRegistry::registerStat(&d_statUpdateConflicts);
-  StatisticsRegistry::registerStat(&d_statEjections);
-  StatisticsRegistry::registerStat(&d_statUnEjections);
   StatisticsRegistry::registerStat(&d_statEarlyConflicts);
   StatisticsRegistry::registerStat(&d_statEarlyConflictImprovements);
   StatisticsRegistry::registerStat(&d_selectInitialConflictTime);
@@ -48,8 +44,6 @@ SimplexDecisionProcedure::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts);
   StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts);
   StatisticsRegistry::unregisterStat(&d_statUpdateConflicts);
-  StatisticsRegistry::unregisterStat(&d_statEjections);
-  StatisticsRegistry::unregisterStat(&d_statUnEjections);
   StatisticsRegistry::unregisterStat(&d_statEarlyConflicts);
   StatisticsRegistry::unregisterStat(&d_statEarlyConflictImprovements);
   StatisticsRegistry::unregisterStat(&d_selectInitialConflictTime);
@@ -59,62 +53,10 @@ SimplexDecisionProcedure::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_pivotTime);
 }
 
-
-/*
-void SimplexDecisionProcedure::ejectInactiveVariables(){
-  return; //die die die
-
-  for(ArithVarSet::iterator i = d_tableau.begin(), end = d_tableau.end(); i != end;){
-    ArithVar variable = *i;
-    ++i;
-    Assert(d_basicManager.isMember(variable));
-
-    if(d_basicManager.isMember(variable) && shouldEject(variable)){
-      Debug("decay") << "ejecting basic " << variable << endl;
-      ++(d_statistics.d_statEjections);
-      d_tableau.ejectBasic(variable);
-    }
-  }
-}
-*/
-
-/*
-void SimplexDecisionProcedure::reinjectVariable(ArithVar x){
-  ++(d_statistics.d_statUnEjections);
-
-  d_tableau.reinjectBasic(x);
-
-  DeltaRational safeAssignment = computeRowValue(x, true);
-  DeltaRational assignment = computeRowValue(x, false);
-  d_partialModel.setAssignment(x,safeAssignment,assignment);
-}
-*/
-
-/*
-bool SimplexDecisionProcedure::shouldEject(ArithVar var){
-  if(d_partialModel.hasEitherBound(var)){
-    return false;
-  }else if(d_tableau.isEjected(var)) {
-    return false;
-  }else if(!d_partialModel.hasEverHadABound(var)){
-    return true;
-  }else if(d_activityMonitor[var] >= ACTIVITY_THRESHOLD){
-    return false;
-  }
-  return false;
-}
-*/
-
 /* procedure AssertLower( x_i >= c_i ) */
 bool SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){
   Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
 
-  /*
-  if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){
-    reinjectVariable(x_i);
-  }
-  */
-
   if(d_partialModel.belowLowerBound(x_i, c_i, false)){
     return false; //sat
   }
@@ -145,11 +87,6 @@ bool SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_
 bool SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode original){
 
   Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
-  /*
-  if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){
-    reinjectVariable(x_i);
-  }
-  */
 
   if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){ // \upperbound(x_i) <= c_i
     return false; //sat
@@ -183,12 +120,6 @@ bool SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational&
 
   Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl;
 
-  /*
-  if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){
-    reinjectVariable(x_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(d_partialModel.belowLowerBound(x_i, c_i, false) &&
@@ -544,7 +475,6 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){
   Debug("arith") << "updateInconsistentVars" << endl;
 
   uint32_t iteratationNum = 0;
-  //static const int EJECT_FREQUENCY = 10;
 
   while(!d_pivotStage || iteratationNum <= d_numVariables){
     if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
@@ -557,10 +487,6 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){
     }
 
     ++iteratationNum;
-    /*
-    if(iteratationNum % EJECT_FREQUENCY == 0)
-      ejectInactiveVariables();
-    */
 
     DeltaRational beta_i = d_partialModel.getAssignment(x_i);
     ArithVar x_j = ARITHVAR_SENTINEL;
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index e02e001e3..abd5cb5e6 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -170,16 +170,12 @@ private:
   Node generateConflictBelow(ArithVar conflictVar);
 
 public:
-  /** Checks to make sure the assignment is consistent with the tableau. */
+  /**
+   * Checks to make sure the assignment is consistent with the tableau.
+   * This code is for debugging.
+   */
   void checkTableau();
 
-private:
-  //bool shouldEject(ArithVar var);
-  //void ejectInactiveVariables();
-
-public:
-  //void reinjectVariable(ArithVar x);
-
   /**
    * Computes the value of a basic variable using the assignments
    * of the values of the variables in the basic variable's row tableau.
@@ -200,17 +196,16 @@ private:
    */
   Node checkBasicForConflict(ArithVar b);
 
-  bool d_foundAConflict;
-  unsigned d_pivotsSinceConflict;
+  bool d_foundAConflict; // This field is used for statistics keeping ONLY!
+  unsigned d_pivotsSinceConflict; // This field is used for statistics keeping ONLY!
 
   /** These fields are designed to be accessable to TheoryArith methods. */
   class Statistics {
   public:
-    IntStat d_statPivots, d_statUpdates, d_statAssertUpperConflicts;
-    IntStat d_statAssertLowerConflicts, d_statUpdateConflicts;
-
-    IntStat d_statEjections, d_statUnEjections;
+    IntStat d_statPivots, d_statUpdates;
 
+    IntStat d_statAssertUpperConflicts, d_statAssertLowerConflicts;
+    IntStat d_statUpdateConflicts;
     IntStat d_statEarlyConflicts, d_statEarlyConflictImprovements;
 
     TimerStat d_selectInitialConflictTime;
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index 75363af7f..5f142fe8a 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -46,12 +46,6 @@ void Tableau::addRow(ArithVar basicVar,
     ArithVar var = *varsIter;
 
     if(d_basicManager.isMember(var)){
-      /*
-      if(!isActiveBasicVariable(var)){
-        reinjectBasic(var);
-      }
-      Assert(isActiveBasicVariable(var));
-      */
       Assert(d_activeBasicVars.isMember(var));
 
       ReducedRowVector& row_var = lookup(var);
@@ -117,23 +111,3 @@ void Tableau::printTableau(){
     }
   }
 }
-
-
-/*
-void Tableau::updateRow(ReducedRowVector* row){
-  ArithVar basic = row->basic();
-  for(ReducedRowVector::NonZeroIterator i=row->beginNonZero(), endIter = row->endNonZero(); i != endIter; ){
-    ArithVar var = i->first;
-    ++i;
-    if(var != basic && d_basicManager.isMember(var)){
-      ReducedRowVector* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var);
-
-      Assert(row_var != row);
-      row->substitute(*row_var);
-
-      i = row->beginNonZero();
-      endIter = row->endNonZero();
-    }
-  }
-}
-*/
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index f74e662cf..bd30dc13e 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -79,22 +79,23 @@ public:
     return *(d_rowsTable[var]);
   }
 
-  /*
-private:
-  ReducedRowVector* lookupEjected(ArithVar var){
-    Assert(isEjected(var));
-    return d_rowsTable[var];
-  }
-  */
 public:
-
-
   uint32_t getRowCount(ArithVar x){
     Assert(x < d_rowCount.size());
     return d_rowCount[x];
   }
 
-
+  /**
+   * Adds a row to the tableau.
+   * The new row is equivalent to:
+   *   basicVar = \sum_i coeffs[i] * variables[i]
+   * preconditions:
+   *   basicVar is already declared to be basic
+   *   basicVar does not have a row associated with it in the tableau.
+   *
+   * Note: each variables[i] does not have to be non-basic.
+   * Pivoting will be mimicked if it is basic.
+   */
   void addRow(ArithVar basicVar,
               const std::vector<Rational>& coeffs,
               const std::vector<ArithVar>& variables);
@@ -109,43 +110,7 @@ public:
 
   void printTableau();
 
-  /*
-  bool isEjected(ArithVar var){
-    return d_basicManager.isMember(var) && !isActiveBasicVariable(var);
-  }
-  */
-
   ReducedRowVector* removeRow(ArithVar basic);
-
-  /*
-  void ejectBasic(ArithVar basic){
-    Assert(d_basicManager.isMember(basic));
-    Assert(isActiveBasicVariable(basic));
-
-    d_activeBasicVars.remove(basic);
-  }
-  */
-
-  /*
-  void reinjectBasic(ArithVar basic){
-    AlwaysAssert(false);
-
-    Assert(d_basicManager.isMember(basic));
-    Assert(isEjected(basic));
-
-    ReducedRowVector* row = lookupEjected(basic);
-    d_activeBasicVars.add(basic);
-    updateRow(row);
-  }
-  */
-private:
-  /*
-  inline bool isActiveBasicVariable(ArithVar var){
-    return d_activeBasicVars.isMember(var);
-  }
-  */
-
-  void updateRow(ReducedRowVector* row);
 };
 
 }; /* namespace arith  */
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index ca3b76410..dbfa86a98 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -507,11 +507,6 @@ void TheoryArith::check(Effort effortLevel){
         TNode rhs = eq[1];
         Assert(rhs.getKind() == CONST_RATIONAL);
         ArithVar lhsVar = determineLeftVariable(eq, kind::EQUAL);
-        /*
-        if(d_tableau.isEjected(lhsVar)){
-          d_simplex.reinjectVariable(lhsVar);
-        }
-        */
         DeltaRational lhsValue = d_partialModel.getAssignment(lhsVar);
         DeltaRational rhsValue = determineRightConstant(eq, kind::EQUAL);
         if (lhsValue == rhsValue) {
@@ -579,11 +574,6 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
   switch(n.getKind()) {
   case kind::VARIABLE: {
     ArithVar var = asArithVar(n);
-    /*
-    if(d_tableau.isEjected(var)){
-      d_simplex.reinjectVariable(var);
-    }
-    */
 
     DeltaRational drat = d_partialModel.getAssignment(var);
     const Rational& delta = d_partialModel.getDelta();