src/theory/arith/tableau.cpp

   1 #include "theory/arith/tableau.h"
   2
   3 using namespace std;
   4 namespace CVC4 {
   5 namespace theory {
   6 namespace arith {
   7
   8
   9 void Tableau::pivot(ArithVar oldBasic, ArithVar newBasic, CoefficientChangeCallback& cb){
  10   Assert(isBasic(oldBasic));
  11   Assert(!isBasic(newBasic));
  12   Assert(d_mergeBuffer.empty());
  13
  14   Debug("tableau") << "Tableau::pivot(" <<  oldBasic <<", " << newBasic <<")"  << endl;
  15
  16   RowIndex ridx = basicToRowIndex(oldBasic);
  17
  18   rowPivot(oldBasic, newBasic, cb);
  19   Assert(ridx == basicToRowIndex(newBasic));
  20
  21   loadRowIntoBuffer(ridx);
  22
  23   ColIterator colIter = colIterator(newBasic);
  24   while(!colIter.atEnd()){
  25     EntryID id = colIter.getID();
  26     Entry& entry = d_entries.get(id);
  27
  28     ++colIter; //needs to be incremented before the variable is removed
  29     if(entry.getRowIndex() == ridx){ continue; }
  30
  31     RowIndex to = entry.getRowIndex();
  32     Rational coeff = entry.getCoefficient();
  33     if(cb.canUseRow(to)){
  34       rowPlusBufferTimesConstant(to, coeff, cb);
  35     }else{
  36       rowPlusBufferTimesConstant(to, coeff);
  37     }
  38   }
  39   clearBuffer();
  40
  41   //Clear the column for used for this variable
  42
  43   Assert(d_mergeBuffer.empty());
  44   Assert(!isBasic(oldBasic));
  45   Assert(isBasic(newBasic));
  46   Assert(getColLength(newBasic) == 1);
  47 }
  48
  49 /**
  50  * Changes basic to newbasic (a variable on the row).
  51  */
  52 void Tableau::rowPivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCallback& cb){
  53   Assert(isBasic(basicOld));
  54   Assert(!isBasic(basicNew));
  55
  56   RowIndex rid = basicToRowIndex(basicOld);
  57
  58   EntryID newBasicID = findOnRow(rid, basicNew);
  59
  60   Assert(newBasicID != ENTRYID_SENTINEL);
  61
  62   Tableau::Entry& newBasicEntry = d_entries.get(newBasicID);
  63   const Rational& a_rs = newBasicEntry.getCoefficient();
  64   int a_rs_sgn = a_rs.sgn();
  65   Rational negInverseA_rs = -(a_rs.inverse());
  66
  67   for(RowIterator i = basicRowIterator(basicOld); !i.atEnd(); ++i){
  68     EntryID id = i.getID();
  69     Tableau::Entry& entry = d_entries.get(id);
  70
  71     entry.getCoefficient() *=  negInverseA_rs;
  72   }
  73
  74   d_basic2RowIndex.remove(basicOld);
  75   d_basic2RowIndex.set(basicNew, rid);
  76   d_rowIndex2basic.set(rid, basicNew);
  77
  78   cb.swap(basicOld, basicNew, a_rs_sgn);
  79 }
  80
  81
  82
  83 void Tableau::addRow(ArithVar basic,
  84                      const std::vector<Rational>& coefficients,
  85                      const std::vector<ArithVar>& variables)
  86 {
  87   Assert(basic < getNumColumns());
  88
  89   Assert(coefficients.size() == variables.size() );
  90   Assert(!isBasic(basic));
  91
  92   RowIndex newRow = Matrix<Rational>::addRow(coefficients, variables);
  93   addEntry(newRow, basic, Rational(-1));
  94
  95   Assert(!d_basic2RowIndex.isKey(basic));
  96   Assert(!d_rowIndex2basic.isKey(newRow));
  97
  98   d_basic2RowIndex.set(basic, newRow);
  99   d_rowIndex2basic.set(newRow, basic);
 100
 101
 102   if(Debug.isOn("matrix")){ printMatrix(); }
 103
 104   NoEffectCCCB noeffect;
 105   NoEffectCCCB* nep = &noeffect;
 106   CoefficientChangeCallback* cccb = static_cast<CoefficientChangeCallback*>(nep);
 107
 108   vector<Rational>::const_iterator coeffIter = coefficients.begin();
 109   vector<ArithVar>::const_iterator varsIter = variables.begin();
 110   vector<ArithVar>::const_iterator varsEnd = variables.end();
 111   for(; varsIter != varsEnd; ++coeffIter, ++varsIter){
 112     ArithVar var = *varsIter;
 113
 114     if(isBasic(var)){
 115       Rational coeff = *coeffIter;
 116
 117       RowIndex ri = basicToRowIndex(var);
 118
 119       loadRowIntoBuffer(ri);
 120       rowPlusBufferTimesConstant(newRow, coeff, *cccb);
 121       clearBuffer();
 122     }
 123   }
 124
 125   if(Debug.isOn("matrix")) { printMatrix(); }
 126
 127   Assert(debugNoZeroCoefficients(newRow));
 128   Assert(debugMatchingCountsForRow(newRow));
 129   Assert(getColLength(basic) == 1);
 130 }
 131
 132 void Tableau::removeBasicRow(ArithVar basic){
 133   RowIndex rid = basicToRowIndex(basic);
 134
 135   removeRow(rid);
 136   d_basic2RowIndex.remove(basic);
 137   d_rowIndex2basic.remove(rid);
 138 }
 139
 140 void Tableau::substitutePlusTimesConstant(ArithVar to, ArithVar from, const Rational& mult,  CoefficientChangeCallback& cb){
 141   if(!mult.isZero()){
 142     RowIndex to_idx = basicToRowIndex(to);
 143     addEntry(to_idx, from, mult); // Add an entry to be cancelled out
 144     RowIndex from_idx = basicToRowIndex(from);
 145
 146     cb.update(to_idx, from, 0, mult.sgn());
 147
 148     loadRowIntoBuffer(from_idx);
 149     rowPlusBufferTimesConstant(to_idx, mult, cb);
 150     clearBuffer();
 151   }
 152 }
 153
 154 uint32_t Tableau::rowComplexity(ArithVar basic) const{
 155   uint32_t complexity = 0;
 156   for(RowIterator i = basicRowIterator(basic); !i.atEnd(); ++i){
 157     const Entry& e = *i;
 158     complexity += e.getCoefficient().complexity();
 159   }
 160   return complexity;
 161 }
 162
 163 double Tableau::avgRowComplexity() const{
 164   double sum = 0;
 165   uint32_t rows = 0;
 166   for(BasicIterator i = beginBasic(), i_end = endBasic(); i != i_end; ++i){
 167     sum += rowComplexity(*i);
 168     rows++;
 169   }
 170   return (rows == 0) ? 0 : (sum/rows);
 171 }
 172
 173 void Tableau::printBasicRow(ArithVar basic, std::ostream& out){
 174   printRow(basicToRowIndex(basic), out);
 175 }
 176
 177 }/* CVC4::theory::arith namespace */
 178 }/* CVC4::theory namespace */
 179 }/* CVC4 namespace */