Row ejection is now completely disabled. Another commit cleaning this one up will follow shortly.

5 files changed, 106 insertions, 55 deletions

diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index f7e3c112c..9e3ba726a 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -60,6 +60,7 @@ SimplexDecisionProcedure::Statistics::~Statistics(){
 }
 
 
+/*
 void SimplexDecisionProcedure::ejectInactiveVariables(){
   return; //die die die
 
@@ -75,7 +76,9 @@ void SimplexDecisionProcedure::ejectInactiveVariables(){
     }
   }
 }
+*/
 
+/*
 void SimplexDecisionProcedure::reinjectVariable(ArithVar x){
   ++(d_statistics.d_statUnEjections);
 
@@ -85,7 +88,9 @@ void SimplexDecisionProcedure::reinjectVariable(ArithVar x){
   DeltaRational assignment = computeRowValue(x, false);
   d_partialModel.setAssignment(x,safeAssignment,assignment);
 }
+*/
 
+/*
 bool SimplexDecisionProcedure::shouldEject(ArithVar var){
   if(d_partialModel.hasEitherBound(var)){
     return false;
@@ -98,14 +103,17 @@ bool SimplexDecisionProcedure::shouldEject(ArithVar var){
   }
   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
@@ -138,9 +146,11 @@ 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
@@ -176,9 +186,11 @@ 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.
@@ -234,10 +246,10 @@ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){
       basicIter != d_tableau.end();
       ++basicIter){
     ArithVar x_j = *basicIter;
-    ReducedRowVector* row_j = d_tableau.lookup(x_j);
+    ReducedRowVector& row_j = d_tableau.lookup(x_j);
 
-    if(row_j->has(x_i)){
-      const Rational& a_ji = row_j->lookup(x_i);
+    if(row_j.has(x_i)){
+      const Rational& a_ji = row_j.lookup(x_i);
 
       const DeltaRational& assignment = d_partialModel.getAssignment(x_j);
       DeltaRational  nAssignment = assignment+(diff * a_ji);
@@ -263,9 +275,9 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR
 
   if(Debug.isOn("arith::pivotAndUpdate")){
     Debug("arith::pivotAndUpdate") << "x_i " << "|->" << x_j << endl;
-    ReducedRowVector* row_k = d_tableau.lookup(x_i);
-    for(ReducedRowVector::NonZeroIterator varIter = row_k->beginNonZero();
-        varIter != row_k->endNonZero();
+    ReducedRowVector& row_k = d_tableau.lookup(x_i);
+    for(ReducedRowVector::NonZeroIterator varIter = row_k.beginNonZero();
+        varIter != row_k.endNonZero();
         ++varIter){
 
       ArithVar var = varIter->first;
@@ -285,8 +297,8 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR
   }
 
 
-  ReducedRowVector* row_i = d_tableau.lookup(x_i);
-  const Rational& a_ij = row_i->lookup(x_j);
+  ReducedRowVector& row_i = d_tableau.lookup(x_i);
+  const Rational& a_ij = row_i.lookup(x_j);
 
 
   const DeltaRational& betaX_i = d_partialModel.getAssignment(x_i);
@@ -300,14 +312,13 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR
   DeltaRational tmp = d_partialModel.getAssignment(x_j) + theta;
   d_partialModel.setAssignment(x_j, tmp);
 
-  for(ArithVarSet::iterator basicIter = d_tableau.begin();
-      basicIter != d_tableau.end();
-      ++basicIter){
+  ArithVarSet::iterator basicIter = d_tableau.begin(), end = d_tableau.end();
+  for(; basicIter != end; ++basicIter){
     ArithVar x_k = *basicIter;
-    ReducedRowVector* row_k = d_tableau.lookup(x_k);
+    ReducedRowVector& row_k = d_tableau.lookup(x_k);
 
-    if(x_k != x_i && row_k->has(x_j)){
-      const Rational& a_kj = row_k->lookup(x_j);
+    if(x_k != x_i && row_k.has(x_j)){
+      const Rational& a_kj = row_k.lookup(x_j);
       DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj);
       d_partialModel.setAssignment(x_k, nextAssignment);
 
@@ -384,12 +395,12 @@ ArithVar SimplexDecisionProcedure::selectSmallestInconsistentVar(){
 
 template <bool above>
 ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){
-  ReducedRowVector* row_i = d_tableau.lookup(x_i);
+  ReducedRowVector& row_i = d_tableau.lookup(x_i);
 
   ArithVar slack = ARITHVAR_SENTINEL;
   uint32_t numRows = std::numeric_limits<uint32_t>::max();
 
-  for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero();
+  for(ReducedRowVector::NonZeroIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero();
       nbi != end; ++nbi){
     ArithVar nonbasic = getArithVar(*nbi);
     if(nonbasic == x_i) continue;
@@ -541,7 +552,7 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){
   Debug("arith") << "updateInconsistentVars" << endl;
 
   uint32_t iteratationNum = 0;
-  static const int EJECT_FREQUENCY = 10;
+  //static const int EJECT_FREQUENCY = 10;
 
   while(!d_pivotStage || iteratationNum <= d_numVariables){
     if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
@@ -554,8 +565,10 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){
     }
 
     ++iteratationNum;
+    /*
     if(iteratationNum % EJECT_FREQUENCY == 0)
       ejectInactiveVariables();
+    */
 
     DeltaRational beta_i = d_partialModel.getAssignment(x_i);
     ArithVar x_j = ARITHVAR_SENTINEL;
