src/theory/arith/tableau.h

   1 #include "cvc4_private.h"
   2
   3 #pragma once
   4
   5 #include "util/dense_map.h"
   6 #include "util/rational.h"
   7 #include "theory/arith/arithvar.h"
   8 #include "theory/arith/matrix.h"
   9 #include <vector>
  10
  11 namespace CVC4 {
  12 namespace theory {
  13 namespace arith {
  14
  15 /**
  16  * A Tableau is a Rational matrix that keeps its rows in solved form.
  17  * Each row has a basic variable with coefficient -1 that is solved.
  18  * Tableau is optimized for pivoting.
  19  * The tableau should only be updated via pivot calls.
  20  */
  21 class Tableau : public Matrix<Rational> {
  22 public:
  23 private:
  24   typedef DenseMap<RowIndex> BasicToRowMap;
  25   // Set of all of the basic variables in the tableau.
  26   // ArithVarMap<RowIndex> : ArithVar |-> RowIndex
  27   BasicToRowMap d_basic2RowIndex;
  28
  29   // RowIndex |-> Basic Variable
  30   typedef DenseMap<ArithVar> RowIndexToBasicMap;
  31   RowIndexToBasicMap d_rowIndex2basic;
  32
  33 public:
  34
  35   Tableau() : Matrix<Rational>(Rational(0)) {}
  36
  37   typedef Matrix<Rational>::ColIterator ColIterator;
  38   typedef Matrix<Rational>::RowIterator RowIterator;
  39   typedef BasicToRowMap::const_iterator BasicIterator;
  40
  41   typedef MatrixEntry<Rational> Entry;
  42
  43   bool isBasic(ArithVar v) const{
  44     return d_basic2RowIndex.isKey(v);
  45   }
  46
  47   void debugPrintIsBasic(ArithVar v) const {
  48     if(isBasic(v)){
  49       Warning() << v << " is basic." << std::endl;
  50     }else{
  51       Warning() << v << " is non-basic." << std::endl;
  52     }
  53   }
  54
  55   BasicIterator beginBasic() const {
  56     return d_basic2RowIndex.begin();
  57   }
  58   BasicIterator endBasic() const {
  59     return d_basic2RowIndex.end();
  60   }
  61
  62   RowIndex basicToRowIndex(ArithVar x) const {
  63     return d_basic2RowIndex[x];
  64   }
  65
  66   ArithVar rowIndexToBasic(RowIndex rid) const {
  67     Assert(rid < d_rowIndex2basic.size());
  68     return d_rowIndex2basic[rid];
  69   }
  70
  71   ColIterator colIterator(ArithVar x) const {
  72     return getColumn(x).begin();
  73   }
  74
  75   RowIterator ridRowIterator(RowIndex rid) const {
  76     return getRow(rid).begin();
  77   }
  78
  79   RowIterator basicRowIterator(ArithVar basic) const {
  80     return ridRowIterator(basicToRowIndex(basic));
  81   }
  82
  83   const Entry& basicFindEntry(ArithVar basic, ArithVar col) const {
  84     return findEntry(basicToRowIndex(basic), col);
  85   }
  86
  87   /**
  88    * Adds a row to the tableau.
  89    * The new row is equivalent to:
  90    *   basicVar = \f$\sum_i\f$ coeffs[i] * variables[i]
  91    * preconditions:
  92    *   basicVar is already declared to be basic
  93    *   basicVar does not have a row associated with it in the tableau.
  94    *
  95    * Note: each variables[i] does not have to be non-basic.
  96    * Pivoting will be mimicked if it is basic.
  97    */
  98   void addRow(ArithVar basicVar,
  99               const std::vector<Rational>& coeffs,
 100               const std::vector<ArithVar>& variables);
 101
 102   /**
 103    * preconditions:
 104    *   x_r is basic,
 105    *   x_s is non-basic, and
 106    *   a_rs != 0.
 107    */
 108   void pivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCallback& cb);
 109
 110   void removeBasicRow(ArithVar basic);
 111
 112   uint32_t basicRowLength(ArithVar basic) const{
 113     RowIndex ridx = basicToRowIndex(basic);
 114     return getRowLength(ridx);
 115   }
 116
 117   /**
 118    *  to += mult * from
 119    * replacing from with its row.
 120    */
 121   void substitutePlusTimesConstant(ArithVar to, ArithVar from, const Rational& mult,  CoefficientChangeCallback& cb);
 122
 123   void directlyAddToCoefficient(ArithVar rowVar, ArithVar col, const Rational& mult,  CoefficientChangeCallback& cb){
 124     RowIndex ridx = basicToRowIndex(rowVar);
 125     manipulateRowEntry(ridx, col, mult, cb);
 126   }
 127
 128   /* Returns the complexity of a row in the tableau. */
 129   uint32_t rowComplexity(ArithVar basic) const;
 130
 131   /* Returns the average complexity of the rows in the tableau. */
 132   double avgRowComplexity() const;
 133
 134   void printBasicRow(ArithVar basic, std::ostream& out);
 135
 136 private:
 137   /* Changes the basic variable on the row for basicOld to basicNew. */
 138   void rowPivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCallback& cb);
 139
 140 };/* class Tableau */
 141
 142
 143
 144 }/* CVC4::theory::arith namespace */
 145 }/* CVC4::theory namespace */
 146 }/* CVC4 namespace */
 147