src/theory/arith/tableau.h

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