Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Tim King, Gereon Kremer, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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.
11 : : * ****************************************************************************
12 : : * Sparse matrix implementations for different types.
13 : : *
14 : : * Sparse matrix implementations for different types.
15 : : * This defines Matrix<T>, IntegerEqualityTables and Tableau.
16 : : */
17 : :
18 : : #include "cvc5_private.h"
19 : :
20 : : #pragma once
21 : :
22 : : #include <queue>
23 : : #include <utility>
24 : : #include <vector>
25 : :
26 : : #include "base/output.h"
27 : : #include "theory/arith/linear/arithvar.h"
28 : : #include "util/dense_map.h"
29 : : #include "util/index.h"
30 : :
31 : : namespace cvc5::internal {
32 : : namespace theory {
33 : : namespace arith::linear {
34 : :
35 : : typedef Index EntryID;
36 : : const EntryID ENTRYID_SENTINEL = std::numeric_limits<EntryID>::max();
37 : :
38 : : typedef Index RowIndex;
39 : : const RowIndex ROW_INDEX_SENTINEL = std::numeric_limits<RowIndex>::max();
40 : :
41 : : class CoefficientChangeCallback {
42 : : public:
43 : 246955 : virtual ~CoefficientChangeCallback() {}
44 : : virtual void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) = 0;
45 : : virtual void multiplyRow(RowIndex ridx, int Sgn) = 0;
46 : : virtual bool canUseRow(RowIndex ridx) const = 0;
47 : : };
48 : :
49 : : class NoEffectCCCB : public CoefficientChangeCallback {
50 : : public:
51 : : void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) override;
52 : : void multiplyRow(RowIndex ridx, int Sgn) override;
53 : : bool canUseRow(RowIndex ridx) const override;
54 : : };
55 : :
56 : : template<class T>
57 : : class MatrixEntry {
58 : : private:
59 : : RowIndex d_rowIndex;
60 : : ArithVar d_colVar;
61 : :
62 : : EntryID d_nextRow;
63 : : EntryID d_nextCol;
64 : :
65 : : EntryID d_prevRow;
66 : : EntryID d_prevCol;
67 : :
68 : : T d_coefficient;
69 : :
70 : : public:
71 : 1516923 : MatrixEntry():
72 : 1516923 : d_rowIndex(ROW_INDEX_SENTINEL),
73 : 1516923 : d_colVar(ARITHVAR_SENTINEL),
74 : 1516923 : d_nextRow(ENTRYID_SENTINEL),
75 : 1516923 : d_nextCol(ENTRYID_SENTINEL),
76 : 1516923 : d_prevRow(ENTRYID_SENTINEL),
77 : 1516923 : d_prevCol(ENTRYID_SENTINEL),
78 : 1516923 : d_coefficient()
79 : 1516923 : {}
80 : :
81 : 41955881 : MatrixEntry(RowIndex row, ArithVar col, const T& coeff):
82 : 41955881 : d_rowIndex(row),
83 : 41955881 : d_colVar(col),
84 : 41955881 : d_nextRow(ENTRYID_SENTINEL),
85 : 41955881 : d_nextCol(ENTRYID_SENTINEL),
86 : 41955881 : d_prevRow(ENTRYID_SENTINEL),
87 : 41955881 : d_prevCol(ENTRYID_SENTINEL),
88 : 41955881 : d_coefficient(coeff)
89 : 41955881 : {}
90 : :
91 : : private:
92 : 41132126 : bool unusedConsistent() const {
93 : : return
94 [ + + ][ - + ]: 41493222 : (d_rowIndex == ROW_INDEX_SENTINEL && d_colVar == ARITHVAR_SENTINEL) ||
95 [ + - ][ + - ]: 41493222 : (d_rowIndex != ROW_INDEX_SENTINEL && d_colVar != ARITHVAR_SENTINEL);
96 : : }
97 : :
98 : : public:
99 : :
100 : 543696122 : EntryID getNextRowEntryID() const {
101 : 543696122 : return d_nextRow;
102 : : }
103 : :
104 : 151412574 : EntryID getNextColEntryID() const {
105 : 151412574 : return d_nextCol;
106 : : }
107 : 40771030 : EntryID getPrevRowEntryID() const {
108 : 40771030 : return d_prevRow;
109 : : }
110 : :
111 : 40771030 : EntryID getPrevColEntryID() const {
112 : 40771030 : return d_prevCol;
113 : : }
114 : :
115 : 64801639 : void setNextRowEntryID(EntryID id) {
116 : 64801639 : d_nextRow = id;
117 : 64801639 : }
118 : 72123619 : void setNextColEntryID(EntryID id) {
119 : 72123619 : d_nextCol = id;
120 : 72123619 : }
121 : 82132567 : void setPrevRowEntryID(EntryID id) {
122 : 82132567 : d_prevRow = id;
123 : 82132567 : }
124 : 81464834 : void setPrevColEntryID(EntryID id) {
125 : 81464834 : d_prevCol = id;
126 : 81464834 : }
127 : :
128 : 136110857 : RowIndex getRowIndex() const{
129 : 136110857 : return d_rowIndex;
130 : : }
131 : :
132 : 401187735 : ArithVar getColVar() const{
133 : 401187735 : return d_colVar;
134 : : }
135 : :
136 : 442984800 : const T& getCoefficient() const {
137 : 442984800 : return d_coefficient;
138 : : }
139 : :
140 : 113344731 : T& getCoefficient(){
141 : 113344731 : return d_coefficient;
142 : : }
143 : :
144 : : void setCoefficient(const T& t){
145 : : d_coefficient = t;
146 : : }
147 : :
148 : 40771030 : void markBlank() {
149 : 40771030 : d_rowIndex = ROW_INDEX_SENTINEL;
150 : 40771030 : d_colVar = ARITHVAR_SENTINEL;
151 : 40771030 : }
152 : :
153 : 41132126 : bool blank() const{
154 [ - + ][ - + ]: 41132126 : Assert(unusedConsistent());
[ - - ]
155 : :
156 : 41132126 : return d_rowIndex == ROW_INDEX_SENTINEL;
157 : : }
158 : : }; /* class MatrixEntry<T> */
159 : :
160 : : template<class T>
161 : : class MatrixEntryVector {
162 : : private:
163 : : typedef MatrixEntry<T> EntryType;
164 : : typedef std::vector<EntryType> EntryArray;
165 : :
166 : : EntryArray d_entries;
167 : : std::queue<EntryID> d_freedEntries;
168 : :
169 : : uint32_t d_size;
170 : :
171 : : public:
172 : 99814 : MatrixEntryVector():
173 : 99814 : d_entries(), d_freedEntries(), d_size(0)
174 : 99814 : {}
175 : :
176 : 1113178731 : const EntryType& operator[](EntryID id) const{
177 [ - + ][ - + ]: 1113178731 : Assert(inBounds(id));
[ - - ]
178 : 1113178731 : return d_entries[id];
179 : : }
180 : :
181 : 767280918 : EntryType& get(EntryID id){
182 [ - + ][ - + ]: 767280918 : Assert(inBounds(id));
[ - - ]
183 : 767280918 : return d_entries[id];
184 : : }
185 : :
186 : 40771030 : void freeEntry(EntryID id){
187 [ - + ][ - + ]: 40771030 : Assert(get(id).blank());
[ - - ]
188 [ - + ][ - + ]: 40771030 : Assert(d_size > 0);
[ - - ]
189 : :
190 : 40771030 : d_freedEntries.push(id);
191 : 40771030 : --d_size;
192 : 40771030 : }
193 : :
194 : 41955881 : EntryID newEntry(){
195 : : EntryID newId;
196 [ + + ]: 41955881 : if(d_freedEntries.empty()){
197 : 1417109 : newId = d_entries.size();
198 : 1417109 : d_entries.push_back(MatrixEntry<T>());
199 : : }else{
200 : 40538772 : newId = d_freedEntries.front();
201 : 40538772 : d_freedEntries.pop();
202 : : }
203 : 41955881 : ++d_size;
204 : 41955881 : return newId;
205 : : }
206 : :
207 : : uint32_t size() const{ return d_size; }
208 : : uint32_t capacity() const{ return d_entries.capacity(); }
209 : :
210 : :
211 : : private:
212 : 1880459649 : bool inBounds(EntryID id) const{
213 : 1880459649 : return id < d_entries.size();
214 : : }
215 : : }; /* class MatrixEntryVector<T> */
216 : :
217 : : template <class T, bool isRow>
218 : : class MatrixVector {
219 : : private:
220 : : EntryID d_head;
221 : : uint32_t d_size;
222 : :
223 : : MatrixEntryVector<T>* d_entries;
224 : :
225 : : class Iterator {
226 : : private:
227 : : EntryID d_curr;
228 : : const MatrixEntryVector<T>* d_entries;
229 : :
230 : : public:
231 : 68293440 : Iterator(EntryID start, const MatrixEntryVector<T>* entries) :
232 : 68293440 : d_curr(start), d_entries(entries)
233 : 68293440 : {}
234 : :
235 : : public:
236 : :
237 : 137509194 : EntryID getID() const {
238 : 137509194 : return d_curr;
239 : : }
240 : :
241 : 499250999 : const MatrixEntry<T>& operator*() const{
242 [ - + ][ - + ]: 499250999 : Assert(!atEnd());
[ - - ]
243 : 499250999 : return (*d_entries)[d_curr];
244 : : }
245 : :
246 : 613566636 : Iterator& operator++(){
247 [ - + ][ - + ]: 613566636 : Assert(!atEnd());
[ - - ]
248 : 613566636 : const MatrixEntry<T>& entry = (*d_entries)[d_curr];
249 : 613566636 : d_curr = isRow ? entry.getNextRowEntryID() : entry.getNextColEntryID();
250 : 613566636 : return *this;
251 : : }
252 : :
253 : 1545646677 : bool atEnd() const {
254 : 1545646677 : return d_curr == ENTRYID_SENTINEL;
255 : : }
256 : :
257 : : bool operator==(const Iterator& i) const{
258 : : return d_curr == i.d_curr && d_entries == i.d_entries;
259 : : }
260 : :
261 : 234813846 : bool operator!=(const Iterator& i) const{
262 [ + + ][ - + ]: 234813846 : return !(d_curr == i.d_curr && d_entries == i.d_entries);
263 : : }
264 : : }; /* class MatrixVector<T, isRow>::Iterator */
265 : :
266 : : public:
267 : 552186 : MatrixVector(MatrixEntryVector<T>* mev)
268 : 552186 : : d_head(ENTRYID_SENTINEL), d_size(0), d_entries(mev)
269 : 552186 : {}
270 : :
271 : : MatrixVector(EntryID head, uint32_t size, MatrixEntryVector<T>* mev)
272 : : : d_head(head), d_size(size), d_entries(mev)
273 : : {}
274 : :
275 : : typedef Iterator const_iterator;
276 : 54076252 : const_iterator begin() const {
277 : 54076252 : return Iterator(d_head, d_entries);
278 : : }
279 : 14217188 : const_iterator end() const {
280 : 14217188 : return Iterator(ENTRYID_SENTINEL, d_entries);
281 : : }
282 : :
283 : : EntryID getHead() const { return d_head; }
284 : :
285 : 107127198 : uint32_t getSize() const { return d_size; }
286 : :
287 : 83911762 : void insert(EntryID newId){
288 : : if(isRow){
289 : 41955881 : d_entries->get(newId).setNextRowEntryID(d_head);
290 : :
291 [ + + ]: 41955881 : if(d_head != ENTRYID_SENTINEL){
292 : 41758488 : d_entries->get(d_head).setPrevRowEntryID(newId);
293 : : }
294 : : }else{
295 : 41955881 : d_entries->get(newId).setNextColEntryID(d_head);
296 : :
297 [ + + ]: 41955881 : if(d_head != ENTRYID_SENTINEL){
298 : 41621475 : d_entries->get(d_head).setPrevColEntryID(newId);
299 : : }
300 : : }
301 : :
302 : 83911762 : d_head = newId;
303 : 83911762 : ++d_size;
304 : 83911762 : }
305 : 81542060 : void remove(EntryID id){
306 [ - + ][ - + ]: 81542060 : Assert(d_size > 0);
[ - - ]
307 : 81542060 : --d_size;
308 : : if(isRow){
309 : 40771030 : EntryID prevRow = d_entries->get(id).getPrevRowEntryID();
310 : 40771030 : EntryID nextRow = d_entries->get(id).getNextRowEntryID();
311 : :
312 [ + + ]: 40771030 : if(d_head == id){
313 : 17925272 : d_head = nextRow;
314 : : }
315 [ + + ]: 40771030 : if(prevRow != ENTRYID_SENTINEL){
316 : 22845758 : d_entries->get(prevRow).setNextRowEntryID(nextRow);
317 : : }
318 [ + + ]: 40771030 : if(nextRow != ENTRYID_SENTINEL){
319 : 40374079 : d_entries->get(nextRow).setPrevRowEntryID(prevRow);
320 : : }
321 : : }else{
322 : 40771030 : EntryID prevCol = d_entries->get(id).getPrevColEntryID();
323 : 40771030 : EntryID nextCol = d_entries->get(id).getNextColEntryID();
324 : :
325 [ + + ]: 40771030 : if(d_head == id){
326 : 10603292 : d_head = nextCol;
327 : : }
328 : :
329 [ + + ]: 40771030 : if(prevCol != ENTRYID_SENTINEL){
330 : 30167738 : d_entries->get(prevCol).setNextColEntryID(nextCol);
331 : : }
332 [ + + ]: 40771030 : if(nextCol != ENTRYID_SENTINEL){
333 : 39843359 : d_entries->get(nextCol).setPrevColEntryID(prevCol);
334 : : }
335 : : }
336 : 81542060 : }
337 : : }; /* class MatrixVector<T, isRow> */
338 : :
339 : : template <class T>
340 : : class RowVector : public MatrixVector<T, true>
341 : : {
342 : : private:
343 : : typedef MatrixVector<T, true> SuperT;
344 : : public:
345 : : typedef typename SuperT::const_iterator const_iterator;
346 : :
347 : 193468 : RowVector(MatrixEntryVector<T>* mev) : SuperT(mev){}
348 : : RowVector(EntryID head, uint32_t size, MatrixEntryVector<T>* mev)
349 : : : SuperT(head, size, mev){}
350 : : };/* class RowVector<T> */
351 : :
352 : : template <class T>
353 : : class ColumnVector : public MatrixVector<T, false>
354 : : {
355 : : private:
356 : : typedef MatrixVector<T, false> SuperT;
357 : : public:
358 : : typedef typename SuperT::const_iterator const_iterator;
359 : :
360 : 358718 : ColumnVector(MatrixEntryVector<T>* mev) : SuperT(mev){}
361 : : ColumnVector(EntryID head, uint32_t size, MatrixEntryVector<T>* mev)
362 : : : SuperT(head, size, mev){}
363 : : };/* class ColumnVector<T> */
364 : :
365 : : template <class T>
366 : : class Matrix {
367 : : public:
368 : : typedef MatrixEntry<T> Entry;
369 : :
370 : : protected:
371 : : typedef RowVector<T> RowVectorT;
372 : : typedef ColumnVector<T> ColumnVectorT;
373 : :
374 : : public:
375 : : typedef typename RowVectorT::const_iterator RowIterator;
376 : : typedef typename ColumnVectorT::const_iterator ColIterator;
377 : :
378 : : protected:
379 : : // RowTable : RowID |-> RowVector
380 : : typedef std::vector< RowVectorT > RowTable;
381 : : RowTable d_rows;
382 : :
383 : : // ColumnTable : ArithVar |-> ColumnVector
384 : : typedef std::vector< ColumnVectorT > ColumnTable;
385 : : ColumnTable d_columns;
386 : :
387 : : /* The merge buffer is used to store a row in order to optimize row addition. */
388 : : typedef std::pair<EntryID, bool> PosUsedPair;
389 : : typedef DenseMap< PosUsedPair > RowToPosUsedPairMap;
390 : : RowToPosUsedPairMap d_mergeBuffer;
391 : :
392 : : /* The row that is in the merge buffer. */
393 : : RowIndex d_rowInMergeBuffer;
394 : :
395 : : uint32_t d_entriesInUse;
396 : : MatrixEntryVector<T> d_entries;
397 : :
398 : : std::vector<RowIndex> d_pool;
399 : :
400 : : T d_zero;
401 : :
402 : : public:
403 : : /**
404 : : * Constructs an empty Matrix.
405 : : */
406 : 0 : Matrix()
407 : 0 : : d_rows(),
408 : 0 : d_columns(),
409 : 0 : d_mergeBuffer(),
410 : 0 : d_rowInMergeBuffer(ROW_INDEX_SENTINEL),
411 : 0 : d_entriesInUse(0),
412 : 0 : d_entries(),
413 : 0 : d_zero(0)
414 : 0 : {}
415 : :
416 : 99814 : Matrix(const T& zero)
417 : 99814 : : d_rows(),
418 : 99814 : d_columns(),
419 : 99814 : d_mergeBuffer(),
420 : 99814 : d_rowInMergeBuffer(ROW_INDEX_SENTINEL),
421 : 99814 : d_entriesInUse(0),
422 : 99814 : d_entries(),
423 : 99814 : d_zero(zero)
424 : 99814 : {}
425 : :
426 : : Matrix(const Matrix& m)
427 : : : d_rows(),
428 : : d_columns(),
429 : : d_mergeBuffer(m.d_mergeBuffer),
430 : : d_rowInMergeBuffer(m.d_rowInMergeBuffer),
431 : : d_entriesInUse(m.d_entriesInUse),
432 : : d_entries(m.d_entries),
433 : : d_zero(m.d_zero)
434 : : {
435 : : d_columns.clear();
436 : : for(typename ColumnTable::const_iterator c=m.d_columns.begin(), cend = m.d_columns.end(); c!=cend; ++c){
437 : : const ColumnVectorT& col = *c;
438 : : d_columns.push_back(ColumnVectorT(col.getHead(),col.getSize(),&d_entries));
439 : : }
440 : : d_rows.clear();
441 : : for(typename RowTable::const_iterator r=m.d_rows.begin(), rend = m.d_rows.end(); r!=rend; ++r){
442 : : const RowVectorT& row = *r;
443 : : d_rows.push_back(RowVectorT(row.getHead(),row.getSize(),&d_entries));
444 : : }
445 : : }
446 : :
447 : : Matrix& operator=(const Matrix& m){
448 : : d_mergeBuffer = (m.d_mergeBuffer);
449 : : d_rowInMergeBuffer = (m.d_rowInMergeBuffer);
450 : : d_entriesInUse = (m.d_entriesInUse);
451 : : d_entries = (m.d_entries);
452 : : d_zero = (m.d_zero);
453 : : d_columns.clear();
454 : : for(typename ColumnTable::const_iterator c=m.d_columns.begin(), cend = m.d_columns.end(); c!=cend; ++c){
455 : : const ColumnVector<T>& col = *c;
456 : : d_columns.push_back(ColumnVector<T>(col.getHead(), col.getSize(), &d_entries));
457 : : }
458 : : d_rows.clear();
459 : : for(typename RowTable::const_iterator r=m.d_rows.begin(), rend = m.d_rows.end(); r!=rend; ++r){
460 : : const RowVector<T>& row = *r;
461 : : d_rows.push_back(RowVector<T>(row.getHead(), row.getSize(), &d_entries));
462 : : }
463 : : return *this;
464 : : }
465 : :
466 : : protected:
467 : :
468 : 41955881 : void addEntry(RowIndex row, ArithVar col, const T& coeff){
469 [ + - ]: 41955881 : Trace("tableau") << "addEntry(" << row << "," << col <<"," << coeff << ")" << std::endl;
470 : :
471 [ - + ][ - + ]: 41955881 : Assert(coeff != 0);
[ - - ]
472 [ - + ][ - + ]: 41955881 : Assert(row < d_rows.size());
[ - - ]
473 [ - + ][ - + ]: 41955881 : Assert(col < d_columns.size());
[ - - ]
474 : :
475 : 41955881 : EntryID newId = d_entries.newEntry();
476 : 41955881 : Entry& newEntry = d_entries.get(newId);
477 : 41955881 : newEntry = Entry(row, col, coeff);
478 : :
479 [ - + ][ - + ]: 41955881 : Assert(newEntry.getCoefficient() != 0);
[ - - ]
480 : :
481 : 41955881 : ++d_entriesInUse;
482 : :
483 : 41955881 : d_rows[row].insert(newId);
484 : 41955881 : d_columns[col].insert(newId);
485 : 41955881 : }
486 : :
487 : 40771030 : void removeEntry(EntryID id){
488 [ - + ][ - + ]: 40771030 : Assert(d_entriesInUse > 0);
[ - - ]
489 : 40771030 : --d_entriesInUse;
490 : :
491 : 40771030 : Entry& entry = d_entries.get(id);
492 : :
493 : 40771030 : RowIndex ridx = entry.getRowIndex();
494 : 40771030 : ArithVar col = entry.getColVar();
495 : :
496 [ - + ][ - + ]: 40771030 : Assert(d_rows[ridx].getSize() > 0);
[ - - ]
497 [ - + ][ - + ]: 40771030 : Assert(d_columns[col].getSize() > 0);
[ - - ]
498 : :
499 : 40771030 : d_rows[ridx].remove(id);
500 : 40771030 : d_columns[col].remove(id);
501 : :
502 : 40771030 : entry.markBlank();
503 : :
504 : 40771030 : d_entries.freeEntry(id);
505 : 40771030 : }
506 : :
507 : : private:
508 : 197393 : RowIndex requestRowIndex(){
509 [ + + ]: 197393 : if(d_pool.empty()){
510 : 193468 : RowIndex ridx = d_rows.size();
511 : 193468 : d_rows.push_back(RowVectorT(&d_entries));
512 : 193468 : return ridx;
513 : : }else{
514 : 3925 : RowIndex rid = d_pool.back();
515 : 3925 : d_pool.pop_back();
516 : 3925 : return rid;
517 : : }
518 : : }
519 : :
520 : 3943 : void releaseRowIndex(RowIndex rid){
521 : 3943 : d_pool.push_back(rid);
522 : 3943 : }
523 : :
524 : : public:
525 : :
526 : : size_t getNumRows() const {
527 : : return d_rows.size();
528 : : }
529 : :
530 : 643733 : size_t getNumColumns() const {
531 : 643733 : return d_columns.size();
532 : : }
533 : :
534 : 358718 : void increaseSize(){
535 : 358718 : d_columns.push_back(ColumnVector<T>(&d_entries));
536 : 358718 : }
537 : :
538 : 0 : void increaseSizeTo(size_t s){
539 [ - - ]: 0 : while(getNumColumns() < s){
540 : 0 : increaseSize();
541 : : }
542 : 0 : }
543 : :
544 : 74366531 : const RowVector<T>& getRow(RowIndex r) const {
545 [ - + ][ - + ]: 74366531 : Assert(r < d_rows.size());
[ - - ]
546 : 74366531 : return d_rows[r];
547 : : }
548 : :
549 : 18058977 : const ColumnVector<T>& getColumn(ArithVar v) const {
550 [ - + ][ - + ]: 18058977 : Assert(v < d_columns.size());
[ - - ]
551 : 18058977 : return d_columns[v];
552 : : }
553 : :
554 : 20918501 : uint32_t getRowLength(RowIndex r) const{
555 : 20918501 : return getRow(r).getSize();
556 : : }
557 : :
558 : 4666637 : uint32_t getColLength(ArithVar x) const{
559 : 4666637 : return getColumn(x).getSize();
560 : : }
561 : :
562 : : /**
563 : : * Adds a row to the matrix.
564 : : * The new row is equivalent to:
565 : : * \f$\sum_i\f$ coeffs[i] * variables[i]
566 : : */
567 : 197393 : RowIndex addRow(const std::vector<T>& coeffs,
568 : : const std::vector<ArithVar>& variables){
569 : :
570 : 197393 : RowIndex ridx = requestRowIndex();
571 : :
572 : : //RowIndex ridx = d_rows.size();
573 : : //d_rows.push_back(RowVectorT(&d_entries));
574 : :
575 : 197393 : typename std::vector<T>::const_iterator coeffIter = coeffs.begin();
576 : 197393 : std::vector<ArithVar>::const_iterator varsIter = variables.begin();
577 : 197393 : std::vector<ArithVar>::const_iterator varsEnd = variables.end();
578 : :
579 [ + + ]: 643733 : for(; varsIter != varsEnd; ++coeffIter, ++varsIter){
580 : 446340 : const T& coeff = *coeffIter;
581 : 446340 : ArithVar var_i = *varsIter;
582 [ - + ][ - + ]: 446340 : Assert(var_i < getNumColumns());
[ - - ]
583 : 446340 : addEntry(ridx, var_i, coeff);
584 : : }
585 : :
586 : 197393 : return ridx;
587 : : }
588 : :
589 : :
590 : 485102 : void loadRowIntoBuffer(RowIndex rid){
591 [ - + ][ - + ]: 485102 : Assert(d_mergeBuffer.empty());
[ - - ]
592 [ - + ][ - + ]: 485102 : Assert(d_rowInMergeBuffer == ROW_INDEX_SENTINEL);
[ - - ]
593 : :
594 : 485102 : RowIterator i = getRow(rid).begin(), i_end = getRow(rid).end();
595 [ + + ]: 9068537 : for(; i != i_end; ++i){
596 : 8583435 : EntryID id = i.getID();
597 : 8583435 : const MatrixEntry<T>& entry = *i;
598 : 8583435 : ArithVar colVar = entry.getColVar();
599 : 8583435 : d_mergeBuffer.set(colVar, std::make_pair(id, false));
600 : : }
601 : :
602 : 485102 : d_rowInMergeBuffer = rid;
603 : 485102 : }
604 : :
605 : 485102 : void clearBuffer() {
606 [ - + ][ - + ]: 485102 : Assert(d_rowInMergeBuffer != ROW_INDEX_SENTINEL);
[ - - ]
607 : :
608 : 485102 : d_rowInMergeBuffer = ROW_INDEX_SENTINEL;
609 : 485102 : d_mergeBuffer.purge();
610 : 485102 : }
611 : :
612 : : /* to *= mult */
613 : 0 : void multiplyRowByConstant(RowIndex to, const T& mult){
614 : 0 : RowIterator i = getRow(to).begin();
615 : 0 : RowIterator i_end = getRow(to).end();
616 [ - - ]: 0 : for( ; i != i_end; ++i){
617 : 0 : EntryID id = i.getID();
618 : 0 : Entry& entry = d_entries.get(id);
619 : 0 : T& coeff = entry.getCoefficient();
620 : 0 : coeff *= mult;
621 : : }
622 : 0 : }
623 : :
624 : : /** to += mult * from.
625 : : * Use the more efficient rowPlusBufferTimesConstant() for
626 : : * repeated use.
627 : : */
628 : 0 : void rowPlusRowTimesConstant(RowIndex to, RowIndex from, const T& mult){
629 : 0 : Assert(to != from);
630 : 0 : loadRowIntoBuffer(from);
631 : 0 : rowPlusBufferTimesConstant(to, mult);
632 : 0 : clearBuffer();
633 : 0 : }
634 : :
635 : : /** to += mult * buffer.
636 : : * Invalidates coefficients on the row.
637 : : * (mult should never be a direct copy of a coefficient!)
638 : : */
639 : 0 : void rowPlusBufferTimesConstant(RowIndex to, const T& mult){
640 : 0 : Assert(d_rowInMergeBuffer != ROW_INDEX_SENTINEL);
641 : 0 : Assert(to != ROW_INDEX_SENTINEL);
642 : :
643 [ - - ]: 0 : Trace("tableau") << "rowPlusRowTimesConstant("
644 : 0 : << to << "," << mult << "," << d_rowInMergeBuffer << ")"
645 : 0 : << std::endl;
646 : :
647 : 0 : Assert(debugNoZeroCoefficients(to));
648 : 0 : Assert(debugNoZeroCoefficients(d_rowInMergeBuffer));
649 : :
650 : 0 : Assert(mult != 0);
651 : :
652 : 0 : RowIterator i = getRow(to).begin();
653 : 0 : RowIterator i_end = getRow(to).end();
654 [ - - ]: 0 : while(i != i_end){
655 : 0 : EntryID id = i.getID();
656 : 0 : Entry& entry = d_entries.get(id);
657 : 0 : ArithVar colVar = entry.getColVar();
658 : :
659 : 0 : ++i;
660 : :
661 [ - - ]: 0 : if(d_mergeBuffer.isKey(colVar)){
662 : 0 : EntryID bufferEntry = d_mergeBuffer[colVar].first;
663 : 0 : Assert(!d_mergeBuffer[colVar].second);
664 : 0 : d_mergeBuffer.get(colVar).second = true;
665 : :
666 : 0 : const Entry& other = d_entries.get(bufferEntry);
667 : 0 : T& coeff = entry.getCoefficient();
668 : 0 : coeff += mult * other.getCoefficient();
669 : :
670 [ - - ]: 0 : if(coeff.sgn() == 0){
671 : 0 : removeEntry(id);
672 : : }
673 : : }
674 : : }
675 : :
676 : 0 : i = getRow(d_rowInMergeBuffer).begin();
677 : 0 : i_end = getRow(d_rowInMergeBuffer).end();
678 : :
679 [ - - ]: 0 : for(; i != i_end; ++i){
680 : 0 : const Entry& entry = *i;
681 : 0 : ArithVar colVar = entry.getColVar();
682 : :
683 [ - - ]: 0 : if(d_mergeBuffer[colVar].second){
684 : 0 : d_mergeBuffer.get(colVar).second = false;
685 : : }else{
686 : 0 : Assert(!(d_mergeBuffer[colVar]).second);
687 : 0 : T newCoeff = mult * entry.getCoefficient();
688 : 0 : addEntry(to, colVar, newCoeff);
689 : 0 : }
690 : : }
691 : :
692 : 0 : Assert(mergeBufferIsClear());
693 : :
694 [ - - ]: 0 : if(TraceIsOn("matrix")) { printMatrix(); }
695 : 0 : }
696 : :
697 : : /** to += mult * buffer. */
698 : 6500804 : void rowPlusBufferTimesConstant(RowIndex to, const T& mult, CoefficientChangeCallback& cb){
699 [ - + ][ - + ]: 6500804 : Assert(d_rowInMergeBuffer != ROW_INDEX_SENTINEL);
[ - - ]
700 [ - + ][ - + ]: 6500804 : Assert(to != ROW_INDEX_SENTINEL);
[ - - ]
701 : :
702 [ + - ]: 6500804 : Trace("tableau") << "rowPlusRowTimesConstant("
703 : 0 : << to << "," << mult << "," << d_rowInMergeBuffer << ")"
704 : 0 : << std::endl;
705 : :
706 [ - + ][ - + ]: 6500804 : Assert(debugNoZeroCoefficients(to));
[ - - ]
707 [ - + ][ - + ]: 6500804 : Assert(debugNoZeroCoefficients(d_rowInMergeBuffer));
[ - - ]
708 : :
709 [ - + ][ - + ]: 6500804 : Assert(mult != 0);
[ - - ]
710 : :
711 : 6500804 : RowIterator i = getRow(to).begin();
712 : 6500804 : RowIterator i_end = getRow(to).end();
713 [ + + ]: 114927056 : while(i != i_end){
714 : 108426252 : EntryID id = i.getID();
715 : 108426252 : Entry& entry = d_entries.get(id);
716 : 108426252 : ArithVar colVar = entry.getColVar();
717 : :
718 : 108426252 : ++i;
719 : :
720 [ + + ]: 108426252 : if(d_mergeBuffer.isKey(colVar)){
721 : 56945696 : EntryID bufferEntry = d_mergeBuffer[colVar].first;
722 [ - + ][ - + ]: 56945696 : Assert(!d_mergeBuffer[colVar].second);
[ - - ]
723 : 56945696 : d_mergeBuffer.get(colVar).second = true;
724 : :
725 : 56945696 : const Entry& other = d_entries.get(bufferEntry);
726 : 56945696 : T& coeff = entry.getCoefficient();
727 : 56945696 : int coeffOldSgn = coeff.sgn();
728 : 56945696 : coeff += mult * other.getCoefficient();
729 : 56945696 : int coeffNewSgn = coeff.sgn();
730 : :
731 [ + + ]: 56945696 : if(coeffOldSgn != coeffNewSgn){
732 : 46235334 : cb.update(to, colVar, coeffOldSgn, coeffNewSgn);
733 : :
734 [ + + ]: 46235334 : if(coeffNewSgn == 0){
735 : 40751524 : removeEntry(id);
736 : : }
737 : : }
738 : : }
739 : : }
740 : :
741 : 6500804 : i = getRow(d_rowInMergeBuffer).begin();
742 : 6500804 : i_end = getRow(d_rowInMergeBuffer).end();
743 : :
744 [ + + ]: 104753614 : for(; i != i_end; ++i){
745 : 98252810 : const Entry& entry = *i;
746 : 98252810 : ArithVar colVar = entry.getColVar();
747 : :
748 [ + + ]: 98252810 : if(d_mergeBuffer[colVar].second){
749 : 56945696 : d_mergeBuffer.get(colVar).second = false;
750 : : }else{
751 [ - + ][ - + ]: 41307114 : Assert(!(d_mergeBuffer[colVar]).second);
[ - - ]
752 : 41307114 : T newCoeff = mult * entry.getCoefficient();
753 : 41307114 : addEntry(to, colVar, newCoeff);
754 : :
755 : 41307114 : cb.update(to, colVar, 0, newCoeff.sgn());
756 : 41307114 : }
757 : : }
758 : :
759 [ - + ][ - + ]: 6500804 : Assert(mergeBufferIsClear());
[ - - ]
760 : :
761 [ - + ]: 6500804 : if(TraceIsOn("matrix")) { printMatrix(); }
762 : 6500804 : }
763 : :
764 : 6500804 : bool mergeBufferIsClear() const{
765 : 6500804 : RowToPosUsedPairMap::const_iterator i = d_mergeBuffer.begin();
766 : 6500804 : RowToPosUsedPairMap::const_iterator i_end = d_mergeBuffer.end();
767 [ + + ]: 104753614 : for(; i != i_end; ++i){
768 : 98252810 : RowIndex rid = *i;
769 [ - + ]: 98252810 : if(d_mergeBuffer[rid].second){
770 : 0 : return false;
771 : : }
772 : : }
773 : 6500804 : return true;
774 : : }
775 : :
776 : : protected:
777 : :
778 : 541322 : EntryID findOnRow(RowIndex rid, ArithVar column) const {
779 : 541322 : RowIterator i = d_rows[rid].begin(), i_end = d_rows[rid].end();
780 [ + + ]: 5546430 : for(; i != i_end; ++i){
781 : 5546345 : EntryID id = i.getID();
782 : 5546345 : const MatrixEntry<T>& entry = *i;
783 : 5546345 : ArithVar colVar = entry.getColVar();
784 : :
785 [ + + ]: 5546345 : if(colVar == column){
786 : 541237 : return id;
787 : : }
788 : : }
789 : 85 : return ENTRYID_SENTINEL;
790 : : }
791 : :
792 : 185213 : EntryID findOnCol(RowIndex rid, ArithVar column) const{
793 : 185213 : ColIterator i = d_columns[column].begin(), i_end = d_columns[column].end();
794 [ + + ]: 498104 : for(; i != i_end; ++i){
795 : 498069 : EntryID id = i.getID();
796 : 498069 : const MatrixEntry<T>& entry = *i;
797 : 498069 : RowIndex currRow = entry.getRowIndex();
798 : :
799 [ + + ]: 498069 : if(currRow == rid){
800 : 185178 : return id;
801 : : }
802 : : }
803 : 35 : return ENTRYID_SENTINEL;
804 : : }
805 : :
806 : 365439 : EntryID findEntryID(RowIndex rid, ArithVar col) const{
807 : 365439 : bool colIsShorter = getColLength(col) < getRowLength(rid);
808 [ + + ]: 365439 : EntryID id = colIsShorter ? findOnCol(rid, col) : findOnRow(rid,col);
809 : 365439 : return id;
810 : : }
811 : : MatrixEntry<T> d_failedFind;
812 : : public:
813 : :
814 : : /** If the find fails, isUnused is true on the entry. */
815 : 361096 : const MatrixEntry<T>& findEntry(RowIndex rid, ArithVar col) const{
816 : 361096 : EntryID id = findEntryID(rid, col);
817 [ - + ]: 361096 : if(id == ENTRYID_SENTINEL){
818 : 0 : return d_failedFind;
819 : : }else{
820 : 361096 : return d_entries[id];
821 : : }
822 : : }
823 : :
824 : : /**
825 : : * Prints the contents of the Matrix to Trace("matrix")
826 : : */
827 : 0 : void printMatrix(std::ostream& out) const {
828 : 0 : out << "Matrix::printMatrix" << std::endl;
829 : :
830 [ - - ]: 0 : for(RowIndex i = 0, N = d_rows.size(); i < N; ++i){
831 : 0 : printRow(i, out);
832 : : }
833 : 0 : }
834 : 0 : void printMatrix() const {
835 [ - - ]: 0 : printMatrix(Trace("matrix"));
836 : 0 : }
837 : :
838 : 0 : void printRow(RowIndex rid, std::ostream& out) const {
839 : 0 : out << "{" << rid << ":";
840 : 0 : const RowVector<T>& row = getRow(rid);
841 : 0 : RowIterator i = row.begin();
842 : 0 : RowIterator i_end = row.end();
843 [ - - ]: 0 : for(; i != i_end; ++i){
844 : 0 : printEntry(*i, out);
845 : 0 : out << ",";
846 : : }
847 : 0 : out << "}" << std::endl;
848 : 0 : }
849 : : void printRow(RowIndex rid) const {
850 : : printRow(rid, Trace("matrix"));
851 : : }
852 : :
853 : 0 : void printEntry(const MatrixEntry<T>& entry, std::ostream& out) const {
854 : 0 : out << entry.getColVar() << "*" << entry.getCoefficient();
855 : 0 : }
856 : : void printEntry(const MatrixEntry<T>& entry) const {
857 : : printEntry(entry, Trace("matrix"));
858 : : }
859 : : public:
860 : 49334 : uint32_t size() const {
861 : 49334 : return d_entriesInUse;
862 : : }
863 : : uint32_t getNumEntriesInTableau() const {
864 : : return d_entries.size();
865 : : }
866 : : uint32_t getEntryCapacity() const {
867 : : return d_entries.capacity();
868 : : }
869 : :
870 : 4343 : void manipulateRowEntry(RowIndex row, ArithVar col, const T& c, CoefficientChangeCallback& cb){
871 : : int coeffOldSgn;
872 : : int coeffNewSgn;
873 : :
874 : 4343 : EntryID id = findEntryID(row, col);
875 [ + + ]: 4343 : if(id == ENTRYID_SENTINEL){
876 : 120 : coeffOldSgn = 0;
877 : 120 : addEntry(row, col, c);
878 : 120 : coeffNewSgn = c.sgn();
879 : : }else{
880 : 4223 : Entry& e = d_entries.get(id);
881 : 4223 : T& t = e.getCoefficient();
882 : 4223 : coeffOldSgn = t.sgn();
883 : 4223 : t += c;
884 : 4223 : coeffNewSgn = t.sgn();
885 : : }
886 : :
887 [ + + ]: 4343 : if(coeffOldSgn != coeffNewSgn){
888 : 3507 : cb.update(row, col, coeffOldSgn, coeffNewSgn);
889 : : }
890 [ + + ]: 4343 : if(coeffNewSgn == 0){
891 : 3344 : removeEntry(id);
892 : : }
893 : 4343 : }
894 : :
895 : 3943 : void removeRow(RowIndex rid){
896 : 3943 : RowIterator i = getRow(rid).begin();
897 : 3943 : RowIterator i_end = getRow(rid).end();
898 [ + + ]: 20105 : for(; i != i_end; ++i){
899 : 16162 : EntryID id = i.getID();
900 : 16162 : removeEntry(id);
901 : : }
902 : 3943 : releaseRowIndex(rid);
903 : 3943 : }
904 : :
905 : : double densityMeasure() const{
906 : : Assert(numNonZeroEntriesByRow() == numNonZeroEntries());
907 : : Assert(numNonZeroEntriesByCol() == numNonZeroEntries());
908 : :
909 : : uint32_t n = getNumRows();
910 : : if(n == 0){
911 : : return 1.0;
912 : : }else {
913 : : uint32_t s = numNonZeroEntries();
914 : : uint32_t m = d_columns.size();
915 : : uint32_t divisor = (n *(m - n + 1));
916 : :
917 : : Assert(n >= 1);
918 : : Assert(m >= n);
919 : : Assert(divisor > 0);
920 : : Assert(divisor >= s);
921 : :
922 : : return (double(s)) / divisor;
923 : : }
924 : : }
925 : :
926 : : void loadSignQueries(RowIndex rid, DenseMap<int>& target) const{
927 : :
928 : : RowIterator i = getRow(rid).begin(), i_end = getRow(rid).end();
929 : : for(; i != i_end; ++i){
930 : : const MatrixEntry<T>& entry = *i;
931 : : target.set(entry.getColVar(), entry.getCoefficient().sgn());
932 : : }
933 : : }
934 : :
935 : : protected:
936 : : uint32_t numNonZeroEntries() const { return size(); }
937 : :
938 : : uint32_t numNonZeroEntriesByRow() const {
939 : : uint32_t rowSum = 0;
940 : : for(RowIndex rid = 0, N = d_rows.size(); rid < N; ++rid){
941 : : rowSum += getRowLength(rid);
942 : : }
943 : : return rowSum;
944 : : }
945 : :
946 : : uint32_t numNonZeroEntriesByCol() const {
947 : : uint32_t colSum = 0;
948 : : for(ArithVar v = 0, N = d_columns.size(); v < N; ++v){
949 : : colSum += getColLength(v);
950 : : }
951 : : return colSum;
952 : : }
953 : :
954 : :
955 : 13199001 : bool debugNoZeroCoefficients(RowIndex ridx){
956 [ + + ]: 220861492 : for(RowIterator i=getRow(ridx).begin(); !i.atEnd(); ++i){
957 : 207662491 : const Entry& entry = *i;
958 [ - + ]: 207662491 : if(entry.getCoefficient() == 0){
959 : 0 : return false;
960 : : }
961 : : }
962 : 13199001 : return true;
963 : : }
964 : 197393 : bool debugMatchingCountsForRow(RowIndex ridx){
965 [ + + ]: 1180822 : for(RowIterator i=getRow(ridx).begin(); !i.atEnd(); ++i){
966 : 983429 : const Entry& entry = *i;
967 : 983429 : ArithVar colVar = entry.getColVar();
968 : 983429 : uint32_t count = debugCountColLength(colVar);
969 [ + - ]: 1966858 : Trace("tableau") << "debugMatchingCountsForRow "
970 : 0 : << ridx << ":" << colVar << " " << count
971 : 983429 : <<" "<< getColLength(colVar) << std::endl;
972 [ - + ]: 983429 : if( count != getColLength(colVar) ){
973 : 0 : return false;
974 : : }
975 : : }
976 : 197393 : return true;
977 : : }
978 : :
979 : 983429 : uint32_t debugCountColLength(ArithVar var){
980 [ + - ]: 983429 : Trace("tableau") << var << " ";
981 : 983429 : uint32_t count = 0;
982 [ + + ]: 23873173 : for(ColIterator i=getColumn(var).begin(); !i.atEnd(); ++i){
983 : 22889744 : const Entry& entry = *i;
984 [ + - ]: 22889744 : Trace("tableau") << "(" << entry.getRowIndex() << ", " << i.getID() << ") ";
985 : 22889744 : ++count;
986 : : }
987 [ + - ]: 983429 : Trace("tableau") << std::endl;
988 : 983429 : return count;
989 : : }
990 : : uint32_t debugCountRowLength(RowIndex ridx){
991 : : uint32_t count = 0;
992 : : for(RowIterator i=getRow(ridx).begin(); !i.atEnd(); ++i){
993 : : ++count;
994 : : }
995 : : return count;
996 : : }
997 : :
998 : : };/* class Matrix<T> */
999 : :
1000 : : } // namespace arith
1001 : : } // namespace theory
1002 : : } // namespace cvc5::internal
|
