1 /********************* */
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
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "cvc4_private.h"
22 #include "util/dense_map.h"
23 #include "util/rational.h"
24 #include "theory/arith/arithvar.h"
25 #include "theory/arith/matrix.h"
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.
38 class Tableau
: public Matrix
<Rational
> {
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
;
46 // RowIndex |-> Basic Variable
47 typedef DenseMap
<ArithVar
> RowIndexToBasicMap
;
48 RowIndexToBasicMap d_rowIndex2basic
;
52 Tableau() : Matrix
<Rational
>(Rational(0)) {}
54 typedef Matrix
<Rational
>::ColIterator ColIterator
;
55 typedef Matrix
<Rational
>::RowIterator RowIterator
;
56 typedef BasicToRowMap::const_iterator BasicIterator
;
58 typedef MatrixEntry
<Rational
> Entry
;
60 bool isBasic(ArithVar v
) const{
61 return d_basic2RowIndex
.isKey(v
);
64 void debugPrintIsBasic(ArithVar v
) const {
66 Warning() << v
<< " is basic." << std::endl
;
68 Warning() << v
<< " is non-basic." << std::endl
;
72 BasicIterator
beginBasic() const {
73 return d_basic2RowIndex
.begin();
75 BasicIterator
endBasic() const {
76 return d_basic2RowIndex
.end();
79 RowIndex
basicToRowIndex(ArithVar x
) const {
80 return d_basic2RowIndex
[x
];
83 ArithVar
rowIndexToBasic(RowIndex rid
) const {
84 Assert(d_rowIndex2basic
.isKey(rid
));
85 return d_rowIndex2basic
[rid
];
88 ColIterator
colIterator(ArithVar x
) const {
89 return getColumn(x
).begin();
92 RowIterator
ridRowIterator(RowIndex rid
) const {
93 return getRow(rid
).begin();
96 RowIterator
basicRowIterator(ArithVar basic
) const {
97 return ridRowIterator(basicToRowIndex(basic
));
100 const Entry
& basicFindEntry(ArithVar basic
, ArithVar col
) const {
101 return findEntry(basicToRowIndex(basic
), col
);
105 * Adds a row to the tableau.
106 * The new row is equivalent to:
107 * basicVar = \f$\sum_i\f$ coeffs[i] * variables[i]
109 * basicVar is already declared to be basic
110 * basicVar does not have a row associated with it in the tableau.
112 * Note: each variables[i] does not have to be non-basic.
113 * Pivoting will be mimicked if it is basic.
115 void addRow(ArithVar basicVar
,
116 const std::vector
<Rational
>& coeffs
,
117 const std::vector
<ArithVar
>& variables
);
122 * x_s is non-basic, and
125 void pivot(ArithVar basicOld
, ArithVar basicNew
, CoefficientChangeCallback
& cb
);
127 void removeBasicRow(ArithVar basic
);
129 uint32_t basicRowLength(ArithVar basic
) const{
130 RowIndex ridx
= basicToRowIndex(basic
);
131 return getRowLength(ridx
);
136 * replacing from with its row.
138 void substitutePlusTimesConstant(ArithVar to
, ArithVar from
, const Rational
& mult
, CoefficientChangeCallback
& cb
);
140 void directlyAddToCoefficient(ArithVar rowVar
, ArithVar col
, const Rational
& mult
, CoefficientChangeCallback
& cb
){
141 RowIndex ridx
= basicToRowIndex(rowVar
);
142 manipulateRowEntry(ridx
, col
, mult
, cb
);
145 /* Returns the complexity of a row in the tableau. */
146 uint32_t rowComplexity(ArithVar basic
) const;
148 /* Returns the average complexity of the rows in the tableau. */
149 double avgRowComplexity() const;
151 void printBasicRow(ArithVar basic
, std::ostream
& out
);
154 /* Changes the basic variable on the row for basicOld to basicNew. */
155 void rowPivot(ArithVar basicOld
, ArithVar basicNew
, CoefficientChangeCallback
& cb
);
157 };/* class Tableau */
161 }/* CVC4::theory::arith namespace */
162 }/* CVC4::theory namespace */
163 }/* CVC4 namespace */