1 /********************* */
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "base/output.h"
19 #include "theory/arith/tableau.h"
27 void Tableau::pivot(ArithVar oldBasic
, ArithVar newBasic
, CoefficientChangeCallback
& cb
){
28 Assert(isBasic(oldBasic
));
29 Assert(!isBasic(newBasic
));
30 Assert(d_mergeBuffer
.empty());
32 Debug("tableau") << "Tableau::pivot(" << oldBasic
<<", " << newBasic
<<")" << endl
;
34 RowIndex ridx
= basicToRowIndex(oldBasic
);
36 rowPivot(oldBasic
, newBasic
, cb
);
37 Assert(ridx
== basicToRowIndex(newBasic
));
39 loadRowIntoBuffer(ridx
);
41 ColIterator colIter
= colIterator(newBasic
);
42 while(!colIter
.atEnd()){
43 EntryID id
= colIter
.getID();
44 Entry
& entry
= d_entries
.get(id
);
46 ++colIter
; //needs to be incremented before the variable is removed
47 if(entry
.getRowIndex() == ridx
){ continue; }
49 RowIndex to
= entry
.getRowIndex();
50 Rational coeff
= entry
.getCoefficient();
52 rowPlusBufferTimesConstant(to
, coeff
, cb
);
54 rowPlusBufferTimesConstant(to
, coeff
);
59 //Clear the column for used for this variable
61 Assert(d_mergeBuffer
.empty());
62 Assert(!isBasic(oldBasic
));
63 Assert(isBasic(newBasic
));
64 Assert(getColLength(newBasic
) == 1);
68 * Changes basic to newbasic (a variable on the row).
70 void Tableau::rowPivot(ArithVar basicOld
, ArithVar basicNew
, CoefficientChangeCallback
& cb
){
71 Assert(isBasic(basicOld
));
72 Assert(!isBasic(basicNew
));
74 RowIndex rid
= basicToRowIndex(basicOld
);
76 EntryID newBasicID
= findOnRow(rid
, basicNew
);
78 Assert(newBasicID
!= ENTRYID_SENTINEL
);
80 Tableau::Entry
& newBasicEntry
= d_entries
.get(newBasicID
);
81 const Rational
& a_rs
= newBasicEntry
.getCoefficient();
82 int a_rs_sgn
= a_rs
.sgn();
83 Rational negInverseA_rs
= -(a_rs
.inverse());
85 for(RowIterator i
= basicRowIterator(basicOld
); !i
.atEnd(); ++i
){
86 EntryID id
= i
.getID();
87 Tableau::Entry
& entry
= d_entries
.get(id
);
89 entry
.getCoefficient() *= negInverseA_rs
;
92 d_basic2RowIndex
.remove(basicOld
);
93 d_basic2RowIndex
.set(basicNew
, rid
);
94 d_rowIndex2basic
.set(rid
, basicNew
);
96 cb
.multiplyRow(rid
, -a_rs_sgn
);
99 void Tableau::addRow(ArithVar basic
,
100 const std::vector
<Rational
>& coefficients
,
101 const std::vector
<ArithVar
>& variables
)
103 Assert(basic
< getNumColumns());
104 Assert(debugIsASet(variables
));
105 Assert(coefficients
.size() == variables
.size() );
106 Assert(!isBasic(basic
));
108 RowIndex newRow
= Matrix
<Rational
>::addRow(coefficients
, variables
);
109 addEntry(newRow
, basic
, Rational(-1));
111 Assert(!d_basic2RowIndex
.isKey(basic
));
112 Assert(!d_rowIndex2basic
.isKey(newRow
));
114 d_basic2RowIndex
.set(basic
, newRow
);
115 d_rowIndex2basic
.set(newRow
, basic
);
118 if(Debug
.isOn("matrix")){ printMatrix(); }
120 NoEffectCCCB noeffect
;
121 NoEffectCCCB
* nep
= &noeffect
;
122 CoefficientChangeCallback
* cccb
= static_cast<CoefficientChangeCallback
*>(nep
);
124 vector
<Rational
>::const_iterator coeffIter
= coefficients
.begin();
125 vector
<ArithVar
>::const_iterator varsIter
= variables
.begin();
126 vector
<ArithVar
>::const_iterator varsEnd
= variables
.end();
127 for(; varsIter
!= varsEnd
; ++coeffIter
, ++varsIter
){
128 ArithVar var
= *varsIter
;
131 Rational coeff
= *coeffIter
;
133 RowIndex ri
= basicToRowIndex(var
);
135 loadRowIntoBuffer(ri
);
136 rowPlusBufferTimesConstant(newRow
, coeff
, *cccb
);
141 if(Debug
.isOn("matrix")) { printMatrix(); }
143 Assert(debugNoZeroCoefficients(newRow
));
144 Assert(debugMatchingCountsForRow(newRow
));
145 Assert(getColLength(basic
) == 1);
148 void Tableau::removeBasicRow(ArithVar basic
){
149 RowIndex rid
= basicToRowIndex(basic
);
152 d_basic2RowIndex
.remove(basic
);
153 d_rowIndex2basic
.remove(rid
);
156 void Tableau::substitutePlusTimesConstant(ArithVar to
, ArithVar from
, const Rational
& mult
, CoefficientChangeCallback
& cb
){
158 RowIndex to_idx
= basicToRowIndex(to
);
159 addEntry(to_idx
, from
, mult
); // Add an entry to be cancelled out
160 RowIndex from_idx
= basicToRowIndex(from
);
162 cb
.update(to_idx
, from
, 0, mult
.sgn());
164 loadRowIntoBuffer(from_idx
);
165 rowPlusBufferTimesConstant(to_idx
, mult
, cb
);
170 uint32_t Tableau::rowComplexity(ArithVar basic
) const{
171 uint32_t complexity
= 0;
172 for(RowIterator i
= basicRowIterator(basic
); !i
.atEnd(); ++i
){
174 complexity
+= e
.getCoefficient().complexity();
179 double Tableau::avgRowComplexity() const{
182 for(BasicIterator i
= beginBasic(), i_end
= endBasic(); i
!= i_end
; ++i
){
183 sum
+= rowComplexity(*i
);
186 return (rows
== 0) ? 0 : (sum
/rows
);
189 void Tableau::printBasicRow(ArithVar basic
, std::ostream
& out
){
190 printRow(basicToRowIndex(basic
), out
);
193 }/* CVC4::theory::arith namespace */
194 }/* CVC4::theory namespace */
195 }/* CVC4 namespace */