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