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
|
#ifndef EQUATION_SYSTEM_HPP
#define EQUATION_SYSTEM_HPP
#include "Expression.hpp"
template<typename T>
struct MaxStrategy;
template<typename T>
struct EquationSystem {
virtual ~EquationSystem() {
for (int i = 0, size = _vars.size(); i < size; ++i) {
delete _vars[i];
}
}
Variable<T>* newVariable(const std::string&) {
_vars.push_back(new Variable<T>(_vars.size()));
return _vars[_vars.size()-1];
}
unsigned int varCount() const {
return _vars.size();
}
MaxExpression<T>* newMaxExpression(const std::vector<Expression<T>*>& args) {
MaxExpression<T>* expr = new MaxExpression<T>(args);
expr->id(_max_expressions.size());
_max_expressions.push_back(expr);
return expr;
}
unsigned int maxCount() const {
return _max_expressions.count();
}
const MaxExpression<T>* getMax(unsigned int i) const {
return _max_expressions[i];
}
MaxStrategy<T> strategy() const {
return MaxStrategy<T>(_max_expressions.size());
}
VariableAssignment<T> assignment() const {
return VariableAssignment<T>(_vars.size());
}
Expression<T>*& operator[] (const Variable<T>& v) {
if (_expressions.size() <= v.id()) {
_expressions.resize(v.id()+1);
}
return _expressions[v.id()];
}
const Expression<T>*& operator[] (const Variable<T>& v) const {
if (_expressions.size() <= v.id()) {
throw "Out of range";
}
return _expressions[v.id()];
}
template<typename F>
VariableAssignment<T> foreach(F op, const VariableAssignment<T>& rho) const {
VariableAssignment<T> result(_vars.size());
for (unsigned int i = 0, size = _vars.size(); i < size; ++i) {
result[*_vars[i]] = op(*_expressions[i], rho);
}
return result;
}
VariableAssignment<T> operator() (const VariableAssignment<T>& rho) const {
VariableAssignment<T> result(_vars.size());
for (unsigned int i = 0, size = _vars.size(); i < size; ++i) {
result[*_vars[i]] = (*_expressions[i])(rho);
}
return result;
}
VariableAssignment<T> maxFixpoint() const {
unsigned int size = _vars.size();
VariableAssignment<T> result(size, infinity<T>());
for (unsigned int i = 0; i < size; ++i) {
result = (*this)(result);
}
result = result.expand((*this)(result), -infinity<T>());
for (unsigned int i = 0; i < size-1; ++i) {
result = (*this)(result);
}
return result;
}
VariableAssignment<T> maxFixpoint(const MaxStrategy<T>& strat) const {
unsigned int size = _vars.size();
VariableAssignment<T> result(size, infinity<T>());
for (unsigned int i = 0; i < size; ++i) {
result = strat(*this, result);
}
result = result.expand(strat(*this, result), -infinity<T>());
for (unsigned int i = 0; i < size-1; ++i) {
result = strat(*this, result);
}
return result;
}
VariableAssignment<T> minFixpoint() const {
VariableAssignment<T> rho = assignment();
VariableAssignment<T> lastRho = assignment();
MaxStrategy<T> strat = strategy();
do {
lastRho = rho;
strat = strat.improve(*this, rho);
rho = maxFixpoint(strat);
} while(lastRho != rho);
return rho;
}
private:
std::vector<Variable<T>*> _vars;
std::vector<MaxExpression<T>*> _max_expressions;
std::vector<Expression<T>*> _expressions;
};
#include "MaxStrategy.hpp"
#endif
|
