1 files changed, 90 insertions, 127 deletions

diff --git a/impl/main.cpp b/impl/main.cpp
index 2006565..6546444 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,124 +16,60 @@ extern "C" {
 using namespace std;
 
 template<typename T>
-std::pair<Expression<T>*, Expression<T>*> treeToExpression(pANTLR3_BASE_TREE node, EquationSystem<T>& system, bool negative=false) {
+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 - variable
   if (num == 0) {
-    if (negative) {
-      vector<Expression<T>*> firstArgs;
-      firstArgs.push_back(system.newExpression(system.newVariable(name + "_u")));
-      vector<Expression<T>*> secondArgs;
-      secondArgs.push_back(system.newExpression(system.newVariable(name + "_l")));
-      return std::pair<Expression<T>*, Expression<T>*>(
-          system.newExpression(new Negate<T>(),
-              firstArgs),
-          system.newExpression(new Negate<T>(),
-              secondArgs));
+    // leaf node -> constant or variable
+    if (name == "inf") {
+      return system.constant(infinity<T>());
     } else {
-      return std::pair<Expression<T>*, Expression<T>*>(
-          system.newExpression(system.newVariable(name + "_l")),
-          system.newExpression(system.newVariable(name + "_u")));
+      stringstream stream(name);
+      T output;
+      if (stream >> output) {
+        return system.constant(output);
+      } else {
+        return system.variable(name);
+      }
     }
   }
 
-  // a range itself
-  if (name == "RANGE") {
-    pANTLR3_BASE_TREE childNode;
-    string childName;
-    T firstValue, secondValue;
-
-    childNode = (pANTLR3_BASE_TREE) node->getChild(node, 0);
-    childName = (char*) childNode->getText(childNode)->chars;
-    stringstream firstStream(childName);
-    if (!(firstStream >> firstValue)) {
-      throw "Invalid number.";
-    }
-    string firstChildName = childName;
-
-    childNode = (pANTLR3_BASE_TREE) node->getChild(node, 1);
-    childName = (char*) childNode->getText(childNode)->chars;
-    stringstream secondStream(childName);
-    if (!(secondStream >> secondValue)) {
-      throw "Invalid number.";
-    }
-    string secondChildName = childName;
-
-    if (negative) {
-      T temp = firstValue;
-      string tempname = firstChildName;
-
-      firstValue = -secondValue;
-      firstChildName = "-" + secondChildName;
-
-      secondValue = -temp;
-      secondChildName = "-" + tempname;
-    }
-
-    return std::pair<Expression<T>*, Expression<T>*>(
-        system.newExpression(new Constant<T>(firstChildName, firstValue)),
-        system.newExpression(new Constant<T>(secondChildName, secondValue)));
-  }
-
-  if (name == "-") {
-    negative = true;
-  }
-
-  // subexpressions
-  std::vector<Expression<T>*> firstArgs;
-  std::vector<Expression<T>*> secondArgs;
+  // 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);
-    std::pair<Expression<T>*, Expression<T>*> expr = treeToExpression(childNode, system, negative);
-    firstArgs.push_back(expr.first);
-    secondArgs.push_back(expr.second);
-  }
-
-  // other operators
-  if (name == "-") {
-    //if (firstArgs.size() == 1) { // secondArgs.size() == firstArgs.size()
-    return std::pair<Expression<T>*, Expression<T>*>(
-        firstArgs[0],
-        secondArgs[0]);
+    args.push_back(&treeToExpression(childNode, system));
   }
 
   if (name == "max") {
-    return std::pair<Expression<T>*, Expression<T>*>(
-        system.newMaxExpression(firstArgs),
-        system.newMaxExpression(secondArgs));
+    return system.maxExpression(args);
   } else {
-    // we need two because expressions delete their operator
-    // bit of a silly design by me
-    Operator<T>* firstOp = NULL;
-    Operator<T>* secondOp = NULL;
+    Operator<T>* op = NULL;
     if (name == "min") {
-      firstOp = new Minimum<T>();
-      secondOp = new Minimum<T>();
+      op = new Minimum<T>();
     } else if (name == "+") {
-      firstOp = new Addition<T>();
-      secondOp = new Addition<T>();
+      op = new Addition<T>();
+    } else if (name == "-") {
+      if (args.size() == 1) {
+        op = new Negation<T>();
+      } else {
+        op = new Subtraction<T>();
+      }
     } else if (name == ";") {
-      firstOp = new Comma<T>();
-      secondOp = new Comma<T>();
+      op = new Comma<T>();
     } else if (name == "GUARD") {
-      firstOp = new Guard<T>();
-      secondOp = new Guard<T>();
+      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 std::pair<Expression<T>*, Expression<T>*>(
-        system.newExpression(firstOp, firstArgs),
-        system.newExpression(secondOp, secondArgs));
+    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)
@@ -148,36 +81,45 @@ void treeToSystem(pANTLR3_BASE_TREE node, EquationSystem<T>& system) {
     varNode = (pANTLR3_BASE_TREE) node->getChild(node, i);
     exprNode = (pANTLR3_BASE_TREE) node->getChild(node, i+1);
 
-    Variable<T>* var;
-    vector<Expression<T>*> args;
-
     string varName = (char*) varNode->getText(varNode)->chars;
-    std::pair<Expression<T>*, Expression<T>*> exprs = treeToExpression(exprNode, system);
-
-    var = system.newVariable(varName + "_l");
-    args.push_back(system.newExpression(new Constant<T>("-inf", -infinity<T>())));
-    args.push_back(exprs.first);
-    system[*var] = system.newMaxExpression(args);
-    std::cout << var->op_name << " = " << *system[*var] << std::endl;
-
-    args.clear();
-    var = system.newVariable(varName + "_u");
-    args.push_back(system.newExpression(new Constant<T>("-inf", -infinity<T>())));
-    args.push_back(exprs.second);
-    system[*var] = system.newMaxExpression(args);
-    std::cout << var->op_name << " = " << *system[*var] << std::endl;
+    Variable<T>& var = system.variable(varName);
+
+    vector<Expression<T>*> args;
+    args.push_back(&system.constant(-infinity<T>()));
+    args.push_back(&treeToExpression(exprNode, system));
+    system[var] = &system.maxExpression(args);
   }
 }
 
 typedef Complete<int> ZBar;
 int main (int argc, char* argv[]) {
+  if (argc <= 3) {
+    cout << "Usage: " << argv[0] << " filename naive|smart naive|repeat" << endl;
+    exit(1);
+  }
   FixpointAlgorithm<ZBar>* algorithm = NULL;
-  if (argc > 2 && !strcmp(argv[2], "naive")) {
-    algorithm = new NaiveFixpoint<ZBar>();
+  if (!strcmp(argv[2], "naive")) {
+    algorithm = new NaiveFixpointAlgorithm<ZBar>();
     cout << "Naive fixpoint" << endl;
+  } else if (!strcmp(argv[2], "smart")) {
+    algorithm = new SmartFixpointAlgorithm<ZBar>();
+    cout << "Smart fixpoint" << endl;
+  } else {
+    cout << "Unknown fixpoint algorithm." << endl;
+  }
+  MaxStrategy<ZBar>::ImprovementOperator* naiveImprovement = new MaxStrategy<ZBar>::NaiveImprovementOperator();
+  MaxStrategy<ZBar>::ImprovementOperator* improvement = NULL;
+  if (!strcmp(argv[3], "repeat")) {
+    improvement = new MaxStrategy<ZBar>::RepeatedImprovementOperator(*naiveImprovement);
+    cout << "Repeated strategy improvement" << endl;
+  } else if (!strcmp(argv[3], "naive")) {
+    improvement = naiveImprovement;
+    cout << "Naive strategy improvement" << endl;
   } else {
-    algorithm = new RecursiveFixpoint<ZBar>();
-    cout << "Recursive fixpoint" << endl;
+    cout << "Unknown strategy improvement algorithm." << endl;
+  }
+  if (!improvement || !algorithm) {
+    exit(1);
   }
 
   pANTLR3_INPUT_STREAM input;
@@ -192,18 +134,39 @@ 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>* result = NULL;
+  MaxStrategy<ZBar> strategy(system);
+  bool changed;
+  do {
+    if (result) delete result;
+    result = algorithm->maxFixpoint(strategy);
+    /*for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
+      Variable<ZBar>& var = system.variable(i);
+      cout << var.name() << " = " << (*result)[var] << ", ";
+    }
+    cout << endl;*/
+    changed = strategy.improve(*improvement, *result);
+  } while(changed);
+
+  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;
   }
 
+  delete result;
+  delete algorithm;
+  if (naiveImprovement != improvement)
+    delete improvement;
+  delete naiveImprovement;
+
   parser -> free(parser);
   tokens -> free(tokens);
   lex -> free(lex);