From ea05c9c5fa30b8822f618e861d12a09df1f8f017 Mon Sep 17 00:00:00 2001
From: Carlo Zancanaro <carlo@carlo-laptop>
Date: Mon, 28 May 2012 13:00:50 +1000
Subject: Fix memory error and x = max(-inf, expr) stuff.

---
 impl/main.cpp | 58 +++++++++++++++++++++++++++++++++++++++-------------------
 1 file changed, 39 insertions(+), 19 deletions(-)

(limited to 'impl/main.cpp')

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;
   }
-- 
cgit v1.2.3