src/theory/arith/tableau.h

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