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-2014 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 "theory/arith/tableau.h"
26 void Tableau::pivot(ArithVar oldBasic
, ArithVar newBasic
, CoefficientChangeCallback
& cb
){
27 Assert(isBasic(oldBasic
));
28 Assert(!isBasic(newBasic
));
29 Assert(d_mergeBuffer
.empty());
31 Debug("tableau") << "Tableau::pivot(" << oldBasic
<<", " << newBasic
<<")" << endl
;
33 RowIndex ridx
= basicToRowIndex(oldBasic
);
35 rowPivot(oldBasic
, newBasic
, cb
);
36 Assert(ridx
== basicToRowIndex(newBasic
));
38 loadRowIntoBuffer(ridx
);
40 ColIterator colIter
= colIterator(newBasic
);
41 while(!colIter
.atEnd()){
42 EntryID id
= colIter
.getID();
43 Entry
& entry
= d_entries
.get(id
);
45 ++colIter
; //needs to be incremented before the variable is removed
46 if(entry
.getRowIndex() == ridx
){ continue; }
48 RowIndex to
= entry
.getRowIndex();
49 Rational coeff
= entry
.getCoefficient();
51 rowPlusBufferTimesConstant(to
, coeff
, cb
);
53 rowPlusBufferTimesConstant(to
, coeff
);
58 //Clear the column for used for this variable
60 Assert(d_mergeBuffer
.empty());
61 Assert(!isBasic(oldBasic
));
62 Assert(isBasic(newBasic
));
63 Assert(getColLength(newBasic
) == 1);
67 * Changes basic to newbasic (a variable on the row).
69 void Tableau::rowPivot(ArithVar basicOld
, ArithVar basicNew
, CoefficientChangeCallback
& cb
){
70 Assert(isBasic(basicOld
));
71 Assert(!isBasic(basicNew
));
73 RowIndex rid
= basicToRowIndex(basicOld
);
75 EntryID newBasicID
= findOnRow(rid
, basicNew
);
77 Assert(newBasicID
!= ENTRYID_SENTINEL
);
79 Tableau::Entry
& newBasicEntry
= d_entries
.get(newBasicID
);
80 const Rational
& a_rs
= newBasicEntry
.getCoefficient();
81 int a_rs_sgn
= a_rs
.sgn();
82 Rational negInverseA_rs
= -(a_rs
.inverse());
84 for(RowIterator i
= basicRowIterator(basicOld
); !i
.atEnd(); ++i
){
85 EntryID id
= i
.getID();
86 Tableau::Entry
& entry
= d_entries
.get(id
);
88 entry
.getCoefficient() *= negInverseA_rs
;
91 d_basic2RowIndex
.remove(basicOld
);
92 d_basic2RowIndex
.set(basicNew
, rid
);
93 d_rowIndex2basic
.set(rid
, basicNew
);
95 cb
.multiplyRow(rid
, -a_rs_sgn
);
100 void Tableau::addRow(ArithVar basic
,
101 const std::vector
<Rational
>& coefficients
,
102 const std::vector
<ArithVar
>& variables
)
104 Assert(basic
< getNumColumns());
106 Assert(coefficients
.size() == variables
.size() );
107 Assert(!isBasic(basic
));
109 RowIndex newRow
= Matrix
<Rational
>::addRow(coefficients
, variables
);
110 addEntry(newRow
, basic
, Rational(-1));
112 Assert(!d_basic2RowIndex
.isKey(basic
));
113 Assert(!d_rowIndex2basic
.isKey(newRow
));
115 d_basic2RowIndex
.set(basic
, newRow
);
116 d_rowIndex2basic
.set(newRow
, basic
);
119 if(Debug
.isOn("matrix")){ printMatrix(); }
121 NoEffectCCCB noeffect
;
122 NoEffectCCCB
* nep
= &noeffect
;
123 CoefficientChangeCallback
* cccb
= static_cast<CoefficientChangeCallback
*>(nep
);
125 vector
<Rational
>::const_iterator coeffIter
= coefficients
.begin();
126 vector
<ArithVar
>::const_iterator varsIter
= variables
.begin();
127 vector
<ArithVar
>::const_iterator varsEnd
= variables
.end();
128 for(; varsIter
!= varsEnd
; ++coeffIter
, ++varsIter
){
129 ArithVar var
= *varsIter
;
132 Rational coeff
= *coeffIter
;
134 RowIndex ri
= basicToRowIndex(var
);
136 loadRowIntoBuffer(ri
);
137 rowPlusBufferTimesConstant(newRow
, coeff
, *cccb
);
142 if(Debug
.isOn("matrix")) { printMatrix(); }
144 Assert(debugNoZeroCoefficients(newRow
));
145 Assert(debugMatchingCountsForRow(newRow
));
146 Assert(getColLength(basic
) == 1);
149 void Tableau::removeBasicRow(ArithVar basic
){
150 RowIndex rid
= basicToRowIndex(basic
);
153 d_basic2RowIndex
.remove(basic
);
154 d_rowIndex2basic
.remove(rid
);
157 void Tableau::substitutePlusTimesConstant(ArithVar to
, ArithVar from
, const Rational
& mult
, CoefficientChangeCallback
& cb
){
159 RowIndex to_idx
= basicToRowIndex(to
);
160 addEntry(to_idx
, from
, mult
); // Add an entry to be cancelled out
161 RowIndex from_idx
= basicToRowIndex(from
);
163 cb
.update(to_idx
, from
, 0, mult
.sgn());
165 loadRowIntoBuffer(from_idx
);
166 rowPlusBufferTimesConstant(to_idx
, mult
, cb
);
171 uint32_t Tableau::rowComplexity(ArithVar basic
) const{
172 uint32_t complexity
= 0;
173 for(RowIterator i
= basicRowIterator(basic
); !i
.atEnd(); ++i
){
175 complexity
+= e
.getCoefficient().complexity();
180 double Tableau::avgRowComplexity() const{
183 for(BasicIterator i
= beginBasic(), i_end
= endBasic(); i
!= i_end
; ++i
){
184 sum
+= rowComplexity(*i
);
187 return (rows
== 0) ? 0 : (sum
/rows
);
190 void Tableau::printBasicRow(ArithVar basic
, std::ostream
& out
){
191 printRow(basicToRowIndex(basic
), out
);
194 }/* CVC4::theory::arith namespace */
195 }/* CVC4::theory namespace */
196 }/* CVC4 namespace */