14 files changed, 298 insertions, 339 deletions

diff --git a/.gitignore b/.gitignore
index 0173d7a..93c639b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,14 +1,3 @@
 /impl/build/*
 /impl/parser/*
-*.log
-*.dvi
-*.ps
-*.aux
-*.blg
-*.bbl
-*.toc
-*.lof
-*.lot
-*.out
-*~
 gmon.out
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp
index f4026dd..57dcdeb 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp
@@ -10,9 +10,6 @@ template<typename Domain>
 struct MaxStrategy {
   virtual ~MaxStrategy() { }
   virtual unsigned int get(const MaxExpression<Domain>& e) const = 0;
-  virtual unsigned int get(const MaxExpression<Domain>& e) {
-    return const_cast<const MaxStrategy*>(this)->get(e);
-  }
 };
 
 unsigned int stack_depth = 1;
@@ -41,38 +38,20 @@ struct DynamicMaxStrategy : public MaxStrategy<Domain> {
       _influence(system.maxExpressionCount(),
                  IdSet<MaxExpression<Domain> >(system.maxExpressionCount())),
       _var_influence(system.variableCount(),
-                     IdSet<MaxExpression<Domain> >(system.maxExpressionCount())),
-      _frozen(false)
+                     IdSet<MaxExpression<Domain> >(system.maxExpressionCount()))
   {}
 
-  void freeze() {
-    _frozen = true;
-  }
-
-  void thaw() {
-    _frozen = false;
-  }
-
-  bool is_frozen() {
-    return _frozen;
-  }
-
   void setRho(DynamicVariableAssignment<Domain>& rho) {
     _rho = &rho;
   }
 
   unsigned int get(const MaxExpression<Domain>& e) const {
+    solve(e);
     return _values[e];
   }
 
-  unsigned int get(const MaxExpression<Domain>& e) {
-    if (!_frozen)
-      solve(e);
-    return _values[e];
-  }
-
-  void invalidate(const Variable<Domain>& v) {
-    log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl; 
+  void invalidate(const Variable<Domain>& v) const {
+    solver_log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl;
     _stable.filter(_var_influence[v]);
 
     IdSet<MaxExpression<Domain> > infl = _var_influence[v];
@@ -88,10 +67,10 @@ struct DynamicMaxStrategy : public MaxStrategy<Domain> {
   }
 
 private:
-  void solve(const MaxExpression<Domain>& x) {
+  void solve(const MaxExpression<Domain>& x) const {
     if (!_stable.contains(x)) {
       _stable.insert(x);
-      log::strategy << indent() << "Stabilise " << x << std::endl;
+      solver_log::strategy << indent() << "Stabilise " << x << std::endl;
 
       stack_depth++;
       unsigned int val = x.bestStrategy(DependencyAssignment(*this, *_rho, x),
@@ -99,7 +78,7 @@ private:
       stack_depth--;
 
       if (val != _values[x]) {
-        log::strategy << x << " => " << *x.arguments()[val] << std::endl;
+        solver_log::strategy << x << " => " << *x.arguments()[val] << std::endl;
 
         IdSet<MaxExpression<Domain> > oldInfluence = _influence[x];
         _influence[x].clear();
@@ -117,17 +96,15 @@ private:
           solve(_system.maxExpression(*it));
         }
       } else {
-        log::strategy << indent() << x << " did not change: "
-		      << x << " => " << *x.arguments()[val] << std::endl;
+        solver_log::strategy << indent() << x << " did not change" << std::endl;
       }
     } else {
-      log::strategy << indent() << x << " is stable: "
-		    << x << " => " << *x.arguments()[_values[x]] << std::endl;
+      solver_log::strategy << indent() << x << " is stable" << std::endl;
     }
   }
 
   struct DependencyAssignment : public VariableAssignment<Domain>{
-    DependencyAssignment(DynamicMaxStrategy& strat,
+    DependencyAssignment(const DynamicMaxStrategy& strat,
                          VariableAssignment<Domain>& rho,
                          const MaxExpression<Domain>& expr)
       : _strat(strat),
@@ -139,13 +116,13 @@ private:
       return _rho[var];
     }
   private:
-    DynamicMaxStrategy& _strat;
+    const DynamicMaxStrategy& _strat;
     VariableAssignment<Domain>& _rho;
     const MaxExpression<Domain>& _expr;
   };
 
   struct DependencyStrategy : public MaxStrategy<Domain> {
-    DependencyStrategy(DynamicMaxStrategy& strat, const MaxExpression<Domain>& expr)
+    DependencyStrategy(const DynamicMaxStrategy& strat, const MaxExpression<Domain>& expr)
       : _strat(strat),
         _expr(expr) {
     }
@@ -157,57 +134,19 @@ private:
       return _strat._values[e];
     }
   private:
-    DynamicMaxStrategy& _strat;
+    const DynamicMaxStrategy& _strat;
     const MaxExpression<Domain>& _expr;
   };
 
-private: 
+private:
   const EquationSystem<Domain>& _system;
-  DynamicVariableAssignment<Domain>* _rho;
-  IdMap<MaxExpression<Domain>,unsigned int> _values;
-  IdSet<MaxExpression<Domain> > _stable;
-  IdMap<MaxExpression<Domain>,IdSet<MaxExpression<Domain> > > _influence;
-  IdMap<Variable<Domain>,IdSet<MaxExpression<Domain> > > _var_influence;
-  bool _frozen;
+  mutable DynamicVariableAssignment<Domain>* _rho;
+  mutable IdMap<MaxExpression<Domain>,unsigned int> _values;
+  mutable IdSet<MaxExpression<Domain> > _stable;
+  mutable IdMap<MaxExpression<Domain>,IdSet<MaxExpression<Domain> > > _influence;
+  mutable IdMap<Variable<Domain>,IdSet<MaxExpression<Domain> > > _var_influence;
 };
 
-
-template<typename T>
-IdMap<Variable<T>,T> solve_for(const EquationSystem<T>& system) {
-  IdMap<Variable<T>,T> result(system.variableCount(), infinity<T>());
-
-  DynamicMaxStrategy<T> strategy(system);
-  DynamicVariableAssignment<T> rho(system, strategy, -infinity<T>());
-  strategy.setRho(rho);
-
-  bool changed;
-  do {
-    changed = false;
-
-    // improve strategy
-    rho.freeze();
-    strategy.thaw();
-    for (unsigned int i = 0; i < system.variableCount(); ++i) {
-      strategy.get(*system[system.variable(i)]);
-    }
-
-    // iterate fixpoint
-    strategy.freeze();
-    rho.thaw();
-    for (unsigned int i = 0; i < system.variableCount(); ++i) {
-      Variable<T>& var = system.variable(i);
-      T val = rho[var];
-      if (result[var] != val) {
-	result[var] = val;
-	changed = true;
-      }
-    }
-  } while(changed);
-
-  return result;
-}
-
-
 /*template<typename Domain>
 std::ostream& operator<<(std::ostream& cout, const MaxStrategy<Domain>& strat) {
   strat.print(cout);
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp
index 2a63756..ba5f650 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp
@@ -8,9 +8,6 @@ template<typename Domain>
 struct VariableAssignment {
   virtual ~VariableAssignment() { }
   virtual const Domain& operator[](const Variable<Domain>&) const = 0;
-  virtual const Domain& operator[](const Variable<Domain>& x) {
-    return (*const_cast<const VariableAssignment*>(this))[x];
-  }
 };
 
 #include "EquationSystem.hpp"
@@ -22,71 +19,46 @@ template<typename Domain>
 struct DynamicVariableAssignment : public VariableAssignment<Domain> {
   DynamicVariableAssignment(
     const EquationSystem<Domain>& system,
-    DynamicMaxStrategy<Domain>& strat,
-    const Domain& value=infinity<Domain>()
+    const DynamicMaxStrategy<Domain>& strat
   ) : _system(system),
       _strategy(strat),
-      _values(system.variableCount(), value),
+      _values(system.variableCount(), infinity<Domain>()),
       _stable(system.variableCount()),
       _influence(system.variableCount(),
-                 IdSet<Variable<Domain> >(system.variableCount())),
-      _frozen(false)
+                 IdSet<Variable<Domain> >(system.variableCount()))
   { }
 
-  void freeze() {
-    _frozen = true;
-  }
-
-  void thaw() {
-    _frozen = false;
-  }
-
-  bool is_frozen() {
-    return _frozen;
-  }
-
   const Domain& operator[](const Variable<Domain>& var) const {
+    solve(var);
     return _values[var];
   }
 
-  const Domain& operator[](const Variable<Domain>& var) {
-    if (!_frozen)
-      solve(var);
-    return _values[var];
-  }
-
-  void invalidate(const Variable<Domain>& x) {
-    log::fixpoint << indent() << "Invalidating " << x << std::endl;
+  void invalidate(const Variable<Domain>& x) const {
+    solver_log::fixpoint << indent() << "Invalidating " << x << std::endl;
     if (_stable.contains(x)) {
       _stable.remove(x);
       _values[x] = infinity<Domain>();
-     
-      IdSet<Variable<Domain> > infl = _influence[x];
-      _influence[x].clear();
-      for (typename IdSet<Variable<Domain> >::iterator
-	     it = infl.begin(),
-	     ei = infl.end();
-	   it != ei;
-	   ++it) {
-	invalidate(_system.variable(*it));
-      }
+      
+      solve(x);
     }
   }
 
 private:
 
-  void solve(const Variable<Domain>& x) {
+  void solve(const Variable<Domain>& x) const {
     if (!_stable.contains(x)) {
       _stable.insert(x);
-      log::fixpoint << indent() << "Stabilise " << x << std::endl;
+      solver_log::fixpoint << indent() << "Stabilise " << x << std::endl;
 
       stack_depth++;
-      Domain val = _system[x]->eval(DependencyAssignment(*this, x),
-                                    _strategy);
+      if (!_system[x])
+        return;
+      Domain val = _system[x]->evalWithStrat(DependencyAssignment(*this, x),
+					     _strategy);
       stack_depth--;
 
       if (val != _values[x]) {
-        log::fixpoint << x << " = " << val << std::endl;
+        solver_log::fixpoint << x << " = " << val << std::endl;
 
         IdSet<Variable<Domain> > oldInfluence = _influence[x];
         _influence[x].clear();
@@ -102,17 +74,15 @@ private:
           solve(_system.variable(*it));
         }
       } else {
-        log::fixpoint << indent() << x << " did not change: "
-		      << x << " = " << val << std::endl;
+        solver_log::fixpoint << indent() << x << " did not change" << std::endl;
       }
     } else {
-      log::fixpoint << indent() << x << " is stable: "
-		    << x << " = " << _values[x] << std::endl;
+      solver_log::fixpoint << indent() << x << " is stable" << std::endl;
     }
   }
 
   struct DependencyAssignment : public VariableAssignment<Domain> {
-    DependencyAssignment(DynamicVariableAssignment& assignment, const Variable<Domain>& var)
+    DependencyAssignment(const DynamicVariableAssignment& assignment, const Variable<Domain>& var)
       : _assignment(assignment), _var(var) { }
     const Domain& operator[](const Variable<Domain>& x) const {
       const Domain& result = _assignment[x];
@@ -120,16 +90,15 @@ private:
       return result;
     }
   private:
-    DynamicVariableAssignment& _assignment;
+    const DynamicVariableAssignment& _assignment;
     const Variable<Domain>& _var;
   };
 
   const EquationSystem<Domain>& _system;
-  DynamicMaxStrategy<Domain>& _strategy;
-  IdMap<Variable<Domain>, Domain> _values;
-  IdSet<Variable<Domain> > _stable;
-  IdMap<Variable<Domain>,IdSet<Variable<Domain> > > _influence;
-  bool _frozen;
+  const DynamicMaxStrategy<Domain>& _strategy;
+  mutable IdMap<Variable<Domain>, Domain> _values;
+  mutable IdSet<Variable<Domain> > _stable;
+  mutable IdMap<Variable<Domain>,IdSet<Variable<Domain> > > _influence;
 };
 
 #endif
diff --git a/clang/lib/Analysis/Interval.cpp b/clang/lib/Analysis/Interval.cpp
index d005048..ac96107 100644
--- a/clang/lib/Analysis/Interval.cpp
+++ b/clang/lib/Analysis/Interval.cpp
@@ -702,24 +702,40 @@ void IntervalAnalysis::runOnAllBlocks() {
     }
   }
 
+  std::vector<EqnExpr*> a;
+
+  a.push_back(&system.constant(-infinity<ZBar>()));
+  a.push_back(&system.constant(0));
+  system[system.variable("x")] = &system.maxExpression(a);
+  a.clear();
+  
+  system.variable("y");
+
+  a.push_back(&system.variable("x"));
+  a.push_back(&system.variable("z"));
+  EqnExpr* minExpr = &system.expression(new Maximum<ZBar>(), a);
+  a.clear();
+
+  a.push_back(&system.constant(-infinity<ZBar>()));
+  a.push_back(minExpr);
+  system[system.variable("y")] = &system.maxExpression(a);
+  a.clear();
+
+  a.push_back(&system.constant(-infinity<ZBar>()));
+  a.push_back(&system.variable("y"));
+  system[system.variable("z")] = &system.maxExpression(a);
+
+  llvm::errs() << toString(system) << "\n";
+
   system.indexMaxExpressions();
+  DynamicMaxStrategy<ZBar> strategy(system);
+  DynamicVariableAssignment<ZBar> rho(system, strategy);
+  strategy.setRho(rho);
 
-  IdMap<EqnVar,ZBar> result = solve_for(system);
   for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
-    EqnVar& var = system.variable(i);
-    cout << var.name() << " = " << result[var] << endl;
-  }
-
-  /*
-    DynamicMaxStrategy<ZBar> strategy(system);
-    DynamicVariableAssignment<ZBar> rho(system, strategy);
-    strategy.setRho(rho);
-    
-    for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
     EqnVar& var = system.variable(size - i - 1);
     llvm::errs() << toString(var.name()) << " = " << toString(rho[var]) << "\n";
-    }
-  */
+  }
 }
 
 
