src/theory/arith/tableau.cpp

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