src/theory/arith/tableau.cpp

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