GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/matrix.h Lines: 307 401 76.6 %
Date: 2021-03-23 Branches: 252 1116 22.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file matrix.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Mathias Preiner, Morgan Deters
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief 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 "cvc4_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/arithvar.h"
28
#include "util/dense_map.h"
29
#include "util/index.h"
30
31
namespace CVC4 {
32
namespace theory {
33
namespace arith {
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
8997
class CoefficientChangeCallback {
42
public:
43
91556
  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
82562
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
54974951
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
677207
  MatrixEntry():
72
    d_rowIndex(ROW_INDEX_SENTINEL),
73
    d_colVar(ARITHVAR_SENTINEL),
74
    d_nextRow(ENTRYID_SENTINEL),
75
    d_nextCol(ENTRYID_SENTINEL),
76
    d_prevRow(ENTRYID_SENTINEL),
77
    d_prevCol(ENTRYID_SENTINEL),
78
677207
    d_coefficient()
79
677207
  {}
80
81
25583680
  MatrixEntry(RowIndex row, ArithVar col, const T& coeff):
82
     d_rowIndex(row),
83
     d_colVar(col),
84
     d_nextRow(ENTRYID_SENTINEL),
85
     d_nextCol(ENTRYID_SENTINEL),
86
     d_prevRow(ENTRYID_SENTINEL),
87
     d_prevCol(ENTRYID_SENTINEL),
88
25583680
     d_coefficient(coeff)
89
25583680
  {}
90
91
private:
92
25206435
  bool unusedConsistent() const {
93
    return
94
50607797
      (d_rowIndex == ROW_INDEX_SENTINEL && d_colVar == ARITHVAR_SENTINEL) ||
95
25596289
      (d_rowIndex != ROW_INDEX_SENTINEL && d_colVar != ARITHVAR_SENTINEL);
96
  }
97
98
public:
99
100
328231982
  EntryID getNextRowEntryID() const {
101
328231982
    return d_nextRow;
102
  }
103
104
74022791
  EntryID getNextColEntryID() const {
105
74022791
    return d_nextCol;
106
  }
107
25011508
  EntryID getPrevRowEntryID() const {
108
25011508
    return d_prevRow;
109
  }
110
111
25011508
  EntryID getPrevColEntryID() const {
112
25011508
    return d_prevCol;
113
  }
114
115
39968042
  void setNextRowEntryID(EntryID id) {
116
39968042
    d_nextRow = id;
117
39968042
  }
118
44477135
  void setNextColEntryID(EntryID id) {
119
44477135
    d_nextCol = id;
120
44477135
  }
121
50317121
  void setPrevRowEntryID(EntryID id) {
122
50317121
    d_prevRow = id;
123
50317121
  }
124
49913140
  void setPrevColEntryID(EntryID id) {
125
49913140
    d_prevCol = id;
126
49913140
  }
127
128
77698466
  RowIndex getRowIndex() const{
129
77698466
    return d_rowIndex;
130
  }
131
132
228936249
  ArithVar getColVar() const{
133
228936249
    return d_colVar;
134
  }
135
136
256634904
  const T& getCoefficient() const {
137
256634904
    return d_coefficient;
138
  }
139
140
70582918
  T& getCoefficient(){
141
70582918
    return d_coefficient;
142
  }
143
144
  void setCoefficient(const T& t){
145
    d_coefficient = t;
146
  }
147
148
25011508
  void markBlank() {
149
25011508
    d_rowIndex = ROW_INDEX_SENTINEL;
150
25011508
    d_colVar = ARITHVAR_SENTINEL;
151
25011508
  }
152
153
25206435
  bool blank() const{
154
25206435
    Assert(unusedConsistent());
155
156
25206435
    return d_rowIndex == ROW_INDEX_SENTINEL;
157
  }
158
}; /* class MatrixEntry<T> */
159
160
template<class T>
161
17988
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
17994
  MatrixEntryVector():
173
17994
    d_entries(), d_freedEntries(), d_size(0)
174
17994
  {}
175
176
633446807
  const EntryType& operator[](EntryID id) const{
177
633446807
    Assert(inBounds(id));
178
633446807
    return d_entries[id];
179
  }
180
181
472361752
  EntryType& get(EntryID id){
182
472361752
    Assert(inBounds(id));
183
472361752
    return d_entries[id];
184
  }
185
186
25011508
  void freeEntry(EntryID id){
187
25011508
    Assert(get(id).blank());
188
25011508
    Assert(d_size > 0);
189
190
25011508
    d_freedEntries.push(id);
191
25011508
    --d_size;
192
25011508
  }
193
194
25583680
  EntryID newEntry(){
195
    EntryID newId;
196
25583680
    if(d_freedEntries.empty()){
197
659213
      newId = d_entries.size();
198
659213
      d_entries.push_back(MatrixEntry<T>());
199
    }else{
200
24924467
      newId = d_freedEntries.front();
201
24924467
      d_freedEntries.pop();
202
    }
203
25583680
    ++d_size;
204
25583680
    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
1105808559
  bool inBounds(EntryID id) const{
213
1105808559
    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
36241052
    Iterator(EntryID start, const MatrixEntryVector<T>* entries) :
232
36241052
      d_curr(start), d_entries(entries)
233
36241052
    {}
234
235
  public:
236
237
91981136
    EntryID getID() const {
238
91981136
      return d_curr;
239
    }
240
241
281020123
    const MatrixEntry<T>& operator*() const{
242
281020123
      Assert(!atEnd());
243
281020123
      return (*d_entries)[d_curr];
244
    }
245
246
352231757
    Iterator& operator++(){
247
352231757
      Assert(!atEnd());
248
352231757
      const MatrixEntry<T>& entry = (*d_entries)[d_curr];
249
352231757
      d_curr = isRow ? entry.getNextRowEntryID() : entry.getNextColEntryID();
250
352231757
      return *this;
251
    }
252
253
868999519
    bool atEnd() const {
254
868999519
      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
144852611
    bool operator!=(const Iterator& i) const{
262
144852611
      return !(d_curr == i.d_curr && d_entries == i.d_entries);
263
    }
264
  }; /* class MatrixVector<T, isRow>::Iterator */
265
266
public:
267
229010
  MatrixVector(MatrixEntryVector<T>* mev)
268
229010
    : d_head(ENTRYID_SENTINEL), d_size(0), d_entries(mev)
269
229010
  {}
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
28368493
  const_iterator begin() const {
277
28368493
    return Iterator(d_head, d_entries);
278
  }
279
7872559
  const_iterator end() const {
280
7872559
    return Iterator(ENTRYID_SENTINEL, d_entries);
281
  }
282
283
  EntryID getHead() const { return d_head; }
284
285
62698186
  uint32_t getSize() const { return d_size; }
286
287
51167360
  void insert(EntryID newId){
288
    if(isRow){
289
25583680
      d_entries->get(newId).setNextRowEntryID(d_head);
290
291
25583680
      if(d_head != ENTRYID_SENTINEL){
292
25501118
        d_entries->get(d_head).setPrevRowEntryID(newId);
293
      }
294
    }else{
295
25583680
      d_entries->get(newId).setNextColEntryID(d_head);
296
297
25583680
      if(d_head != ENTRYID_SENTINEL){
298
25447875
        d_entries->get(d_head).setPrevColEntryID(newId);
299
      }
300
    }
301
302
51167360
    d_head = newId;
303
51167360
    ++d_size;
304
51167360
  }
305
50023016
  void remove(EntryID id){
306
50023016
    Assert(d_size > 0);
307
50023016
    --d_size;
308
    if(isRow){
309
25011508
      EntryID prevRow = d_entries->get(id).getPrevRowEntryID();
310
25011508
      EntryID nextRow = d_entries->get(id).getNextRowEntryID();
311
312
25011508
      if(d_head == id){
313
10627146
        d_head = nextRow;
314
      }
315
25011508
      if(prevRow != ENTRYID_SENTINEL){
316
14384362
        d_entries->get(prevRow).setNextRowEntryID(nextRow);
317
      }
318
25011508
      if(nextRow != ENTRYID_SENTINEL){
319
24816003
        d_entries->get(nextRow).setPrevRowEntryID(prevRow);
320
      }
321
    }else{
322
25011508
      EntryID prevCol = d_entries->get(id).getPrevColEntryID();
323
25011508
      EntryID nextCol = d_entries->get(id).getNextColEntryID();
324
325
25011508
      if(d_head == id){
326
6118053
        d_head = nextCol;
327
      }
328
329
25011508
      if(prevCol != ENTRYID_SENTINEL){
330
18893455
        d_entries->get(prevCol).setNextColEntryID(nextCol);
331
      }
332
25011508
      if(nextCol != ENTRYID_SENTINEL){
333
24465265
        d_entries->get(nextCol).setPrevColEntryID(prevCol);
334
      }
335
    }
336
50023016
  }
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
82562
  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
146448
  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
17988
class Matrix {
367
public:
368
  typedef MatrixEntry<T> Entry;
369
370
protected:
371
  typedef CVC4::theory::arith::RowVector<T> RowVectorT;
372
  typedef CVC4::theory::arith::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
  Matrix()
407
  : d_rows(),
408
    d_columns(),
409
    d_mergeBuffer(),
410
    d_rowInMergeBuffer(ROW_INDEX_SENTINEL),
411
    d_entriesInUse(0),
412
    d_entries(),
413
    d_zero(0)
414
  {}
415
416
17994
  Matrix(const T& zero)
417
  : d_rows(),
418
    d_columns(),
419
    d_mergeBuffer(),
420
    d_rowInMergeBuffer(ROW_INDEX_SENTINEL),
421
    d_entriesInUse(0),
422
    d_entries(),
423
17994
    d_zero(zero)
424
17994
  {}
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
25583680
  void addEntry(RowIndex row, ArithVar col, const T& coeff){
469
25583680
    Debug("tableau") << "addEntry(" << row << "," << col <<"," << coeff << ")" << std::endl;
470
471
25583680
    Assert(coeff != 0);
472
25583680
    Assert(row < d_rows.size());
473
25583680
    Assert(col < d_columns.size());
474
475
25583680
    EntryID newId = d_entries.newEntry();
476
25583680
    Entry& newEntry = d_entries.get(newId);
477
25583680
    newEntry = Entry(row, col, coeff);
478
479
25583680
    Assert(newEntry.getCoefficient() != 0);
480
481
25583680
    ++d_entriesInUse;
482
483
25583680
    d_rows[row].insert(newId);
484
25583680
    d_columns[col].insert(newId);
485
25583680
  }
486
487
25011508
  void removeEntry(EntryID id){
488
25011508
    Assert(d_entriesInUse > 0);
489
25011508
    --d_entriesInUse;
490
491
25011508
    Entry& entry = d_entries.get(id);
492
493
25011508
    RowIndex ridx = entry.getRowIndex();
494
25011508
    ArithVar col = entry.getColVar();
495
496
25011508
    Assert(d_rows[ridx].getSize() > 0);
497
25011508
    Assert(d_columns[col].getSize() > 0);
498
499
25011508
    d_rows[ridx].remove(id);
500
25011508
    d_columns[col].remove(id);
501
502
25011508
    entry.markBlank();
503
504
25011508
    d_entries.freeEntry(id);
505
25011508
  }
506
507
 private:
508
82562
  RowIndex requestRowIndex(){
509
82562
    if(d_pool.empty()){
510
82562
      RowIndex ridx = d_rows.size();
511
82562
      d_rows.push_back(RowVectorT(&d_entries));
512
82562
      return ridx;
513
    }else{
514
      RowIndex rid = d_pool.back();
515
      d_pool.pop_back();
516
      return rid;
517
    }
518
  }
519
520
  void releaseRowIndex(RowIndex rid){
521
    d_pool.push_back(rid);
522
  }
523
524
public:
525
526
  size_t getNumRows() const {
527
    return d_rows.size();
528
  }
529
530
272567
  size_t getNumColumns() const {
531
272567
    return d_columns.size();
532
  }
533
534
146448
  void increaseSize(){
535
146448
    d_columns.push_back(ColumnVector<T>(&d_entries));
536
146448
  }
537
538
  void increaseSizeTo(size_t s){
539
    while(getNumColumns() < s){
540
      increaseSize();
541
    }
542
  }
543
544
38771352
  const RowVector<T>& getRow(RowIndex r) const {
545
38771352
    Assert(r < d_rows.size());
546
38771352
    return d_rows[r];
547
  }
548
549
9365162
  const ColumnVector<T>& getColumn(ArithVar v) const {
550
9365162
    Assert(v < d_columns.size());
551
9365162
    return d_columns[v];
552
  }
553
554
9837250
  uint32_t getRowLength(RowIndex r) const{
555
9837250
    return getRow(r).getSize();
556
  }
557
558
2837920
  uint32_t getColLength(ArithVar x) const{
559
2837920
    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
82562
  RowIndex addRow(const std::vector<T>& coeffs,
568
                  const std::vector<ArithVar>& variables){
569
570
82562
    RowIndex ridx = requestRowIndex();
571
572
    //RowIndex ridx = d_rows.size();
573
    //d_rows.push_back(RowVectorT(&d_entries));
574
575
82562
    typename std::vector<T>::const_iterator coeffIter = coeffs.begin();
576
82562
    std::vector<ArithVar>::const_iterator varsIter = variables.begin();
577
82562
    std::vector<ArithVar>::const_iterator varsEnd = variables.end();
578
579
462572
    for(; varsIter != varsEnd; ++coeffIter, ++varsIter){
580
190005
      const T& coeff = *coeffIter;
581
190005
      ArithVar var_i = *varsIter;
582
190005
      Assert(var_i < getNumColumns());
583
190005
      addEntry(ridx, var_i, coeff);
584
    }
585
586
82562
    return ridx;
587
  }
588
589
590
236755
  void loadRowIntoBuffer(RowIndex rid){
591
236755
    Assert(d_mergeBuffer.empty());
592
236755
    Assert(d_rowInMergeBuffer == ROW_INDEX_SENTINEL);
593
594
236755
    RowIterator i = getRow(rid).begin(), i_end = getRow(rid).end();
595
10474599
    for(; i != i_end; ++i){
596
5118922
      EntryID id = i.getID();
597
5118922
      const MatrixEntry<T>& entry = *i;
598
5118922
      ArithVar colVar = entry.getColVar();
599
10237844
      d_mergeBuffer.set(colVar, std::make_pair(id, false));
600
    }
601
602
236755
    d_rowInMergeBuffer = rid;
603
236755
  }
604
605
236755
  void clearBuffer() {
606
236755
    Assert(d_rowInMergeBuffer != ROW_INDEX_SENTINEL);
607
608
236755
    d_rowInMergeBuffer = ROW_INDEX_SENTINEL;
609
236755
    d_mergeBuffer.purge();
610
236755
  }
611
612
  /* to *= mult */
613
  void multiplyRowByConstant(RowIndex to, const T& mult){
614
    RowIterator i = getRow(to).begin();
615
    RowIterator i_end = getRow(to).end();
616
    for( ; i != i_end; ++i){
617
      EntryID id = i.getID();
618
      Entry& entry = d_entries.get(id);
619
      T& coeff = entry.getCoefficient();
620
      coeff *= mult;
621
    }
622
  }
623
624
  /**  to += mult * from.
625
   * Use the more efficient rowPlusBufferTimesConstant() for
626
   * repeated use.
627
   */
628
  void rowPlusRowTimesConstant(RowIndex to, RowIndex from, const T& mult){
629
    Assert(to != from);
630
    loadRowIntoBuffer(from);
631
    rowPlusBufferTimesConstant(to, mult);
632
    clearBuffer();
633
  }
634
635
  /**  to += mult * buffer.
636
   * Invalidates coefficients on the row.
637
   * (mult should never be a direct copy of a coefficient!)
638
   */
639
  void rowPlusBufferTimesConstant(RowIndex to, const T& mult){
640
    Assert(d_rowInMergeBuffer != ROW_INDEX_SENTINEL);
641
    Assert(to != ROW_INDEX_SENTINEL);
642
643
    Debug("tableau") << "rowPlusRowTimesConstant("
644
                     << to << "," << mult << "," << d_rowInMergeBuffer << ")"
645
                     << std::endl;
646
647
    Assert(debugNoZeroCoefficients(to));
648
    Assert(debugNoZeroCoefficients(d_rowInMergeBuffer));
649
650
    Assert(mult != 0);
651
652
    RowIterator i = getRow(to).begin();
653
    RowIterator i_end = getRow(to).end();
654
    while(i != i_end){
655
      EntryID id = i.getID();
656
      Entry& entry = d_entries.get(id);
657
      ArithVar colVar = entry.getColVar();
658
659
      ++i;
660
661
      if(d_mergeBuffer.isKey(colVar)){
662
        EntryID bufferEntry = d_mergeBuffer[colVar].first;
663
        Assert(!d_mergeBuffer[colVar].second);
664
        d_mergeBuffer.get(colVar).second = true;
665
666
        const Entry& other = d_entries.get(bufferEntry);
667
        T& coeff = entry.getCoefficient();
668
        coeff += mult * other.getCoefficient();
669
670
        if(coeff.sgn() == 0){
671
          removeEntry(id);
672
        }
673
      }
674
    }
675
676
    i = getRow(d_rowInMergeBuffer).begin();
677
    i_end = getRow(d_rowInMergeBuffer).end();
678
679
    for(; i != i_end; ++i){
680
      const Entry& entry = *i;
681
      ArithVar colVar = entry.getColVar();
682
683
      if(d_mergeBuffer[colVar].second){
684
        d_mergeBuffer.get(colVar).second = false;
685
      }else{
686
        Assert(!(d_mergeBuffer[colVar]).second);
687
        T newCoeff =  mult * entry.getCoefficient();
688
        addEntry(to, colVar, newCoeff);
689
      }
690
    }
691
692
    Assert(mergeBufferIsClear());
693
694
    if(Debug.isOn("matrix")) { printMatrix(); }
695
  }
696
697
  /**  to += mult * buffer. */
698
3622975
  void rowPlusBufferTimesConstant(RowIndex to, const T& mult, CoefficientChangeCallback& cb){
699
3622975
    Assert(d_rowInMergeBuffer != ROW_INDEX_SENTINEL);
700
3622975
    Assert(to != ROW_INDEX_SENTINEL);
701
702
7245950
    Debug("tableau") << "rowPlusRowTimesConstant("
703
3622975
                     << to << "," << mult << "," << d_rowInMergeBuffer << ")"
704
                     << std::endl;
705
706
3622975
    Assert(debugNoZeroCoefficients(to));
707
3622975
    Assert(debugNoZeroCoefficients(d_rowInMergeBuffer));
708
709
3622975
    Assert(mult != 0);
710
711
3622975
    RowIterator i = getRow(to).begin();
712
3622975
    RowIterator i_end = getRow(to).end();
713
137301817
    while(i != i_end){
714
66839421
      EntryID id = i.getID();
715
66839421
      Entry& entry = d_entries.get(id);
716
66839421
      ArithVar colVar = entry.getColVar();
717
718
66839421
      ++i;
719
720
66839421
      if(d_mergeBuffer.isKey(colVar)){
721
36387934
        EntryID bufferEntry = d_mergeBuffer[colVar].first;
722
36387934
        Assert(!d_mergeBuffer[colVar].second);
723
36387934
        d_mergeBuffer.get(colVar).second = true;
724
725
36387934
        const Entry& other = d_entries.get(bufferEntry);
726
36387934
        T& coeff = entry.getCoefficient();
727
36387934
        int coeffOldSgn = coeff.sgn();
728
36387934
        coeff += mult * other.getCoefficient();
729
36387934
        int coeffNewSgn = coeff.sgn();
730
731
36387934
        if(coeffOldSgn != coeffNewSgn){
732
28882612
          cb.update(to, colVar, coeffOldSgn,  coeffNewSgn);
733
734
28882612
          if(coeffNewSgn == 0){
735
25011508
            removeEntry(id);
736
          }
737
        }
738
      }
739
    }
740
741
3622975
    i = getRow(d_rowInMergeBuffer).begin();
742
3622975
    i_end = getRow(d_rowInMergeBuffer).end();
743
744
127021069
    for(; i != i_end; ++i){
745
61699047
      const Entry& entry = *i;
746
61699047
      ArithVar colVar = entry.getColVar();
747
748
61699047
      if(d_mergeBuffer[colVar].second){
749
36387934
        d_mergeBuffer.get(colVar).second = false;
750
      }else{
751
25311113
        Assert(!(d_mergeBuffer[colVar]).second);
752
50622226
        T newCoeff =  mult * entry.getCoefficient();
753
25311113
        addEntry(to, colVar, newCoeff);
754
755
25311113
        cb.update(to, colVar, 0,  newCoeff.sgn());
756
      }
757
    }
758
759
3622975
    Assert(mergeBufferIsClear());
760
761
3622975
    if(Debug.isOn("matrix")) { printMatrix(); }
762
3622975
  }
763
764
3622975
  bool mergeBufferIsClear() const{
765
3622975
    RowToPosUsedPairMap::const_iterator i = d_mergeBuffer.begin();
766
3622975
    RowToPosUsedPairMap::const_iterator i_end = d_mergeBuffer.end();
767
127021069
    for(; i != i_end; ++i){
768
61699047
      RowIndex rid = *i;
769
61699047
      if(d_mergeBuffer[rid].second){
770
        return false;
771
      }
772
    }
773
3622975
    return true;
774
  }
775
776
protected:
777
778
295326
  EntryID findOnRow(RowIndex rid, ArithVar column) const {
779
295326
    RowIterator i = d_rows[rid].begin(), i_end = d_rows[rid].end();
780
6545982
    for(; i != i_end; ++i){
781
3420654
      EntryID id = i.getID();
782
3420654
      const MatrixEntry<T>& entry = *i;
783
3420654
      ArithVar colVar = entry.getColVar();
784
785
3420654
      if(colVar == column){
786
295326
        return id;
787
      }
788
    }
789
    return ENTRYID_SENTINEL;
790
  }
791
792
94528
  EntryID findOnCol(RowIndex rid, ArithVar column) const{
793
94528
    ColIterator i = d_columns[column].begin(), i_end = d_columns[column].end();
794
489196
    for(; i != i_end; ++i){
795
291862
      EntryID id = i.getID();
796
291862
      const MatrixEntry<T>& entry = *i;
797
291862
      RowIndex currRow = entry.getRowIndex();
798
799
291862
      if(currRow == rid){
800
94528
        return id;
801
      }
802
    }
803
    return ENTRYID_SENTINEL;
804
  }
805
806
194927
  EntryID findEntryID(RowIndex rid, ArithVar col) const{
807
194927
    bool colIsShorter = getColLength(col) < getRowLength(rid);
808
194927
    EntryID id = colIsShorter ? findOnCol(rid, col) : findOnRow(rid,col);
809
194927
    return id;
810
  }
811
  MatrixEntry<T> d_failedFind;
812
public:
813
814
  /** If the find fails, isUnused is true on the entry. */
815
194927
  const MatrixEntry<T>& findEntry(RowIndex rid, ArithVar col) const{
816
194927
    EntryID id = findEntryID(rid, col);
817
194927
    if(id == ENTRYID_SENTINEL){
818
      return d_failedFind;
819
    }else{
820
194927
      return d_entries[id];
821
    }
822
  }
823
824
  /**
825
   * Prints the contents of the Matrix to Debug("matrix")
826
   */
827
  void printMatrix(std::ostream& out) const {
828
    out << "Matrix::printMatrix"  << std::endl;
829
830
    for(RowIndex i = 0, N = d_rows.size(); i < N; ++i){
831
      printRow(i, out);
832
    }
833
  }
834
  void printMatrix() const {
835
    printMatrix(Debug("matrix"));
836
  }
837
838
  void printRow(RowIndex rid, std::ostream& out) const {
839
    out << "{" << rid << ":";
840
    const RowVector<T>& row = getRow(rid);
841
    RowIterator i = row.begin();
842
    RowIterator i_end = row.end();
843
    for(; i != i_end; ++i){
844
      printEntry(*i, out);
845
      out << ",";
846
    }
847
    out << "}" << std::endl;
848
  }
849
  void printRow(RowIndex rid) const {
850
    printRow(rid, Debug("matrix"));
851
  }
852
853
  void printEntry(const MatrixEntry<T>& entry, std::ostream& out) const {
854
    out << entry.getColVar() << "*" << entry.getCoefficient();
855
  }
856
  void printEntry(const MatrixEntry<T>& entry) const {
857
    printEntry(entry, Debug("matrix"));
858
  }
859
public:
860
12418
  uint32_t size() const {
861
12418
    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
  void manipulateRowEntry(RowIndex row, ArithVar col, const T& c, CoefficientChangeCallback& cb){
871
    int coeffOldSgn;
872
    int coeffNewSgn;
873
874
    EntryID id = findEntryID(row, col);
875
    if(id == ENTRYID_SENTINEL){
876
      coeffOldSgn = 0;
877
      addEntry(row, col, c);
878
      coeffNewSgn = c.sgn();
879
    }else{
880
      Entry& e = d_entries.get(id);
881
      T& t = e.getCoefficient();
882
      coeffOldSgn = t.sgn();
883
      t += c;
884
      coeffNewSgn = t.sgn();
885
    }
886
887
    if(coeffOldSgn != coeffNewSgn){
888
      cb.update(row, col, coeffOldSgn,  coeffNewSgn);
889
    }
890
    if(coeffNewSgn == 0){
891
      removeEntry(id);
892
    }
893
  }
894
895
  void removeRow(RowIndex rid){
896
    RowIterator i = getRow(rid).begin();
897
    RowIterator i_end = getRow(rid).end();
898
    for(; i != i_end; ++i){
899
      EntryID id = i.getID();
900
      removeEntry(id);
901
    }
902
    releaseRowIndex(rid);
903
  }
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
7328512
  bool debugNoZeroCoefficients(RowIndex ridx){
956
136248131
    for(RowIterator i=getRow(ridx).begin(); !i.atEnd(); ++i){
957
128919619
      const Entry& entry = *i;
958
128919619
      if(entry.getCoefficient() == 0){
959
        return false;
960
      }
961
    }
962
7328512
    return true;
963
  }
964
82562
  bool debugMatchingCountsForRow(RowIndex ridx){
965
463713
    for(RowIterator i=getRow(ridx).begin(); !i.atEnd(); ++i){
966
381151
      const Entry& entry = *i;
967
381151
      ArithVar colVar = entry.getColVar();
968
381151
      uint32_t count = debugCountColLength(colVar);
969
1143453
      Debug("tableau") << "debugMatchingCountsForRow "
970
381151
                       << ridx << ":" << colVar << " " << count
971
762302
                       <<" "<< getColLength(colVar) << std::endl;
972
381151
      if( count != getColLength(colVar) ){
973
        return false;
974
      }
975
    }
976
82562
    return true;
977
  }
978
979
381151
  uint32_t debugCountColLength(ArithVar var){
980
381151
    Debug("tableau") << var << " ";
981
381151
    uint32_t count = 0;
982
8080124
    for(ColIterator i=getColumn(var).begin(); !i.atEnd(); ++i){
983
7698973
      const Entry& entry = *i;
984
7698973
      Debug("tableau") << "(" << entry.getRowIndex() << ", " << i.getID() << ") ";
985
7698973
      ++count;
986
    }
987
381151
    Debug("tableau") << std::endl;
988
381151
    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
}/* CVC4::theory::arith namespace */
1001
}/* CVC4::theory namespace */
1002
}/* CVC4 namespace */
1003