blob: 433f6472f1bd9da0d47cc7c1cbded7ee2363da6f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
|
/********************* */
/*! \file tableau.h
** \verbatim
** Original author: taking
** Major contributors: mdeters
** Minor contributors (to current version): dejan
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief [[ Add one-line brief description here ]]
**
** [[ Add lengthier description here ]]
** \todo document this file
**/
#include "expr/node.h"
#include "expr/attribute.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/arithvar_set.h"
#include "theory/arith/normal_form.h"
#include "theory/arith/row_vector.h"
#include <ext/hash_map>
#include <set>
#ifndef __CVC4__THEORY__ARITH__TABLEAU_H
#define __CVC4__THEORY__ARITH__TABLEAU_H
namespace CVC4 {
namespace theory {
namespace arith {
class Tableau {
private:
typedef std::vector< ReducedRowVector* > RowsTable;
ArithVarSet d_activeBasicVars;
RowsTable d_rowsTable;
ArithVarSet& d_basicManager;
std::vector<uint32_t> d_rowCount;
public:
/**
* Constructs an empty tableau.
*/
Tableau(ArithVarSet& bm) :
d_activeBasicVars(),
d_rowsTable(),
d_basicManager(bm)
{}
~Tableau();
void increaseSize(){
d_activeBasicVars.increaseSize();
d_rowsTable.push_back(NULL);
d_rowCount.push_back(0);
}
ArithVarSet::iterator begin(){
return d_activeBasicVars.begin();
}
ArithVarSet::iterator end(){
return d_activeBasicVars.end();
}
ReducedRowVector& lookup(ArithVar var){
Assert(d_activeBasicVars.isMember(var));
Assert(d_rowsTable[var] != NULL);
return *(d_rowsTable[var]);
}
public:
uint32_t getRowCount(ArithVar x){
Assert(x < d_rowCount.size());
return d_rowCount[x];
}
/**
* Adds a row to the tableau.
* The new row is equivalent to:
* basicVar = \sum_i coeffs[i] * variables[i]
* preconditions:
* basicVar is already declared to be basic
* basicVar does not have a row associated with it in the tableau.
*
* Note: each variables[i] does not have to be non-basic.
* Pivoting will be mimicked if it is basic.
*/
void addRow(ArithVar basicVar,
const std::vector<Rational>& coeffs,
const std::vector<ArithVar>& variables);
/**
* preconditions:
* x_r is basic,
* x_s is non-basic, and
* a_rs != 0.
*/
void pivot(ArithVar x_r, ArithVar x_s);
void printTableau();
ReducedRowVector* removeRow(ArithVar basic);
};
}; /* namespace arith */
}; /* namespace theory */
}; /* namespace CVC4 */
#endif /* __CVC4__THEORY__ARITH__TABLEAU_H */
|