@@ -605,7 +618,7 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){
 
 Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){
 
-  ReducedRowVector* row_i = d_tableau.lookup(conflictVar);
+  ReducedRowVector& row_i = d_tableau.lookup(conflictVar);
 
   NodeBuilder<> nb(kind::AND);
   TNode bound = d_partialModel.getUpperConstraint(conflictVar);
@@ -617,8 +630,10 @@ Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){
 
   nb << bound;
 
-  for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero();
-      nbi != end; ++nbi){
+  typedef ReducedRowVector::NonZeroIterator RowIterator;
+  RowIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero();
+
+  for(; nbi != end; ++nbi){
     ArithVar nonbasic = getArithVar(*nbi);
     if(nonbasic == conflictVar) continue;
 
@@ -645,7 +660,7 @@ Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){
 }
 
 Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){
-  ReducedRowVector* row_i = d_tableau.lookup(conflictVar);
+  ReducedRowVector& row_i = d_tableau.lookup(conflictVar);
 
   NodeBuilder<> nb(kind::AND);
   TNode bound = d_partialModel.getLowerConstraint(conflictVar);
@@ -656,7 +671,9 @@ Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){
                  << " " << bound << endl;
   nb << bound;
 
-  for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero(); nbi != end; ++nbi){
+  typedef ReducedRowVector::NonZeroIterator RowIterator;
+  RowIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero();
+  for(; nbi != end; ++nbi){
     ArithVar nonbasic = getArithVar(*nbi);
     if(nonbasic == conflictVar) continue;
 
@@ -691,11 +708,11 @@ DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe
   Assert(d_basicManager.isMember(x));
   DeltaRational sum = d_constants.d_ZERO_DELTA;
 
-  ReducedRowVector* row = d_tableau.lookup(x);
-  for(ReducedRowVector::NonZeroIterator i = row->beginNonZero(), end = row->endNonZero();
+  ReducedRowVector& row = d_tableau.lookup(x);
+  for(ReducedRowVector::NonZeroIterator i = row.beginNonZero(), end = row.endNonZero();
       i != end;++i){
     ArithVar nonbasic = getArithVar(*i);
-    if(nonbasic == row->basic()) continue;
+    if(nonbasic == row.basic()) continue;
     const Rational& coeff = getCoefficient(*i);
 
     const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic, useSafe);
@@ -732,11 +749,11 @@ void SimplexDecisionProcedure::checkTableau(){
   for(ArithVarSet::iterator basicIter = d_tableau.begin();
       basicIter != d_tableau.end(); ++basicIter){
     ArithVar basic = *basicIter;
-    ReducedRowVector* row_k = d_tableau.lookup(basic);
+    ReducedRowVector& row_k = d_tableau.lookup(basic);
     DeltaRational sum;
     Debug("paranoid:check_tableau") << "starting row" << basic << endl;
-    for(ReducedRowVector::NonZeroIterator nonbasicIter = row_k->beginNonZero();
-        nonbasicIter != row_k->endNonZero();
+    for(ReducedRowVector::NonZeroIterator nonbasicIter = row_k.beginNonZero();
+        nonbasicIter != row_k.endNonZero();
         ++nonbasicIter){
       ArithVar nonbasic = nonbasicIter->first;
       if(basic == nonbasic) continue;
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 587f468e0..7589e7936 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -178,11 +178,11 @@ public:
   void checkTableau();
 
 private:
-  bool shouldEject(ArithVar var);
-  void ejectInactiveVariables();
+  //bool shouldEject(ArithVar var);
+  //void ejectInactiveVariables();
 
 public:
-  void reinjectVariable(ArithVar x);
+  //void reinjectVariable(ArithVar x);
 
   /**
    * Computes the value of a basic variable using the assignments
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index 1cf6d07cd..95ea166af 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -32,41 +32,54 @@ void Tableau::addRow(ArithVar basicVar,
   Assert(d_basicManager.isMember(basicVar));
 
   //The new basic variable cannot already be a basic variable
-  Assert(!isActiveBasicVariable(basicVar));
+  Assert(!d_activeBasicVars.isMember(basicVar));
   d_activeBasicVars.add(basicVar);
   ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount);
   d_rowsTable[basicVar] = row_current;
 
   //A variable in the row may have been made non-basic already.
   //If this is the case we fake pivoting this variable
-  vector<Rational>::const_iterator coeffsIter = coeffs.begin();
-  vector<Rational>::const_iterator coeffsEnd = coeffs.end();
-
   vector<ArithVar>::const_iterator varsIter = variables.begin();
+  vector<ArithVar>::const_iterator varsEnd = variables.end();
 
-  for( ; coeffsIter != coeffsEnd; ++coeffsIter, ++ varsIter){
+  for( ; varsIter != varsEnd; ++varsIter){
     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);
-      row_current->substitute(*row_var);
+      ReducedRowVector& row_var = lookup(var);
+      row_current->substitute(row_var);
     }
   }
 }
 
+ReducedRowVector* Tableau::removeRow(ArithVar basic){
+  Assert(d_basicManager.isMember(basic));
+  Assert(d_activeBasicVars.isMember(basic));
+
+  ReducedRowVector* row = d_rowsTable[basic];
+
+  d_activeBasicVars.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));
 
-  Debug("tableau") << "Tableau::pivot("
-                   <<  x_r <<", " <<x_s <<")"  << endl;
+  Debug("tableau") << "Tableau::pivot(" <<  x_r <<", " <<x_s <<")"  << endl;
 
-  ReducedRowVector* row_s = lookup(x_r);
+  ReducedRowVector* row_s = d_rowsTable[x_r];
+  Assert(row_s != NULL);
   Assert(row_s->has(x_s));
 
   //Swap x_r and x_s in d_activeRows
@@ -86,10 +99,10 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){
     ArithVar basic = *basicIter;
     if(basic == x_s) continue;
 
-    ReducedRowVector* row_k = lookup(basic);
-    if(row_k->has(x_s)){
+    ReducedRowVector& row_k = lookup(basic);
+    if(row_k.has(x_s)){
       d_activityMonitor[basic] += 30;
-      row_k->substitute(*row_s);
+      row_k.substitute(*row_s);
     }
   }
 }
@@ -107,6 +120,7 @@ void Tableau::printTableau(){
 }
 
 
+/*
 void Tableau::updateRow(ReducedRowVector* row){
   ArithVar basic = row->basic();
   for(ReducedRowVector::NonZeroIterator i=row->beginNonZero(), endIter = row->endNonZero(); i != endIter; ){
@@ -123,3 +137,4 @@ void Tableau::updateRow(ReducedRowVector* row){
     }
   }
 }
+*/
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 05fcf6cf8..5f2a36505 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -76,23 +76,28 @@ public:
     return d_activeBasicVars.end();
   }
 
-  ReducedRowVector* lookup(ArithVar var){
-    Assert(isActiveBasicVariable(var));
-    return d_rowsTable[var];
+  ReducedRowVector& lookup(ArithVar var){
+    Assert(d_activeBasicVars.isMember(var));
+    Assert(d_rowsTable[var] != NULL);
+    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];
   }
 
+
   void addRow(ArithVar basicVar,
               const std::vector<Rational>& coeffs,
               const std::vector<ArithVar>& variables);
@@ -107,17 +112,24 @@ 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);
 
@@ -128,10 +140,13 @@ public:
     d_activeBasicVars.add(basic);
     updateRow(row);
   }
+  */
 private:
+  /*
   inline bool isActiveBasicVariable(ArithVar var){
     return d_activeBasicVars.isMember(var);
   }
+  */
 
   void updateRow(ReducedRowVector* row);
 };
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 1e1ac03ba..ecc740655 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -199,13 +199,13 @@ ArithVar TheoryArith::findShortestBasicRow(ArithVar variable){
       basicIter != d_tableau.end();
       ++basicIter){
     ArithVar x_j = *basicIter;
-    ReducedRowVector* row_j = d_tableau.lookup(x_j);
+    ReducedRowVector& row_j = d_tableau.lookup(x_j);
 
-    if(row_j->has(variable)){
+    if(row_j.has(variable)){
       if((bestBasic == ARITHVAR_SENTINEL) ||
-         (bestBasic != ARITHVAR_SENTINEL && row_j->size() < rowLength)){
+         (bestBasic != ARITHVAR_SENTINEL && row_j.size() < rowLength)){
         bestBasic = x_j;
-        rowLength = row_j->size();
+        rowLength = row_j.size();
       }
     }
   }
@@ -511,9 +511,11 @@ 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) {
@@ -581,9 +583,11 @@ 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();
@@ -683,6 +687,8 @@ void TheoryArith::permanentlyRemoveVariable(ArithVar v){
     if(basic == ARITHVAR_SENTINEL){
       //Case 3) do nothing else.
       //TODO think hard about if this is okay...
+      //Probably wrecks havoc with model generation
+      //*feh* DO IT ANYWAYS!
       return;
     }
 
@@ -692,11 +698,9 @@ void TheoryArith::permanentlyRemoveVariable(ArithVar v){
 
   Assert(d_basicManager.isMember(v));
 
-  d_tableau.ejectBasic(v);
   //remove the row from the tableau
-  //TODO: It would be better to remove the row from the tableau
-  //and store this row in another data structure
-
+  ReducedRowVector* row  = d_tableau.removeRow(v);
+  d_removedRows[v] = row;
 
   Debug("arith::permanentlyRemoveVariable") << v << " died an ignoble death."<< endl;
   ++(d_statistics.d_permanentlyRemovedVariables);