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::iterator i_colIter = d_columnMatrix.begin();
  49   ColumnMatrix::iterator end_colIter = d_columnMatrix.end();
  50   for(; i_colIter != end_colIter; ++i_colIter){
  51     Column& col = *i_colIter;
  52     col.increaseSize(d_columnMatrix.size());
  53   }
  54
  55   ArithVarSet::iterator i_basicIter = tab.d_basicVariables.begin();
  56   ArithVarSet::iterator i_basicEnd = tab.d_basicVariables.end();
  57   for(; i_basicIter != i_basicEnd; ++i_basicIter){
  58     ArithVar basicVar = *i_basicIter;
  59     const ReducedRowVector* otherRow = tab.d_rowsTable[basicVar];
  60
  61     Assert(otherRow != NULL);
  62
  63     std::vector< ArithVar > variables;
  64     std::vector< Rational > coefficients;
  65     otherRow->enqueueNonBasicVariablesAndCoefficients(variables, coefficients);
  66
  67     ReducedRowVector* copy = new ReducedRowVector(basicVar, variables, coefficients, d_rowCount, d_columnMatrix);
  68
  69     Debug("tableau::copy") << "copying " << basicVar << endl;
  70     copy->printRow();
  71
  72     d_basicVariables.add(basicVar);
  73     d_rowsTable[basicVar] = copy;
  74   }
  75 }
  76
  77 Tableau& Tableau::operator=(const Tableau& other){
  78   clear();
  79   internalCopy(other);
  80   return (*this);
  81 }
  82
  83 Tableau::~Tableau(){
  84   clear();
  85 }
  86
  87 void Tableau::clear(){
  88   while(!d_basicVariables.empty()){
  89     ArithVar curr = *(d_basicVariables.begin());
  90     ReducedRowVector* vec = removeRow(curr);
  91     delete vec;
  92   }
  93
  94   d_rowsTable.clear();
  95   d_basicVariables.clear();
  96   d_rowCount.clear();
  97   d_columnMatrix.clear();
  98 }
  99
 100 void Tableau::addRow(ArithVar basicVar,
 101                      const std::vector<Rational>& coeffs,
 102                      const std::vector<ArithVar>& variables){
 103
 104   Assert(coeffs.size() == variables.size());
 105
 106   //The new basic variable cannot already be a basic variable
 107   Assert(!d_basicVariables.isMember(basicVar));
 108   d_basicVariables.add(basicVar);
 109   ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount, d_columnMatrix);
 110   d_rowsTable[basicVar] = row_current;
 111
 112   //A variable in the row may have been made non-basic already.
 113   //If this is the case we fake pivoting this variable
 114   vector<ArithVar>::const_iterator varsIter = variables.begin();
 115   vector<ArithVar>::const_iterator varsEnd = variables.end();
 116
 117   for( ; varsIter != varsEnd; ++varsIter){
 118     ArithVar var = *varsIter;
 119
 120     if(d_basicVariables.isMember(var)){
 121       ReducedRowVector& row_var = lookup(var);
 122       row_current->substitute(row_var);
 123     }
 124   }
 125 }
 126
 127 ReducedRowVector* Tableau::removeRow(ArithVar basic){
 128   Assert(d_basicVariables.isMember(basic));
 129
 130   ReducedRowVector* row = d_rowsTable[basic];
 131
 132   d_basicVariables.remove(basic);
 133   d_rowsTable[basic] = NULL;
 134
 135   return row;
 136 }
 137
 138 void Tableau::pivot(ArithVar x_r, ArithVar x_s){
 139   Assert(d_basicVariables.isMember(x_r));
 140   Assert(!d_basicVariables.isMember(x_s));
 141
 142   Debug("tableau") << "Tableau::pivot(" <<  x_r <<", " <<x_s <<")"  << endl;
 143
 144   ReducedRowVector* row_s = d_rowsTable[x_r];
 145   Assert(row_s != NULL);
 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_basicVariables.remove(x_r);
 153
 154   d_basicVariables.add(x_s);
 155
 156   row_s->pivot(x_s);
 157
 158   Column::VarList copy(getColumn(x_s).getList());
 159   vector<ArithVar>::iterator basicIter = copy.begin(), endIter = copy.end();
 160
 161   for(; basicIter != endIter; ++basicIter){
 162     ArithVar basic = *basicIter;
 163     if(basic == x_s) continue;
 164
 165     ReducedRowVector& row_k = lookup(basic);
 166     Assert(row_k.has(x_s));
 167
 168     row_k.substitute(*row_s);
 169   }
 170   Assert(getColumn(x_s).size() == 1);
 171   Assert(getRowCount(x_s) == 1);
 172 }
 173
 174 void Tableau::printTableau(){
 175   Debug("tableau") << "Tableau::d_activeRows"  << endl;
 176
 177   typedef RowsTable::iterator table_iter;
 178   for(table_iter rowIter = d_rowsTable.begin(), end = d_rowsTable.end();
 179       rowIter != end; ++rowIter){
 180     ReducedRowVector* row_k = *rowIter;
 181     if(row_k != NULL){
 182       row_k->printRow();
 183     }
 184   }
 185 }