A bunch of fixes to the solver, and moving it in to clang.

Also some contribution writing stuff.

Basically: lots of work.

22 files changed, 330 insertions, 231 deletions

diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/Complete.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/Complete.hpp
index 9acb9d0..e3ec15a 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/Complete.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/Complete.hpp
@@ -1,6 +1,7 @@
 #ifndef COMPLETE_HPP
 #define COMPLETE_HPP
 
+#include <cassert>
 #include <ostream>
 #include <istream>
 
@@ -39,7 +40,11 @@ struct Complete {
     return Complete<T>(- _value, _infinity);
   }
   Complete operator+(const Complete& other) const {
-    if (_infinity) {
+    if (_infinity && other._infinity) {
+      if (_value > 0 || other._value > 0)
+        return Complete<T>(1, true);
+      return Complete<T>(-1, true);
+    } else if (_infinity) {
       return *this;
     } else if (other._infinity) {
       return other;
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp
index d95366d..3342cc7 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp
@@ -91,13 +91,12 @@ struct EquationSystem {
   void indexMaxExpressions() {
     _expr_to_var = new IdMap<MaxExpression<Domain>,Variable<Domain>*>(maxExpressionCount(), NULL); 
     for (unsigned int i = 0, length = _right_sides.size(); i < length; ++i) {
-      if (_right_sides[i])
-        _right_sides[i]->mapTo(*_variables[i], *_expr_to_var);
+      _right_sides[i]->mapTo(*_variables[i], *_expr_to_var);
     }
   }
 
   Variable<Domain>* varFromExpr(const Expression<Domain>& expr) const {
-    assert(_expr_to_var != NULL); // ensure we've indexed
+    assert(_expr_to_var); // make sure we've indexed
     const MaxExpression<Domain>* maxExpr = expr.toMaxExpression();//dynamic_cast<const MaxExpression<Domain>*>(&expr);
     if (maxExpr) {
       return (*_expr_to_var)[*maxExpr];
@@ -106,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) {
@@ -121,10 +120,7 @@ struct EquationSystem {
     for (unsigned int i = 0, length = _variables.size();
          i < length;
          ++i) {
-      if (_right_sides[i])
-        cout << *_variables[i] << " = " << *_right_sides[i] << std::endl;
-      else
-        cout << *_variables[i] << " = NULL" << std::endl;
+      cout << *_variables[i] << " = " << *_right_sides[i] << std::endl;
     }
   }
 
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp
index ac9b052..b59c7a2 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp
@@ -4,6 +4,7 @@
 #include <string>
 #include <vector>
 #include <sstream>
+#include <set>
 #include "IdMap.hpp"
 #include "Operator.hpp"
 
@@ -27,15 +28,26 @@ struct Expression {
     return NULL;
   }
 
-  virtual Domain eval(const VariableAssignment<Domain>&) const = 0;
-  virtual Domain evalWithStrat(const VariableAssignment<Domain>& rho,
+  virtual MaxExpression<Domain>* toMaxExpression() {
+    return NULL;
+  }
+
+  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;
 };
 
@@ -44,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;
   }
 
@@ -68,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];
   }
 
@@ -84,11 +96,9 @@ struct Variable : public Expression<Domain> {
 template<typename Domain>
 struct OperatorExpression : public Expression<Domain> {
   OperatorExpression(const Operator<Domain>& op, const std::vector<Expression<Domain>*>& arguments)
-    : _operator(op), _arguments(arguments) {
-    assert(!arguments.empty());
-  }
+    : _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();
@@ -98,12 +108,22 @@ struct OperatorExpression : public Expression<Domain> {
     return _operator.eval(argumentValues);
   }
 
-  virtual Domain evalWithStrat(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();
          ++it) {
-      argumentValues.push_back((*it)->evalWithStrat(rho, strat));
+      argumentValues.push_back((*it)->eval(rho, strat));
     }
     return _operator.eval(argumentValues);
   }
@@ -128,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,31 +179,40 @@ 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) { }
 
+  MaxExpression* toMaxExpression() {
+    return this;
+  }
+
   const MaxExpression* toMaxExpression() const {
     return this;
   }
 
-  virtual Domain evalWithStrat(const VariableAssignment<Domain>& rho, const MaxStrategy<Domain>& strat) const {
-    return this->_arguments[strat.get(*this)]->evalWithStrat(rho, strat);
+  virtual Domain eval(VariableAssignment<Domain>& rho, const MaxStrategy<Domain>& strat) const {
+    solver_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 {
+    solver_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->evalWithStrat(rho, strat);
-    unsigned int bestIndex = strat.get(*this);
+  unsigned int bestStrategy(VariableAssignment<Domain>& rho, MaxStrategy<Domain>& strat, unsigned int bestIndex) const {
+    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]->evalWithStrat(rho, strat);
+      const Domain value = this->_arguments[i]->eval(rho, strat);
       if (bestValue < value) {
-        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;
@@ -184,6 +221,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/clang/include/clang/Analysis/Analyses/IntervalSolver/IdMap.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/IdMap.hpp
index 5e3aa3b..8cb25f8 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/IdMap.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/IdMap.hpp
@@ -1,13 +1,14 @@
 #ifndef ID_MAP_HPP
 #define ID_MAP_HPP
 
+#include <cassert>
 #include <ostream>
 
 template<typename T, typename V>
 struct IdMap {
   IdMap(unsigned int length, V initial)
     : _length(length), _assignment(new V[length]) {
-    for (unsigned int i = 0; i < length; ++i) {
+    for (unsigned int i = 0; i < _length; ++i) {
       _assignment[i] = initial;
     }
   }
@@ -32,17 +33,11 @@ struct IdMap {
     return *this;
   }
   virtual const V& operator[] (const T& x) const {
-    if (x.id() >= _length) {
-      std::cout << "throw exception" << *(char*)NULL;
-      //throw "Array out of bounds";
-    }
+    assert(x.id() < _length);
     return _assignment[x.id()];
   }
   virtual V& operator[] (const T& x) {
-    if (x.id() >= _length) {
-      std::cout << "throw exception" << *(char*)NULL;
-      //throw "Array out of bounds";
-    }
+    assert(x.id() < _length);
     return _assignment[x.id()];
   }
 
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/IdSet.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/IdSet.hpp
index 950b1e1..bf98502 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/IdSet.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/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/clang/include/clang/Analysis/Analyses/IntervalSolver/Log.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/Log.hpp
index f9af7f2..90ab7e5 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/Log.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/Log.hpp
@@ -1,26 +1,20 @@
 #ifndef LOG_HPP
 #define LOG_HPP
 
+// could not be hackier, but C++ is annoying
+#define protected public
+#include <streambuf>
+#undef protected
+
 #include <string>
 #include <iostream>
 #include <map>
 #include <cstdio>
 
 namespace solver_log {
-
   struct Logger : public std::ostream {
-    Logger(std::streambuf*, const std::string&)
+    Logger(std::streambuf* buffer, const std::string& name)
       : std::ostream(NULL) { }
-
-    bool enabled() const {
-      return false;
-    }
-
-    bool enabled(bool) {
-      return false;
-    }
-
-  private:
   };
 
   Logger strategy(std::cerr.rdbuf(), "strategy");
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp
index 57dcdeb..9ae7394 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp
@@ -9,6 +9,9 @@
 template<typename Domain>
 struct MaxStrategy {
   virtual ~MaxStrategy() { }
+  virtual unsigned int get(const MaxExpression<Domain>& e) {
+    return const_cast<const MaxStrategy<Domain>*>(this)->get(e);
+  }
   virtual unsigned int get(const MaxExpression<Domain>& e) const = 0;
 };
 
@@ -37,54 +40,85 @@ struct DynamicMaxStrategy : public MaxStrategy<Domain> {
       _stable(system.maxExpressionCount()),
       _influence(system.maxExpressionCount(),
                  IdSet<MaxExpression<Domain> >(system.maxExpressionCount())),
-      _var_influence(system.variableCount(),
-                     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 {
-    solve(e);
+    solver_log::strategy << indent() << "Look up " << e << std::endl;
     return _values[e];
   }
 
-  void invalidate(const Variable<Domain>& v) const {
-    solver_log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl;
-    _stable.filter(_var_influence[v]);
+  unsigned int get(const MaxExpression<Domain>& e) {
+    solver_log::strategy << indent() << "Solve for " << e << std::endl;
+    solve(e);
+    return _values[e];
+  }
 
-    IdSet<MaxExpression<Domain> > infl = _var_influence[v];
-    _var_influence[v].clear();
+  void invalidate(const Variable<Domain>& v) {
+    solver_log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl; 
 
+    IdSet<MaxExpression<Domain> > infl = _influence[*_system[v]];
     for (typename IdSet<MaxExpression<Domain> >::iterator
            it = infl.begin(),
            end = infl.end();
          it != end;
          ++it) {
-      solve(_system.maxExpression(*it));
+      invalidate(_system.maxExpression(*it));
+    }
+  }
+
+  void invalidate(const MaxExpression<Domain>& v) {
+    if (_stable.contains(v)) {
+      solver_log::strategy << indent() << "Invalidating " << v << std::endl; 
+      //solver_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) {
+        invalidate(_system.maxExpression(*it));
+      }
     }
   }
 
 private:
-  void solve(const MaxExpression<Domain>& x) const {
+  void solve(const MaxExpression<Domain>& x) {
     if (!_stable.contains(x)) {
       _stable.insert(x);
       solver_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, _values[x]);
       stack_depth--;
 
       if (val != _values[x]) {
         solver_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);
 
@@ -96,57 +130,107 @@ private:
           solve(_system.maxExpression(*it));
         }
       } else {
-        solver_log::strategy << indent() << x << " did not change" << std::endl;
+        solver_log::strategy << indent() << x << " did not change: "
+		      << x << " => " << *x.arguments()[val] << std::endl;
       }
     } else {
-      solver_log::strategy << indent() << x << " is stable" << std::endl;
+      solver_log::strategy << indent() << x << " is stable: "
+		    << x << " => " << *x.arguments()[_values[x]] << std::endl;
     }
   }
 
   struct DependencyAssignment : public VariableAssignment<Domain>{
-    DependencyAssignment(const DynamicMaxStrategy& strat,
+    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 {
-      _strat._var_influence[var].insert(_expr);
+    const Domain operator[](const Variable<Domain>& var) {
+      // solve the strategy for this variable, too
+      _strat.solve(*_strat._system[var]);
+      _strat._influence[*_strat._system[var]].insert(_expr);
       return _rho[var];
     }
   private:
-    const DynamicMaxStrategy& _strat;
+    DynamicMaxStrategy& _strat;
     VariableAssignment<Domain>& _rho;
     const MaxExpression<Domain>& _expr;
+    IdSet<Variable<Domain> > _current;
   };
 
   struct DependencyStrategy : public MaxStrategy<Domain> {
-    DependencyStrategy(const DynamicMaxStrategy& strat, const MaxExpression<Domain>& expr)
+    DependencyStrategy(DynamicMaxStrategy& strat, const MaxExpression<Domain>& expr)
       : _strat(strat),
         _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:
-    const DynamicMaxStrategy& _strat;
+    DynamicMaxStrategy& _strat;
     const MaxExpression<Domain>& _expr;
   };
 
+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;
+  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);
+      
+      solver_log::debug << "Stabilise assignment (toplevel)" << std::endl;
+      _rho.stabilise();
+      
+      solver_log::debug << "Improve strategy (toplevel)" << std::endl;
+      // improve strategy
+      _strategy.get(rhs);
+      solver_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;
-  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;
+  DynamicMaxStrategy<Domain> _strategy;
+  DynamicVariableAssignment<Domain> _rho;
 };
 
+
 /*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/Operator.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/Operator.hpp
index 08c66ff..64ef096 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/Operator.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/Operator.hpp
@@ -1,6 +1,7 @@
 #ifndef OPERATOR_HPP
 #define OPERATOR_HPP
 
+#include <cassert>
 #include <vector>
 
 template<typename Domain>
@@ -28,11 +29,6 @@ struct Maximum : public Operator<Domain> {
   }
 };
 
-
-template<class T>
-T minimum(const T& l, const T& r) {
-  return (l < r ? l : r);
-}
 template<typename Domain>
 struct Minimum : public Operator<Domain> {
   virtual Domain eval(const std::vector<Domain>& arguments) const {
@@ -40,7 +36,7 @@ struct Minimum : public Operator<Domain> {
     for (typename std::vector<Domain>::const_iterator it = arguments.begin();
          it != arguments.end();
          ++it) {
-      result = minimum(*it, result); //*it < result ? *it : result);
+      result = (*it < result ? *it : result);
     }
     return result;
   }
@@ -52,8 +48,7 @@ struct Minimum : public Operator<Domain> {
 template<typename Domain>
 struct Negation : public Operator<Domain> {
   virtual Domain eval(const std::vector<Domain>& arguments) const {
-    if (arguments.size() > 1)
-      throw "Too many arguments to a negation.";
+    assert(arguments.size() == 1);
     return -arguments[0];
   }
   void print(std::ostream& cout) const {
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp
index ba5f650..746e5ef 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp
@@ -7,7 +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) = 0;
 };
 
 #include "EquationSystem.hpp"
@@ -19,54 +19,73 @@ template<typename Domain>
 struct DynamicVariableAssignment : public VariableAssignment<Domain> {
   DynamicVariableAssignment(
     const EquationSystem<Domain>& system,
-    const DynamicMaxStrategy<Domain>& strat
+    DynamicMaxStrategy<Domain>& strat,
+    const Domain& value=infinity<Domain>()
   ) : _system(system),
       _strategy(strat),
-      _values(system.variableCount(), infinity<Domain>()),
-      _stable(system.variableCount()),
+      _values(system.variableCount(), value),
+      _unstable(system.variableCount()),
       _influence(system.variableCount(),
                  IdSet<Variable<Domain> >(system.variableCount()))
   { }
 
-  const Domain& operator[](const Variable<Domain>& var) const {
+  const Domain operator[](const Variable<Domain>& var) {
     solve(var);
     return _values[var];
   }
 
-  void invalidate(const Variable<Domain>& x) const {
-    solver_log::fixpoint << indent() << "Invalidating " << x << std::endl;
-    if (_stable.contains(x)) {
-      _stable.remove(x);
+  /*void stabilise() {
+    if (!_unstable.empty()) {
+      Variable<Domain>& var = _system.variable(*_unstable.begin());
+      solve(var);
+    }
+    }*/
+
+  void invalidate(const Variable<Domain>& x) {
+    if (!_unstable.contains(x)) {
+      solver_log::fixpoint << indent() << "Invalidating " << x << std::endl;
+ 
+      _unstable.insert(x);
       _values[x] = infinity<Domain>();
-      
-      solve(x);
+
+      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));
+      }
     }
   }
 
 private:
 
-  void solve(const Variable<Domain>& x) const {
-    if (!_stable.contains(x)) {
-      _stable.insert(x);
+  void solve(const Variable<Domain>& x) {
+    if (_unstable.contains(x)) {
+      _unstable.remove(x);
       solver_log::fixpoint << indent() << "Stabilise " << x << std::endl;
 
       stack_depth++;
-      if (!_system[x])
-        return;
-      Domain val = _system[x]->evalWithStrat(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]) {
         solver_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();
@@ -74,31 +93,33 @@ private:
           solve(_system.variable(*it));
         }
       } else {
-        solver_log::fixpoint << indent() << x << " did not change" << std::endl;
+        solver_log::fixpoint << indent() << x << " did not change: "
+		      << x << " = " << val << std::endl;
       }
     } else {
-      solver_log::fixpoint << indent() << x << " is stable" << std::endl;
+      solver_log::fixpoint << indent() << x << " is stable: "
+		    << x << " = " << _values[x] << std::endl;
     }
   }
 
   struct DependencyAssignment : public VariableAssignment<Domain> {
-    DependencyAssignment(const DynamicVariableAssignment& assignment, const Variable<Domain>& var)
+    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;
     }
   private:
-    const DynamicVariableAssignment& _assignment;
+    DynamicVariableAssignment& _assignment;
     const Variable<Domain>& _var;
   };
 
   const EquationSystem<Domain>& _system;
-  const DynamicMaxStrategy<Domain>& _strategy;
-  mutable IdMap<Variable<Domain>, Domain> _values;
-  mutable IdSet<Variable<Domain> > _stable;
-  mutable IdMap<Variable<Domain>,IdSet<Variable<Domain> > > _influence;
+  DynamicMaxStrategy<Domain>& _strategy;
+  IdMap<Variable<Domain>, Domain> _values;
+  IdSet<Variable<Domain> > _unstable;
+  IdMap<Variable<Domain>,IdSet<Variable<Domain> > > _influence;
 };
 
 #endif
diff --git a/clang/lib/Analysis/Interval.cpp b/clang/lib/Analysis/Interval.cpp
index ac96107..3a82344 100644
--- a/clang/lib/Analysis/Interval.cpp
+++ b/clang/lib/Analysis/Interval.cpp
@@ -221,11 +221,6 @@ M merge_maps_with(const F& f, const M& left, const M& right) {
   return result;
 }
 
-template<>
-Vector minimum(const Vector& l, const Vector& r) {
-  return (l < r ? l : r);
-  return merge_maps_with(minimum<ZBar>, l, r);
-}
 template<class T>
 T max(const T& l, const T& r) {
   return (l < r ? l : r);
@@ -702,39 +697,15 @@ 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);
+
+  Solver<ZBar> solver(system);
 
   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";
+    llvm::errs() << toString(var.name()) << " = " << toString(solver.solve(var)) << "\n";
   }
 }
 
diff --git a/impl/Expression.hpp b/impl/Expression.hpp
index dcf7201..619bc7e 100644
--- a/impl/Expression.hpp
+++ b/impl/Expression.hpp
@@ -197,8 +197,7 @@ struct MaxExpression : public OperatorExpression<Domain> {
     return this->_arguments[strat.get(*this)]->eval(rho, strat);
   }
 
-  unsigned int bestStrategy(VariableAssignment<Domain>& rho, MaxStrategy<Domain>& strat) const {
-    unsigned int bestIndex = const_cast<const MaxStrategy<Domain>&>(strat).get(*this);
+  unsigned int bestStrategy(VariableAssignment<Domain>& rho, MaxStrategy<Domain>& strat, unsigned int bestIndex) const {
     Domain bestValue = this->_arguments[bestIndex]->eval(rho, strat);
 
     for (unsigned int i = 0, length = this->_arguments.size();
diff --git a/impl/MaxStrategy.hpp b/impl/MaxStrategy.hpp
index 71ea4f4..6fee921 100644
--- a/impl/MaxStrategy.hpp
+++ b/impl/MaxStrategy.hpp
@@ -20,7 +20,7 @@ unsigned int stack_depth = 1;
 std::string indent() {
   std::string result = "";
   for (unsigned int i = 0; i < stack_depth; ++i) {
-    result += '\t';
+    result += ' ';
   }
   return result;
 }
@@ -39,22 +39,13 @@ struct DynamicMaxStrategy : public MaxStrategy<Domain> {
       _values(system.maxExpressionCount(), 0),
       _stable(system.maxExpressionCount()),
       _influence(system.maxExpressionCount(),
-                 IdSet<MaxExpression<Domain> >(system.maxExpressionCount())),
-      _changed(false)
+                 IdSet<MaxExpression<Domain> >(system.maxExpressionCount()))
   {}
 
   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 {
     log::strategy << indent() << "Look up " << e << std::endl;
     return _values[e];
@@ -99,32 +90,32 @@ struct DynamicMaxStrategy : public MaxStrategy<Domain> {
 private:
   void solve(const MaxExpression<Domain>& x) {
     if (!_stable.contains(x)) {
+      std::cerr << indent() << x.id() << std::endl; 
       _stable.insert(x);
       log::strategy << indent() << "Stabilise " << x << std::endl;
 
       stack_depth++; 
       DependencyAssignment assignment(*this, *_rho, x);
       DependencyStrategy depStrat(*this, x);
-      unsigned int val = x.bestStrategy(assignment, depStrat);
+      unsigned int val = x.bestStrategy(assignment, depStrat, _values[x]);
       stack_depth--;
 
       if (val != _values[x]) {
+        std::cerr << indent() << "-" << std::endl;
         log::strategy << x << " => " << *x.arguments()[val] << std::endl;
 
-        IdSet<MaxExpression<Domain> > oldInfluence = _influence[x];
-        //_influence[x].clear();
         _values[x] = val;
-        _changed = true;
 
         _rho->invalidate(*_system.varFromExpr(x));
         
 	//_rho->stabilise();
 
-        _stable.filter(oldInfluence);
-
+        IdSet<MaxExpression<Domain> > infl = _influence[x];
+        _stable.filter(infl); 
+        
         for (typename IdSet<MaxExpression<Domain> >::iterator
-               it = oldInfluence.begin(),
-               end = oldInfluence.end();
+               it = infl.begin(),
+               end = infl.end();
              it != end;
              ++it) {
           solve(_system.maxExpression(*it));
@@ -150,6 +141,7 @@ private:
     }
     const Domain operator[](const Variable<Domain>& var) {
       // solve the strategy for this variable, too
+      // recursive magic!
       _strat.solve(*_strat._system[var]);
       _strat._influence[*_strat._system[var]].insert(_expr);
       return _rho[var];
@@ -186,7 +178,6 @@ private:
   IdMap<MaxExpression<Domain>,unsigned int> _values;
   IdSet<MaxExpression<Domain> > _stable;
   IdMap<MaxExpression<Domain>,IdSet<MaxExpression<Domain> > > _influence;
-  bool _changed;
 };
 
 
@@ -200,28 +191,12 @@ struct Solver {
   }
 
   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
-
+      MaxExpression<Domain>& rhs = *_system[var];
+    // this will automatically work sufficiently to get the final
+    // strategy for this variable's RHS
     _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());
-    */
-
+    // this will automatically solve for the value of the RHS, if required
     return _rho[var];
   }
 private:
diff --git a/impl/VariableAssignment.hpp b/impl/VariableAssignment.hpp
index 2e081e6..e575d60 100644
--- a/impl/VariableAssignment.hpp
+++ b/impl/VariableAssignment.hpp
@@ -34,13 +34,6 @@ struct DynamicVariableAssignment : public VariableAssignment<Domain> {
     return _values[var];
   }
 
-  /*void stabilise() {
-    if (!_unstable.empty()) {
-      Variable<Domain>& var = _system.variable(*_unstable.begin());
-      solve(var);
-    }
-    }*/
-
   void invalidate(const Variable<Domain>& x) {
     if (!_unstable.contains(x)) {
       log::fixpoint << indent() << "Invalidating " << x << std::endl;
diff --git a/impl/main.cpp b/impl/main.cpp
index 1fed389..be9cc82 100644
--- a/impl/main.cpp
+++ b/impl/main.cpp
@@ -159,8 +159,7 @@ int main (int argc, char* argv[]) {
     }
   } else {
     for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
-      Variable<ZBar>& var = system.variable(i);
-      solver.solve(var);
+      solver.solve(system.variable(i));
     }
   }
   clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &finish);
diff --git a/impl/systems/test.eqns b/impl/systems/test.eqns
index a3b521d..a320049 100644
--- a/impl/systems/test.eqns
+++ b/impl/systems/test.eqns
@@ -1,19 +1,19 @@
 i-6[0] = max(-inf, 0)
 neg-i-6[0] = max(-inf, 0)
-neg-i-1-pre = max(-inf, guard(add(min(neg-i-6[0], inf), min(i-6[0], inf)), 0, neg-i-6[0]), guard(add(min(neg-i-2[0], inf), min(i-2[0], inf)), 0, neg-i-2[0]))
-i-1-pre = max(-inf, guard(add(min(neg-i-6[0], inf), min(i-6[0], inf)), 0, i-6[0]), guard(add(min(neg-i-2[0], inf), min(i-2[0], inf)), 0, i-2[0]))
-neg-i-5-pre = max(-inf, guard(add(min(neg-i-1-pre, inf), min(i-1-pre, 2)), 0, neg-i-1-pre))
-i-5-pre = max(-inf, guard(add(min(neg-i-1-pre, inf), min(i-1-pre, 2)), 0, min(2, i-1-pre)))
-neg-i-0-pre = max(-inf, guard(add(min(neg-i-1-pre, -3), min(i-1-pre, inf)), 0, min(-3, neg-i-1-pre)))
-i-0-pre = max(-inf, guard(add(min(neg-i-1-pre, -3), min(i-1-pre, inf)), 0, i-1-pre))
-neg-i-4-pre = max(-inf, guard(add(min(neg-i-5-pre, inf), min(i-5-pre, 1)), 0, neg-i-5-pre))
-i-4-pre = max(-inf, guard(add(min(neg-i-5-pre, inf), min(i-5-pre, 1)), 0, min(1, i-5-pre)))
-neg-i-3-pre = max(-inf, guard(add(min(neg-i-5-pre, -2), min(i-5-pre, inf)), 0, min(-2, neg-i-5-pre)))
-i-3-pre = max(-inf, guard(add(min(neg-i-5-pre, -2), min(i-5-pre, inf)), 0, i-5-pre))
+neg-i-1-pre = max(-inf, neg-i-6[0], neg-i-2[0])
+i-1-pre = max(-inf, i-6[0], i-2[0])
+neg-i-5-pre = max(-inf, neg-i-1-pre)
+i-5-pre = max(-inf, min(2, i-1-pre))
+neg-i-0-pre = max(-inf, min(-3, neg-i-1-pre))
+i-0-pre = max(-inf, i-1-pre)
+neg-i-4-pre = max(-inf, neg-i-5-pre)
+i-4-pre = max(-inf, min(1, i-5-pre))
+neg-i-3-pre = max(-inf, min(-2, neg-i-5-pre))
+i-3-pre = max(-inf, i-5-pre)
 i-4[0] = max(-inf, add(1, i-4-pre))
 neg-i-4[0] = max(-inf, add(-1, neg-i-4-pre))
-neg-i-2-pre = max(-inf, guard(add(min(neg-i-4[0], inf), min(i-4[0], inf)), 0, neg-i-4[0]), guard(add(min(neg-i-3[0], inf), min(i-3[0], inf)), 0, neg-i-3[0]))
-i-2-pre = max(-inf, guard(add(min(neg-i-4[0], inf), min(i-4[0], inf)), 0, i-4[0]), guard(add(min(neg-i-3[0], inf), min(i-3[0], inf)), 0, i-3[0]))
+neg-i-2-pre = max(-inf, neg-i-4[0], neg-i-3[0])
+i-2-pre = max(-inf, i-4[0], i-3[0])
 i-3[0] = max(-inf, 10)
 neg-i-3[0] = max(-inf, -10)
 i-2[0] = max(-inf, add(1, i-2-pre))
diff --git a/impl/test/1.eqns b/impl/test/1.eqns
index 0cdfd24..34c51de 100644
--- a/impl/test/1.eqns
+++ b/impl/test/1.eqns
@@ -1,3 +1,3 @@
-x = max(0, min(-1 + x, y))
 y = max(0, 5 + x, x)
 z = max(0, 1 + z, 0 + x)
+x = max(0, min(-1 + x, y))
diff --git a/impl/test/10.soln b/impl/test/10.soln
index 20a47ca..238b7d5 100644
--- a/impl/test/10.soln
+++ b/impl/test/10.soln
@@ -1,9 +1,9 @@
-x = 0
-w = 0
-y = 0
-z = 0
-u = 0
 a = 0
 b = 0
 c = 0
 d = 0
+u = 0
+w = 0
+x = 0
+y = 0
+z = 0
diff --git a/impl/test/7.soln b/impl/test/7.soln
index 0d85468..2c9b183 100644
--- a/impl/test/7.soln
+++ b/impl/test/7.soln
@@ -1,8 +1,8 @@
-x = 0
-y = 0
 a = 0
 b = 0
 c = 0
 d = 0
 e = 0
 f = 0
+x = 0
+y = 0
diff --git a/impl/test/8.soln b/impl/test/8.soln
index 1945057..73d26df 100644
--- a/impl/test/8.soln
+++ b/impl/test/8.soln
@@ -1,4 +1,4 @@
-x = 0
 w = 0
+x = 0
 y = 0
 z = 0
diff --git a/impl/test/9.soln b/impl/test/9.soln
index 616c5e5..7116cf4 100644
--- a/impl/test/9.soln
+++ b/impl/test/9.soln
@@ -1,5 +1,5 @@
-x = 0
+u = 0
 w = 0
+x = 0
 y = 0
 z = 0
-u = 0
diff --git a/impl/test/run b/impl/test/run
index 169edda..d15fb68 100644
--- a/impl/test/run
+++ b/impl/test/run
@@ -7,15 +7,17 @@ FAILED=0
 echo "Testing binary: $1 in directory $DIR"
 while [ -f "$DIR/$NUM.eqns" ]
 do
+  cat "$DIR/$NUM.soln" | sort > "/tmp/$NUM.soln.tmp"
+  mv "/tmp/$NUM.soln.tmp" "$DIR/$NUM.soln" 2> /dev/null
   OUTPUT=$(timeout 5s $1 "$DIR/$NUM.eqns" 2> /dev/null)
   if [ $? -eq 124 ]; then
     OUTPUT="did not terminate"
   fi
-  DIFF=$(echo "$OUTPUT" | diff - "$DIR/$NUM.soln")
+  DIFF=$(echo "$OUTPUT" | sort | diff - "$DIR/$NUM.soln")
   if [ ! -z "$DIFF" ]; then
     echo "=================="
     echo "Test #$NUM failed:"
-    echo "$OUTPUT" | sdiff - "$DIR/$NUM.soln"
+    echo "$OUTPUT" | sort | sdiff - "$DIR/$NUM.soln"
     echo
     FAILED=$(($FAILED + 1))
   fi
diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex
index 66d5b4a..3d00b86 100644
--- a/tex/thesis/contribution/contribution.tex
+++ b/tex/thesis/contribution/contribution.tex
@@ -130,11 +130,31 @@ algorithm is presented in Listing \ref{algo:kleene}.
 For each iteration the entire system is evaluated, irrespective of
 whether it could possibly have changed value. This results in a
 considerable inefficiency in practice, requiring the evaluation of
-$O(n^3)$ right-hand-sides, and thus an approach which can evaluate
-smaller portions of the system in each iteration would be a
-significant improvement.
+many right-hand-sides repeatedly for the same value. Thus an
+approach which can evaluate smaller portions of the system in each
+iteration would be a significant improvement.
+
+An additional deficiency of Kleene iteration is that it is not
+guaranteed to terminate. In some cases Kleene iteration must iterate
+an infinite number of times in order to reach a fixpoint. An example
+system is presented as Figure \ref{fig:kleene-infinite}. In this case
+$x$ will take the value of $0$ in the first iteration, then $y$ will
+evaluate to $-1$. In the next iteration $x$ will also take the value
+$-1$, thereby requiring $y$ to take the value $-2$. This will continue
+without bound, resulting in the Kleene iteration never reaching the
+greatest fixpoint of $\{ x \mapsto -\infty, y \mapsto -\infty \}$.
+
+\begin{figure}[H]
+  \begin{align*}
+    x &= \min(0, x) \\
+    y &= x - 1
+  \end{align*}
+  \caption{An example equation system for which Kleene iteration will
+    not terminate}
+  \label{fig:kleene-infinite}
+\end{figure}
 
-\subsection{W-DFS algorithm} \ref{sec:wdfs}
+\subsection{W-DFS algorithm} \label{sec:wdfs}
 
 The W-DFS algorithm presented by Seidl, et al. takes into account some
 form of data-dependencies as it solves the system. This gives it the
@@ -255,7 +275,7 @@ problem it is possible
 \end{algorithm}
 
 
-\subsection{Adapted W-DFS algorithm} \ref{sec:adapted-wdfs}
+\subsection{Adapted W-DFS algorithm} \label{sec:adapted-wdfs}
 
 This, then, allows us to use the W-DFS algorithm to re-evaluate only
 those parts of the strategy which have changed. Listing