GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/tableau.h Lines: 18 33 54.5 %
Date: 2021-03-22 Branches: 3 36 8.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file tableau.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, 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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "cvc4_private.h"
19
20
#pragma once
21
22
#include <vector>
23
24
#include "theory/arith/arithvar.h"
25
#include "theory/arith/matrix.h"
26
#include "util/dense_map.h"
27
#include "util/rational.h"
28
29
namespace CVC4 {
30
namespace theory {
31
namespace arith {
32
33
/**
34
 * A Tableau is a Rational matrix that keeps its rows in solved form.
35
 * Each row has a basic variable with coefficient -1 that is solved.
36
 * Tableau is optimized for pivoting.
37
 * The tableau should only be updated via pivot calls.
38
 */
39
17984
class Tableau : public Matrix<Rational> {
40
public:
41
private:
42
  typedef DenseMap<RowIndex> BasicToRowMap;
43
  // Set of all of the basic variables in the tableau.
44
  // ArithVarMap<RowIndex> : ArithVar |-> RowIndex
45
  BasicToRowMap d_basic2RowIndex;
46
47
  // RowIndex |-> Basic Variable
48
  typedef DenseMap<ArithVar> RowIndexToBasicMap;
49
  RowIndexToBasicMap d_rowIndex2basic;
50
51
public:
52
53
17990
  Tableau() : Matrix<Rational>(Rational(0)) {}
54
55
  typedef Matrix<Rational>::ColIterator ColIterator;
56
  typedef Matrix<Rational>::RowIterator RowIterator;
57
  typedef BasicToRowMap::const_iterator BasicIterator;
58
59
  typedef MatrixEntry<Rational> Entry;
60
61
19283881
  bool isBasic(ArithVar v) const{
62
19283881
    return d_basic2RowIndex.isKey(v);
63
  }
64
65
  void debugPrintIsBasic(ArithVar v) const {
66
    if(isBasic(v)){
67
      Warning() << v << " is basic." << std::endl;
68
    }else{
69
      Warning() << v << " is non-basic." << std::endl;
70
    }
71
  }
72
73
  BasicIterator beginBasic() const {
74
    return d_basic2RowIndex.begin();
75
  }
76
  BasicIterator endBasic() const {
77
    return d_basic2RowIndex.end();
78
  }
79
80
10643334
  RowIndex basicToRowIndex(ArithVar x) const {
81
10643334
    return d_basic2RowIndex[x];
82
  }
83
84
29914363
  ArithVar rowIndexToBasic(RowIndex rid) const {
85
29914363
    Assert(d_rowIndex2basic.isKey(rid));
86
29914363
    return d_rowIndex2basic[rid];
87
  }
88
89
6145632
  ColIterator colIterator(ArithVar x) const {
90
6145632
    return getColumn(x).begin();
91
  }
92
93
6557240
  RowIterator ridRowIterator(RowIndex rid) const {
94
6557240
    return getRow(rid).begin();
95
  }
96
97
621496
  RowIterator basicRowIterator(ArithVar basic) const {
98
621496
    return ridRowIterator(basicToRowIndex(basic));
99
  }
100
101
  const Entry& basicFindEntry(ArithVar basic, ArithVar col) const {
102
    return findEntry(basicToRowIndex(basic), col);
103
  }
104
105
  /**
106
   * Adds a row to the tableau.
107
   * The new row is equivalent to:
108
   *   basicVar = \f$\sum_i\f$ coeffs[i] * variables[i]
109
   * preconditions:
110
   *   basicVar is already declared to be basic
111
   *   basicVar does not have a row associated with it in the tableau.
112
   *
113
   * Note: each variables[i] does not have to be non-basic.
114
   * Pivoting will be mimicked if it is basic.
115
   */
116
  void addRow(ArithVar basicVar,
117
              const std::vector<Rational>& coeffs,
118
              const std::vector<ArithVar>& variables);
119
120
  /**
121
   * preconditions:
122
   *   x_r is basic,
123
   *   x_s is non-basic, and
124
   *   a_rs != 0.
125
   */
126
  void pivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCallback& cb);
127
128
  void removeBasicRow(ArithVar basic);
129
130
896141
  uint32_t basicRowLength(ArithVar basic) const{
131
896141
    RowIndex ridx = basicToRowIndex(basic);
132
896141
    return getRowLength(ridx);
133
  }
134
135
  /**
136
   *  to += mult * from
137
   * replacing from with its row.
138
   */
139
  void substitutePlusTimesConstant(ArithVar to, ArithVar from, const Rational& mult,  CoefficientChangeCallback& cb);
140
141
  void directlyAddToCoefficient(ArithVar rowVar, ArithVar col, const Rational& mult,  CoefficientChangeCallback& cb){
142
    RowIndex ridx = basicToRowIndex(rowVar);
143
    manipulateRowEntry(ridx, col, mult, cb);
144
  }
145
146
  /* Returns the complexity of a row in the tableau. */
147
  uint32_t rowComplexity(ArithVar basic) const;
148
149
  /* Returns the average complexity of the rows in the tableau. */
150
  double avgRowComplexity() const;
151
152
  void printBasicRow(ArithVar basic, std::ostream& out);
153
154
private:
155
  /* Changes the basic variable on the row for basicOld to basicNew. */
156
  void rowPivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCallback& cb);
157
158
};/* class Tableau */
159
160
161
162
}/* CVC4::theory::arith namespace */
163
}/* CVC4::theory namespace */
164
}/* CVC4 namespace */