1 #include "theory/arith/tableau.h"
9 void Tableau::pivot(ArithVar oldBasic
, ArithVar newBasic
, CoefficientChangeCallback
& cb
){
10 Assert(isBasic(oldBasic
));
11 Assert(!isBasic(newBasic
));
12 Assert(d_mergeBuffer
.empty());
14 Debug("tableau") << "Tableau::pivot(" << oldBasic
<<", " << newBasic
<<")" << endl
;
16 RowIndex ridx
= basicToRowIndex(oldBasic
);
18 rowPivot(oldBasic
, newBasic
, cb
);
19 Assert(ridx
== basicToRowIndex(newBasic
));
21 loadRowIntoBuffer(ridx
);
23 ColIterator colIter
= colIterator(newBasic
);
24 while(!colIter
.atEnd()){
25 EntryID id
= colIter
.getID();
26 Entry
& entry
= d_entries
.get(id
);
28 ++colIter
; //needs to be incremented before the variable is removed
29 if(entry
.getRowIndex() == ridx
){ continue; }
31 RowIndex to
= entry
.getRowIndex();
32 Rational coeff
= entry
.getCoefficient();
34 rowPlusBufferTimesConstant(to
, coeff
, cb
);
36 rowPlusBufferTimesConstant(to
, coeff
);
41 //Clear the column for used for this variable
43 Assert(d_mergeBuffer
.empty());
44 Assert(!isBasic(oldBasic
));
45 Assert(isBasic(newBasic
));
46 Assert(getColLength(newBasic
) == 1);
50 * Changes basic to newbasic (a variable on the row).
52 void Tableau::rowPivot(ArithVar basicOld
, ArithVar basicNew
, CoefficientChangeCallback
& cb
){
53 Assert(isBasic(basicOld
));
54 Assert(!isBasic(basicNew
));
56 RowIndex rid
= basicToRowIndex(basicOld
);
58 EntryID newBasicID
= findOnRow(rid
, basicNew
);
60 Assert(newBasicID
!= ENTRYID_SENTINEL
);
62 Tableau::Entry
& newBasicEntry
= d_entries
.get(newBasicID
);
63 const Rational
& a_rs
= newBasicEntry
.getCoefficient();
64 int a_rs_sgn
= a_rs
.sgn();
65 Rational negInverseA_rs
= -(a_rs
.inverse());
67 for(RowIterator i
= basicRowIterator(basicOld
); !i
.atEnd(); ++i
){
68 EntryID id
= i
.getID();
69 Tableau::Entry
& entry
= d_entries
.get(id
);
71 entry
.getCoefficient() *= negInverseA_rs
;
74 d_basic2RowIndex
.remove(basicOld
);
75 d_basic2RowIndex
.set(basicNew
, rid
);
76 d_rowIndex2basic
.set(rid
, basicNew
);
78 cb
.multiplyRow(rid
, -a_rs_sgn
);
83 void Tableau::addRow(ArithVar basic
,
84 const std::vector
<Rational
>& coefficients
,
85 const std::vector
<ArithVar
>& variables
)
87 Assert(basic
< getNumColumns());
89 Assert(coefficients
.size() == variables
.size() );
90 Assert(!isBasic(basic
));
92 RowIndex newRow
= Matrix
<Rational
>::addRow(coefficients
, variables
);
93 addEntry(newRow
, basic
, Rational(-1));
95 Assert(!d_basic2RowIndex
.isKey(basic
));
96 Assert(!d_rowIndex2basic
.isKey(newRow
));
98 d_basic2RowIndex
.set(basic
, newRow
);
99 d_rowIndex2basic
.set(newRow
, basic
);
102 if(Debug
.isOn("matrix")){ printMatrix(); }
104 NoEffectCCCB noeffect
;
105 NoEffectCCCB
* nep
= &noeffect
;
106 CoefficientChangeCallback
* cccb
= static_cast<CoefficientChangeCallback
*>(nep
);
108 vector
<Rational
>::const_iterator coeffIter
= coefficients
.begin();
109 vector
<ArithVar
>::const_iterator varsIter
= variables
.begin();
110 vector
<ArithVar
>::const_iterator varsEnd
= variables
.end();
111 for(; varsIter
!= varsEnd
; ++coeffIter
, ++varsIter
){
112 ArithVar var
= *varsIter
;
115 Rational coeff
= *coeffIter
;
117 RowIndex ri
= basicToRowIndex(var
);
119 loadRowIntoBuffer(ri
);
120 rowPlusBufferTimesConstant(newRow
, coeff
, *cccb
);
125 if(Debug
.isOn("matrix")) { printMatrix(); }
127 Assert(debugNoZeroCoefficients(newRow
));
128 Assert(debugMatchingCountsForRow(newRow
));
129 Assert(getColLength(basic
) == 1);
132 void Tableau::removeBasicRow(ArithVar basic
){
133 RowIndex rid
= basicToRowIndex(basic
);
136 d_basic2RowIndex
.remove(basic
);
137 d_rowIndex2basic
.remove(rid
);
140 void Tableau::substitutePlusTimesConstant(ArithVar to
, ArithVar from
, const Rational
& mult
, CoefficientChangeCallback
& cb
){
142 RowIndex to_idx
= basicToRowIndex(to
);
143 addEntry(to_idx
, from
, mult
); // Add an entry to be cancelled out
144 RowIndex from_idx
= basicToRowIndex(from
);
146 cb
.update(to_idx
, from
, 0, mult
.sgn());
148 loadRowIntoBuffer(from_idx
);
149 rowPlusBufferTimesConstant(to_idx
, mult
, cb
);
154 uint32_t Tableau::rowComplexity(ArithVar basic
) const{
155 uint32_t complexity
= 0;
156 for(RowIterator i
= basicRowIterator(basic
); !i
.atEnd(); ++i
){
158 complexity
+= e
.getCoefficient().complexity();
163 double Tableau::avgRowComplexity() const{
166 for(BasicIterator i
= beginBasic(), i_end
= endBasic(); i
!= i_end
; ++i
){
167 sum
+= rowComplexity(*i
);
170 return (rows
== 0) ? 0 : (sum
/rows
);
173 void Tableau::printBasicRow(ArithVar basic
, std::ostream
& out
){
174 printRow(basicToRowIndex(basic
), out
);
177 }/* CVC4::theory::arith namespace */
178 }/* CVC4::theory namespace */
179 }/* CVC4 namespace */