13 files changed, 249 insertions, 318 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..c005fd6 100644
--- a/impl/Expression.hpp
+++ b/impl/Expression.hpp
@@ -31,9 +31,9 @@ struct Expression {
     return NULL;
   }
 
-  virtual Domain eval(const VariableAssignment<Domain>&) const = 0;
-  virtual Domain eval(const VariableAssignment<Domain>& rho,
-                      const MaxStrategy<Domain>&) const {
+  virtual Domain eval(VariableAssignment<Domain>&) const = 0;
+  virtual Domain eval(VariableAssignment<Domain>& rho,
+                      MaxStrategy<Domain>&) const {
     return eval(rho);
   }
 
@@ -48,7 +48,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 +72,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 +90,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 +100,7 @@ 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, MaxStrategy<Domain>& strat) const {
     std::vector<Domain> argumentValues;
     for (typename std::vector<Expression<Domain>*>::const_iterator it = _arguments.begin();
          it != _arguments.end();
@@ -151,7 +151,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,11 +161,11 @@ 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, MaxStrategy<Domain>& strat) const {
     return this->_arguments[strat.get(*this)]->eval(rho, strat);
   }
 
-  unsigned int bestStrategy(const VariableAssignment<Domain>& rho, const MaxStrategy<Domain>& strat) const {
+  unsigned int bestStrategy(VariableAssignment<Domain>& rho, MaxStrategy<Domain>& strat) const {
     Domain bestValue = this->eval(rho, strat);
     unsigned int bestIndex = strat.get(*this);
 
@@ -173,11 +173,9 @@ struct MaxExpression : public OperatorExpression<Domain> {
          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) {
+        bestValue = value;
+        bestIndex = i;
       }
     }
     return bestIndex;
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/MaxStrategy.hpp b/impl/MaxStrategy.hpp
index 3ed7972..d908c7b 100644
--- a/impl/MaxStrategy.hpp
+++ b/impl/MaxStrategy.hpp
@@ -9,10 +9,7 @@
 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);
-  }
+  virtual unsigned int get(const MaxExpression<Domain>& e) = 0;
 };
 
 unsigned int stack_depth = 1;
@@ -34,24 +31,31 @@ 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())),
+      _frozen(false)
   {}
 
-  void setRho(DynamicVariableAssignment<Domain>& rho) {
-    _rho = &rho;
+  void freeze() {
+    _frozen = true;
   }
 
-  unsigned int get(const MaxExpression<Domain>& e) const {
-    // slightly hacky
-    return const_cast<DynamicMaxStrategy<Domain>*>(this)->get(e);
+  void thaw() {
+    _frozen = false;
+  }
+
+  bool is_frozen() {
+    return _frozen;
+  }
+
+  void setRho(DynamicVariableAssignment<Domain>& rho) {
+    _rho = &rho;
   }
 
   unsigned int get(const MaxExpression<Domain>& e) {
@@ -61,20 +65,18 @@ struct DynamicMaxStrategy : public MaxStrategy<Domain> {
   }
 
   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]);
-
-      IdSet<MaxExpression<Domain> > infl = _var_influence[v];
-      _var_influence[v].clear();
-      for (typename IdSet<MaxExpression<Domain> >::iterator
-             it = infl.begin(),
-             end = infl.end();
-           it != end;
-           ++it) {
-        solve(_system.maxExpression(*it));
-      }
+    log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl; 
+    _stable.filter(_var_influence[v]);
+
+    IdSet<MaxExpression<Domain> > infl = _var_influence[v];
+    _var_influence[v].clear();
+
+    for (typename IdSet<MaxExpression<Domain> >::iterator
+           it = infl.begin(),
+           end = infl.end();
+         it != end;
+         ++it) {
+      solve(_system.maxExpression(*it));
     }
   }
 
@@ -84,13 +86,13 @@ 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];
@@ -99,6 +101,12 @@ private:
 
         _rho->invalidate(*_system.varFromExpr(x));
 