diff --git a/impl/Complete.hpp b/impl/Complete.hpp
index 336ab24..e3ec15a 100644
--- a/impl/Complete.hpp
+++ b/impl/Complete.hpp
@@ -7,38 +7,23 @@
 
 template<typename T>
 T infinity() { }
-template<typename T>
-T unknown(const T&) { }
 
 template<typename T>
 struct Complete {
   Complete()
-    : _value(0), _infinity(false), _unknown(false) { }
+    : _value(0), _infinity(false) { }
   Complete(const T& value)
-    : _value(value), _infinity(false), _unknown(false) { }
+    : _value(value), _infinity(false) { }
   Complete(const T& value, const bool& infinity)
-    : _value(value), _infinity(infinity), _unknown(false) {
+    : _value(value), _infinity(infinity) {
     assert(value != 0 || infinity == false);
   }
   Complete(const Complete& other)
-    : _value(other._value), _infinity(other._infinity), _unknown(other._unknown) { }
-  Complete(const Complete& other, bool unknown)
-    : _value(other._value), _infinity(other._infinity), _unknown(unknown) { }
-
-  Complete asUnknown() const {
-    return Complete(*this, true);
-  }
-  Complete asKnown() const {
-    return Complete(*this, false);
-  }
-  bool isUnknown() const {
-    return _unknown;
-  }
+    : _value(other._value), _infinity(other._infinity) { }
 
   Complete& operator=(const Complete& other) {
     _value = other._value;
     _infinity = other._infinity;
-    _unknown = other._unknown;
     return *this;
   }
   Complete& operator+=(const Complete& other) {
@@ -117,7 +102,6 @@ struct Complete {
   private:
   T _value;
   bool _infinity;
-  bool _unknown;
 };
 
 template<typename Z>
@@ -130,8 +114,6 @@ std::istream& operator>>(std::istream& cin, Complete<Z>& num) {
 
 template<typename Z>
 std::ostream& operator<<(std::ostream& cout, const Complete<Z>& num) {
-  if (num._unknown)
-    cout << "(unknown)";
   if (num._infinity) {
     cout << (num._value > 0 ? "inf" : "-inf");
   } else {
@@ -144,9 +126,5 @@ template<>
 Complete<int> infinity() {
   return Complete<int>(1, true);
 }
-template<>
-Complete<int> unknown(const Complete<int>& x) {
-  return Complete<int>(x, true);
-}
 
 #endif
diff --git a/impl/EquationSystem.hpp b/impl/EquationSystem.hpp
index a0ba8a1..3342cc7 100644
--- a/impl/EquationSystem.hpp
+++ b/impl/EquationSystem.hpp
@@ -31,7 +31,7 @@ struct EquationSystem {
     delete _expr_to_var;
   }
 
-  MaxExpression<Domain>& maxExpression(const std::vector<Expression<Domain>*> arguments) {
+  MaxExpression<Domain>& maxExpression(const std::vector<Expression<Domain>*>& arguments) {
     unsigned int id = _max_expressions.size();
     Maximum<Domain>* max = new Maximum<Domain>();
     MaxExpression<Domain>* expr = new MaxExpression<Domain>(id, *max, arguments);
@@ -105,7 +105,7 @@ struct EquationSystem {
     }
   }
 
-  virtual bool equalAssignments(const VariableAssignment<Domain>& l, const VariableAssignment<Domain>& r) const {
+  virtual bool equalAssignments(VariableAssignment<Domain>& l, VariableAssignment<Domain>& r) const {
     for (unsigned int i = 0, length = _variables.size();
          i < length;
          ++i) {
diff --git a/impl/Expression.hpp b/impl/Expression.hpp
index cba9582..dcf7201 100644
--- a/impl/Expression.hpp
+++ b/impl/Expression.hpp
@@ -4,6 +4,7 @@
 #include <string>
 #include <vector>
 #include <sstream>
+#include <set>
 #include "IdMap.hpp"
 #include "Operator.hpp"
 
@@ -31,15 +32,22 @@ struct Expression {
     return NULL;
   }
 
-  virtual Domain eval(const VariableAssignment<Domain>&) const = 0;
-  virtual Domain eval(const VariableAssignment<Domain>& rho,
+  virtual Domain eval(VariableAssignment<Domain>&) const = 0;
+  virtual Domain eval(VariableAssignment<Domain>& rho,
                       const MaxStrategy<Domain>&) const {
     return eval(rho);
   }
+  virtual Domain eval(VariableAssignment<Domain>& rho,
+                      MaxStrategy<Domain>&) const {
+    return eval(rho);
+  }
 
   virtual void mapTo(Variable<Domain>&, IdMap<MaxExpression<Domain>, Variable<Domain>*>&) const {
   }
 
+  virtual void subMaxExprs(std::set<const MaxExpression<Domain>*>&) const {
+  }
+
   virtual void print(std::ostream&) const = 0;
 };
 
@@ -48,7 +56,7 @@ struct Constant : public Expression<Domain> {
   Constant(const Domain& value)
     : _value(value) { }
 
-  virtual Domain eval(const VariableAssignment<Domain>&) const {
+  virtual Domain eval(VariableAssignment<Domain>&) const {
     return _value;
   }
 
@@ -72,7 +80,7 @@ struct Variable : public Expression<Domain> {
     return _name;
   }
 
-  virtual Domain eval(const VariableAssignment<Domain>& rho) const {
+  virtual Domain eval(VariableAssignment<Domain>& rho) const {
     return rho[*this];
   }
 
@@ -90,7 +98,7 @@ struct OperatorExpression : public Expression<Domain> {
   OperatorExpression(const Operator<Domain>& op, const std::vector<Expression<Domain>*>& arguments)
     : _operator(op), _arguments(arguments) { }
 
-  virtual Domain eval(const VariableAssignment<Domain>& rho) const {
+  virtual Domain eval(VariableAssignment<Domain>& rho) const {
     std::vector<Domain> argumentValues;
     for (typename std::vector<Expression<Domain>*>::const_iterator it = _arguments.begin();
          it != _arguments.end();
@@ -100,7 +108,17 @@ struct OperatorExpression : public Expression<Domain> {
     return _operator.eval(argumentValues);
   }
 
-  virtual Domain eval(const VariableAssignment<Domain>& rho, const MaxStrategy<Domain>& strat) const {
+  virtual Domain eval(VariableAssignment<Domain>& rho, const MaxStrategy<Domain>& strat) const {
+    std::vector<Domain> argumentValues;
+    for (typename std::vector<Expression<Domain>*>::const_iterator it = _arguments.begin();
+         it != _arguments.end();
+         ++it) {
+      argumentValues.push_back((*it)->eval(rho, strat));
+    }
+    return _operator.eval(argumentValues);
+  }
+
+  virtual Domain eval(VariableAssignment<Domain>& rho, MaxStrategy<Domain>& strat) const {
     std::vector<Domain> argumentValues;
     for (typename std::vector<Expression<Domain>*>::const_iterator it = _arguments.begin();
          it != _arguments.end();
@@ -130,6 +148,14 @@ struct OperatorExpression : public Expression<Domain> {
     }
   }
 
+  virtual void subMaxExprs(std::set<const MaxExpression<Domain>*>& exprs) const {
+    for (unsigned int i = 0, length = _arguments.size();
+         i < length;
+         ++i) {
+      _arguments[i]->subMaxExprs(exprs);
+    }
+  }
+
   void print(std::ostream& cout) const {
     cout << _operator << "(";
     for (unsigned int i = 0, length = _arguments.size();
@@ -151,7 +177,7 @@ struct OperatorExpression : public Expression<Domain> {
 template<typename Domain>
 struct MaxExpression : public OperatorExpression<Domain> {
   MaxExpression(const unsigned int& id, const Maximum<Domain>& op, const std::vector<Expression<Domain>*>& arguments)
-    : OperatorExpression<Domain>(op, arguments), _id(id) {}
+    : OperatorExpression<Domain>(op, arguments), _id(id) { }
 
   MaxExpression* toMaxExpression() {
     return this;
@@ -161,29 +187,33 @@ struct MaxExpression : public OperatorExpression<Domain> {
     return this;
   }
 
-  virtual Domain eval(const VariableAssignment<Domain>& rho, const MaxStrategy<Domain>& strat) const {
+  virtual Domain eval(VariableAssignment<Domain>& rho, const MaxStrategy<Domain>& strat) const {
+    log::fixpoint << "const MaxExpression eval" << std::endl;
+    return this->_arguments[strat.get(*this)]->eval(rho, strat);
+  }
+
+  virtual Domain eval(VariableAssignment<Domain>& rho, MaxStrategy<Domain>& strat) const {
+    log::strategy << "const MaxExpression eval" << std::endl;
     return this->_arguments[strat.get(*this)]->eval(rho, strat);
   }
 
-  unsigned int bestStrategy(const VariableAssignment<Domain>& rho, const MaxStrategy<Domain>& strat) const {
-    Domain bestValue = this->eval(rho, strat);
-    unsigned int bestIndex = strat.get(*this);
+  unsigned int bestStrategy(VariableAssignment<Domain>& rho, MaxStrategy<Domain>& strat) const {
+    unsigned int bestIndex = const_cast<const MaxStrategy<Domain>&>(strat).get(*this);
+    Domain bestValue = this->_arguments[bestIndex]->eval(rho, strat);
 
     for (unsigned int i = 0, length = this->_arguments.size();
          i < length;
          ++i) {
       const Domain value = this->_arguments[i]->eval(rho, strat);
-      if (!value.isUnknown()) {
-        if (bestValue < value) {
-          bestValue = value;
-          bestIndex = i;
-        }
+      if (bestValue < value) {
+        bestIndex = i;
+        bestValue = value;
       }
     }
     return bestIndex;
   }
 
-  virtual void mapTo(Variable<Domain>& v, IdMap<MaxExpression<Domain>, Variable<Domain>*>& m) const {
+  virtual void mapTo(Variable<Domain>& v, IdMap<MaxExpression<Domain>,Variable<Domain>*>& m) const {
     m[*this] = &v;
     for (unsigned int i = 0, length = this->_arguments.size();
          i < length;
@@ -192,6 +222,15 @@ struct MaxExpression : public OperatorExpression<Domain> {
     }
   }
 
+  virtual void subMaxExprs(std::set<const MaxExpression<Domain>*>& exprs) const {
+    exprs.insert(this);
+    for (unsigned int i = 0, length = this->_arguments.size();
+         i < length;
+         ++i) {
+      this->_arguments[i]->subMaxExprs(exprs);
+    }
+  }
+
   unsigned int id() const {
     return _id;
   }
diff --git a/impl/IdSet.hpp b/impl/IdSet.hpp
index 950b1e1..bf98502 100644
--- a/impl/IdSet.hpp
+++ b/impl/IdSet.hpp
@@ -96,6 +96,10 @@ class IdSet {
     return _set.size();
   }
 
+  bool empty() const {
+    return _set.empty();
+  }
+
   private:
   unsigned int _range;
   std::set<unsigned int> _set;
diff --git a/impl/Makefile b/impl/Makefile
index 6fc6f3b..ca0b37d 100644
--- a/impl/Makefile
+++ b/impl/Makefile
@@ -2,7 +2,7 @@ CC=gcc
 CPP=g++
 BUILD=build
 PARSER=parser
-FLAGS=-Wall -Werror -Wextra -pedantic -lantlr3c -fno-exceptions
+FLAGS=-Wall -Werror -Wextra -pedantic -lantlr3c -fno-exceptions -lrt
 NORMAL_FLAGS=$(FLAGS) -g -pg
 OPTIMISED_FLAGS=$(FLAGS) -O3
 
diff --git a/impl/MaxStrategy.hpp b/impl/MaxStrategy.hpp
index 3ed7972..5534597 100644
--- a/impl/MaxStrategy.hpp
+++ b/impl/MaxStrategy.hpp
@@ -9,10 +9,10 @@
 template<typename Domain>
 struct MaxStrategy {
   virtual ~MaxStrategy() { }
-  virtual unsigned int get(const MaxExpression<Domain>& e) const = 0;
   virtual unsigned int get(const MaxExpression<Domain>& e) {
-    return const_cast<const MaxStrategy*>(this)->get(e);
+    return const_cast<const MaxStrategy<Domain>*>(this)->get(e);
   }
+  virtual unsigned int get(const MaxExpression<Domain>& e) const = 0;
 };
 
 unsigned int stack_depth = 1;
@@ -34,46 +34,67 @@ template<typename Domain>
 struct DynamicMaxStrategy : public MaxStrategy<Domain> {
   DynamicMaxStrategy(
     const EquationSystem<Domain>& system
-  ) : _frozen(false),
-      _system(system),
+  ) : _system(system),
       _rho(NULL),
       _values(system.maxExpressionCount(), 0),
       _stable(system.maxExpressionCount()),
       _influence(system.maxExpressionCount(),
                  IdSet<MaxExpression<Domain> >(system.maxExpressionCount())),
       _var_influence(system.variableCount(),
-                     IdSet<MaxExpression<Domain> >(system.maxExpressionCount()))
+                     IdSet<MaxExpression<Domain> >(system.maxExpressionCount())),
+      _changed(false)
   {}
 
   void setRho(DynamicVariableAssignment<Domain>& rho) {
     _rho = &rho;
   }
 
+  void hasChanged(bool c) {
+    _changed = c;
+  }
+
+  bool hasChanged() const {
+    return _changed;
+  }
+
   unsigned int get(const MaxExpression<Domain>& e) const {
-    // slightly hacky
-    return const_cast<DynamicMaxStrategy<Domain>*>(this)->get(e);
+    log::strategy << indent() << "Look up " << e << std::endl;
+    return _values[e];
   }
 
   unsigned int get(const MaxExpression<Domain>& e) {
-    if (!_frozen)
-      solve(e);
+    log::strategy << indent() << "Solve for " << e << std::endl;
+    solve(e);
     return _values[e];
   }
 
   void invalidate(const Variable<Domain>& v) {
-    log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl;
-    if (_system[v] && _stable.contains(*_system[v])) {
-      _stable.remove(*_system[v]);
-      _stable.filter(_var_influence[v]);
+    log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl; 
+    //log::debug << indent() << "  var-influence sets " << _var_influence << std::endl;
+
+    IdSet<MaxExpression<Domain> > infl = _var_influence[v];
+    for (typename IdSet<MaxExpression<Domain> >::iterator
+           it = infl.begin(),
+           end = infl.end();
+         it != end;
+         ++it) {
+      invalidate(_system.maxExpression(*it));
+    }
+  }
 
-      IdSet<MaxExpression<Domain> > infl = _var_influence[v];
-      _var_influence[v].clear();
+  void invalidate(const MaxExpression<Domain>& v) {
+    if (_stable.contains(v)) {
+      log::strategy << indent() << "Invalidating " << v << std::endl; 
+      //log::debug << indent() << "  influence sets " << _influence << std::endl;
+      _stable.remove(v);
+      
+      IdSet<MaxExpression<Domain> > infl = _influence[v];
       for (typename IdSet<MaxExpression<Domain> >::iterator
              it = infl.begin(),
              end = infl.end();
            it != end;
            ++it) {
-        solve(_system.maxExpression(*it));
+        invalidate(_system.maxExpression(*it));
       }
     }
   }
@@ -84,20 +105,23 @@ private:
       _stable.insert(x);
       log::strategy << indent() << "Stabilise " << x << std::endl;
 
-      stack_depth++;
-      unsigned int val = x.bestStrategy(DependencyAssignment(*this, *_rho, x),
-                                        DependencyStrategy(*this, x));
+      stack_depth++; 
+      DependencyAssignment assignment(*this, *_rho, x);
+      DependencyStrategy depStrat(*this, x);
+      unsigned int val = x.bestStrategy(assignment, depStrat);
       stack_depth--;
 
       if (val != _values[x]) {
-
         log::strategy << x << " => " << *x.arguments()[val] << std::endl;
 
         IdSet<MaxExpression<Domain> > oldInfluence = _influence[x];
-        _influence[x].clear();
+        //_influence[x].clear();
         _values[x] = val;
+        _changed = true;
 
         _rho->invalidate(*_system.varFromExpr(x));
+        
+	//_rho->stabilise();
 
         _stable.filter(oldInfluence);
 
@@ -118,56 +142,27 @@ private:
     }
   }
 
-  const DynamicMaxStrategy& freeze() const {
-    _frozen = true;
-    return *this;
-  }
-
-  const DynamicMaxStrategy& thaw() const {
-    _frozen = false;
-    return *this;
-  }
-
   struct DependencyAssignment : public VariableAssignment<Domain>{
     DependencyAssignment(DynamicMaxStrategy& strat,
                          VariableAssignment<Domain>& rho,
                          const MaxExpression<Domain>& expr)
       : _strat(strat),
         _rho(rho),
-        _expr(expr) {
+        _expr(expr),
+	_current(strat._system.variableCount()) {
     }
-    const Domain& operator[](const Variable<Domain>& var) const {
+    const Domain operator[](const Variable<Domain>& var) {
+      // solve the strategy for this variable, too
+      _strat.solve(*_strat._system[var]);
       _strat._var_influence[var].insert(_expr);
+      _strat._influence[*_strat._system[var]].insert(_expr);
       return _rho[var];
     }
   private:
     DynamicMaxStrategy& _strat;
     VariableAssignment<Domain>& _rho;
     const MaxExpression<Domain>& _expr;
-  };
-
-  struct InvalidatingAssignment : public VariableAssignment<Domain>{
-    InvalidatingAssignment(DynamicVariableAssignment<Domain>& rho)
-      : _rho(rho) {
-    }
-    ~InvalidatingAssignment() {
-      for (typename std::set<const Variable<Domain>*>::iterator
-             it = seen.begin(),
-             ei = seen.end();
-           it != ei;
-           ++it) {
-        if (!_old_stable.contains(**it))
-          _rho.invalidate(**it);
-      }
-    }
-    const Domain& operator[](const Variable<Domain>& var) const {
-      seen.insert(&var);
-      return _rho[var];
-    }
-  private:
-    DynamicVariableAssignment<Domain>& _rho;
-    IdSet<Variable<Domain> > _old_stable;
-    mutable std::set<const Variable<Domain>*> seen;
+    IdSet<Variable<Domain> > _current;
   };
 
   struct DependencyStrategy : public MaxStrategy<Domain> {
@@ -176,10 +171,12 @@ private:
         _expr(expr) {
     }
     unsigned int get(const MaxExpression<Domain>& e) const {
+      _strat._influence[e].insert(_expr);
+      return _strat._values[e];
+    }
+    unsigned int get(const MaxExpression<Domain>& e) {
       _strat.solve(e);
-      if (&_expr != &e) {
-        _strat._influence[e].insert(_expr);
-      }
+      _strat._influence[e].insert(_expr);
       return _strat._values[e];
     }
   private:
@@ -187,14 +184,55 @@ private:
     const MaxExpression<Domain>& _expr;
   };
 
-private:
-  mutable bool _frozen;
+private: 
   const EquationSystem<Domain>& _system;
   DynamicVariableAssignment<Domain>* _rho;
   IdMap<MaxExpression<Domain>,unsigned int> _values;
   IdSet<MaxExpression<Domain> > _stable;
   IdMap<MaxExpression<Domain>,IdSet<MaxExpression<Domain> > > _influence;
   IdMap<Variable<Domain>,IdSet<MaxExpression<Domain> > > _var_influence;
+  bool _changed;
+};
+
+
+template<typename Domain>
+struct Solver {
+  Solver(const EquationSystem<Domain>& system)
+    : _system(system),
+      _strategy(system),
+      _rho(_system, _strategy, -infinity<Domain>()) {
+    _strategy.setRho(_rho);
+  }
+
+  Domain solve(Variable<Domain>& var) {
+    MaxExpression<Domain>& rhs = *_system[var];
+
+    // _rho automatically keeps up to date with changes made to the
+    // strategy, so you don't need to stabilise it
+
+    _strategy.get(rhs);
+
+
+    /*
+    do {
+      _strategy.hasChanged(false);
+      
+      log::debug << "Stabilise assignment (toplevel)" << std::endl;
+      _rho.stabilise();
+      
+      log::debug << "Improve strategy (toplevel)" << std::endl;
+      // improve strategy
+      _strategy.get(rhs);
+      log::debug << (_strategy.hasChanged() ? "Strategy has changed - loop again" : "Strategy has not changed - terminate") << std::endl;
+    } while (_strategy.hasChanged());
+    */
+
+    return _rho[var];
+  }
+private:
+  const EquationSystem<Domain>& _system;
+  DynamicMaxStrategy<Domain> _strategy;
+  DynamicVariableAssignment<Domain> _rho;
 };
 
 
diff --git a/impl/VariableAssignment.hpp b/impl/VariableAssignment.hpp
index 19403a8..2e081e6 100644
--- a/impl/VariableAssignment.hpp
+++ b/impl/VariableAssignment.hpp
@@ -7,10 +7,7 @@
 template<typename Domain>
 struct VariableAssignment {
   virtual ~VariableAssignment() { }
-  virtual const Domain& operator[](const Variable<Domain>&) const = 0;
-  virtual const Domain& operator[](const Variable<Domain>& x) {
-    return (*const_cast<const VariableAssignment*>(this))[x];
-  }
+  virtual const Domain operator[](const Variable<Domain>& x) = 0;
 };
 
 #include "EquationSystem.hpp"
@@ -22,58 +19,44 @@ template<typename Domain>
 struct DynamicVariableAssignment : public VariableAssignment<Domain> {
   DynamicVariableAssignment(
     const EquationSystem<Domain>& system,
-    DynamicMaxStrategy<Domain>& strat
+    DynamicMaxStrategy<Domain>& strat,
+    const Domain& value=infinity<Domain>()
   ) : _system(system),
       _strategy(strat),
-      _values(system.variableCount(), unknown(infinity<Domain>())),
-      _stable(system.variableCount()),
+      _values(system.variableCount(), value),
+      _unstable(system.variableCount()),
       _influence(system.variableCount(),
-                 IdSet<Variable<Domain> >(system.variableCount())),
-      _frozen(false)
+                 IdSet<Variable<Domain> >(system.variableCount()))
   { }
 
-  void freeze() {
-    _frozen = true;
-  }
-
-  void thaw() {
-    _frozen = false;
-  }
-
-  bool is_frozen() {
-    return _frozen;
-  }
-
-  const Domain& operator[](const Variable<Domain>& var) const {
-    // slightly hacky
-    return const_cast<DynamicVariableAssignment<Domain>&>(*this)[var];
+  const Domain operator[](const Variable<Domain>& var) {
+    solve(var);
+    return _values[var];
   }
 
-  const Domain& operator[](const Variable<Domain>& var) {
-    if (!_frozen)
+  /*void stabilise() {
+    if (!_unstable.empty()) {
+      Variable<Domain>& var = _system.variable(*_unstable.begin());
       solve(var);
-    return _values[var];
-  }
+    }
+    }*/
 
-  void invalidate(const Variable<Domain>& x, bool also_solve=true) {
-    log::fixpoint << indent() << "Invalidating " << x << std::endl;
-    if (_stable.contains(x)) {
-      _stable.remove(x);
-      _values[x] = unknown(infinity<Domain>());
+  void invalidate(const Variable<Domain>& x) {
+    if (!_unstable.contains(x)) {
+      log::fixpoint << indent() << "Invalidating " << x << std::endl;
+ 
+      _unstable.insert(x);
+      _values[x] = infinity<Domain>();
 
       IdSet<Variable<Domain> > infl = _influence[x];
+      _influence[x].clear();
+
       for (typename IdSet<Variable<Domain> >::iterator
-             it = infl.begin(),
-             ei = infl.end();
-           it != ei;
-           ++it) {
-        invalidate(_system.variable(*it), false);
-      }
-      
-      if (also_solve) {
-        solve(x);
-        if (_values[x] == infinity<Domain>())
-          _values[x] = _values[x].asKnown();
+	     it = infl.begin(),
+	     ei = infl.end();
+	   it != ei;
+	   ++it) {
+	invalidate(_system.variable(*it));
       }
     }
   }
@@ -81,25 +64,28 @@ struct DynamicVariableAssignment : public VariableAssignment<Domain> {
 private:
 
   void solve(const Variable<Domain>& x) {
-    if (!_stable.contains(x)) {
-      _stable.insert(x);
+    if (_unstable.contains(x)) {
+      _unstable.remove(x);
       log::fixpoint << indent() << "Stabilise " << x << std::endl;
 
       stack_depth++;
-      Domain val = _system[x]->eval(DependencyAssignment(*this, x),
-                                    _strategy);
+      // we don't want the assignment to affect the strategy, so we're
+      // going to use a const reference here
+      const DynamicMaxStrategy<Domain>& const_strat = _strategy;
+      DependencyAssignment assignment(*this, x);
+      Domain val = _system[x]->eval(assignment, const_strat);
       stack_depth--;
 
       if (val != _values[x]) {
         log::fixpoint << x << " = " << val << std::endl;
+ 
+        _strategy.invalidate(x);
 
         IdSet<Variable<Domain> > oldInfluence = _influence[x];
         _influence[x].clear();
         _values[x] = val;
 
-        _strategy.invalidate(x);
-
-        _stable.filter(oldInfluence);
+        _unstable.absorb(oldInfluence);
 
         for (typename IdSet<Variable<Domain> >::iterator it = oldInfluence.begin();
              it != oldInfluence.end();
@@ -119,8 +105,8 @@ private:
   struct DependencyAssignment : public VariableAssignment<Domain> {
     DependencyAssignment(DynamicVariableAssignment& assignment, const Variable<Domain>& var)
       : _assignment(assignment), _var(var) { }
-    const Domain& operator[](const Variable<Domain>& x) const {
-      const Domain& result = _assignment[x];
+    const Domain operator[](const Variable<Domain>& x) {
+      const Domain result = _assignment[x];
       _assignment._influence[x].insert(_var);
       return result;
     }
@@ -132,9 +118,8 @@ private:
   const EquationSystem<Domain>& _system;
   DynamicMaxStrategy<Domain>& _strategy;
   IdMap<Variable<Domain>, Domain> _values;
-  IdSet<Variable<Domain> > _stable;
+  IdSet<Variable<Domain> > _unstable;
   IdMap<Variable<Domain>,IdSet<Variable<Domain> > > _influence;
-  bool _frozen;
 };
 
 #endif
diff --git a/impl/main.cpp b/impl/main.cpp
index b83894d..1fed389 100644
--- a/impl/main.cpp
+++ b/impl/main.cpp
@@ -1,5 +1,6 @@
 #include "Log.hpp"
 #include <iostream>
+#include <iomanip>
 #include <vector>
 #include <sstream>
 #include "Complete.hpp"
@@ -136,44 +137,46 @@ int main (int argc, char* argv[]) {
 
   EquationSystemParser_equation_system_return ret = parser -> equation_system(parser);
 
+  std::cerr << "Parse complete." << std::endl;
+
   EquationSystem<ZBar> system;
   treeToSystem<ZBar>(ret.tree, system);
 
   log::debug << system << endl;
   system.indexMaxExpressions(); // make reverse-lookup O(1) instead of O(n)
 
-  DynamicMaxStrategy<ZBar> strategy(system);
-  DynamicVariableAssignment<ZBar> rho(system, strategy);
-  strategy.setRho(rho);
+  std::cerr << "System created and indexed." << std::endl;
+
+  Solver<ZBar> solver(system); // local *and* lazy. I love it!
 
   timespec start, finish;
   clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &start);
   if (variables.size() > 0) {
-    for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
-      Variable<ZBar>& var = system.variable(i);
-      if (variables.find(var.name()) != variables.end()) {
-        rho[var];
-      }
+    for (set<string>::iterator it = variables.begin(), ei = variables.end();
+         it != ei;
+         ++it) {
+      solver.solve(system.variable(*it));
     }
   } else {
     for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
       Variable<ZBar>& var = system.variable(i);
-      rho[var];
+      solver.solve(var);
     }
   }
   clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &finish);
 
+  std::cerr << "System solved." << std::endl;
+
   if (variables.size() > 0) {
     for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
       Variable<ZBar>& var = system.variable(i);
-      if (variables.find(var.name()) != variables.end()) {
-        cout << var.name() << " = " << rho[var].asKnown() << endl;
-      }
+      if (variables.find(var.name()) != variables.end())
+        cout << var.name() << " = " << solver.solve(var) << endl;
     }
   } else {
     for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
       Variable<ZBar>& var = system.variable(i);
-      cout << var.name() << " = " << rho[var].asKnown() << endl;
+      cout << var.name() << " = " << solver.solve(var) << endl;
     }
   }
 
@@ -185,8 +188,7 @@ int main (int argc, char* argv[]) {
     temp.tv_sec = finish.tv_sec-start.tv_sec;
     temp.tv_nsec = finish.tv_nsec-start.tv_nsec;
   }
-  cerr << "Time taken: " << temp.tv_sec << " seconds and " << temp.tv_nsec << " nanoseconds." << endl;
-  
+  cerr << "Time taken: " << temp.tv_sec << "." << setfill('0') << setw(9) << temp.tv_nsec << " seconds." << endl;
 
   parser -> free(parser);
   tokens -> free(tokens);
diff --git a/impl/systems/example.eqns b/impl/systems/example.eqns
index 71ee74a..dc59a01 100644
--- a/impl/systems/example.eqns
+++ b/impl/systems/example.eqns
@@ -1,3 +1,3 @@
-x1 = max(0, min(x1-1, x2))
+x1 = max(0, min(x1 - 1, x2))
 x2 = max(0, 5+x1, x1)
-x3 = max(0, 1+x3, 0+x1)
+x3 = max(0, 1 + x3, 0 + x1)
diff --git a/impl/test/7.eqns b/impl/test/7.eqns
index 1f69268..2789f0e 100644
--- a/impl/test/7.eqns
+++ b/impl/test/7.eqns
@@ -1,5 +1,5 @@
 x = 0
-y = max(x,a)
+y = max(-inf, x, a)
 a = b
 b = c
 c = d