branches/arith-indexed-variables merged into the main trunk.

1 files changed, 184 insertions, 0 deletions

diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
new file mode 100644
index 000000000..e43458a23
--- /dev/null
+++ b/src/theory/arith/tableau.cpp
@@ -0,0 +1,184 @@
+
+#include "theory/arith/tableau.h"
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::arith;
+
+Row::Row(ArithVar basic,
+         const std::vector< Rational >& coefficients,
+         const std::vector< ArithVar >& variables):
+  d_x_i(basic),
+  d_coeffs(){
+
+  Assert(coefficients.size() == variables.size() );
+
+  std::vector<Rational>::const_iterator coeffIter = coefficients.begin();
+  std::vector<Rational>::const_iterator coeffEnd = coefficients.end();
+  std::vector<ArithVar>::const_iterator varIter = variables.begin();
+
+  for(; coeffIter != coeffEnd; ++coeffIter, ++varIter){
+    const Rational& coeff = *coeffIter;
+    ArithVar var_i = *varIter;
+
+    Assert(var_i != d_x_i);
+    Assert(!has(var_i));
+    Assert(coeff != Rational(0,1));
+
+    d_coeffs[var_i] = coeff;
+    Assert(d_coeffs[var_i] != Rational(0,1));
+  }
+}
+
+void Row::subsitute(Row& row_s){
+  ArithVar x_s = row_s.basicVar();
+
+  Assert(has(x_s));
+  Assert(x_s != d_x_i);
+
+  Rational zero(0,1);
+
+  Rational a_rs = lookup(x_s);
+  Assert(a_rs != zero);
+  d_coeffs.erase(x_s);
+
+  for(iterator iter = row_s.begin(), iter_end = row_s.end();
+      iter != iter_end; ++iter){
+    ArithVar x_j = iter->first;
+    Rational a_sj = iter->second;
+    a_sj *= a_rs;
+    CoefficientTable::iterator coeff_iter = d_coeffs.find(x_j);
+
+    if(coeff_iter != d_coeffs.end()){
+      coeff_iter->second += a_sj;
+      if(coeff_iter->second == zero){
+        d_coeffs.erase(coeff_iter);
+      }
+    }else{
+      d_coeffs.insert(std::make_pair(x_j,a_sj));
+    }
+  }
+}
+
+void Row::pivot(ArithVar x_j){
+  Rational negInverseA_rs = -(lookup(x_j).inverse());
+  d_coeffs[d_x_i] = Rational(Integer(-1));
+  d_coeffs.erase(x_j);
+
+  d_x_i = x_j;
+
+  for(iterator nonbasicIter = begin(), nonbasicIter_end = end();
+      nonbasicIter != nonbasicIter_end; ++nonbasicIter){
+    nonbasicIter->second *= negInverseA_rs;
+  }
+
+}
+
+void Row::printRow(){
+  Debug("tableau") << d_x_i << " ";
+  for(iterator nonbasicIter = d_coeffs.begin();
+      nonbasicIter != d_coeffs.end();
+      ++nonbasicIter){
+    ArithVar nb = nonbasicIter->first;
+    Debug("tableau") << "{" << nb << "," << d_coeffs[nb] << "}";
+  }
+  Debug("tableau") << std::endl;
+}
+
+void Tableau::addRow(ArithVar basicVar,
+                     const std::vector<Rational>& coeffs,
+                     const std::vector<ArithVar>& variables){
+
+  Assert(coeffs.size() == variables.size());
+  Assert(d_basicManager.isBasic(basicVar));
+
+  //The new basic variable cannot already be a basic variable
+  Assert(!isActiveBasicVariable(basicVar));
+  d_activeBasicVars.insert(basicVar);
+  Row* row_current = new Row(basicVar,coeffs,variables);
+  d_activeRows[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
+  std::vector<Rational>::const_iterator coeffsIter = coeffs.begin();
+  std::vector<Rational>::const_iterator coeffsEnd = coeffs.end();
+
+  std::vector<ArithVar>::const_iterator varsIter = variables.begin();
+
+  for( ; coeffsIter != coeffsEnd; ++coeffsIter, ++ varsIter){
+    ArithVar var = *varsIter;
+
+    if(d_basicManager.isBasic(var)){
+      if(!isActiveBasicVariable(var)){
+        reinjectBasic(var);
+      }
+      Assert(isActiveBasicVariable(var));
+
+      Row* row_var = lookup(var);
+      row_current->subsitute(*row_var);
+    }
+  }
+}
+
+void Tableau::pivot(ArithVar x_r, ArithVar x_s){
+  Assert(d_basicManager.isBasic(x_r));
+  Assert(!d_basicManager.isBasic(x_s));
+
+  RowsTable::iterator ptrRow_r = d_activeRows.find(x_r);
+  Assert(ptrRow_r != d_activeRows.end());
+
+  Row* row_s = (*ptrRow_r).second;
+
+  Assert(row_s->has(x_s));
+  row_s->pivot(x_s);
+
+  d_activeRows.erase(ptrRow_r);
+  d_activeBasicVars.erase(x_r);
+  d_basicManager.makeNonbasic(x_r);
+
+  d_activeRows.insert(std::make_pair(x_s,row_s));
+  d_activeBasicVars.insert(x_s);
+  d_basicManager.makeBasic(x_s);
+
+  for(VarSet::iterator basicIter = begin(), endIter = end();
+      basicIter != endIter; ++basicIter){
+    ArithVar basic = *basicIter;
+    Row* row_k = lookup(basic);
+    if(row_k->has(x_s)){
+      d_activityMonitor.increaseActivity(basic, 30);
+      row_k->subsitute(*row_s);
+    }
+  }
+}
+
+void Tableau::printTableau(){
+  for(VarSet::iterator basicIter = begin(), endIter = end();
+      basicIter != endIter; ++basicIter){
+    ArithVar basic = *basicIter;
+    Row* row_k = lookup(basic);
+    row_k->printRow();
+  }
+  for(RowsTable::iterator basicIter = d_inactiveRows.begin(), endIter =  d_inactiveRows.end();
+      basicIter != endIter; ++basicIter){
+    ArithVar basic = (*basicIter).first;
+    Row* row_k = lookupEjected(basic);
+    row_k->printRow();
+  }
+}
+
+
+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)){
+      Row* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var);
+
+      Assert(row_var != row);
+      row->subsitute(*row_var);
+
+      i = row->begin();
+      endIter = row->end();
+    }
+  }
+}