diff options
Diffstat (limited to 'src/theory/arith/tableau.h')
-rw-r--r-- | src/theory/arith/tableau.h | 143 |
1 files changed, 143 insertions, 0 deletions
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h new file mode 100644 index 000000000..8b6ef1df6 --- /dev/null +++ b/src/theory/arith/tableau.h @@ -0,0 +1,143 @@ +#include "cvc4_private.h" + +#pragma once + +#include "util/dense_map.h" +#include "util/rational.h" +#include "theory/arith/arithvar.h" +#include "theory/arith/matrix.h" +#include <vector> + +namespace CVC4 { +namespace theory { +namespace arith { + +/** + * A Tableau is a Rational matrix that keeps its rows in solved form. + * Each row has a basic variable with coefficient -1 that is solved. + * Tableau is optimized for pivoting. + * The tableau should only be updated via pivot calls. + */ +class Tableau : public Matrix<Rational> { +public: +private: + typedef DenseMap<RowIndex> BasicToRowMap; + // Set of all of the basic variables in the tableau. + // ArithVarMap<RowIndex> : ArithVar |-> RowIndex + BasicToRowMap d_basic2RowIndex; + + // RowIndex |-> Basic Variable + typedef DenseMap<ArithVar> RowIndexToBasicMap; + RowIndexToBasicMap d_rowIndex2basic; + +public: + + Tableau() : Matrix<Rational>(Rational(0)) {} + + typedef Matrix<Rational>::ColIterator ColIterator; + typedef Matrix<Rational>::RowIterator RowIterator; + typedef BasicToRowMap::const_iterator BasicIterator; + + typedef MatrixEntry<Rational> Entry; + + bool isBasic(ArithVar v) const{ + return d_basic2RowIndex.isKey(v); + } + + void debugPrintIsBasic(ArithVar v) const { + if(isBasic(v)){ + Warning() << v << " is basic." << std::endl; + }else{ + Warning() << v << " is non-basic." << std::endl; + } + } + + BasicIterator beginBasic() const { + return d_basic2RowIndex.begin(); + } + BasicIterator endBasic() const { + return d_basic2RowIndex.end(); + } + + RowIndex basicToRowIndex(ArithVar x) const { + return d_basic2RowIndex[x]; + } + + ArithVar rowIndexToBasic(RowIndex rid) const { + Assert(rid < d_rowIndex2basic.size()); + return d_rowIndex2basic[rid]; + } + + ColIterator colIterator(ArithVar x) const { + return getColumn(x).begin(); + } + + RowIterator basicRowIterator(ArithVar basic) const { + return getRow(basicToRowIndex(basic)).begin(); + } + + const Entry& basicFindEntry(ArithVar basic, ArithVar col) const { + return findEntry(basicToRowIndex(basic), col); + } + + /** + * Adds a row to the tableau. + * The new row is equivalent to: + * basicVar = \f$\sum_i\f$ coeffs[i] * variables[i] + * preconditions: + * basicVar is already declared to be basic + * basicVar does not have a row associated with it in the tableau. + * + * Note: each variables[i] does not have to be non-basic. + * Pivoting will be mimicked if it is basic. + */ + void addRow(ArithVar basicVar, + const std::vector<Rational>& coeffs, + const std::vector<ArithVar>& variables); + + /** + * preconditions: + * x_r is basic, + * x_s is non-basic, and + * a_rs != 0. + */ + void pivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCallback& cb); + + void removeBasicRow(ArithVar basic); + + uint32_t basicRowLength(ArithVar basic) const{ + RowIndex ridx = basicToRowIndex(basic); + return getRowLength(ridx); + } + + /** + * to += mult * from + * replacing from with its row. + */ + void substitutePlusTimesConstant(ArithVar to, ArithVar from, const Rational& mult, CoefficientChangeCallback& cb); + + void directlyAddToCoefficient(ArithVar rowVar, ArithVar col, const Rational& mult, CoefficientChangeCallback& cb){ + RowIndex ridx = basicToRowIndex(rowVar); + manipulateRowEntry(ridx, col, mult, cb); + } + + /* Returns the complexity of a row in the tableau. */ + uint32_t rowComplexity(ArithVar basic) const; + + /* Returns the average complexity of the rows in the tableau. */ + double avgRowComplexity() const; + + void printBasicRow(ArithVar basic, std::ostream& out); + +private: + /* Changes the basic variable on the row for basicOld to basicNew. */ + void rowPivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCallback& cb); + +};/* class Tableau */ + + + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + |