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);