From e207a8fec1bae01068bdb3a27a2090a4af5f8cb2 Mon Sep 17 00:00:00 2001
From: Carlo Zancanaro <carlo@carlo-laptop>
Date: Wed, 31 Oct 2012 00:50:29 +1100
Subject: Remove _var_influence and do some writeup

_var_influence was really just duplicating data that was available
elsewhere, so I got rid of it.

I also did some writing about the algorithm and stuff for the thesis.
---
 tex/thesis/contribution/contribution.tex | 221 +++++++++++++++++++++----------
 1 file changed, 154 insertions(+), 67 deletions(-)

(limited to 'tex/thesis/contribution/contribution.tex')

diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex
index 7d12299..66d5b4a 100644
--- a/tex/thesis/contribution/contribution.tex
+++ b/tex/thesis/contribution/contribution.tex
@@ -134,7 +134,7 @@ $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.
 
-\subsection{W-DFS algorithm}
+\subsection{W-DFS algorithm} \ref{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 +255,7 @@ problem it is possible
 \end{algorithm}
 
 
-\subsection{Adapted W-DFS algorithm}
+\subsection{Adapted W-DFS algorithm} \ref{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
@@ -327,17 +327,26 @@ be evaluated.
 The new \emph{Local Demand-driven Strategy Improvement} algorithm,
 \emph{LDSI}, seeks to do this. By adding an ``invalidate''
 function to both W-DFS instances we provide an interface for the two
-sides of the algorithm to indicate which values have changed. The
-fixpoint-iteration operation can then be provided with a ``stabilise''
-function to solve a partially-unstable system.
+sides of the algorithm to indicate which values have changed and
+``destabilise'' that portion of the system.
 
 This essentially results in a $\max$-strategy iteration which, at each
 strategy-improvement step, invalidates a portion of the current
-fixpoint iteration. The fixpoint iteration then re-stabilises itself
-by evaluating what values have been changed before returning control
-to the $\max$-strategy iteration to change the system again. The back
-and forth continues in this way until the $\max$-strategy can not
-improve the strategy any further.
+fixpoint iteration which may depend on the changed strategy. The
+fixpoint iteration then re-stabilises itself by evaluating what values
+have been changed, but only when such values are requested by the
+$\max$-strategy iteration. The $\max$-strategy can continue as normal,
+invalidating the fixpoint-iteration as required, and simply assume
+that the fixpoint-iteration will provide it with the correct values
+from the greatest fixpoint.
+
+
+This entire approach is demand driven, and so any necessary evaluation
+is delayed until the point when it is actually required. Additionally,
+if it is not necessary to evaluate a particular right hand side in
+order to make a decision then the algorithm will attempt to avoid
+evaluating it.
+
 
 
 
@@ -356,23 +365,23 @@ correctness of this new algorithm is argued in
   \begin{algorithmic}
     \Globals
     \begin{tabularx}{0.9\textwidth}{rX}
-      $V$ & $\{X \to \D\}$ - a mapping from variables to values,
+      $D$ & $X \to \D$ - a mapping from variables to values,
       starting at $\{ x \mapsto \infty \}$ \\
 
-      $I_{X,X}$ & $\{X \to X\}$ - a mapping from a variable to the
+      $\sigma$ & $E_{\max} \to E$ - a mapping from $\max$-expressions
+      to their sub-expressions (a $\max$-strategy) \\
+
+      $I_{X,X}$ & $X \to X$ - a mapping from a variable to the
       variables it influences \\
 
-      $I_{\max,\max}$ & $\{E_{\max} \to E_{\max}\}$ - a mapping from a
+      $I_{\max,\max}$ & $E_{\max} \to E_{\max}$ - a mapping from a
       $\max$-expression to the $\max$-expressions it influences \\
 
-      $I_{X,\max}$ & $\{X \to E_{\max}\}$ - a mapping from a variable
-      to the $\max$-expressions it influences \\
-
       $U_{X}$ & The set of all variables whose values have not
       stabilised to a final fixpoint value (unstable variables) \\
 
-      $U_{\max}$ & The set of all $\max$ expressions whose strategies
-      have not yet stabilised to their final strategy (unstable
+      $S_{\max}$ & The set of all $\max$ expressions whose strategies
+      have stabilised to their final strategy (stable
       $\max$-expressions) \\
 
       $\varepsilon$ & The equation system, a mapping from a variable
@@ -384,12 +393,27 @@ correctness of this new algorithm is argued in
   \label{algo:ldsi:fixpoint:globals}
 \end{algorithm}
 
+A few things are of particular note for the global variables. In
+particular the difference between $U_X$ being an unstable set and
+$S_{\max}$ being a stable set. In reality these two are entirely
+equivalent, but because the fixpoint-iteration will be started as
+being entirely ``stable'' (with values of $-\infty$) it is of more
+practical benefit to avoid the extra work populating the ``stable''
+set by instead storing unstable values.
+
+The other variables are just the state from each of the previous
+algorithms for intelligently performing $\max$-strategy iteration and
+fixpoint iteration (as were presented in Sections \ref{sec:wdfs}
+and \ref{sec:adapted-wdfs}). $D$ and $I_{X,X}$ are taken from the
+W-DFS algorithm, while $\sigma$ and $I_{\max,\max}$ are taken from the
+Adapted W-DFS algorithm.
+
 
 
 
 \begin{algorithm}[H]
   \begin{algorithmic}
-    \Function {evalfixpoint} {$x$, $y$}
+    \Function {evalfixpoint} {$x \in X$, $y \in X$}
       \State $\solve \fixpoint(y)$
       \State $I_{X,X}[y] = I_{X,X}[y] \cup \{x\}$
       \State \Return $D[y]$
@@ -399,9 +423,17 @@ correctness of this new algorithm is argued in
   \label{algo:ldsi:fixpoint:eval}
 \end{algorithm}
 
+This procedure is exactly the same as the equivalent method in the
+W-DFS algorithm. It allows us to more easily track dependencies
+between fixpoint variables by injecting this function as our
+variable-lookup function. It then both calculates a new value for the
+variable (the $\solve \fixpoint$ call) and notes the dependency
+between $x$ and $y$.
+
 \begin{algorithm}[H]
   \begin{algorithmic}
-    \Function {invalidatefixpoint} {$x$}
+    \Function {invalidatefixpoint} {$x \in X$}
+    \Comment{Invalidate a fixpoint variable}
     \If {$x \not \in U_X$}
       \State $U_X = U_X \cup \{x\}$
       \State $D[x] = \infty$
@@ -418,6 +450,16 @@ correctness of this new algorithm is argued in
   \label{algo:ldsi:fixpoint:invalidate}
 \end{algorithm}
 
+This procedure is not called in the fixpoint iteration process, but is
+rather the method by which the $\max$-strategy iteration can
+communicate with the fixpoint-iteration. It allows the $\max$-strategy
+iteration to inform the fixpoint-iteration which values have changed
+and will require re-evaluation. This makes it possible to only
+re-evaluate a partial system (the solving of which is also be delayed
+until requested by the $\solve \fixpoint$ procedure).
+
+
+
 \begin{algorithm}[H]
   \begin{algorithmic}
     \Function {solvefixpoint} {$x$}
@@ -425,7 +467,7 @@ correctness of this new algorithm is argued in
     \If {$x \in U_X$}
       \State $f = \system[x]$
       \State $U_X = U_X \backslash \{x\}$
-      \State $v = f( \lambda y . \eval(x, y) )$
+      \State $v = \sigma(\system[x])( \lambda y . \eval \fixpoint(x, y) )$
       \If {$v \ne D[x]$}
         \State $D = \{ x \mapsto v \} \oplus D$
         \State $W = I_{X,X}[x]$
@@ -446,62 +488,110 @@ correctness of this new algorithm is argued in
 
 After an evaluation of the $\solve \fixpoint$ procedure, the variable
 supplied as its argument will have been stabilised within the current
-$\max$-strategy.
+$\max$-strategy. This means that it will have taken on the same value
+as it would take in the greatest fixpoint of this system. Because the
+$\solve \fixpoint$ calls need not be made immediately it's possible
+for a variable to be invalidated by several $\max$-strategy
+improvements without being re-evaluated.
+
 
-After an evaluation of the $\stabilise \fixpoint$ procedure all
-currently ``unstable'' variables in the current fixpoint will be
-solved. This correlates to performing an entire fixpoint-iteration for
-the greatest-fixpoint of the unstable portion of the equation
-system. This is meant to be used to perform a sufficient
-fixpoint-iteration to allow for the next $\max$-strategy improvement
-step, but this relies on the $\max$-strategy solver to correctly
-invalidate the fixpoint-iteration portion of the algorithm.
 
 
 \begin{algorithm}[H]
   \begin{algorithmic}
-    \Function {evalstrategy} {$x$, $y$}
-    \Comment{Evaluate $y$ for its value and note that when $y$
-      changes, $x$ must be re-evaluated}
-      \State $\solve(y)$
-      \State $I[y] = I[y] \cup \{x\}$
+    \Function {evalstrategy} {$x \in E_{\max}$, $y \in E_{\max}$}
+      \Comment{Evaluate $y$ for its value and note that when $y$
+        changes, $x$ must be re-evaluated}
+      \State $\solve \strategy(y)$
+      \State $I_{\max,\max}[y] = I_{\max,\max}[y] \cup \{x\}$
       \State \Return $\sigma[y]$
     \EndFunction
+    \Function {evalstrategyfixpoint} {$x \in E_{\max}$, $y \in X$}
+      \Comment{Evaluate $y$ for its value and note that when $y$
+        changes, $x$ must be re-evaluated}
+      \State $\solve \fixpoint(y)$
+      \State $I_{\max,\max}[y] = I_{\max,\max}[\system[y]] \cup \{x\}$
+      \State \Return $D[y]$
+    \EndFunction
+  \end{algorithmic}
+  \label{algo:ldsi:strategy:eval}
+  \caption{Evaluate a portion of the $\max$-strategy and note a
+    dependency}
+\end{algorithm}
+
+The $\eval \strategy$ function is essentially the same as the $\eval
+\fixpoint$ function, except that it notes the dependencies in a
+different variable, $I_{\max,\max}$. This is because the dependency
+information for the $\max$-strategy iteration is entirely separate to
+that of the fixpoint iteration.
+
+The $\solve \fixpoint$ calls in $\eval \strategy \fixpoint$ are
+top-level calls, meaning that upon their return we know that $D$
+contains the value it would take in the greatest fixpoint of the
+current strategy $\sigma$. This function, therefore, acts as a simple
+intermediate layer between the fixpoint-iteration and the
+$\max$-strategy iteration to allow for dependencies to be tracked.
 
+
+\begin{algorithm}[H]
+  \begin{algorithmic}
     \Function {invalidatestrategy} {$x \in X$} \Comment{$x$ is a
         \emph{variable}}
-      \If {$x \not \in U_X$}
-        \State $U_X = U_X \cup \{x\}$
-        \State $W = I[x]$
-        \State $I[x] = \emptyset$
-        \For {$v \in W$}
-          \State $\invalidate \fixpoint(v)$
+      \For {$v \in I_{\max,\max}(\system[x])$} \Comment{$v$ is
+        influenced by $x$}
+        \State $\invalidate \strategy (v)$
+      \EndFor
+    \EndFunction
+
+    \Function {invalidatestrategy} {$x \in E_{\max}$} \Comment{$x$ is
+      a \emph{$\max$-expression}}
+      \If {$x \in S_{\max}$}
+        \State $S_{\max} = S_{\max} \backslash \{x\}$
+        \For {$v \in I_{\max,\max}$} \Comment {$v$ is influenced by $x$}
+          \State $\invalidate \strategy (v)$
         \EndFor
       \EndIf
     \EndFunction
+  \end{algorithmic}    
+  \label{algo:ldsi:strategy:invalidate}
+  \caption{Evaluate a portion of the $\max$-strategy and note a
+    dependency}
+\end{algorithm}
+
+Invalidating the $\max$-strategy iteration is slightly more
+complicated than invalidating the fixpoint iteration stage. As the
+invalidation interface consists of variables, we must first translate
+a variable into a $\max$-expression (which is easily done by looking
+it up in the equation system). We must then invalidate the strategies
+for each variable which depends on this resultant
+$\max$-expression. The invalidation for $\max$-expressions consists of
+transitively invalidating everything which depends on the
+$\max$-expression, as well as itself.
+
+
 
-    \Function {solvestrategy} {$x$}
+\begin{algorithm}[H]
+  \begin{algorithmic}    
+    \Function {solvestrategy} {$x \in E_{\max}$}
     \Comment{Solve a specific variable and place its value in $\sigma$}
-    \If {$x \not \in \stable$}
-      \State $f = \system[x]$
-      \State $\stable = \stable \cup \{x\}$
-      \State $v = bestStrategy(f, \sigma(), \lambda y . \eval(x, y))$
-      \If {$v \ne \sigma[x]$}
-        \State $\sigma = \{ x \mapsto v \} \oplus \sigma$
-        \State $W = I[x]$
-        \State $I(x) = \emptyset$
-        \State $\invalidate \fixpoint(\mathsf{lookupVarFor}(x))$
-        \State $\stable = \stable \backslash W$
-        \For {$v \in W$}
+    \If {$x \not \in S_{\max}$}
+      \State $S_{\max} = S_{\max} \cup \{x\}$
+      \State $\sigma_{dynamic} = \lambda y . \eval \strategy(x,y)$
+      \State $e = P_{\max}(\sigma_{dynamic},
+                          \lambda y . \eval \strategy \fixpoint(x, y))(x)$
+      \If {$e \ne \sigma[x]$}
+        \State $\sigma = \{ x \mapsto e \} \oplus \sigma$
+        \State $\invalidate \fixpoint(\system^{-1}(x))$
+        \State $S_{\max} = S_{\max} \backslash I[x]$
+        \For {$v \in I[x]$}
           \State $\solve(v)$
         \EndFor
       \EndIf
     \EndIf
     \EndFunction
   \end{algorithmic}
-
   \caption{The $\max$-strategy portion of the Combined W-DFS.}
-  \label{algo:combined-max}
+  \label{algo:ldsi:solve}
 \end{algorithm}
 
 
@@ -516,15 +606,12 @@ combination algorithm is correct. For this it is sufficient to show
 that the invalidate calls in both directions preserve the correctness
 of the original algorithm.
 
-// TODO finish this.
-General idea:
-\begin{itemize}
-  \item
-    Invalidate calls from fixpoint $\to$ max strategy are correct if
-    the calls the other way are, because it completely re-solves the
-    equations
-  \item
-    Invalidate calls from max strategy $\to$ fixpoint are correct
-    because they effectively ``reset'' that part of the system,
-    creating it to be entirely re-calculated.
-\end{itemize}
+The fixpoint iteration step invalidates anything that \emph{might}
+depend on $x$ while it invalidates $x$, thereby ensuring that any
+further calls to $\solve \fixpoint$ will result in a correct value for
+the given strategy.
+
+The strategy-iteration step invalidates anything that \emph{might}
+depend on $\system[x]$ while it invalidates $x$, thereby ensuring that
+any further calls to $\solve \strategy$ will result in a correct value
+for the given strategy.
-- 
cgit v1.2.3


From b7eaa99578037789a337c5061c0ea8ee3150b63c Mon Sep 17 00:00:00 2001
From: "Zancanaro; Carlo" <czan8762@plang3.cs.usyd.edu.au>
Date: Thu, 1 Nov 2012 18:06:13 +1100
Subject: A bunch of fixes to the solver, and moving it in to clang.

Also some contribution writing stuff.

Basically: lots of work.
---
 .../Analysis/Analyses/IntervalSolver/Complete.hpp  |   7 +-
 .../Analyses/IntervalSolver/EquationSystem.hpp     |  12 +-
 .../Analyses/IntervalSolver/Expression.hpp         |  82 +++++++++---
 .../Analysis/Analyses/IntervalSolver/IdMap.hpp     |  13 +-
 .../Analysis/Analyses/IntervalSolver/IdSet.hpp     |   4 +
 .../clang/Analysis/Analyses/IntervalSolver/Log.hpp |  18 +--
 .../Analyses/IntervalSolver/MaxStrategy.hpp        | 146 ++++++++++++++++-----
 .../Analysis/Analyses/IntervalSolver/Operator.hpp  |  11 +-
 .../Analyses/IntervalSolver/VariableAssignment.hpp |  83 +++++++-----
 clang/lib/Analysis/Interval.cpp                    |  35 +----
 impl/Expression.hpp                                |   3 +-
 impl/MaxStrategy.hpp                               |  55 +++-----
 impl/VariableAssignment.hpp                        |   7 -
 impl/main.cpp                                      |   3 +-
 impl/systems/test.eqns                             |  24 ++--
 impl/test/1.eqns                                   |   2 +-
 impl/test/10.soln                                  |  10 +-
 impl/test/7.soln                                   |   4 +-
 impl/test/8.soln                                   |   2 +-
 impl/test/9.soln                                   |   4 +-
 impl/test/run                                      |   6 +-
 tex/thesis/contribution/contribution.tex           |  30 ++++-
 22 files changed, 330 insertions(+), 231 deletions(-)

(limited to 'tex/thesis/contribution/contribution.tex')

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

