GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/tableau.cpp Lines: 76 109 69.7 %
Date: 2021-03-23 Branches: 117 492 23.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file tableau.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King
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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "base/output.h"
19
#include "theory/arith/tableau.h"
20
21
using namespace std;
22
namespace CVC4 {
23
namespace theory {
24
namespace arith {
25
26
27
194927
void Tableau::pivot(ArithVar oldBasic, ArithVar newBasic, CoefficientChangeCallback& cb){
28
194927
  Assert(isBasic(oldBasic));
29
194927
  Assert(!isBasic(newBasic));
30
194927
  Assert(d_mergeBuffer.empty());
31
32
194927
  Debug("tableau") << "Tableau::pivot(" <<  oldBasic <<", " << newBasic <<")"  << endl;
33
34
194927
  RowIndex ridx = basicToRowIndex(oldBasic);
35
36
194927
  rowPivot(oldBasic, newBasic, cb);
37
194927
  Assert(ridx == basicToRowIndex(newBasic));
38
39
194927
  loadRowIntoBuffer(ridx);
40
41
194927
  ColIterator colIter = colIterator(newBasic);
42
7747075
  while(!colIter.atEnd()){
43
3776074
    EntryID id = colIter.getID();
44
3776074
    Entry& entry = d_entries.get(id);
45
46
3776074
    ++colIter; //needs to be incremented before the variable is removed
47
3776074
    if(entry.getRowIndex() == ridx){ continue; }
48
49
3581147
    RowIndex to = entry.getRowIndex();
50
7162294
    Rational coeff = entry.getCoefficient();
51
3581147
    if(cb.canUseRow(to)){
52
3581147
      rowPlusBufferTimesConstant(to, coeff, cb);
53
    }else{
54
      rowPlusBufferTimesConstant(to, coeff);
55
    }
56
  }
57
194927
  clearBuffer();
58
59
  //Clear the column for used for this variable
60
61
194927
  Assert(d_mergeBuffer.empty());
62
194927
  Assert(!isBasic(oldBasic));
63
194927
  Assert(isBasic(newBasic));
64
194927
  Assert(getColLength(newBasic) == 1);
65
194927
}
66
67
/**
68
 * Changes basic to newbasic (a variable on the row).
69
 */
70
194927
void Tableau::rowPivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCallback& cb){
71
194927
  Assert(isBasic(basicOld));
72
194927
  Assert(!isBasic(basicNew));
73
74
194927
  RowIndex rid = basicToRowIndex(basicOld);
75
76
194927
  EntryID newBasicID = findOnRow(rid, basicNew);
77
78
194927
  Assert(newBasicID != ENTRYID_SENTINEL);
79
80
194927
  Tableau::Entry& newBasicEntry = d_entries.get(newBasicID);
81
194927
  const Rational& a_rs = newBasicEntry.getCoefficient();
82
194927
  int a_rs_sgn = a_rs.sgn();
83
389854
  Rational negInverseA_rs = -(a_rs.inverse());
84
85
5030157
  for(RowIterator i = basicRowIterator(basicOld); !i.atEnd(); ++i){
86
4835230
    EntryID id = i.getID();
87
4835230
    Tableau::Entry& entry = d_entries.get(id);
88
89
4835230
    entry.getCoefficient() *=  negInverseA_rs;
90
  }
91
92
194927
  d_basic2RowIndex.remove(basicOld);
93
194927
  d_basic2RowIndex.set(basicNew, rid);
94
194927
  d_rowIndex2basic.set(rid, basicNew);
95
96
194927
  cb.multiplyRow(rid, -a_rs_sgn);
97
194927
}
98
99
82562
void Tableau::addRow(ArithVar basic,
100
                     const std::vector<Rational>& coefficients,
101
                     const std::vector<ArithVar>& variables)
102
{
103
82562
  Assert(basic < getNumColumns());
104
82562
  Assert(debugIsASet(variables));
105
82562
  Assert(coefficients.size() == variables.size());
106
82562
  Assert(!isBasic(basic));
107
108
82562
  RowIndex newRow = Matrix<Rational>::addRow(coefficients, variables);
109
82562
  addEntry(newRow, basic, Rational(-1));
110
111
82562
  Assert(!d_basic2RowIndex.isKey(basic));
112
82562
  Assert(!d_rowIndex2basic.isKey(newRow));
113
114
82562
  d_basic2RowIndex.set(basic, newRow);
115
82562
  d_rowIndex2basic.set(newRow, basic);
116
117
118
82562
  if(Debug.isOn("matrix")){ printMatrix(); }
119
120
165124
  NoEffectCCCB noeffect;
121
82562
  NoEffectCCCB* nep = &noeffect;
122
82562
  CoefficientChangeCallback* cccb = static_cast<CoefficientChangeCallback*>(nep);
123
124
82562
  vector<Rational>::const_iterator coeffIter = coefficients.begin();
125
82562
  vector<ArithVar>::const_iterator varsIter = variables.begin();
126
82562
  vector<ArithVar>::const_iterator varsEnd = variables.end();
127
462572
  for(; varsIter != varsEnd; ++coeffIter, ++varsIter){
128
190005
    ArithVar var = *varsIter;
129
130
190005
    if(isBasic(var)){
131
83656
      Rational coeff = *coeffIter;
132
133
41828
      RowIndex ri = basicToRowIndex(var);
134
135
41828
      loadRowIntoBuffer(ri);
136
41828
      rowPlusBufferTimesConstant(newRow, coeff, *cccb);
137
41828
      clearBuffer();
138
    }
139
  }
140
141
82562
  if(Debug.isOn("matrix")) { printMatrix(); }
142
143
82562
  Assert(debugNoZeroCoefficients(newRow));
144
82562
  Assert(debugMatchingCountsForRow(newRow));
145
82562
  Assert(getColLength(basic) == 1);
146
82562
}
147
148
void Tableau::removeBasicRow(ArithVar basic){
149
  RowIndex rid = basicToRowIndex(basic);
150
151
  removeRow(rid);
152
  d_basic2RowIndex.remove(basic);
153
  d_rowIndex2basic.remove(rid);
154
}
155
156
void Tableau::substitutePlusTimesConstant(ArithVar to, ArithVar from, const Rational& mult,  CoefficientChangeCallback& cb){
157
  if(!mult.isZero()){
158
    RowIndex to_idx = basicToRowIndex(to);
159
    addEntry(to_idx, from, mult); // Add an entry to be cancelled out
160
    RowIndex from_idx = basicToRowIndex(from);
161
162
    cb.update(to_idx, from, 0, mult.sgn());
163
164
    loadRowIntoBuffer(from_idx);
165
    rowPlusBufferTimesConstant(to_idx, mult, cb);
166
    clearBuffer();
167
  }
168
}
169
170
uint32_t Tableau::rowComplexity(ArithVar basic) const{
171
  uint32_t complexity = 0;
172
  for(RowIterator i = basicRowIterator(basic); !i.atEnd(); ++i){
173
    const Entry& e = *i;
174
    complexity += e.getCoefficient().complexity();
175
  }
176
  return complexity;
177
}
178
179
double Tableau::avgRowComplexity() const{
180
  double sum = 0;
181
  uint32_t rows = 0;
182
  for(BasicIterator i = beginBasic(), i_end = endBasic(); i != i_end; ++i){
183
    sum += rowComplexity(*i);
184
    rows++;
185
  }
186
  return (rows == 0) ? 0 : (sum/rows);
187
}
188
189
void Tableau::printBasicRow(ArithVar basic, std::ostream& out){
190
  printRow(basicToRowIndex(basic), out);
191
}
192
193
}/* CVC4::theory::arith namespace */
194
}/* CVC4::theory namespace */
195
26685
}/* CVC4 namespace */