diff options
author | Carlo Zancanaro <carlo@pc-4w14-0.cs.usyd.edu.au> | 2012-06-15 11:26:32 +1000 |
---|---|---|
committer | Carlo Zancanaro <carlo@pc-4w14-0.cs.usyd.edu.au> | 2012-06-15 11:26:32 +1000 |
commit | 5f3cb0bf02ed32976370cf6c7f656d000b4d7694 (patch) | |
tree | 2100c31e7b57d895592904b683954cc3e74838db /impl/main.cpp | |
parent | f09ce60d45d5524e36d07e76814b6e0cbc554288 (diff) |
Re-write heaps of code to work better.
Diffstat (limited to 'impl/main.cpp')
-rw-r--r-- | impl/main.cpp | 84 |
1 files changed, 50 insertions, 34 deletions
diff --git a/impl/main.cpp b/impl/main.cpp index 530556f..b03a4f2 100644 --- a/impl/main.cpp +++ b/impl/main.cpp @@ -1,15 +1,12 @@ #include <iostream> #include <vector> -#include <map> -#include <string> #include <sstream> -#include <math.h> - -#include "Operator.hpp" +#include "Complete.hpp" #include "Expression.hpp" -#include "MaxStrategy.hpp" +#include "Operator.hpp" #include "EquationSystem.hpp" -#include "Complete.hpp" +#include "MaxStrategy.hpp" +#include "FixpointAlgorithm.hpp" extern "C" { #include "EquationSystemParser.h" @@ -19,36 +16,35 @@ extern "C" { using namespace std; template<typename T> -Expression<T>* treeToExpression(pANTLR3_BASE_TREE node, EquationSystem<T>& system) { +Expression<T>& treeToExpression(pANTLR3_BASE_TREE node, ConcreteEquationSystem<T>& system) { ANTLR3_UINT32 num = node->getChildCount(node); - string name = (char*) node->getText(node)->chars; - // leaf node - constant or variable if (num == 0) { + // leaf node -> constant or variable if (name == "inf") { - return system.newExpression(new Constant<T>(infinity<T>())); + return system.constant(infinity<T>()); } else { stringstream stream(name); T output; if (stream >> output) { - return system.newExpression(new Constant<T>(output)); + return system.constant(output); } else { - return system.newExpression(system.newVariable(name)); + return system.variable(name); } } } - // other operators + // anything that's not a constant/variable 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)); + args.push_back(&treeToExpression(childNode, system)); } if (name == "max") { - return system.newMaxExpression(args); + return system.maxExpression(args); } else { Operator<T>* op = NULL; if (name == "min") { @@ -56,21 +52,24 @@ Expression<T>* treeToExpression(pANTLR3_BASE_TREE node, EquationSystem<T>& syste } else if (name == "+") { op = new Addition<T>(); } else if (name == "-") { - op = new Subtraction<T>(); + if (args.size() == 1) { + op = new Negation<T>(); + } else { + 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"; + throw "Parse error: Unknown operator"; } - return system.newExpression(op, args); + return system.expression(op, args); } } template<typename T> -void treeToSystem(pANTLR3_BASE_TREE node, EquationSystem<T>& system) { +void treeToSystem(pANTLR3_BASE_TREE node, ConcreteEquationSystem<T>& system) { ANTLR3_UINT32 num = node->getChildCount(node); if (num % 2 == 1) @@ -83,12 +82,12 @@ void treeToSystem(pANTLR3_BASE_TREE node, EquationSystem<T>& system) { exprNode = (pANTLR3_BASE_TREE) node->getChild(node, i+1); string varName = (char*) varNode->getText(varNode)->chars; - Variable<T>* var = system.newVariable(varName); + Variable<T>& var = system.variable(varName); 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); + args.push_back(&system.constant(-infinity<T>())); + args.push_back(&treeToExpression(exprNode, system)); + system[var] = &system.maxExpression(args); } } @@ -96,11 +95,11 @@ 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>(); + algorithm = new NaiveFixpointAlgorithm<ZBar>(); cout << "Naive fixpoint" << endl; } else { - algorithm = new RecursiveFixpoint<ZBar>(); - cout << "Recursive fixpoint" << endl; + algorithm = new SmartFixpointAlgorithm<ZBar>(); + cout << "Smart fixpoint" << endl; } pANTLR3_INPUT_STREAM input; @@ -115,16 +114,33 @@ int main (int argc, char* argv[]) { EquationSystemParser_equation_system_return ret = parser -> equation_system(parser); - EquationSystem<ZBar> system; + ConcreteEquationSystem<ZBar> system; treeToSystem<ZBar>(ret.tree, system); // DO MORE HERE - VariableAssignment<ZBar> rho = system.minFixpoint(*algorithm); - std::cout << rho << std::endl; + cout << system << endl; + VariableAssignment<ZBar>* prev = NULL; + VariableAssignment<ZBar>* result = system.assignment(-infinity<ZBar>()); + MaxStrategy<ZBar> strategy(system); + do { + if (prev) delete prev; + prev = result; + strategy.improve(*prev); + for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) { + Variable<ZBar>& var = system.variable(i); + cout << var.name() << " = " << (*result)[var] << ", "; + } + cout << endl; + result = algorithm->maxFixpoint(strategy); + } while(!system.equalAssignments(*prev, *result)); + if (prev) delete prev; + + VariableAssignment<ZBar>* rho = result; - 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; + cout << endl; + for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) { + Variable<ZBar>& var = system.variable(i); + cout << var.name() << " = " << (*rho)[var] << endl; } parser -> free(parser); |