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 : : {
40 : : public:
41 : 251915 : virtual ~CoefficientChangeCallback() {}
42 : : virtual void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) = 0;
43 : : virtual void multiplyRow(RowIndex ridx, int Sgn) = 0;
44 : : virtual bool canUseRow(RowIndex ridx) const = 0;
45 : : };
46 : :
47 : : class NoEffectCCCB : public CoefficientChangeCallback
48 : : {
49 : : public:
50 : : void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) override;
51 : : void multiplyRow(RowIndex ridx, int Sgn) override;
52 : : bool canUseRow(RowIndex ridx) const override;
53 : : };
54 : :
55 : : template <class T>
56 : : class MatrixEntry
57 : : {
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 : 1552926 : MatrixEntry()
72 : 1552926 : : d_rowIndex(ROW_INDEX_SENTINEL),
73 : 1552926 : d_colVar(ARITHVAR_SENTINEL),
74 : 1552926 : d_nextRow(ENTRYID_SENTINEL),
75 : 1552926 : d_nextCol(ENTRYID_SENTINEL),
76 : 1552926 : d_prevRow(ENTRYID_SENTINEL),
77 : 1552926 : d_prevCol(ENTRYID_SENTINEL),
78 : 1552926 : d_coefficient()
79 : : {
80 : 1552926 : }
81 : :
82 : 34747421 : MatrixEntry(RowIndex row, ArithVar col, const T& coeff)
83 : 34747421 : : d_rowIndex(row),
84 : 34747421 : d_colVar(col),
85 : 34747421 : d_nextRow(ENTRYID_SENTINEL),
86 : 34747421 : d_nextCol(ENTRYID_SENTINEL),
87 : 34747421 : d_prevRow(ENTRYID_SENTINEL),
88 : 34747421 : d_prevCol(ENTRYID_SENTINEL),
89 : 34747421 : d_coefficient(coeff)
90 : : {
91 : 34747421 : }
92 : :
93 : : private:
94 : 33860525 : bool unusedConsistent() const
95 : : {
96 [ - + ]: 33519233 : return (d_rowIndex == ROW_INDEX_SENTINEL && d_colVar == ARITHVAR_SENTINEL)
97 [ + + ][ + - ]: 67721050 : || (d_rowIndex != ROW_INDEX_SENTINEL
98 [ + - ]: 34201817 : && d_colVar != ARITHVAR_SENTINEL);
99 : : }
100 : :
101 : : public:
102 : 472754549 : EntryID getNextRowEntryID() const { return d_nextRow; }
103 : :
104 : 144704804 : EntryID getNextColEntryID() const { return d_nextCol; }
105 : 33519233 : EntryID getPrevRowEntryID() const { return d_prevRow; }
106 : :
107 : 33519233 : EntryID getPrevColEntryID() const { return d_prevCol; }
108 : :
109 : 53126574 : void setNextRowEntryID(EntryID id) { d_nextRow = id; }
110 : 59840789 : void setNextColEntryID(EntryID id) { d_nextCol = id; }
111 : 67678699 : void setPrevRowEntryID(EntryID id) { d_prevRow = id; }
112 : 67148490 : void setPrevColEntryID(EntryID id) { d_prevCol = id; }
113 : :
114 : 127975455 : RowIndex getRowIndex() const { return d_rowIndex; }
115 : :
116 : 360923342 : ArithVar getColVar() const { return d_colVar; }
117 : :
118 : 397141521 : const T& getCoefficient() const { return d_coefficient; }
119 : :
120 : 95546183 : T& getCoefficient() { return d_coefficient; }
121 : :
122 : : void setCoefficient(const T& t) { d_coefficient = t; }
123 : :
124 : 33519233 : void markBlank()
125 : : {
126 : 33519233 : d_rowIndex = ROW_INDEX_SENTINEL;
127 : 33519233 : d_colVar = ARITHVAR_SENTINEL;
128 : 33519233 : }
129 : :
130 : 33860525 : bool blank() const
131 : : {
132 [ - + ][ - + ]: 33860525 : Assert(unusedConsistent());
[ - - ]
133 : :
134 : 33860525 : return d_rowIndex == ROW_INDEX_SENTINEL;
135 : : }
136 : : }; /* class MatrixEntry<T> */
137 : :
138 : : template <class T>
139 : : class MatrixEntryVector
140 : : {
141 : : private:
142 : : typedef MatrixEntry<T> EntryType;
143 : : typedef std::vector<EntryType> EntryArray;
144 : :
145 : : EntryArray d_entries;
146 : : std::queue<EntryID> d_freedEntries;
147 : :
148 : : uint32_t d_size;
149 : :
150 : : public:
151 : 102032 : MatrixEntryVector() : d_entries(), d_freedEntries(), d_size(0) {}
152 : :
153 : 1002197312 : const EntryType& operator[](EntryID id) const
154 : : {
155 [ - + ][ - + ]: 1002197312 : Assert(inBounds(id));
[ - - ]
156 : 1002197312 : return d_entries[id];
157 : : }
158 : :
159 : 639964243 : EntryType& get(EntryID id)
160 : : {
161 [ - + ][ - + ]: 639964243 : Assert(inBounds(id));
[ - - ]
162 : 639964243 : return d_entries[id];
163 : : }
164 : :
165 : 33519233 : void freeEntry(EntryID id)
166 : : {
167 [ - + ][ - + ]: 33519233 : Assert(get(id).blank());
[ - - ]
168 [ - + ][ - + ]: 33519233 : Assert(d_size > 0);
[ - - ]
169 : :
170 : 33519233 : d_freedEntries.push(id);
171 : 33519233 : --d_size;
172 : 33519233 : }
173 : :
174 : 34747421 : EntryID newEntry()
175 : : {
176 : : EntryID newId;
177 [ + + ]: 34747421 : if (d_freedEntries.empty())
178 : : {
179 : 1450894 : newId = d_entries.size();
180 : 1450894 : d_entries.push_back(MatrixEntry<T>());
181 : : }
182 : : else
183 : : {
184 : 33296527 : newId = d_freedEntries.front();
185 : 33296527 : d_freedEntries.pop();
186 : : }
187 : 34747421 : ++d_size;
188 : 34747421 : return newId;
189 : : }
190 : :
191 : : uint32_t size() const { return d_size; }
192 : : uint32_t capacity() const { return d_entries.capacity(); }
193 : :
194 : : private:
195 : 1642161555 : bool inBounds(EntryID id) const { return id < d_entries.size(); }
196 : : }; /* class MatrixEntryVector<T> */
197 : :
198 : : template <class T, bool isRow>
199 : : class MatrixVector
200 : : {
201 : : private:
202 : : EntryID d_head;
203 : : uint32_t d_size;
204 : :
205 : : MatrixEntryVector<T>* d_entries;
206 : :
207 : : class Iterator
208 : : {
209 : : private:
210 : : EntryID d_curr;
211 : : const MatrixEntryVector<T>* d_entries;
212 : :
213 : : public:
214 : 67581886 : Iterator(EntryID start, const MatrixEntryVector<T>* entries)
215 : 67581886 : : d_curr(start), d_entries(entries)
216 : : {
217 : 67581886 : }
218 : :
219 : : public:
220 : 119119207 : EntryID getID() const { return d_curr; }
221 : :
222 : 451435133 : const MatrixEntry<T>& operator*() const
223 : : {
224 [ - + ][ - + ]: 451435133 : Assert(!atEnd());
[ - - ]
225 : 451435133 : return (*d_entries)[d_curr];
226 : : }
227 : :
228 : 550420887 : Iterator& operator++()
229 : : {
230 [ - + ][ - + ]: 550420887 : Assert(!atEnd());
[ - - ]
231 : 550420887 : const MatrixEntry<T>& entry = (*d_entries)[d_curr];
232 : 550420887 : d_curr = isRow ? entry.getNextRowEntryID() : entry.getNextColEntryID();
233 : 550420887 : return *this;
234 : : }
235 : :
236 : 1403477639 : bool atEnd() const { return d_curr == ENTRYID_SENTINEL; }
237 : :
238 : : bool operator==(const Iterator& i) const
239 : : {
240 : : return d_curr == i.d_curr && d_entries == i.d_entries;
241 : : }
242 : :
243 : 202410733 : bool operator!=(const Iterator& i) const
244 : : {
245 [ + + ][ - + ]: 202410733 : return !(d_curr == i.d_curr && d_entries == i.d_entries);
246 : : }
247 : : }; /* class MatrixVector<T, isRow>::Iterator */
248 : :
249 : : public:
250 : 561666 : MatrixVector(MatrixEntryVector<T>* mev)
251 : 561666 : : d_head(ENTRYID_SENTINEL), d_size(0), d_entries(mev)
252 : : {
253 : 561666 : }
254 : :
255 : : MatrixVector(EntryID head, uint32_t size, MatrixEntryVector<T>* mev)
256 : : : d_head(head), d_size(size), d_entries(mev)
257 : : {
258 : : }
259 : :
260 : : typedef Iterator const_iterator;
261 : 53611465 : const_iterator begin() const { return Iterator(d_head, d_entries); }
262 : 13970421 : const_iterator end() const { return Iterator(ENTRYID_SENTINEL, d_entries); }
263 : :
264 : : EntryID getHead() const { return d_head; }
265 : :
266 : 91976758 : uint32_t getSize() const { return d_size; }
267 : :
268 : 69494842 : void insert(EntryID newId)
269 : : {
270 : : if (isRow)
271 : : {
272 : 34747421 : d_entries->get(newId).setNextRowEntryID(d_head);
273 : :
274 [ + + ]: 34747421 : if (d_head != ENTRYID_SENTINEL)
275 : : {
276 : 34546174 : d_entries->get(d_head).setPrevRowEntryID(newId);
277 : : }
278 : : }
279 : : else
280 : : {
281 : 34747421 : d_entries->get(newId).setNextColEntryID(d_head);
282 : :
283 [ + + ]: 34747421 : if (d_head != ENTRYID_SENTINEL)
284 : : {
285 : 34407658 : d_entries->get(d_head).setPrevColEntryID(newId);
286 : : }
287 : : }
288 : :
289 : 69494842 : d_head = newId;
290 : 69494842 : ++d_size;
291 : 69494842 : }
292 : 67038466 : void remove(EntryID id)
293 : : {
294 [ - + ][ - + ]: 67038466 : Assert(d_size > 0);
[ - - ]
295 : 67038466 : --d_size;
296 : : if (isRow)
297 : : {
298 : 33519233 : EntryID prevRow = d_entries->get(id).getPrevRowEntryID();
299 : 33519233 : EntryID nextRow = d_entries->get(id).getNextRowEntryID();
300 : :
301 [ + + ]: 33519233 : if (d_head == id)
302 : : {
303 : 15140080 : d_head = nextRow;
304 : : }
305 [ + + ]: 33519233 : if (prevRow != ENTRYID_SENTINEL)
306 : : {
307 : 18379153 : d_entries->get(prevRow).setNextRowEntryID(nextRow);
308 : : }
309 [ + + ]: 33519233 : if (nextRow != ENTRYID_SENTINEL)
310 : : {
311 : 33132525 : d_entries->get(nextRow).setPrevRowEntryID(prevRow);
312 : : }
313 : : }
314 : : else
315 : : {
316 : 33519233 : EntryID prevCol = d_entries->get(id).getPrevColEntryID();
317 : 33519233 : EntryID nextCol = d_entries->get(id).getNextColEntryID();
318 : :
319 [ + + ]: 33519233 : if (d_head == id)
320 : : {
321 : 8425865 : d_head = nextCol;
322 : : }
323 : :
324 [ + + ]: 33519233 : if (prevCol != ENTRYID_SENTINEL)
325 : : {
326 : 25093368 : d_entries->get(prevCol).setNextColEntryID(nextCol);
327 : : }
328 [ + + ]: 33519233 : if (nextCol != ENTRYID_SENTINEL)
329 : : {
330 : 32740832 : d_entries->get(nextCol).setPrevColEntryID(prevCol);
331 : : }
332 : : }
333 : 67038466 : }
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 : :
342 : : public:
343 : : typedef typename SuperT::const_iterator const_iterator;
344 : :
345 : 197169 : RowVector(MatrixEntryVector<T>* mev) : SuperT(mev) {}
346 : : RowVector(EntryID head, uint32_t size, MatrixEntryVector<T>* mev)
347 : : : SuperT(head, size, mev)
348 : : {
349 : : }
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 : :
358 : : public:
359 : : typedef typename SuperT::const_iterator const_iterator;
360 : :
361 : 364497 : ColumnVector(MatrixEntryVector<T>* mev) : SuperT(mev) {}
362 : : ColumnVector(EntryID head, uint32_t size, MatrixEntryVector<T>* mev)
363 : : : SuperT(head, size, mev)
364 : : {
365 : : }
366 : : }; /* class ColumnVector<T> */
367 : :
368 : : template <class T>
369 : : class Matrix
370 : : {
371 : : public:
372 : : typedef MatrixEntry<T> Entry;
373 : :
374 : : protected:
375 : : typedef RowVector<T> RowVectorT;
376 : : typedef ColumnVector<T> ColumnVectorT;
377 : :
378 : : public:
379 : : typedef typename RowVectorT::const_iterator RowIterator;
380 : : typedef typename ColumnVectorT::const_iterator ColIterator;
381 : :
382 : : protected:
383 : : // RowTable : RowID |-> RowVector
384 : : typedef std::vector<RowVectorT> RowTable;
385 : : RowTable d_rows;
386 : :
387 : : // ColumnTable : ArithVar |-> ColumnVector
388 : : typedef std::vector<ColumnVectorT> ColumnTable;
389 : : ColumnTable d_columns;
390 : :
391 : : /* The merge buffer is used to store a row in order to optimize row addition.
392 : : */
393 : : typedef std::pair<EntryID, bool> PosUsedPair;
394 : : typedef DenseMap<PosUsedPair> RowToPosUsedPairMap;
395 : : RowToPosUsedPairMap d_mergeBuffer;
396 : :
397 : : /* The row that is in the merge buffer. */
398 : : RowIndex d_rowInMergeBuffer;
399 : :
400 : : uint32_t d_entriesInUse;
401 : : MatrixEntryVector<T> d_entries;
402 : :
403 : : std::vector<RowIndex> d_pool;
404 : :
405 : : T d_zero;
406 : :
407 : : public:
408 : : /**
409 : : * Constructs an empty Matrix.
410 : : */
411 : 0 : Matrix()
412 : 0 : : d_rows(),
413 : 0 : d_columns(),
414 : 0 : d_mergeBuffer(),
415 : 0 : d_rowInMergeBuffer(ROW_INDEX_SENTINEL),
416 : 0 : d_entriesInUse(0),
417 : 0 : d_entries(),
418 : 0 : d_zero(0)
419 : : {
420 : 0 : }
421 : :
422 : 102032 : Matrix(const T& zero)
423 : 102032 : : d_rows(),
424 : 102032 : d_columns(),
425 : 102032 : d_mergeBuffer(),
426 : 102032 : d_rowInMergeBuffer(ROW_INDEX_SENTINEL),
427 : 102032 : d_entriesInUse(0),
428 : 102032 : d_entries(),
429 : 102032 : d_zero(zero)
430 : : {
431 : 102032 : }
432 : :
433 : : Matrix(const Matrix& m)
434 : : : d_rows(),
435 : : d_columns(),
436 : : d_mergeBuffer(m.d_mergeBuffer),
437 : : d_rowInMergeBuffer(m.d_rowInMergeBuffer),
438 : : d_entriesInUse(m.d_entriesInUse),
439 : : d_entries(m.d_entries),
440 : : d_zero(m.d_zero)
441 : : {
442 : : d_columns.clear();
443 : : for (typename ColumnTable::const_iterator c = m.d_columns.begin(),
444 : : cend = m.d_columns.end();
445 : : c != cend;
446 : : ++c)
447 : : {
448 : : const ColumnVectorT& col = *c;
449 : : d_columns.push_back(
450 : : ColumnVectorT(col.getHead(), col.getSize(), &d_entries));
451 : : }
452 : : d_rows.clear();
453 : : for (typename RowTable::const_iterator r = m.d_rows.begin(),
454 : : rend = m.d_rows.end();
455 : : r != rend;
456 : : ++r)
457 : : {
458 : : const RowVectorT& row = *r;
459 : : d_rows.push_back(RowVectorT(row.getHead(), row.getSize(), &d_entries));
460 : : }
461 : : }
462 : :
463 : : Matrix& operator=(const Matrix& m)
464 : : {
465 : : d_mergeBuffer = (m.d_mergeBuffer);
466 : : d_rowInMergeBuffer = (m.d_rowInMergeBuffer);
467 : : d_entriesInUse = (m.d_entriesInUse);
468 : : d_entries = (m.d_entries);
469 : : d_zero = (m.d_zero);
470 : : d_columns.clear();
471 : : for (typename ColumnTable::const_iterator c = m.d_columns.begin(),
472 : : cend = m.d_columns.end();
473 : : c != cend;
474 : : ++c)
475 : : {
476 : : const ColumnVector<T>& col = *c;
477 : : d_columns.push_back(
478 : : ColumnVector<T>(col.getHead(), col.getSize(), &d_entries));
479 : : }
480 : : d_rows.clear();
481 : : for (typename RowTable::const_iterator r = m.d_rows.begin(),
482 : : rend = m.d_rows.end();
483 : : r != rend;
484 : : ++r)
485 : : {
486 : : const RowVector<T>& row = *r;
487 : : d_rows.push_back(RowVector<T>(row.getHead(), row.getSize(), &d_entries));
488 : : }
489 : : return *this;
490 : : }
491 : :
492 : : protected:
493 : 34747421 : void addEntry(RowIndex row, ArithVar col, const T& coeff)
494 : : {
495 [ + - ]: 34747421 : Trace("tableau") << "addEntry(" << row << "," << col << "," << coeff << ")"
496 : 0 : << std::endl;
497 : :
498 [ - + ][ - + ]: 34747421 : Assert(coeff != 0);
[ - - ]
499 [ - + ][ - + ]: 34747421 : Assert(row < d_rows.size());
[ - - ]
500 [ - + ][ - + ]: 34747421 : Assert(col < d_columns.size());
[ - - ]
501 : :
502 : 34747421 : EntryID newId = d_entries.newEntry();
503 : 34747421 : Entry& newEntry = d_entries.get(newId);
504 : 34747421 : newEntry = Entry(row, col, coeff);
505 : :
506 [ - + ][ - + ]: 34747421 : Assert(newEntry.getCoefficient() != 0);
[ - - ]
507 : :
508 : 34747421 : ++d_entriesInUse;
509 : :
510 : 34747421 : d_rows[row].insert(newId);
511 : 34747421 : d_columns[col].insert(newId);
512 : 34747421 : }
513 : :
514 : 33519233 : void removeEntry(EntryID id)
515 : : {
516 [ - + ][ - + ]: 33519233 : Assert(d_entriesInUse > 0);
[ - - ]
517 : 33519233 : --d_entriesInUse;
518 : :
519 : 33519233 : Entry& entry = d_entries.get(id);
520 : :
521 : 33519233 : RowIndex ridx = entry.getRowIndex();
522 : 33519233 : ArithVar col = entry.getColVar();
523 : :
524 [ - + ][ - + ]: 33519233 : Assert(d_rows[ridx].getSize() > 0);
[ - - ]
525 [ - + ][ - + ]: 33519233 : Assert(d_columns[col].getSize() > 0);
[ - - ]
526 : :
527 : 33519233 : d_rows[ridx].remove(id);
528 : 33519233 : d_columns[col].remove(id);
529 : :
530 : 33519233 : entry.markBlank();
531 : :
532 : 33519233 : d_entries.freeEntry(id);
533 : 33519233 : }
534 : :
535 : : private:
536 : 201247 : RowIndex requestRowIndex()
537 : : {
538 [ + + ]: 201247 : if (d_pool.empty())
539 : : {
540 : 197169 : RowIndex ridx = d_rows.size();
541 : 197169 : d_rows.push_back(RowVectorT(&d_entries));
542 : 197169 : return ridx;
543 : : }
544 : : else
545 : : {
546 : 4078 : RowIndex rid = d_pool.back();
547 : 4078 : d_pool.pop_back();
548 : 4078 : return rid;
549 : : }
550 : : }
551 : :
552 : 4096 : void releaseRowIndex(RowIndex rid) { d_pool.push_back(rid); }
553 : :
554 : : public:
555 : : size_t getNumRows() const { return d_rows.size(); }
556 : :
557 : 658640 : size_t getNumColumns() const { return d_columns.size(); }
558 : :
559 : 364497 : void increaseSize() { d_columns.push_back(ColumnVector<T>(&d_entries)); }
560 : :
561 : 0 : void increaseSizeTo(size_t s)
562 : : {
563 [ - - ]: 0 : while (getNumColumns() < s)
564 : : {
565 : 0 : increaseSize();
566 : : }
567 : 0 : }
568 : :
569 : 73853443 : const RowVector<T>& getRow(RowIndex r) const
570 : : {
571 [ - + ][ - + ]: 73853443 : Assert(r < d_rows.size());
[ - - ]
572 : 73853443 : return d_rows[r];
573 : : }
574 : :
575 : 17292485 : const ColumnVector<T>& getColumn(ArithVar v) const
576 : : {
577 [ - + ][ - + ]: 17292485 : Assert(v < d_columns.size());
[ - - ]
578 : 17292485 : return d_columns[v];
579 : : }
580 : :
581 : 20957491 : uint32_t getRowLength(RowIndex r) const { return getRow(r).getSize(); }
582 : :
583 : 3980801 : uint32_t getColLength(ArithVar x) const { return getColumn(x).getSize(); }
584 : :
585 : : /**
586 : : * Adds a row to the matrix.
587 : : * The new row is equivalent to:
588 : : * \f$\sum_i\f$ coeffs[i] * variables[i]
589 : : */
590 : 201247 : RowIndex addRow(const std::vector<T>& coeffs,
591 : : const std::vector<ArithVar>& variables)
592 : : {
593 : 201247 : RowIndex ridx = requestRowIndex();
594 : :
595 : : // RowIndex ridx = d_rows.size();
596 : : // d_rows.push_back(RowVectorT(&d_entries));
597 : :
598 : 201247 : typename std::vector<T>::const_iterator coeffIter = coeffs.begin();
599 : 201247 : std::vector<ArithVar>::const_iterator varsIter = variables.begin();
600 : 201247 : std::vector<ArithVar>::const_iterator varsEnd = variables.end();
601 : :
602 [ + + ]: 658640 : for (; varsIter != varsEnd; ++coeffIter, ++varsIter)
603 : : {
604 : 457393 : const T& coeff = *coeffIter;
605 : 457393 : ArithVar var_i = *varsIter;
606 [ - + ][ - + ]: 457393 : Assert(var_i < getNumColumns());
[ - - ]
607 : 457393 : addEntry(ridx, var_i, coeff);
608 : : }
609 : :
610 : 201247 : return ridx;
611 : : }
612 : :
613 : 471804 : void loadRowIntoBuffer(RowIndex rid)
614 : : {
615 [ - + ][ - + ]: 471804 : Assert(d_mergeBuffer.empty());
[ - - ]
616 [ - + ][ - + ]: 471804 : Assert(d_rowInMergeBuffer == ROW_INDEX_SENTINEL);
[ - - ]
617 : :
618 : 471804 : RowIterator i = getRow(rid).begin(), i_end = getRow(rid).end();
619 [ + + ]: 7216761 : for (; i != i_end; ++i)
620 : : {
621 : 6744957 : EntryID id = i.getID();
622 : 6744957 : const MatrixEntry<T>& entry = *i;
623 : 6744957 : ArithVar colVar = entry.getColVar();
624 : 6744957 : d_mergeBuffer.set(colVar, std::make_pair(id, false));
625 : : }
626 : :
627 : 471804 : d_rowInMergeBuffer = rid;
628 : 471804 : }
629 : :
630 : 471804 : void clearBuffer()
631 : : {
632 [ - + ][ - + ]: 471804 : Assert(d_rowInMergeBuffer != ROW_INDEX_SENTINEL);
[ - - ]
633 : :
634 : 471804 : d_rowInMergeBuffer = ROW_INDEX_SENTINEL;
635 : 471804 : d_mergeBuffer.purge();
636 : 471804 : }
637 : :
638 : : /* to *= mult */
639 : 0 : void multiplyRowByConstant(RowIndex to, const T& mult)
640 : : {
641 : 0 : RowIterator i = getRow(to).begin();
642 : 0 : RowIterator i_end = getRow(to).end();
643 [ - - ]: 0 : for (; i != i_end; ++i)
644 : : {
645 : 0 : EntryID id = i.getID();
646 : 0 : Entry& entry = d_entries.get(id);
647 : 0 : T& coeff = entry.getCoefficient();
648 : 0 : coeff *= mult;
649 : : }
650 : 0 : }
651 : :
652 : : /** to += mult * from.
653 : : * Use the more efficient rowPlusBufferTimesConstant() for
654 : : * repeated use.
655 : : */
656 : 0 : void rowPlusRowTimesConstant(RowIndex to, RowIndex from, const T& mult)
657 : : {
658 : 0 : Assert(to != from);
659 : 0 : loadRowIntoBuffer(from);
660 : 0 : rowPlusBufferTimesConstant(to, mult);
661 : 0 : clearBuffer();
662 : 0 : }
663 : :
664 : : /** to += mult * buffer.
665 : : * Invalidates coefficients on the row.
666 : : * (mult should never be a direct copy of a coefficient!)
667 : : */
668 : 0 : void rowPlusBufferTimesConstant(RowIndex to, const T& mult)
669 : : {
670 : 0 : Assert(d_rowInMergeBuffer != ROW_INDEX_SENTINEL);
671 : 0 : Assert(to != ROW_INDEX_SENTINEL);
672 : :
673 [ - - ]: 0 : Trace("tableau") << "rowPlusRowTimesConstant(" << to << "," << mult << ","
674 : 0 : << d_rowInMergeBuffer << ")" << std::endl;
675 : :
676 : 0 : Assert(debugNoZeroCoefficients(to));
677 : 0 : Assert(debugNoZeroCoefficients(d_rowInMergeBuffer));
678 : :
679 : 0 : Assert(mult != 0);
680 : :
681 : 0 : RowIterator i = getRow(to).begin();
682 : 0 : RowIterator i_end = getRow(to).end();
683 [ - - ]: 0 : while (i != i_end)
684 : : {
685 : 0 : EntryID id = i.getID();
686 : 0 : Entry& entry = d_entries.get(id);
687 : 0 : ArithVar colVar = entry.getColVar();
688 : :
689 : 0 : ++i;
690 : :
691 [ - - ]: 0 : if (d_mergeBuffer.isKey(colVar))
692 : : {
693 : 0 : EntryID bufferEntry = d_mergeBuffer[colVar].first;
694 : 0 : Assert(!d_mergeBuffer[colVar].second);
695 : 0 : d_mergeBuffer.get(colVar).second = true;
696 : :
697 : 0 : const Entry& other = d_entries.get(bufferEntry);
698 : 0 : T& coeff = entry.getCoefficient();
699 : 0 : coeff += mult * other.getCoefficient();
700 : :
701 [ - - ]: 0 : if (coeff.sgn() == 0)
702 : : {
703 : 0 : removeEntry(id);
704 : : }
705 : : }
706 : : }
707 : :
708 : 0 : i = getRow(d_rowInMergeBuffer).begin();
709 : 0 : i_end = getRow(d_rowInMergeBuffer).end();
710 : :
711 [ - - ]: 0 : for (; i != i_end; ++i)
712 : : {
713 : 0 : const Entry& entry = *i;
714 : 0 : ArithVar colVar = entry.getColVar();
715 : :
716 [ - - ]: 0 : if (d_mergeBuffer[colVar].second)
717 : : {
718 : 0 : d_mergeBuffer.get(colVar).second = false;
719 : : }
720 : : else
721 : : {
722 : 0 : Assert(!(d_mergeBuffer[colVar]).second);
723 : 0 : T newCoeff = mult * entry.getCoefficient();
724 : 0 : addEntry(to, colVar, newCoeff);
725 : 0 : }
726 : : }
727 : :
728 : 0 : Assert(mergeBufferIsClear());
729 : :
730 [ - - ]: 0 : if (TraceIsOn("matrix"))
731 : : {
732 : 0 : printMatrix();
733 : : }
734 : 0 : }
735 : :
736 : : /** to += mult * buffer. */
737 : 6403698 : void rowPlusBufferTimesConstant(RowIndex to,
738 : : const T& mult,
739 : : CoefficientChangeCallback& cb)
740 : : {
741 [ - + ][ - + ]: 6403698 : Assert(d_rowInMergeBuffer != ROW_INDEX_SENTINEL);
[ - - ]
742 [ - + ][ - + ]: 6403698 : Assert(to != ROW_INDEX_SENTINEL);
[ - - ]
743 : :
744 [ + - ]: 6403698 : Trace("tableau") << "rowPlusRowTimesConstant(" << to << "," << mult << ","
745 : 0 : << d_rowInMergeBuffer << ")" << std::endl;
746 : :
747 [ - + ][ - + ]: 6403698 : Assert(debugNoZeroCoefficients(to));
[ - - ]
748 [ - + ][ - + ]: 6403698 : Assert(debugNoZeroCoefficients(d_rowInMergeBuffer));
[ - - ]
749 : :
750 [ - + ][ - + ]: 6403698 : Assert(mult != 0);
[ - - ]
751 : :
752 : 6403698 : RowIterator i = getRow(to).begin();
753 : 6403698 : RowIterator i_end = getRow(to).end();
754 [ + + ]: 101570516 : while (i != i_end)
755 : : {
756 : 95166818 : EntryID id = i.getID();
757 : 95166818 : Entry& entry = d_entries.get(id);
758 : 95166818 : ArithVar colVar = entry.getColVar();
759 : :
760 : 95166818 : ++i;
761 : :
762 [ + + ]: 95166818 : if (d_mergeBuffer.isKey(colVar))
763 : : {
764 : 48359407 : EntryID bufferEntry = d_mergeBuffer[colVar].first;
765 [ - + ][ - + ]: 48359407 : Assert(!d_mergeBuffer[colVar].second);
[ - - ]
766 : 48359407 : d_mergeBuffer.get(colVar).second = true;
767 : :
768 : 48359407 : const Entry& other = d_entries.get(bufferEntry);
769 : 48359407 : T& coeff = entry.getCoefficient();
770 : 48359407 : int coeffOldSgn = coeff.sgn();
771 : 48359407 : coeff += mult * other.getCoefficient();
772 : 48359407 : int coeffNewSgn = coeff.sgn();
773 : :
774 [ + + ]: 48359407 : if (coeffOldSgn != coeffNewSgn)
775 : : {
776 : 38417829 : cb.update(to, colVar, coeffOldSgn, coeffNewSgn);
777 : :
778 [ + + ]: 38417829 : if (coeffNewSgn == 0)
779 : : {
780 : 33500283 : removeEntry(id);
781 : : }
782 : : }
783 : : }
784 : : }
785 : :
786 : 6403698 : i = getRow(d_rowInMergeBuffer).begin();
787 : 6403698 : i_end = getRow(d_rowInMergeBuffer).end();
788 : :
789 [ + + ]: 88846742 : for (; i != i_end; ++i)
790 : : {
791 : 82443044 : const Entry& entry = *i;
792 : 82443044 : ArithVar colVar = entry.getColVar();
793 : :
794 [ + + ]: 82443044 : if (d_mergeBuffer[colVar].second)
795 : : {
796 : 48359407 : d_mergeBuffer.get(colVar).second = false;
797 : : }
798 : : else
799 : : {
800 [ - + ][ - + ]: 34083637 : Assert(!(d_mergeBuffer[colVar]).second);
[ - - ]
801 : 34083637 : T newCoeff = mult * entry.getCoefficient();
802 : 34083637 : addEntry(to, colVar, newCoeff);
803 : :
804 : 34083637 : cb.update(to, colVar, 0, newCoeff.sgn());
805 : 34083637 : }
806 : : }
807 : :
808 [ - + ][ - + ]: 6403698 : Assert(mergeBufferIsClear());
[ - - ]
809 : :
810 [ - + ]: 6403698 : if (TraceIsOn("matrix"))
811 : : {
812 : 0 : printMatrix();
813 : : }
814 : 6403698 : }
815 : :
816 : 6403698 : bool mergeBufferIsClear() const
817 : : {
818 : 6403698 : RowToPosUsedPairMap::const_iterator i = d_mergeBuffer.begin();
819 : 6403698 : RowToPosUsedPairMap::const_iterator i_end = d_mergeBuffer.end();
820 [ + + ]: 88846742 : for (; i != i_end; ++i)
821 : : {
822 : 82443044 : RowIndex rid = *i;
823 [ - + ]: 82443044 : if (d_mergeBuffer[rid].second)
824 : : {
825 : 0 : return false;
826 : : }
827 : : }
828 : 6403698 : return true;
829 : : }
830 : :
831 : : protected:
832 : 521588 : EntryID findOnRow(RowIndex rid, ArithVar column) const
833 : : {
834 : 521588 : RowIterator i = d_rows[rid].begin(), i_end = d_rows[rid].end();
835 [ + + ]: 4335887 : for (; i != i_end; ++i)
836 : : {
837 : 4335807 : EntryID id = i.getID();
838 : 4335807 : const MatrixEntry<T>& entry = *i;
839 : 4335807 : ArithVar colVar = entry.getColVar();
840 : :
841 [ + + ]: 4335807 : if (colVar == column)
842 : : {
843 : 521508 : return id;
844 : : }
845 : : }
846 : 80 : return ENTRYID_SENTINEL;
847 : : }
848 : :
849 : 165537 : EntryID findOnCol(RowIndex rid, ArithVar column) const
850 : : {
851 : 165537 : ColIterator i = d_columns[column].begin(), i_end = d_columns[column].end();
852 [ + + ]: 421096 : for (; i != i_end; ++i)
853 : : {
854 : 421071 : EntryID id = i.getID();
855 : 421071 : const MatrixEntry<T>& entry = *i;
856 : 421071 : RowIndex currRow = entry.getRowIndex();
857 : :
858 [ + + ]: 421071 : if (currRow == rid)
859 : : {
860 : 165512 : return id;
861 : : }
862 : : }
863 : 25 : return ENTRYID_SENTINEL;
864 : : }
865 : :
866 : 345833 : EntryID findEntryID(RowIndex rid, ArithVar col) const
867 : : {
868 : 345833 : bool colIsShorter = getColLength(col) < getRowLength(rid);
869 [ + + ]: 345833 : EntryID id = colIsShorter ? findOnCol(rid, col) : findOnRow(rid, col);
870 : 345833 : return id;
871 : : }
872 : : MatrixEntry<T> d_failedFind;
873 : :
874 : : public:
875 : : /** If the find fails, isUnused is true on the entry. */
876 : 341292 : const MatrixEntry<T>& findEntry(RowIndex rid, ArithVar col) const
877 : : {
878 : 341292 : EntryID id = findEntryID(rid, col);
879 [ - + ]: 341292 : if (id == ENTRYID_SENTINEL)
880 : : {
881 : 0 : return d_failedFind;
882 : : }
883 : : else
884 : : {
885 : 341292 : return d_entries[id];
886 : : }
887 : : }
888 : :
889 : : /**
890 : : * Prints the contents of the Matrix to Trace("matrix")
891 : : */
892 : 0 : void printMatrix(std::ostream& out) const
893 : : {
894 : 0 : out << "Matrix::printMatrix" << std::endl;
895 : :
896 [ - - ]: 0 : for (RowIndex i = 0, N = d_rows.size(); i < N; ++i)
897 : : {
898 : 0 : printRow(i, out);
899 : : }
900 : 0 : }
901 [ - - ]: 0 : void printMatrix() const { printMatrix(Trace("matrix")); }
902 : :
903 : 0 : void printRow(RowIndex rid, std::ostream& out) const
904 : : {
905 : 0 : out << "{" << rid << ":";
906 : 0 : const RowVector<T>& row = getRow(rid);
907 : 0 : RowIterator i = row.begin();
908 : 0 : RowIterator i_end = row.end();
909 [ - - ]: 0 : for (; i != i_end; ++i)
910 : : {
911 : 0 : printEntry(*i, out);
912 : 0 : out << ",";
913 : : }
914 : 0 : out << "}" << std::endl;
915 : 0 : }
916 : : void printRow(RowIndex rid) const { printRow(rid, Trace("matrix")); }
917 : :
918 : 0 : void printEntry(const MatrixEntry<T>& entry, std::ostream& out) const
919 : : {
920 : 0 : out << entry.getColVar() << "*" << entry.getCoefficient();
921 : 0 : }
922 : : void printEntry(const MatrixEntry<T>& entry) const
923 : : {
924 : : printEntry(entry, Trace("matrix"));
925 : : }
926 : :
927 : : public:
928 : 50442 : uint32_t size() const { return d_entriesInUse; }
929 : : uint32_t getNumEntriesInTableau() const { return d_entries.size(); }
930 : : uint32_t getEntryCapacity() const { return d_entries.capacity(); }
931 : :
932 : 4541 : void manipulateRowEntry(RowIndex row,
933 : : ArithVar col,
934 : : const T& c,
935 : : CoefficientChangeCallback& cb)
936 : : {
937 : : int coeffOldSgn;
938 : : int coeffNewSgn;
939 : :
940 : 4541 : EntryID id = findEntryID(row, col);
941 [ + + ]: 4541 : if (id == ENTRYID_SENTINEL)
942 : : {
943 : 105 : coeffOldSgn = 0;
944 : 105 : addEntry(row, col, c);
945 : 105 : coeffNewSgn = c.sgn();
946 : : }
947 : : else
948 : : {
949 : 4436 : Entry& e = d_entries.get(id);
950 : 4436 : T& t = e.getCoefficient();
951 : 4436 : coeffOldSgn = t.sgn();
952 : 4436 : t += c;
953 : 4436 : coeffNewSgn = t.sgn();
954 : : }
955 : :
956 [ + + ]: 4541 : if (coeffOldSgn != coeffNewSgn)
957 : : {
958 : 3458 : cb.update(row, col, coeffOldSgn, coeffNewSgn);
959 : : }
960 [ + + ]: 4541 : if (coeffNewSgn == 0)
961 : : {
962 : 3315 : removeEntry(id);
963 : : }
964 : 4541 : }
965 : :
966 : 4096 : void removeRow(RowIndex rid)
967 : : {
968 : 4096 : RowIterator i = getRow(rid).begin();
969 : 4096 : RowIterator i_end = getRow(rid).end();
970 [ + + ]: 19731 : for (; i != i_end; ++i)
971 : : {
972 : 15635 : EntryID id = i.getID();
973 : 15635 : removeEntry(id);
974 : : }
975 : 4096 : releaseRowIndex(rid);
976 : 4096 : }
977 : :
978 : : double densityMeasure() const
979 : : {
980 : : Assert(numNonZeroEntriesByRow() == numNonZeroEntries());
981 : : Assert(numNonZeroEntriesByCol() == numNonZeroEntries());
982 : :
983 : : uint32_t n = getNumRows();
984 : : if (n == 0)
985 : : {
986 : : return 1.0;
987 : : }
988 : : else
989 : : {
990 : : uint32_t s = numNonZeroEntries();
991 : : uint32_t m = d_columns.size();
992 : : uint32_t divisor = (n * (m - n + 1));
993 : :
994 : : Assert(n >= 1);
995 : : Assert(m >= n);
996 : : Assert(divisor > 0);
997 : : Assert(divisor >= s);
998 : :
999 : : return (double(s)) / divisor;
1000 : : }
1001 : : }
1002 : :
1003 : : void loadSignQueries(RowIndex rid, DenseMap<int>& target) const
1004 : : {
1005 : : RowIterator i = getRow(rid).begin(), i_end = getRow(rid).end();
1006 : : for (; i != i_end; ++i)
1007 : : {
1008 : : const MatrixEntry<T>& entry = *i;
1009 : : target.set(entry.getColVar(), entry.getCoefficient().sgn());
1010 : : }
1011 : : }
1012 : :
1013 : : protected:
1014 : : uint32_t numNonZeroEntries() const { return size(); }
1015 : :
1016 : : uint32_t numNonZeroEntriesByRow() const
1017 : : {
1018 : : uint32_t rowSum = 0;
1019 : : for (RowIndex rid = 0, N = d_rows.size(); rid < N; ++rid)
1020 : : {
1021 : : rowSum += getRowLength(rid);
1022 : : }
1023 : : return rowSum;
1024 : : }
1025 : :
1026 : : uint32_t numNonZeroEntriesByCol() const
1027 : : {
1028 : : uint32_t colSum = 0;
1029 : : for (ArithVar v = 0, N = d_columns.size(); v < N; ++v)
1030 : : {
1031 : : colSum += getColLength(v);
1032 : : }
1033 : : return colSum;
1034 : : }
1035 : :
1036 : 13008643 : bool debugNoZeroCoefficients(RowIndex ridx)
1037 : : {
1038 [ + + ]: 191636568 : for (RowIterator i = getRow(ridx).begin(); !i.atEnd(); ++i)
1039 : : {
1040 : 178627925 : const Entry& entry = *i;
1041 [ - + ]: 178627925 : if (entry.getCoefficient() == 0)
1042 : : {
1043 : 0 : return false;
1044 : : }
1045 : : }
1046 : 13008643 : return true;
1047 : : }
1048 : 201247 : bool debugMatchingCountsForRow(RowIndex ridx)
1049 : : {
1050 [ + + ]: 1219310 : for (RowIterator i = getRow(ridx).begin(); !i.atEnd(); ++i)
1051 : : {
1052 : 1018063 : const Entry& entry = *i;
1053 : 1018063 : ArithVar colVar = entry.getColVar();
1054 : 1018063 : uint32_t count = debugCountColLength(colVar);
1055 [ + - ]: 2036126 : Trace("tableau") << "debugMatchingCountsForRow " << ridx << ":" << colVar
1056 : 1018063 : << " " << count << " " << getColLength(colVar)
1057 : 0 : << std::endl;
1058 [ - + ]: 1018063 : if (count != getColLength(colVar))
1059 : : {
1060 : 0 : return false;
1061 : : }
1062 : : }
1063 : 201247 : return true;
1064 : : }
1065 : :
1066 : 1018063 : uint32_t debugCountColLength(ArithVar var)
1067 : : {
1068 [ + - ]: 1018063 : Trace("tableau") << var << " ";
1069 : 1018063 : uint32_t count = 0;
1070 [ + + ]: 25316897 : for (ColIterator i = getColumn(var).begin(); !i.atEnd(); ++i)
1071 : : {
1072 : 24298834 : const Entry& entry = *i;
1073 [ + - ]: 24298834 : Trace("tableau") << "(" << entry.getRowIndex() << ", " << i.getID()
1074 : 0 : << ") ";
1075 : 24298834 : ++count;
1076 : : }
1077 [ + - ]: 1018063 : Trace("tableau") << std::endl;
1078 : 1018063 : return count;
1079 : : }
1080 : : uint32_t debugCountRowLength(RowIndex ridx)
1081 : : {
1082 : : uint32_t count = 0;
1083 : : for (RowIterator i = getRow(ridx).begin(); !i.atEnd(); ++i)
1084 : : {
1085 : : ++count;
1086 : : }
1087 : : return count;
1088 : : }
1089 : :
1090 : : }; /* class Matrix<T> */
1091 : :
1092 : : } // namespace arith::linear
1093 : : } // namespace theory
1094 : : } // namespace cvc5::internal
|
