Fix issues with some things ignoring strategies.

8 files changed, 39 insertions, 45 deletions

diff --git a/impl/EquationSystem.hpp b/impl/EquationSystem.hpp
index 772ac37..13319e0 100644
--- a/impl/EquationSystem.hpp
+++ b/impl/EquationSystem.hpp
@@ -119,7 +119,7 @@ struct EquationSystem {
 
   VariableAssignment<T> minFixpoint(const FixpointAlgorithm<T>& algo) const {
     VariableAssignment<T> rho = assignment();
-    VariableAssignment<T> lastRho = assignment();
+    VariableAssignment<T> lastRho(0);
     MaxStrategy<T> strat = strategy();
     do {
       lastRho = rho;
diff --git a/impl/Expression.hpp b/impl/Expression.hpp
index 4798e60..d3dfcf3 100644
--- a/impl/Expression.hpp
+++ b/impl/Expression.hpp
@@ -7,6 +7,8 @@
 
 template<typename T>
 struct Variable;
+template<typename T>
+struct MaxStrategy;
 
 int ExpressionCount;
 
@@ -22,9 +24,6 @@ struct Expression {
   virtual T operator() (const VariableAssignment<T>& assignment) const {
     return (*_operator)(_arguments, assignment);
   }
-  virtual T operator() (const VariableAssignment<T>& assignment, VariableSet<T>* visited) const {
-    return (*_operator)(_arguments, assignment, visited);
-  }
   protected:
   Operator<T>* _operator;
   std::vector< Expression<T>* > _arguments;
@@ -46,14 +45,17 @@ struct MaxExpression : public Expression<T> {
     }
     return Expression<T>::_arguments[i];
   }
-  std::pair<T, unsigned int> bestStrategy(const VariableAssignment<T>& rho) const {
+  virtual T operator() (const VariableAssignment<T>& assignment) const {
+    throw "error";
+  }
+  std::pair<T, unsigned int> bestStrategy(const VariableAssignment<T>& rho, const MaxStrategy<T>& strat) const {
     std::pair<T, unsigned int> best = std::pair<T, unsigned int>(-infinity<T>(), 0);
     for (unsigned int i = 0, size = Expression<T>::_arguments.size(); i < size; ++i) {
-      T value = (*Expression<T>::_arguments[i])(rho);
+      T value = strat(*Expression<T>::_arguments[i], rho);
       if (value > best.first)
         best = std::pair<T, unsigned int>(value, i);
     }
-    std::cerr << "Best strategy: (" << best.first << ", " << best.second << ")" << std::endl;
+    std::cerr << "Best strategy: (" << best.first << ", " << best.second << ")" << std::endl << std::endl;
     return best;
   }
   private:
@@ -61,5 +63,6 @@ struct MaxExpression : public Expression<T> {
 };
 
 #include "Variable.hpp"
+#include "MaxStrategy.hpp"
 
 #endif
diff --git a/impl/MaxStrategy.hpp b/impl/MaxStrategy.hpp
index a1c50d8..aa49c9d 100644
--- a/impl/MaxStrategy.hpp
+++ b/impl/MaxStrategy.hpp
@@ -59,7 +59,7 @@ struct MaxStrategy {
     if (max == NULL) {
       return expr(rho);
     } else {
-      return (*max->argument(_assignment[max->id()]))(rho);
+      return (*this)(*max->argument(_assignment[max->id()]), rho);
     }
   }
   MaxStrategy<T> improve(const EquationSystem<T>& s, const VariableAssignment<T>& rho) const {
@@ -67,16 +67,15 @@ struct MaxStrategy {
     for (unsigned int i = 0; i < _length; ++i) {
       const MaxExpression<T>& expr = *s.getMax(i);
       const T oldValue = (*this)(expr, rho);
-      std::pair<const T,unsigned int> best = expr.bestStrategy(rho);
+
+      // this relies on the fact that deeper MaxExpressions have a lower id
+      // than the MaxExpressions containing them. This means that we know that
+      // we have enough of a strategy to work with what we have within us
+      std::pair<const T,unsigned int> best = expr.bestStrategy(rho, newStrategy);
+
       if (best.first > oldValue)
         newStrategy[expr] = best.second;
     }
-    std::cerr << "Strat improvement: ";
-    if (_length > 0)
-      std::cerr << newStrategy[*s.getMax(0)];
-    else
-      std::cerr << "no max expressions";
-    std::cerr << std::endl;
     return newStrategy;
   }
 
diff --git a/impl/Operator.hpp b/impl/Operator.hpp
index 80bc8b2..5f7cd1e 100644
--- a/impl/Operator.hpp
+++ b/impl/Operator.hpp
@@ -13,8 +13,6 @@ float infinity() {
 
 template<typename T>
 struct Variable;
-template<typename T>
-struct VariableSet : public IdSet<const Variable<T> > {};
 
 template<typename T>
 struct VariableAssignment;
@@ -24,35 +22,32 @@ struct Expression;
 template<typename T>
 struct Operator {
   virtual ~Operator() { }
-  T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& rho) const {
-    return (*this)(args, rho, (VariableSet<T>*) NULL);
-  }
-  virtual T operator() (const std::vector< Expression<T>* >&, const VariableAssignment<T>&, VariableSet<T>*) const = 0;
+  virtual T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& rho) const = 0;
 };
 template<typename T>
 struct Maximum : public Operator<T> {
-  virtual T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& assignment, VariableSet<T>* visited) const {
+  virtual T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& assignment) const {
     T value = -infinity<T>();
     for (typename std::vector< Expression<T>* >::const_iterator it = args.begin();
          it != args.end();
          ++it) {
-      T temporary = (**it)(assignment, visited);
-      value = (temporary < value ? value : temporary);
-      if (value == infinity<T>()) break;
+      T temporary = (**it)(assignment);
+      value = (temporary > value ? temporary : value);
+      //if (value == infinity<T>()) break;
     }
     return value;
   }
 };
 template<typename T>
 struct Minimum : public Operator<T> {
-  virtual T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& assignment, VariableSet<T>* visited) const {
+  virtual T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& assignment) const {
     T value = infinity<T>();
     for (typename std::vector< Expression<T>* >::const_iterator it = args.begin();
          it != args.end();
          ++it) {
-      T temporary = (**it)(assignment, visited);
+      T temporary = (**it)(assignment);
       value = (temporary < value ? temporary : value);
-      if (value == -infinity<T>()) break;
+      //if (value == -infinity<T>()) break;
     }
     return value;
   }
@@ -62,7 +57,7 @@ template<typename T>
 struct Constant : public Operator<T> {
   Constant(const T& val)
     : _value(val) { }
-  T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& ass, VariableSet<T>*) const {
+  T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& ass) const {
     return _value;
   }
   private:
@@ -71,10 +66,10 @@ struct Constant : public Operator<T> {
 
 template<typename T>
 struct Addition: public Operator<T> {
-  T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& ass, VariableSet<T>* visited) const {
+  T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& ass) const {
     T sum = (*args[0])(ass);
     for (unsigned int i = 1, size = args.size(); i < size; ++i) {
-      sum += (*args[i])(ass, visited);
+      sum += (*args[i])(ass);
     }
     return sum;
   }
@@ -82,10 +77,10 @@ struct Addition: public Operator<T> {
 
 template<typename T>
 struct Subtraction: public Operator<T> {
-  T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& ass, VariableSet<T>* visited) const {
+  T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& ass) const {
     T sum = (*args[0])(ass);
     for (unsigned int i = 1, size = args.size(); i < size; ++i) {
-      sum -= (*args[i])(ass, visited);
+      sum -= (*args[i])(ass);
     }
     return sum;
   }
@@ -93,24 +88,24 @@ struct Subtraction: public Operator<T> {
 
 template<typename T>
 struct Comma: public Operator<T> {
-  T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& ass, VariableSet<T>* visited) const {
-    if ((*args[0])(ass, visited) == -infinity<T>()) {
+  T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& ass) const {
+    if ((*args[0])(ass) == -infinity<T>()) {
       std::cout << "Comma - neg inf" << std::endl;
       return -infinity<T>();
     } else {
       std::cout << "Comma - finite" << std::endl;
-      return (*args[1])(ass, visited);
+      return (*args[1])(ass);
     }
   }
 };
 
 template<typename T>
 struct Guard: public Operator<T> {
-  T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& ass, VariableSet<T>* visited) const {
-    if ((*args[0])(ass, visited) < (*args[1])(ass, visited)) {
+  T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& ass) const {
+    if ((*args[0])(ass) < (*args[1])(ass)) {
       return -infinity<T>();
     } else {
-      return (*args[2])(ass, visited);
+      return (*args[2])(ass);
     }
   }
 };
diff --git a/impl/Variable.hpp b/impl/Variable.hpp
index 5ebbbed..a174ea8 100644
--- a/impl/Variable.hpp
+++ b/impl/Variable.hpp
@@ -17,10 +17,8 @@ struct Variable : public Operator<T> {
     return _name;
   }
   //T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& ass) const {
-  virtual T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& assignment, VariableSet<T>* visited) const {
+  virtual T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& assignment) const {
     //assert(args.size() == 0)
-    if (visited != NULL)
-      visited->insert(*this);
     return assignment[*this];
   }
   private:
diff --git a/impl/main.cpp b/impl/main.cpp
index abd27ba..530556f 100644
--- a/impl/main.cpp
+++ b/impl/main.cpp
@@ -19,7 +19,7 @@ extern "C" {
 using namespace std;
 
 template<typename T>
-Expression<T>* treeToExpression(pANTLR3_BASE_TREE node, EquationSystem<T>& system, bool topLevel=true) {
+Expression<T>* treeToExpression(pANTLR3_BASE_TREE node, EquationSystem<T>& system) {
   ANTLR3_UINT32 num = node->getChildCount(node);
 
   string name = (char*) node->getText(node)->chars;
@@ -44,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, false));
+    args.push_back(treeToExpression(childNode, system));
   }
 
   if (name == "max") {
diff --git a/impl/systems/.long-fixpoint.swp b/impl/systems/.long-fixpoint.swp
deleted file mode 100644
index 726d6ce..0000000
--- a/impl/systems/.long-fixpoint.swp
+++ /dev/null
diff --git a/impl/systems/long-fixpoint b/impl/systems/long-fixpoint
index f56b700..5838910 100644
--- a/impl/systems/long-fixpoint
+++ b/impl/systems/long-fixpoint
@@ -98,7 +98,6 @@ x96 = x95
 x97 = x96
 x98 = x97
 x99 = x98
-<<<<<<< HEAD
 x100 = x99
 x101 = x100
 x102 = x101