+	_rho->thaw();
+	this->freeze();
+	_rho->stabilise();
+	_rho->freeze();
+	this->thaw();
+
         _stable.filter(oldInfluence);
 
         for (typename IdSet<MaxExpression<Domain> >::iterator
@@ -118,56 +126,31 @@ 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) {
       _strat._var_influence[var].insert(_expr);
-      return _rho[var];
+      if (_current.contains(var)) {
+	return _rho[var];
+      } else {
+	_current.insert(var);
+	Domain val = _strat._system[var]->eval(_rho, _strat);
+	_current.remove(var);
+	return val;
+      }
     }
   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> {
@@ -175,7 +158,7 @@ private:
       : _strat(strat),
         _expr(expr) {
     }
-    unsigned int get(const MaxExpression<Domain>& e) const {
+    unsigned int get(const MaxExpression<Domain>& e) {
       _strat.solve(e);
       if (&_expr != &e) {
         _strat._influence[e].insert(_expr);
@@ -187,14 +170,49 @@ 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 _frozen;
+};
+
+
+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];
+
+    do {
+      _rho.has_changed(false);
+
+      // improve strategy
+      _rho.freeze();
+      _strategy.thaw();
+      _strategy.get(rhs);
+
+      // iterate fixpoint
+      _strategy.freeze();
+      _rho.thaw();
+      _rho.stabilise();
+    } while (_rho.has_changed());
+
+    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..e074f6f 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,15 +19,18 @@ 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)
-  { }
+      _frozen(false),
+      _changed(false)
+  {
+  }
 
   void freeze() {
     _frozen = true;
@@ -40,40 +40,46 @@ struct DynamicVariableAssignment : public VariableAssignment<Domain> {
     _frozen = false;
   }
 
-  bool is_frozen() {
+  bool is_frozen() const {
     return _frozen;
   }
 
-  const Domain& operator[](const Variable<Domain>& var) const {
-    // slightly hacky
-    return const_cast<DynamicVariableAssignment<Domain>&>(*this)[var];
+  void has_changed(bool c) {
+    _changed = c;
   }
 
-  const Domain& operator[](const Variable<Domain>& var) {
+  bool has_changed() const {
+    return _changed;
+  }
+
+  const Domain operator[](const Variable<Domain>& var) {
     if (!_frozen)
       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 stabilise() {
+    if (!_unstable.empty()) {
+      Variable<Domain>& var = _system.variable(*_unstable.begin());
+      solve(var);
+    }
+  }
 
+  void invalidate(const Variable<Domain>& x) {
+    log::fixpoint << indent() << "Invalidating " << x << std::endl;
+    if (!_unstable.contains(x)) {
+      _unstable.insert(x);
+      _values[x] = infinity<Domain>();
+      _changed = true;
+     
       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,13 +87,13 @@ 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);
+      DependencyAssignment assignment(*this, x);
+      Domain val = _system[x]->eval(assignment, _strategy);
       stack_depth--;
 
       if (val != _values[x]) {
@@ -96,10 +102,11 @@ private:
         IdSet<Variable<Domain> > oldInfluence = _influence[x];
         _influence[x].clear();
         _values[x] = val;
+	_changed = true;
 
         _strategy.invalidate(x);
 
-        _stable.filter(oldInfluence);
+        _unstable.absorb(oldInfluence);
 
         for (typename IdSet<Variable<Domain> >::iterator it = oldInfluence.begin();
              it != oldInfluence.end();
@@ -119,8 +126,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 +139,10 @@ 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;
+  bool _changed;
 };
 
 #endif
diff --git a/impl/main.cpp b/impl/main.cpp
index b547c48..94351ec 100644
--- a/impl/main.cpp
+++ b/impl/main.cpp
@@ -140,6 +140,21 @@ int main (int argc, char* argv[]) {
   log::debug << system << endl;
   system.indexMaxExpressions(); // make reverse-lookup O(1) instead of O(n)
 
+  Solver<ZBar> solver(system); // local *and* lazy. I love it!
+  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() << " = " << 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() << " = " << solver.solve(var) << endl;
+    }
+  }
+
+  /*
   DynamicMaxStrategy<ZBar> strategy(system);
   DynamicVariableAssignment<ZBar> rho(system, strategy);
   strategy.setRho(rho);
@@ -147,16 +162,16 @@ int main (int argc, char* argv[]) {
   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() << " = " << rho[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() << " = " << rho[var] << endl;
     }
   }
+  */
 
   parser -> free(parser);
   tokens -> free(tokens);
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
diff --git a/impl/test/run b/impl/test/run
index 826bbde..0c1886d 100644
--- a/impl/test/run
+++ b/impl/test/run
@@ -7,10 +7,7 @@ FAILED=0
 echo "Testing binary: $1 in directory $DIR"
 while [ -f "$DIR/$NUM.eqns" ]
 do
-  OUTPUT=$(timeout 5s $1 "$DIR/$NUM.eqns")
-  if [ $? -eq 124 ]; then
-    OUTPUT="did not terminate"
-  fi
+  OUTPUT=$($1 "$DIR/$NUM.eqns")
   DIFF=$(echo "$OUTPUT" | diff - "$DIR/$NUM.soln")
   if [ ! -z "$DIFF" ]; then
     echo "=================="