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
|
#include <iostream>
#include <vector>
#include <math.h>
#include "Operator.hpp"
#include "Expression.hpp"
#include "MaxStrategy.hpp"
#include "EquationSystem.hpp"
using namespace std;
typedef std::vector<Expression<float>*> Args;
typedef Expression<float> E;
typedef Constant<float> C;
typedef Addition<float> A;
typedef Minimum<float> Min;
std::vector< Expression<float>* > empty;
int main () {
{
EquationSystem<float> sys;
Variable<float>* x = sys.newVariable("x");
Variable<float>* y = sys.newVariable("y");
Variable<float>* z = sys.newVariable("z");
Args xPlusArgs;
xPlusArgs.push_back(sys.newExpression(x, empty));
Args xMinArgs;
xMinArgs.push_back(sys.newExpression(new A(-1), xPlusArgs));
xMinArgs.push_back(sys.newExpression(y, empty));
Args xMaxArgs;
xMaxArgs.push_back(sys.newExpression(new C(0), empty));
xMaxArgs.push_back(sys.newExpression(new Min(), xMinArgs));
sys[*x] = sys.newMaxExpression(xMaxArgs);
// x = max(0, min(x-1, y))
Args yPlusArgs;
yPlusArgs.push_back(sys.newExpression(x, empty));
Args yMaxArgs;
yMaxArgs.push_back(sys.newExpression(new C(0), empty));
yMaxArgs.push_back(sys.newExpression(new A(5), yPlusArgs));
yMaxArgs.push_back(sys.newExpression(x, empty));
sys[*y] = sys.newMaxExpression(yMaxArgs);
// y = max(0, x+5, x)
Args zPlusArgs1;
zPlusArgs1.push_back(sys.newExpression(z, empty));
Args zPlusArgs2;
zPlusArgs2.push_back(sys.newExpression(x, empty));
Args zMaxArgs;
zMaxArgs.push_back(sys.newExpression(new C(0), empty));
zMaxArgs.push_back(sys.newExpression(new A(1), zPlusArgs1));
zMaxArgs.push_back(sys.newExpression(new A(0), zPlusArgs2));
sys[*z] = sys.newMaxExpression(zMaxArgs);
// z = max(0, z+1, x)
// x = max(0, min(x-1, y))
// y = max(0, x+5, x)
// z = max(0, z+1, x)
// => x: 0, y: 5, z: inf
VariableAssignment<float> fixpoint = sys.minFixpoint();
cout << "x = " << fixpoint[*x] << endl;
cout << "y = " << fixpoint[*y] << endl;
cout << "z = " << fixpoint[*z] << endl;
}
return 0;
}
|
