summaryrefslogtreecommitdiff
path: root/impl/main.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'impl/main.cpp')
-rw-r--r--impl/main.cpp42
1 files changed, 26 insertions, 16 deletions
diff --git a/impl/main.cpp b/impl/main.cpp
index c5a0be6..0082686 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,12 +18,6 @@ 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) {
ANTLR3_UINT32 num = node->getChildCount(node);
@@ -31,12 +26,16 @@ Expression<T>* treeToExpression(pANTLR3_BASE_TREE node, EquationSystem<T>& syste
// 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>()), vector<Expression<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), vector<Expression<T>*>());
+ } else {
+ return system.newExpression(system.newVariable(name), vector<Expression<T>*>());
+ }
}
}
@@ -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);
}
@@ -83,7 +89,7 @@ void treeToSystem(pANTLR3_BASE_TREE node, EquationSystem<T>& system) {
}
}
-std::vector< Expression<float>* > empty;
+typedef Complete<int> ZBar;
int main (int argc, char* argv[]) {
pANTLR3_INPUT_STREAM input;
pEquationSystemLexer lex;
@@ -97,12 +103,16 @@ 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(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;
}