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 std;
  24 using namespace CVC4;
  25 using namespace CVC4::theory;
  26 using namespace CVC4::theory::arith;
  27
  28
  29 Tableau::Tableau(const Tableau& tab){
  30   internalCopy(tab);
  31 }
  32
  33 void Tableau::internalCopy(const Tableau& tab){
  34   uint32_t N = tab.d_rowsTable.size();
  35
  36   Debug("tableau::copy") << "tableau copy "<< N << endl;
  37
  38   if(N > 1){
  39     d_columnMatrix.insert(d_columnMatrix.end(), N, Column());
  40     d_rowsTable.insert(d_rowsTable.end(), N, NULL);
  41     d_basicVariables.increaseSize(N-1);
  42
  43     Assert(d_basicVariables.allocated() == tab.d_basicVariables.allocated());
  44
  45     d_rowCount.insert(d_rowCount.end(), N, 0);
  46   }
  47
  48   ColumnMatrix::const_iterator otherIter = tab.d_columnMatrix.begin();
  49   ColumnMatrix::iterator i_colIter = d_columnMatrix.begin();
  50   ColumnMatrix::iterator end_colIter = d_columnMatrix.end();
  51   for(; i_colIter != end_colIter; ++i_colIter, ++otherIter){
  52     Assert(otherIter != tab.d_columnMatrix.end());
  53     Column& col = *i_colIter;
  54     const Column& otherCol = *otherIter;
  55     col.increaseSize(otherCol.allocated());
  56   }
  57
  58   ArithVarSet::iterator i_basicIter = tab.d_basicVariables.begin();
  59   ArithVarSet::iterator i_basicEnd = tab.d_basicVariables.end();
  60   for(; i_basicIter != i_basicEnd; ++i_basicIter){
  61     ArithVar basicVar = *i_basicIter;
  62     const ReducedRowVector* otherRow = tab.d_rowsTable[basicVar];
  63
  64     Assert(otherRow != NULL);
  65
  66     std::vector< ArithVar > variables;
  67     std::vector< Rational > coefficients;
  68     otherRow->enqueueNonBasicVariablesAndCoefficients(variables, coefficients);
  69
  70     ReducedRowVector* copy = new ReducedRowVector(basicVar, variables, coefficients, d_rowCount, d_columnMatrix);
  71
  72     Debug("tableau::copy") << "copying " << basicVar << endl;
  73     copy->printRow();
  74
  75     d_basicVariables.add(basicVar);
  76     d_rowsTable[basicVar] = copy;
  77   }
  78 }
  79
  80 Tableau& Tableau::operator=(const Tableau& other){
  81   clear();
  82   internalCopy(other);
  83   return (*this);
  84 }
  85
  86 Tableau::~Tableau(){
  87   clear();
  88 }
  89
  90 void Tableau::clear(){
  91   while(!d_basicVariables.empty()){
  92     ArithVar curr = *(d_basicVariables.begin());
  93     ReducedRowVector* vec = removeRow(curr);
  94     delete vec;
  95   }
  96
  97   d_rowsTable.clear();
  98   d_basicVariables.clear();
  99   d_rowCount.clear();
 100   d_columnMatrix.clear();
 101 }
 102
 103 void Tableau::addRow(ArithVar basicVar,
 104                      const std::vector<Rational>& coeffs,
 105                      const std::vector<ArithVar>& variables){
 106
 107   Assert(coeffs.size() == variables.size());
 108
 109   //The new basic variable cannot already be a basic variable
 110   Assert(!d_basicVariables.isMember(basicVar));
 111   d_basicVariables.add(basicVar);
 112   ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount, d_columnMatrix);
 113   d_rowsTable[basicVar] = row_current;
 114
 115   //A variable in the row may have been made non-basic already.
 116   //If this is the case we fake pivoting this variable
 117   vector<ArithVar>::const_iterator varsIter = variables.begin();
 118   vector<ArithVar>::const_iterator varsEnd = variables.end();
 119
 120   for( ; varsIter != varsEnd; ++varsIter){
 121     ArithVar var = *varsIter;
 122
 123     if(d_basicVariables.isMember(var)){
 124       ReducedRowVector& row_var = lookup(var);
 125       row_current->substitute(row_var);
 126     }
 127   }
 128 }
 129
 130 ReducedRowVector* Tableau::removeRow(ArithVar basic){
 131   Assert(d_basicVariables.isMember(basic));
 132
 133   ReducedRowVector* row = d_rowsTable[basic];
 134
 135   d_basicVariables.remove(basic);
 136   d_rowsTable[basic] = NULL;
 137
 138   return row;
 139 }
 140
 141 void Tableau::pivot(ArithVar x_r, ArithVar x_s){
 142   Assert(d_basicVariables.isMember(x_r));
 143   Assert(!d_basicVariables.isMember(x_s));
 144
 145   Debug("tableau") << "Tableau::pivot(" <<  x_r <<", " <<x_s <<")"  << endl;
 146
 147   ReducedRowVector* row_s = d_rowsTable[x_r];
 148   Assert(row_s != NULL);
 149   Assert(row_s->has(x_s));
 150
 151   //Swap x_r and x_s in d_activeRows
 152   d_rowsTable[x_s] = row_s;
 153   d_rowsTable[x_r] = NULL;
 154
 155   d_basicVariables.remove(x_r);
 156
 157   d_basicVariables.add(x_s);
 158
 159   row_s->pivot(x_s);
 160
 161   Column::VarList copy(getColumn(x_s).getList());
 162   vector<ArithVar>::iterator basicIter = copy.begin(), endIter = copy.end();
 163
 164   for(; basicIter != endIter; ++basicIter){
 165     ArithVar basic = *basicIter;
 166     if(basic == x_s) continue;
 167
 168     ReducedRowVector& row_k = lookup(basic);
 169     Assert(row_k.has(x_s));
 170
 171     row_k.substitute(*row_s);
 172   }
 173   Assert(getColumn(x_s).size() == 1);
 174   Assert(getRowCount(x_s) == 1);
 175 }
 176
 177 void Tableau::printTableau(){
 178   Debug("tableau") << "Tableau::d_activeRows"  << endl;
 179
 180   typedef RowsTable::iterator table_iter;
 181   for(table_iter rowIter = d_rowsTable.begin(), end = d_rowsTable.end();
 182       rowIter != end; ++rowIter){
 183     ReducedRowVector* row_k = *rowIter;
 184     if(row_k != NULL){
 185       row_k->printRow();
 186     }
 187   }
 188 }
 189
 190 uint32_t Tableau::numNonZeroEntries() const {
 191   uint32_t colSum = 0;
 192   ColumnMatrix::const_iterator i = d_columnMatrix.begin(), end = d_columnMatrix.end();
 193   for(; i != end; ++i){
 194     const Column& col = *i;
 195     colSum += col.size();
 196   }
 197   return colSum;
 198 }
 199
 200 uint32_t Tableau::numNonZeroEntriesByRow() const {
 201   uint32_t rowSum = 0;
 202   ArithVarSet::iterator i = d_basicVariables.begin(), end = d_basicVariables.end();
 203   for(; i != end; ++i){
 204     ArithVar basic = *i;
 205     const ReducedRowVector& row = *(d_rowsTable[basic]);
 206     rowSum += row.size();
 207   }
 208   return rowSum;
 209 }