Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * [[ Add one-line brief description here ]]
11 : : *
12 : : * [[ Add lengthier description here ]]
13 : : * \todo document this file
14 : : */
15 : :
16 : : #include "theory/arith/linear/tableau.h"
17 : :
18 : : #include "base/output.h"
19 : :
20 : : using namespace std;
21 : : namespace cvc5::internal {
22 : : namespace theory {
23 : : namespace arith::linear {
24 : :
25 : 341292 : void Tableau::pivot(ArithVar oldBasic,
26 : : ArithVar newBasic,
27 : : CoefficientChangeCallback& cb)
28 : : {
29 [ - + ][ - + ]: 341292 : Assert(isBasic(oldBasic));
[ - - ]
30 [ - + ][ - + ]: 341292 : Assert(!isBasic(newBasic));
[ - - ]
31 [ - + ][ - + ]: 341292 : Assert(d_mergeBuffer.empty());
[ - - ]
32 : :
33 [ + - ]: 682584 : Trace("tableau") << "Tableau::pivot(" << oldBasic << ", " << newBasic << ")"
34 : 341292 : << endl;
35 : :
36 : 341292 : RowIndex ridx = basicToRowIndex(oldBasic);
37 : :
38 : 341292 : rowPivot(oldBasic, newBasic, cb);
39 [ - + ][ - + ]: 341292 : Assert(ridx == basicToRowIndex(newBasic));
[ - - ]
40 : :
41 : 341292 : loadRowIntoBuffer(ridx);
42 : :
43 : 341292 : ColIterator colIter = colIterator(newBasic);
44 [ + + ]: 6955770 : while (!colIter.atEnd())
45 : : {
46 : 6614478 : EntryID id = colIter.getID();
47 : 6614478 : Entry& entry = d_entries.get(id);
48 : :
49 : 6614478 : ++colIter; // needs to be incremented before the variable is removed
50 [ + + ]: 6614478 : if (entry.getRowIndex() == ridx)
51 : : {
52 : 341292 : continue;
53 : : }
54 : :
55 : 6273186 : RowIndex to = entry.getRowIndex();
56 : 6273186 : Rational coeff = entry.getCoefficient();
57 [ + - ]: 6273186 : if (cb.canUseRow(to))
58 : : {
59 : 6273186 : rowPlusBufferTimesConstant(to, coeff, cb);
60 : : }
61 : : else
62 : : {
63 : 0 : rowPlusBufferTimesConstant(to, coeff);
64 : : }
65 : 6273186 : }
66 : 341292 : clearBuffer();
67 : :
68 : : // Clear the column for used for this variable
69 : :
70 [ - + ][ - + ]: 341292 : Assert(d_mergeBuffer.empty());
[ - - ]
71 [ - + ][ - + ]: 341292 : Assert(!isBasic(oldBasic));
[ - - ]
72 [ - + ][ - + ]: 341292 : Assert(isBasic(newBasic));
[ - - ]
73 [ - + ][ - + ]: 341292 : Assert(getColLength(newBasic) == 1);
[ - - ]
74 : 341292 : }
75 : :
76 : : /**
77 : : * Changes basic to newbasic (a variable on the row).
78 : : */
79 : 341292 : void Tableau::rowPivot(ArithVar basicOld,
80 : : ArithVar basicNew,
81 : : CoefficientChangeCallback& cb)
82 : : {
83 [ - + ][ - + ]: 341292 : Assert(isBasic(basicOld));
[ - - ]
84 [ - + ][ - + ]: 341292 : Assert(!isBasic(basicNew));
[ - - ]
85 : :
86 : 341292 : RowIndex rid = basicToRowIndex(basicOld);
87 : :
88 : 341292 : EntryID newBasicID = findOnRow(rid, basicNew);
89 : :
90 [ - + ][ - + ]: 341292 : Assert(newBasicID != ENTRYID_SENTINEL);
[ - - ]
91 : :
92 : 341292 : Tableau::Entry& newBasicEntry = d_entries.get(newBasicID);
93 : 341292 : const Rational& a_rs = newBasicEntry.getCoefficient();
94 : 341292 : int a_rs_sgn = a_rs.sgn();
95 : 341292 : Rational negInverseA_rs = -(a_rs.inverse());
96 : :
97 [ + + ]: 6161733 : for (RowIterator i = basicRowIterator(basicOld); !i.atEnd(); ++i)
98 : : {
99 : 5820441 : EntryID id = i.getID();
100 : 5820441 : Tableau::Entry& entry = d_entries.get(id);
101 : :
102 : 5820441 : entry.getCoefficient() *= negInverseA_rs;
103 : : }
104 : :
105 : 341292 : d_basic2RowIndex.remove(basicOld);
106 : 341292 : d_basic2RowIndex.set(basicNew, rid);
107 : 341292 : d_rowIndex2basic.set(rid, basicNew);
108 : :
109 : 341292 : cb.multiplyRow(rid, -a_rs_sgn);
110 : 341292 : }
111 : :
112 : 201247 : void Tableau::addRow(ArithVar basic,
113 : : const std::vector<Rational>& coefficients,
114 : : const std::vector<ArithVar>& variables)
115 : : {
116 [ - + ][ - + ]: 201247 : Assert(basic < getNumColumns());
[ - - ]
117 [ - + ][ - + ]: 201247 : Assert(debugIsASet(variables));
[ - - ]
118 [ - + ][ - + ]: 201247 : Assert(coefficients.size() == variables.size());
[ - - ]
119 [ - + ][ - + ]: 201247 : Assert(!isBasic(basic));
[ - - ]
120 : :
121 : 201247 : RowIndex newRow = Matrix<Rational>::addRow(coefficients, variables);
122 : 201247 : addEntry(newRow, basic, Rational(-1));
123 : :
124 [ - + ][ - + ]: 201247 : Assert(!d_basic2RowIndex.isKey(basic));
[ - - ]
125 [ - + ][ - + ]: 201247 : Assert(!d_rowIndex2basic.isKey(newRow));
[ - - ]
126 : :
127 : 201247 : d_basic2RowIndex.set(basic, newRow);
128 : 201247 : d_rowIndex2basic.set(newRow, basic);
129 : :
130 [ - + ]: 201247 : if (TraceIsOn("matrix"))
131 : : {
132 : 0 : printMatrix();
133 : : }
134 : :
135 : 201247 : NoEffectCCCB noeffect;
136 : 201247 : NoEffectCCCB* nep = &noeffect;
137 : 201247 : CoefficientChangeCallback* cccb =
138 : : static_cast<CoefficientChangeCallback*>(nep);
139 : :
140 : 201247 : vector<Rational>::const_iterator coeffIter = coefficients.begin();
141 : 201247 : vector<ArithVar>::const_iterator varsIter = variables.begin();
142 : 201247 : vector<ArithVar>::const_iterator varsEnd = variables.end();
143 [ + + ]: 658640 : for (; varsIter != varsEnd; ++coeffIter, ++varsIter)
144 : : {
145 : 457393 : ArithVar var = *varsIter;
146 : :
147 [ + + ]: 457393 : if (isBasic(var))
148 : : {
149 : 125473 : Rational coeff = *coeffIter;
150 : :
151 : 125473 : RowIndex ri = basicToRowIndex(var);
152 : :
153 : 125473 : loadRowIntoBuffer(ri);
154 : 125473 : rowPlusBufferTimesConstant(newRow, coeff, *cccb);
155 : 125473 : clearBuffer();
156 : 125473 : }
157 : : }
158 : :
159 [ - + ]: 201247 : if (TraceIsOn("matrix"))
160 : : {
161 : 0 : printMatrix();
162 : : }
163 : :
164 [ - + ][ - + ]: 201247 : Assert(debugNoZeroCoefficients(newRow));
[ - - ]
165 [ - + ][ - + ]: 201247 : Assert(debugMatchingCountsForRow(newRow));
[ - - ]
166 [ - + ][ - + ]: 201247 : Assert(getColLength(basic) == 1);
[ - - ]
167 : 201247 : }
168 : :
169 : 4096 : void Tableau::removeBasicRow(ArithVar basic)
170 : : {
171 : 4096 : RowIndex rid = basicToRowIndex(basic);
172 : :
173 : 4096 : removeRow(rid);
174 : 4096 : d_basic2RowIndex.remove(basic);
175 : 4096 : d_rowIndex2basic.remove(rid);
176 : 4096 : }
177 : :
178 : 5039 : void Tableau::substitutePlusTimesConstant(ArithVar to,
179 : : ArithVar from,
180 : : const Rational& mult,
181 : : CoefficientChangeCallback& cb)
182 : : {
183 [ + - ]: 5039 : if (!mult.isZero())
184 : : {
185 : 5039 : RowIndex to_idx = basicToRowIndex(to);
186 : 5039 : addEntry(to_idx, from, mult); // Add an entry to be cancelled out
187 : 5039 : RowIndex from_idx = basicToRowIndex(from);
188 : :
189 : 5039 : cb.update(to_idx, from, 0, mult.sgn());
190 : :
191 : 5039 : loadRowIntoBuffer(from_idx);
192 : 5039 : rowPlusBufferTimesConstant(to_idx, mult, cb);
193 : 5039 : clearBuffer();
194 : : }
195 : 5039 : }
196 : :
197 : 0 : uint32_t Tableau::rowComplexity(ArithVar basic) const
198 : : {
199 : 0 : uint32_t complexity = 0;
200 [ - - ]: 0 : for (RowIterator i = basicRowIterator(basic); !i.atEnd(); ++i)
201 : : {
202 : 0 : const Entry& e = *i;
203 : 0 : complexity += e.getCoefficient().complexity();
204 : : }
205 : 0 : return complexity;
206 : : }
207 : :
208 : 0 : double Tableau::avgRowComplexity() const
209 : : {
210 : 0 : double sum = 0;
211 : 0 : uint32_t rows = 0;
212 [ - - ]: 0 : for (BasicIterator i = beginBasic(), i_end = endBasic(); i != i_end; ++i)
213 : : {
214 : 0 : sum += rowComplexity(*i);
215 : 0 : rows++;
216 : : }
217 [ - - ]: 0 : return (rows == 0) ? 0 : (sum / rows);
218 : : }
219 : :
220 : 0 : void Tableau::printBasicRow(ArithVar basic, std::ostream& out)
221 : : {
222 : 0 : printRow(basicToRowIndex(basic), out);
223 : 0 : }
224 : :
225 : : } // namespace arith::linear
226 : : } // namespace theory
227 : : } // namespace cvc5::internal
|
