src/theory/arith/tableau.cpp

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