1 #include "cvc4_private.h"
5 #include "util/dense_map.h"
6 #include "util/rational.h"
7 #include "theory/arith/arithvar.h"
8 #include "theory/arith/matrix.h"
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.
21 class Tableau
: public Matrix
<Rational
> {
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
;
29 // RowIndex |-> Basic Variable
30 typedef DenseMap
<ArithVar
> RowIndexToBasicMap
;
31 RowIndexToBasicMap d_rowIndex2basic
;
35 Tableau() : Matrix
<Rational
>(Rational(0)) {}
37 typedef Matrix
<Rational
>::ColIterator ColIterator
;
38 typedef Matrix
<Rational
>::RowIterator RowIterator
;
39 typedef BasicToRowMap::const_iterator BasicIterator
;
41 typedef MatrixEntry
<Rational
> Entry
;
43 bool isBasic(ArithVar v
) const{
44 return d_basic2RowIndex
.isKey(v
);
47 void debugPrintIsBasic(ArithVar v
) const {
49 Warning() << v
<< " is basic." << std::endl
;
51 Warning() << v
<< " is non-basic." << std::endl
;
55 BasicIterator
beginBasic() const {
56 return d_basic2RowIndex
.begin();
58 BasicIterator
endBasic() const {
59 return d_basic2RowIndex
.end();
62 RowIndex
basicToRowIndex(ArithVar x
) const {
63 return d_basic2RowIndex
[x
];
66 ArithVar
rowIndexToBasic(RowIndex rid
) const {
67 Assert(rid
< d_rowIndex2basic
.size());
68 return d_rowIndex2basic
[rid
];
71 ColIterator
colIterator(ArithVar x
) const {
72 return getColumn(x
).begin();
75 RowIterator
ridRowIterator(RowIndex rid
) const {
76 return getRow(rid
).begin();
79 RowIterator
basicRowIterator(ArithVar basic
) const {
80 return ridRowIterator(basicToRowIndex(basic
));
83 const Entry
& basicFindEntry(ArithVar basic
, ArithVar col
) const {
84 return findEntry(basicToRowIndex(basic
), col
);
88 * Adds a row to the tableau.
89 * The new row is equivalent to:
90 * basicVar = \f$\sum_i\f$ coeffs[i] * variables[i]
92 * basicVar is already declared to be basic
93 * basicVar does not have a row associated with it in the tableau.
95 * Note: each variables[i] does not have to be non-basic.
96 * Pivoting will be mimicked if it is basic.
98 void addRow(ArithVar basicVar
,
99 const std::vector
<Rational
>& coeffs
,
100 const std::vector
<ArithVar
>& variables
);
105 * x_s is non-basic, and
108 void pivot(ArithVar basicOld
, ArithVar basicNew
, CoefficientChangeCallback
& cb
);
110 void removeBasicRow(ArithVar basic
);
112 uint32_t basicRowLength(ArithVar basic
) const{
113 RowIndex ridx
= basicToRowIndex(basic
);
114 return getRowLength(ridx
);
119 * replacing from with its row.
121 void substitutePlusTimesConstant(ArithVar to
, ArithVar from
, const Rational
& mult
, CoefficientChangeCallback
& cb
);
123 void directlyAddToCoefficient(ArithVar rowVar
, ArithVar col
, const Rational
& mult
, CoefficientChangeCallback
& cb
){
124 RowIndex ridx
= basicToRowIndex(rowVar
);
125 manipulateRowEntry(ridx
, col
, mult
, cb
);
128 /* Returns the complexity of a row in the tableau. */
129 uint32_t rowComplexity(ArithVar basic
) const;
131 /* Returns the average complexity of the rows in the tableau. */
132 double avgRowComplexity() const;
134 void printBasicRow(ArithVar basic
, std::ostream
& out
);
137 /* Changes the basic variable on the row for basicOld to basicNew. */
138 void rowPivot(ArithVar basicOld
, ArithVar basicNew
, CoefficientChangeCallback
& cb
);
140 };/* class Tableau */
144 }/* CVC4::theory::arith namespace */
145 }/* CVC4::theory namespace */
146 }/* CVC4 namespace */