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