summaryrefslogtreecommitdiff
path: root/impl/main.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'impl/main.cpp')
-rw-r--r--impl/main.cpp58
1 files changed, 39 insertions, 19 deletions
diff --git a/impl/main.cpp b/impl/main.cpp
index c5a0be6..abd27ba 100644
--- a/impl/main.cpp
+++ b/impl/main.cpp
@@ -9,6 +9,7 @@
#include "Expression.hpp"
#include "MaxStrategy.hpp"
#include "EquationSystem.hpp"
+#include "Complete.hpp"
extern "C" {
#include "EquationSystemParser.h"
@@ -17,26 +18,24 @@ extern "C" {
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;
-
template<typename T>
-Expression<T>* treeToExpression(pANTLR3_BASE_TREE node, EquationSystem<T>& system) {
+Expression<T>* treeToExpression(pANTLR3_BASE_TREE node, EquationSystem<T>& system, bool topLevel=true) {
ANTLR3_UINT32 num = node->getChildCount(node);
string name = (char*) node->getText(node)->chars;
// leaf node - constant or variable
if (num == 0) {
- stringstream stream(name);
- T output;
- if (stream >> output) {
- return system.newExpression(new Constant<T>(output), vector<Expression<T>*>());
+ if (name == "inf") {
+ return system.newExpression(new Constant<T>(infinity<T>()));
} else {
- return system.newExpression(system.newVariable(name), vector<Expression<T>*>());
+ stringstream stream(name);
+ T output;
+ if (stream >> output) {
+ return system.newExpression(new Constant<T>(output));
+ } else {
+ return system.newExpression(system.newVariable(name));
+ }
}
}
@@ -45,7 +44,7 @@ Expression<T>* treeToExpression(pANTLR3_BASE_TREE node, EquationSystem<T>& syste
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));
+ args.push_back(treeToExpression(childNode, system, false));
}
if (name == "max") {
@@ -58,6 +57,13 @@ Expression<T>* treeToExpression(pANTLR3_BASE_TREE node, EquationSystem<T>& syste
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);
}
@@ -79,12 +85,24 @@ void treeToSystem(pANTLR3_BASE_TREE node, EquationSystem<T>& system) {
string varName = (char*) varNode->getText(varNode)->chars;
Variable<T>* var = system.newVariable(varName);
- system[*var] = treeToExpression(exprNode, system);
+ vector<Expression<T>*> args;
+ args.push_back(system.newExpression(new Constant<T>(-infinity<T>())));
+ args.push_back(treeToExpression(exprNode, system));
+ system[*var] = system.newMaxExpression(args);
}
}
-std::vector< Expression<float>* > empty;
+typedef Complete<int> ZBar;
int main (int argc, char* argv[]) {
+ FixpointAlgorithm<ZBar>* algorithm = NULL;
+ if (argc > 2 && !strcmp(argv[2], "naive")) {
+ algorithm = new NaiveFixpoint<ZBar>();
+ cout << "Naive fixpoint" << endl;
+ } else {
+ algorithm = new RecursiveFixpoint<ZBar>();
+ cout << "Recursive fixpoint" << endl;
+ }
+
pANTLR3_INPUT_STREAM input;
pEquationSystemLexer lex;
pANTLR3_COMMON_TOKEN_STREAM tokens;
@@ -97,12 +115,14 @@ int main (int argc, char* argv[]) {
EquationSystemParser_equation_system_return ret = parser -> equation_system(parser);
- EquationSystem<float> system;
- treeToSystem<float>(ret.tree, system);
+ EquationSystem<ZBar> system;
+ treeToSystem<ZBar>(ret.tree, system);
// DO MORE HERE
- VariableAssignment<float> rho = system.minFixpoint();
- const std::vector<Variable<float>*> vars = system.vars();
+ VariableAssignment<ZBar> rho = system.minFixpoint(*algorithm);
+ 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;
}