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
122
123
124
125
126
|
#include <iostream>
#include <vector>
#include <map>
#include <string>
#include <sstream>
#include <math.h>
#include "Operator.hpp"
#include "Expression.hpp"
#include "MaxStrategy.hpp"
#include "EquationSystem.hpp"
#include "Complete.hpp"
extern "C" {
#include "EquationSystemParser.h"
#include "EquationSystemLexer.h"
}
using namespace std;
template<typename T>
Expression<T>* treeToExpression(pANTLR3_BASE_TREE node, EquationSystem<T>& system) {
ANTLR3_UINT32 num = node->getChildCount(node);
string name = (char*) node->getText(node)->chars;
// leaf node - constant or variable
if (num == 0) {
if (name == "inf") {
return system.newExpression(new Constant<T>(infinity<T>()), vector<Expression<T>*>());
} else {
stringstream stream(name);
T output;
if (stream >> output) {
return system.newExpression(new Constant<T>(output), vector<Expression<T>*>());
} else {
return system.newExpression(system.newVariable(name), vector<Expression<T>*>());
}
}
}
// other operators
std::vector<Expression<T>*> args;
pANTLR3_BASE_TREE childNode;
for (unsigned int i = 0; i < num; ++i) {
childNode = (pANTLR3_BASE_TREE) node->getChild(node, i);
args.push_back(treeToExpression(childNode, system));
}
if (name == "max") {
return system.newMaxExpression(args);
} else {
Operator<T>* op = NULL;
if (name == "min") {
op = new Minimum<T>();
} else if (name == "+") {
op = new Addition<T>();
} else if (name == "-") {
op = new Subtraction<T>();
} else if (name == ";") {
op = new Comma<T>();
} else if (name == "GUARD") {
op = new Guard<T>();
} else {
std::cerr << "Unknown leaf node type: " << name << std::endl;
throw "Unknown leaf node type";
}
return system.newExpression(op, args);
}
}
template<typename T>
void treeToSystem(pANTLR3_BASE_TREE node, EquationSystem<T>& system) {
ANTLR3_UINT32 num = node->getChildCount(node);
if (num % 2 == 1)
throw "Big problem here.";
pANTLR3_BASE_TREE varNode;
pANTLR3_BASE_TREE exprNode;
for (unsigned int i = 0; i < num; i += 2) {
varNode = (pANTLR3_BASE_TREE) node->getChild(node, i);
exprNode = (pANTLR3_BASE_TREE) node->getChild(node, i+1);
string varName = (char*) varNode->getText(varNode)->chars;
Variable<T>* var = system.newVariable(varName);
system[*var] = treeToExpression(exprNode, system);
}
}
typedef Complete<int> ZBar;
int main (int argc, char* argv[]) {
pANTLR3_INPUT_STREAM input;
pEquationSystemLexer lex;
pANTLR3_COMMON_TOKEN_STREAM tokens;
pEquationSystemParser parser;
input = antlr3FileStreamNew((pANTLR3_UINT8)argv[1], ANTLR3_ENC_8BIT);
lex = EquationSystemLexerNew(input);
tokens = antlr3CommonTokenStreamSourceNew(ANTLR3_SIZE_HINT, TOKENSOURCE(lex));
parser = EquationSystemParserNew(tokens);
EquationSystemParser_equation_system_return ret = parser -> equation_system(parser);
EquationSystem<ZBar> system;
treeToSystem<ZBar>(ret.tree, system);
// DO MORE HERE
VariableAssignment<ZBar> rho = system.minFixpoint(NaiveFixpoint<ZBar>());
std::cout << rho << std::endl;
rho = system.minFixpoint(RecursiveFixpoint<ZBar>());
std::cout << rho << std::endl;
const std::vector<Variable<ZBar>*> vars = system.vars();
for (unsigned int i = 0, size = vars.size(); i < size; ++i) {
cout << vars[i]->name() << " = " << rho[*vars[i]] << endl;
}
parser -> free(parser);
tokens -> free(tokens);
lex -> free(lex);
input -> close(input);
return 0;
}
|
