src/theory/arith/tableau.cpp

   1
   2 #include "theory/arith/tableau.h"
   3
   4 using namespace CVC4;
   5 using namespace CVC4::theory;
   6 using namespace CVC4::theory::arith;
   7
   8 Row::Row(ArithVar basic,
   9          const std::vector< Rational >& coefficients,
  10          const std::vector< ArithVar >& variables):
  11   d_x_i(basic),
  12   d_coeffs(){
  13
  14   Assert(coefficients.size() == variables.size() );
  15
  16   std::vector<Rational>::const_iterator coeffIter = coefficients.begin();
  17   std::vector<Rational>::const_iterator coeffEnd = coefficients.end();
  18   std::vector<ArithVar>::const_iterator varIter = variables.begin();
  19
  20   for(; coeffIter != coeffEnd; ++coeffIter, ++varIter){
  21     const Rational& coeff = *coeffIter;
  22     ArithVar var_i = *varIter;
  23
  24     Assert(var_i != d_x_i);
  25     Assert(!has(var_i));
  26     Assert(coeff != Rational(0,1));
  27
  28     d_coeffs[var_i] = coeff;
  29     Assert(d_coeffs[var_i] != Rational(0,1));
  30   }
  31 }
  32
  33 void Row::subsitute(Row& row_s){
  34   ArithVar x_s = row_s.basicVar();
  35
  36   Assert(has(x_s));
  37   Assert(x_s != d_x_i);
  38
  39   Rational zero(0,1);
  40
  41   Rational a_rs = lookup(x_s);
  42   Assert(a_rs != zero);
  43   d_coeffs.erase(x_s);
  44
  45   for(iterator iter = row_s.begin(), iter_end = row_s.end();
  46       iter != iter_end; ++iter){
  47     ArithVar x_j = iter->first;
  48     Rational a_sj = iter->second;
  49     a_sj *= a_rs;
  50     CoefficientTable::iterator coeff_iter = d_coeffs.find(x_j);
  51
  52     if(coeff_iter != d_coeffs.end()){
  53       coeff_iter->second += a_sj;
  54       if(coeff_iter->second == zero){
  55         d_coeffs.erase(coeff_iter);
  56       }
  57     }else{
  58       d_coeffs.insert(std::make_pair(x_j,a_sj));
  59     }
  60   }
  61 }
  62
  63 void Row::pivot(ArithVar x_j){
  64   Rational negInverseA_rs = -(lookup(x_j).inverse());
  65   d_coeffs[d_x_i] = Rational(Integer(-1));
  66   d_coeffs.erase(x_j);
  67
  68   d_x_i = x_j;
  69
  70   for(iterator nonbasicIter = begin(), nonbasicIter_end = end();
  71       nonbasicIter != nonbasicIter_end; ++nonbasicIter){
  72     nonbasicIter->second *= negInverseA_rs;
  73   }
  74
  75 }
  76
  77 void Row::printRow(){
  78   Debug("tableau") << d_x_i << " ";
  79   for(iterator nonbasicIter = d_coeffs.begin();
  80       nonbasicIter != d_coeffs.end();
  81       ++nonbasicIter){
  82     ArithVar nb = nonbasicIter->first;
  83     Debug("tableau") << "{" << nb << "," << d_coeffs[nb] << "}";
  84   }
  85   Debug("tableau") << std::endl;
  86 }
  87
  88 void Tableau::addRow(ArithVar basicVar,
  89                      const std::vector<Rational>& coeffs,
  90                      const std::vector<ArithVar>& variables){
  91
  92   Assert(coeffs.size() == variables.size());
  93   Assert(d_basicManager.isBasic(basicVar));
  94
  95   //The new basic variable cannot already be a basic variable
  96   Assert(!isActiveBasicVariable(basicVar));
  97   d_activeBasicVars.insert(basicVar);
  98   Row* row_current = new Row(basicVar,coeffs,variables);
  99   d_activeRows[basicVar] = row_current;
 100
 101   //A variable in the row may have been made non-basic already.
 102   //If this is the case we fake pivoting this variable
 103   std::vector<Rational>::const_iterator coeffsIter = coeffs.begin();
 104   std::vector<Rational>::const_iterator coeffsEnd = coeffs.end();
 105
 106   std::vector<ArithVar>::const_iterator varsIter = variables.begin();
 107
 108   for( ; coeffsIter != coeffsEnd; ++coeffsIter, ++ varsIter){
 109     ArithVar var = *varsIter;
 110
 111     if(d_basicManager.isBasic(var)){
 112       if(!isActiveBasicVariable(var)){
 113         reinjectBasic(var);
 114       }
 115       Assert(isActiveBasicVariable(var));
 116
 117       Row* row_var = lookup(var);
 118       row_current->subsitute(*row_var);
 119     }
 120   }
 121 }
 122
 123 void Tableau::pivot(ArithVar x_r, ArithVar x_s){
 124   Assert(d_basicManager.isBasic(x_r));
 125   Assert(!d_basicManager.isBasic(x_s));
 126
 127   RowsTable::iterator ptrRow_r = d_activeRows.find(x_r);
 128   Assert(ptrRow_r != d_activeRows.end());
 129
 130   Row* row_s = (*ptrRow_r).second;
 131
 132   Assert(row_s->has(x_s));
 133   row_s->pivot(x_s);
 134
 135   d_activeRows.erase(ptrRow_r);
 136   d_activeBasicVars.erase(x_r);
 137   d_basicManager.makeNonbasic(x_r);
 138
 139   d_activeRows.insert(std::make_pair(x_s,row_s));
 140   d_activeBasicVars.insert(x_s);
 141   d_basicManager.makeBasic(x_s);
 142
 143   for(VarSet::iterator basicIter = begin(), endIter = end();
 144       basicIter != endIter; ++basicIter){
 145     ArithVar basic = *basicIter;
 146     Row* row_k = lookup(basic);
 147     if(row_k->has(x_s)){
 148       d_activityMonitor.increaseActivity(basic, 30);
 149       row_k->subsitute(*row_s);
 150     }
 151   }
 152 }
 153
 154 void Tableau::printTableau(){
 155   for(VarSet::iterator basicIter = begin(), endIter = end();
 156       basicIter != endIter; ++basicIter){
 157     ArithVar basic = *basicIter;
 158     Row* row_k = lookup(basic);
 159     row_k->printRow();
 160   }
 161   for(RowsTable::iterator basicIter = d_inactiveRows.begin(), endIter =  d_inactiveRows.end();
 162       basicIter != endIter; ++basicIter){
 163     ArithVar basic = (*basicIter).first;
 164     Row* row_k = lookupEjected(basic);
 165     row_k->printRow();
 166   }
 167 }
 168
 169
 170 void Tableau::updateRow(Row* row){
 171   for(Row::iterator i=row->begin(), endIter = row->end(); i != endIter; ){
 172     ArithVar var = i->first;
 173     ++i;
 174     if(d_basicManager.isBasic(var)){
 175       Row* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var);
 176
 177       Assert(row_var != row);
 178       row->subsitute(*row_var);
 179
 180       i = row->begin();
 181       endIter = row->end();
 182     }
 183   }
 184 }