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 using namespace std;
  28
  29 Tableau::~Tableau(){
  30   while(!d_basicVariables.empty()){
  31     ArithVar curr = *(d_basicVariables.begin());
  32     ReducedRowVector* vec = removeRow(curr);
  33     delete vec;
  34   }
  35 }
  36
  37 void Tableau::addRow(ArithVar basicVar,
  38                      const std::vector<Rational>& coeffs,
  39                      const std::vector<ArithVar>& variables){
  40
  41   Assert(coeffs.size() == variables.size());
  42
  43   //The new basic variable cannot already be a basic variable
  44   Assert(!d_basicVariables.isMember(basicVar));
  45   d_basicVariables.add(basicVar);
  46   ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount, d_columnMatrix);
  47   d_rowsTable[basicVar] = row_current;
  48
  49   //A variable in the row may have been made non-basic already.
  50   //If this is the case we fake pivoting this variable
  51   vector<ArithVar>::const_iterator varsIter = variables.begin();
  52   vector<ArithVar>::const_iterator varsEnd = variables.end();
  53
  54   for( ; varsIter != varsEnd; ++varsIter){
  55     ArithVar var = *varsIter;
  56
  57     if(d_basicVariables.isMember(var)){
  58       ReducedRowVector& row_var = lookup(var);
  59       row_current->substitute(row_var);
  60     }
  61   }
  62 }
  63
  64 ReducedRowVector* Tableau::removeRow(ArithVar basic){
  65   Assert(d_basicVariables.isMember(basic));
  66
  67   ReducedRowVector* row = d_rowsTable[basic];
  68
  69   d_basicVariables.remove(basic);
  70   d_rowsTable[basic] = NULL;
  71
  72   return row;
  73 }
  74
  75 void Tableau::pivot(ArithVar x_r, ArithVar x_s){
  76   Assert(d_basicVariables.isMember(x_r));
  77   Assert(!d_basicVariables.isMember(x_s));
  78
  79   Debug("tableau") << "Tableau::pivot(" <<  x_r <<", " <<x_s <<")"  << endl;
  80
  81   ReducedRowVector* row_s = d_rowsTable[x_r];
  82   Assert(row_s != NULL);
  83   Assert(row_s->has(x_s));
  84
  85   //Swap x_r and x_s in d_activeRows
  86   d_rowsTable[x_s] = row_s;
  87   d_rowsTable[x_r] = NULL;
  88
  89   d_basicVariables.remove(x_r);
  90
  91   d_basicVariables.add(x_s);
  92
  93   row_s->pivot(x_s);
  94
  95   ArithVarSet::VarList copy(getColumn(x_s).getList());
  96   vector<ArithVar>::iterator basicIter = copy.begin(), endIter = copy.end();
  97
  98   for(; basicIter != endIter; ++basicIter){
  99     ArithVar basic = *basicIter;
 100     if(basic == x_s) continue;
 101
 102     ReducedRowVector& row_k = lookup(basic);
 103     Assert(row_k.has(x_s));
 104
 105     row_k.substitute(*row_s);
 106   }
 107   Assert(getColumn(x_s).size() == 1);
 108   Assert(getRowCount(x_s) == 1);
 109 }
 110
 111 void Tableau::printTableau(){
 112   Debug("tableau") << "Tableau::d_activeRows"  << endl;
 113
 114   typedef RowsTable::iterator table_iter;
 115   for(table_iter rowIter = d_rowsTable.begin(), end = d_rowsTable.end();
 116       rowIter != end; ++rowIter){
 117     ReducedRowVector* row_k = *rowIter;
 118     if(row_k != NULL){
 119       row_k->printRow();
 120     }
 121   }
 122 }