14 files changed, 730 insertions, 108 deletions

diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp
index 57dcdeb..f4026dd 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp
@@ -10,6 +10,9 @@ template<typename Domain>
 struct MaxStrategy {
   virtual ~MaxStrategy() { }
   virtual unsigned int get(const MaxExpression<Domain>& e) const = 0;
+  virtual unsigned int get(const MaxExpression<Domain>& e) {
+    return const_cast<const MaxStrategy*>(this)->get(e);
+  }
 };
 
 unsigned int stack_depth = 1;
@@ -38,20 +41,38 @@ struct DynamicMaxStrategy : public MaxStrategy<Domain> {
       _influence(system.maxExpressionCount(),
                  IdSet<MaxExpression<Domain> >(system.maxExpressionCount())),
       _var_influence(system.variableCount(),
-                     IdSet<MaxExpression<Domain> >(system.maxExpressionCount()))
+                     IdSet<MaxExpression<Domain> >(system.maxExpressionCount())),
+      _frozen(false)
   {}
 
+  void freeze() {
+    _frozen = true;
+  }
+
+  void thaw() {
+    _frozen = false;
+  }
+
+  bool is_frozen() {
+    return _frozen;
+  }
+
   void setRho(DynamicVariableAssignment<Domain>& rho) {
     _rho = &rho;
   }
 
   unsigned int get(const MaxExpression<Domain>& e) const {
-    solve(e);
     return _values[e];
   }
 
-  void invalidate(const Variable<Domain>& v) const {
-    solver_log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl;
+  unsigned int get(const MaxExpression<Domain>& e) {
+    if (!_frozen)
+      solve(e);
+    return _values[e];
+  }
+
+  void invalidate(const Variable<Domain>& v) {
+    log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl; 
     _stable.filter(_var_influence[v]);
 
     IdSet<MaxExpression<Domain> > infl = _var_influence[v];
@@ -67,10 +88,10 @@ struct DynamicMaxStrategy : public MaxStrategy<Domain> {
   }
 
 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;
+      log::strategy << indent() << "Stabilise " << x << std::endl;
 
       stack_depth++;
       unsigned int val = x.bestStrategy(DependencyAssignment(*this, *_rho, x),
@@ -78,7 +99,7 @@ private:
       stack_depth--;
 
       if (val != _values[x]) {
-        solver_log::strategy << x << " => " << *x.arguments()[val] << std::endl;
+        log::strategy << x << " => " << *x.arguments()[val] << std::endl;
 
         IdSet<MaxExpression<Domain> > oldInfluence = _influence[x];
         _influence[x].clear();
@@ -96,15 +117,17 @@ private:
           solve(_system.maxExpression(*it));
         }
       } else {
-        solver_log::strategy << indent() << x << " did not change" << std::endl;
+        log::strategy << indent() << x << " did not change: "
+		      << x << " => " << *x.arguments()[val] << std::endl;
       }
     } else {
-      solver_log::strategy << indent() << x << " is stable" << std::endl;
+      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),
@@ -116,13 +139,13 @@ private:
       return _rho[var];
     }
   private:
-    const DynamicMaxStrategy& _strat;
+    DynamicMaxStrategy& _strat;
     VariableAssignment<Domain>& _rho;
     const MaxExpression<Domain>& _expr;
   };
 
   struct DependencyStrategy : public MaxStrategy<Domain> {
-    DependencyStrategy(const DynamicMaxStrategy& strat, const MaxExpression<Domain>& expr)
+    DependencyStrategy(DynamicMaxStrategy& strat, const MaxExpression<Domain>& expr)
       : _strat(strat),
         _expr(expr) {
     }
@@ -134,19 +157,57 @@ private:
       return _strat._values[e];
     }
   private:
-    const DynamicMaxStrategy& _strat;
+    DynamicMaxStrategy& _strat;
     const MaxExpression<Domain>& _expr;
   };
 
-private:
+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;
+  DynamicVariableAssignment<Domain>* _rho;
+  IdMap<MaxExpression<Domain>,unsigned int> _values;
+  IdSet<MaxExpression<Domain> > _stable;
+  IdMap<MaxExpression<Domain>,IdSet<MaxExpression<Domain> > > _influence;
+  IdMap<Variable<Domain>,IdSet<MaxExpression<Domain> > > _var_influence;
+  bool _frozen;
 };
 
+
+template<typename T>
+IdMap<Variable<T>,T> solve_for(const EquationSystem<T>& system) {
+  IdMap<Variable<T>,T> result(system.variableCount(), infinity<T>());
+
+  DynamicMaxStrategy<T> strategy(system);
+  DynamicVariableAssignment<T> rho(system, strategy, -infinity<T>());
+  strategy.setRho(rho);
+
+  bool changed;
+  do {
+    changed = false;
+
+    // improve strategy
+    rho.freeze();
+    strategy.thaw();
+    for (unsigned int i = 0; i < system.variableCount(); ++i) {
+      strategy.get(*system[system.variable(i)]);
+    }
+
+    // iterate fixpoint
+    strategy.freeze();
+    rho.thaw();
+    for (unsigned int i = 0; i < system.variableCount(); ++i) {
+      Variable<T>& var = system.variable(i);
+      T val = rho[var];
+      if (result[var] != val) {
+	result[var] = val;
+	changed = true;
+      }
+    }
+  } while(changed);
+
+  return result;
+}
+
+
 /*template<typename Domain>
 std::ostream& operator<<(std::ostream& cout, const MaxStrategy<Domain>& strat) {
   strat.print(cout);
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp
index ba5f650..2a63756 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp
@@ -8,6 +8,9 @@ template<typename Domain>
 struct VariableAssignment {
   virtual ~VariableAssignment() { }
   virtual const Domain& operator[](const Variable<Domain>&) const = 0;
+  virtual const Domain& operator[](const Variable<Domain>& x) {
+    return (*const_cast<const VariableAssignment*>(this))[x];
+  }
 };
 
 #include "EquationSystem.hpp"
@@ -19,46 +22,71 @@ 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>()),
+      _values(system.variableCount(), value),
       _stable(system.variableCount()),
       _influence(system.variableCount(),
-                 IdSet<Variable<Domain> >(system.variableCount()))
+                 IdSet<Variable<Domain> >(system.variableCount())),
+      _frozen(false)
   { }
 
+  void freeze() {
+    _frozen = true;
+  }
+
+  void thaw() {
+    _frozen = false;
+  }
+
+  bool is_frozen() {
+    return _frozen;
+  }
+
   const Domain& operator[](const Variable<Domain>& var) const {
-    solve(var);
     return _values[var];
   }
 
-  void invalidate(const Variable<Domain>& x) const {
-    solver_log::fixpoint << indent() << "Invalidating " << x << std::endl;
+  const Domain& operator[](const Variable<Domain>& var) {
+    if (!_frozen)
+      solve(var);
+    return _values[var];
+  }
+
+  void invalidate(const Variable<Domain>& x) {
+    log::fixpoint << indent() << "Invalidating " << x << std::endl;
     if (_stable.contains(x)) {
       _stable.remove(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 {
+  void solve(const Variable<Domain>& x) {
     if (!_stable.contains(x)) {
       _stable.insert(x);
-      solver_log::fixpoint << indent() << "Stabilise " << x << std::endl;
+      log::fixpoint << indent() << "Stabilise " << x << std::endl;
 
       stack_depth++;
-      if (!_system[x])
-        return;
-      Domain val = _system[x]->evalWithStrat(DependencyAssignment(*this, x),
-					     _strategy);
+      Domain val = _system[x]->eval(DependencyAssignment(*this, x),
+                                    _strategy);
       stack_depth--;
 
       if (val != _values[x]) {
-        solver_log::fixpoint << x << " = " << val << std::endl;
+        log::fixpoint << x << " = " << val << std::endl;
 
         IdSet<Variable<Domain> > oldInfluence = _influence[x];
         _influence[x].clear();
@@ -74,15 +102,17 @@ private:
           solve(_system.variable(*it));
         }
       } else {
-        solver_log::fixpoint << indent() << x << " did not change" << std::endl;
+        log::fixpoint << indent() << x << " did not change: "
+		      << x << " = " << val << std::endl;
       }
     } else {
-      solver_log::fixpoint << indent() << x << " is stable" << std::endl;
+      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];
@@ -90,15 +120,16 @@ private:
       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> > _stable;
+  IdMap<Variable<Domain>,IdSet<Variable<Domain> > > _influence;
+  bool _frozen;
 };
 
 #endif
diff --git a/clang/lib/Analysis/Interval.cpp b/clang/lib/Analysis/Interval.cpp
index ac96107..d005048 100644
--- a/clang/lib/Analysis/Interval.cpp
+++ b/clang/lib/Analysis/Interval.cpp
@@ -702,40 +702,24 @@ void IntervalAnalysis::runOnAllBlocks() {
     }
   }
 
-  std::vector<EqnExpr*> a;
-
-  a.push_back(&system.constant(-infinity<ZBar>()));
-  a.push_back(&system.constant(0));
-  system[system.variable("x")] = &system.maxExpression(a);
-  a.clear();
-  
-  system.variable("y");
-
-  a.push_back(&system.variable("x"));
-  a.push_back(&system.variable("z"));
-  EqnExpr* minExpr = &system.expression(new Maximum<ZBar>(), a);
-  a.clear();
-
-  a.push_back(&system.constant(-infinity<ZBar>()));
-  a.push_back(minExpr);
-  system[system.variable("y")] = &system.maxExpression(a);
-  a.clear();
-
-  a.push_back(&system.constant(-infinity<ZBar>()));
-  a.push_back(&system.variable("y"));
-  system[system.variable("z")] = &system.maxExpression(a);
-
-  llvm::errs() << toString(system) << "\n";
-
   system.indexMaxExpressions();
-  DynamicMaxStrategy<ZBar> strategy(system);
-  DynamicVariableAssignment<ZBar> rho(system, strategy);
-  strategy.setRho(rho);
 
+  IdMap<EqnVar,ZBar> result = solve_for(system);
   for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
+    EqnVar& var = system.variable(i);
+    cout << var.name() << " = " << result[var] << endl;
+  }
+
+  /*
+    DynamicMaxStrategy<ZBar> strategy(system);
+    DynamicVariableAssignment<ZBar> rho(system, strategy);
+    strategy.setRho(rho);
+    
+    for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
     EqnVar& var = system.variable(size - i - 1);
     llvm::errs() << toString(var.name()) << " = " << toString(rho[var]) << "\n";
-  }
+    }
+  */
 }
 
 
diff --git a/impl/Complete.hpp b/impl/Complete.hpp
index 38b637e..336ab24 100644
--- a/impl/Complete.hpp
+++ b/impl/Complete.hpp
@@ -55,7 +55,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/impl/Expression.hpp b/impl/Expression.hpp
index 0f3717f..cba9582 100644
--- a/impl/Expression.hpp
+++ b/impl/Expression.hpp
@@ -27,6 +27,10 @@ struct Expression {
     return NULL;
   }
 
+  virtual MaxExpression<Domain>* toMaxExpression() {
+    return NULL;
+  }
+
   virtual Domain eval(const VariableAssignment<Domain>&) const = 0;
   virtual Domain eval(const VariableAssignment<Domain>& rho,
                       const MaxStrategy<Domain>&) const {
@@ -106,6 +110,10 @@ struct OperatorExpression : public Expression<Domain> {
     return _operator.eval(argumentValues);
   }
 
+  std::vector<Expression<Domain>*>& arguments() {
+    return _arguments;
+  }
+
   const std::vector<Expression<Domain>*>& arguments() const {
     return _arguments;
   }
@@ -137,7 +145,7 @@ struct OperatorExpression : public Expression<Domain> {
   private:
   const Operator<Domain>& _operator;
   protected:
-  const std::vector<Expression<Domain>*> _arguments;
+  std::vector<Expression<Domain>*> _arguments;
 };
 
 template<typename Domain>
@@ -145,6 +153,10 @@ 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;
   }
diff --git a/impl/MaxStrategy.hpp b/impl/MaxStrategy.hpp
index 96d0492..ba7cc11 100644
--- a/impl/MaxStrategy.hpp
+++ b/impl/MaxStrategy.hpp
@@ -10,6 +10,9 @@ template<typename Domain>
 struct MaxStrategy {
   virtual ~MaxStrategy() { }
   virtual unsigned int get(const MaxExpression<Domain>& e) const = 0;
+  virtual unsigned int get(const MaxExpression<Domain>& e) {
+    return const_cast<const MaxStrategy*>(this)->get(e);
+  }
 };
 
 unsigned int stack_depth = 1;
@@ -39,9 +42,22 @@ struct DynamicMaxStrategy : public MaxStrategy<Domain> {
       _influence(system.maxExpressionCount(),
                  IdSet<MaxExpression<Domain> >(system.maxExpressionCount())),
       _var_influence(system.variableCount(),
-                     IdSet<MaxExpression<Domain> >(system.maxExpressionCount()))
+                     IdSet<MaxExpression<Domain> >(system.maxExpressionCount())),
+      _frozen(false)
   {}
 
+  void freeze() {
+    _frozen = true;
+  }
+
+  void thaw() {
+    _frozen = false;
+  }
+
+  bool is_frozen() {
+    return _frozen;
+  }
+
   void setRho(DynamicVariableAssignment<Domain>& rho) {
     _rho = &rho;
   }
@@ -71,7 +87,7 @@ struct DynamicMaxStrategy : public MaxStrategy<Domain> {
   }
 
 private:
-  void solve(const MaxExpression<Domain>& x) const {
+  void solve(const MaxExpression<Domain>& x) {
     if (!_stable.contains(x)) {
       _stable.insert(x);
       log::strategy << indent() << "Stabilise " << x << std::endl;
@@ -121,7 +137,7 @@ private:
   }
 
   struct DependencyAssignment : public VariableAssignment<Domain>{
-    DependencyAssignment(const DynamicMaxStrategy& strat,
+    DependencyAssignment(DynamicMaxStrategy& strat,
                          VariableAssignment<Domain>& rho,
                          const MaxExpression<Domain>& expr)
       : _strat(strat),
@@ -133,7 +149,7 @@ private:
       return _rho[var];
     }
   private:
-    const DynamicMaxStrategy& _strat;
+    DynamicMaxStrategy& _strat;
     VariableAssignment<Domain>& _rho;
     const MaxExpression<Domain>& _expr;
   };
@@ -163,7 +179,7 @@ private:
   };
 
   struct DependencyStrategy : public MaxStrategy<Domain> {
-    DependencyStrategy(const DynamicMaxStrategy& strat, const MaxExpression<Domain>& expr)
+    DependencyStrategy(DynamicMaxStrategy& strat, const MaxExpression<Domain>& expr)
       : _strat(strat),
         _expr(expr) {
     }
@@ -175,20 +191,58 @@ private:
       return _strat._values[e];
     }
   private:
-    const DynamicMaxStrategy& _strat;
+    DynamicMaxStrategy& _strat;
     const MaxExpression<Domain>& _expr;
   };
 
 private:
   mutable bool _frozen;
   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;
+  DynamicVariableAssignment<Domain>* _rho;
+  IdMap<MaxExpression<Domain>,unsigned int> _values;
+  IdSet<MaxExpression<Domain> > _stable;
+  IdMap<MaxExpression<Domain>,IdSet<MaxExpression<Domain> > > _influence;
+  IdMap<Variable<Domain>,IdSet<MaxExpression<Domain> > > _var_influence;
+  bool _frozen;
 };
 
+
+template<typename T>
+IdMap<Variable<T>,T> solve_for(const EquationSystem<T>& system) {
+  IdMap<Variable<T>,T> result(system.variableCount(), infinity<T>());
+
+  DynamicMaxStrategy<T> strategy(system);
+  DynamicVariableAssignment<T> rho(system, strategy, -infinity<T>());
+  strategy.setRho(rho);
+
+  bool changed;
+  do {
+    changed = false;
+
+    // improve strategy
+    rho.freeze();
+    strategy.thaw();
+    for (unsigned int i = 0; i < system.variableCount(); ++i) {
+      strategy.get(*system[system.variable(i)]);
+    }
+
+    // iterate fixpoint
+    strategy.freeze();
+    rho.thaw();
+    for (unsigned int i = 0; i < system.variableCount(); ++i) {
+      Variable<T>& var = system.variable(i);
+      T val = rho[var];
+      if (result[var] != val) {
+	result[var] = val;
+	changed = true;
+      }
+    }
+  } while(changed);
+
+  return result;
+}
+
+
 /*template<typename Domain>
 std::ostream& operator<<(std::ostream& cout, const MaxStrategy<Domain>& strat) {
   strat.print(cout);
diff --git a/impl/VariableAssignment.hpp b/impl/VariableAssignment.hpp
index a1f0b5b..cfce925 100644
--- a/impl/VariableAssignment.hpp
+++ b/impl/VariableAssignment.hpp
@@ -8,6 +8,9 @@ template<typename Domain>
 struct VariableAssignment {
   virtual ~VariableAssignment() { }
   virtual const Domain& operator[](const Variable<Domain>&) const = 0;
+  virtual const Domain& operator[](const Variable<Domain>& x) {
+    return (*const_cast<const VariableAssignment*>(this))[x];
+  }
 };
 
 #include "EquationSystem.hpp"
@@ -19,21 +22,40 @@ 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(), unknown(infinity<Domain>())),
       _stable(system.variableCount()),
       _influence(system.variableCount(),
-                 IdSet<Variable<Domain> >(system.variableCount()))
+                 IdSet<Variable<Domain> >(system.variableCount())),
+      _frozen(false)
   { }
 
+  void freeze() {
+    _frozen = true;
+  }
+
+  void thaw() {
+    _frozen = false;
+  }
+
+  bool is_frozen() {
+    return _frozen;
+  }
+
   const Domain& operator[](const Variable<Domain>& var) const {
-    solve(var);
     return _values[var];
   }
 
-  void invalidate(const Variable<Domain>& x) const {
+  const Domain& operator[](const Variable<Domain>& var) {
+    if (!_frozen)
+      solve(var);
+    return _values[var];
+  }
+
+  void invalidate(const Variable<Domain>& x) {
     log::fixpoint << indent() << "Invalidating " << x << std::endl;
     if (_stable.contains(x)) {
       _stable.remove(x);
@@ -56,7 +78,7 @@ struct DynamicVariableAssignment : public VariableAssignment<Domain> {
 
 private:
 
-  void solve(const Variable<Domain>& x) const {
+  void solve(const Variable<Domain>& x) {
     if (!_stable.contains(x)) {
       _stable.insert(x);
       log::fixpoint << indent() << "Stabilise " << x << std::endl;
@@ -93,7 +115,7 @@ private:
   }
 
   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];
@@ -101,7 +123,7 @@ private:
       return result;
     }
   private:
-    const DynamicVariableAssignment& _assignment;
+    DynamicVariableAssignment& _assignment;
     const Variable<Domain>& _var;
   };
 
diff --git a/impl/main.cpp b/impl/main.cpp
index b547c48..02faca5 100644
--- a/impl/main.cpp
+++ b/impl/main.cpp
@@ -140,6 +140,20 @@ int main (int argc, char* argv[]) {
   log::debug << system << endl;
   system.indexMaxExpressions(); // make reverse-lookup O(1) instead of O(n)
 
+  IdMap<Variable<ZBar>,ZBar> result = solve_for(system);
+  if (variables.size() > 0) {
+    for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
+      Variable<ZBar>& var = system.variable(i);
+      if (variables.find(var.name()) != variables.end())
+        cout << var.name() << " = " << result[var] << endl;
+    }
+  } else {
+    for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
+      Variable<ZBar>& var = system.variable(i);
+      cout << var.name() << " = " << result[var] << endl;
+    }
+  }
+  /*
   DynamicMaxStrategy<ZBar> strategy(system);
   DynamicVariableAssignment<ZBar> rho(system, strategy);
   strategy.setRho(rho);
@@ -157,6 +171,7 @@ int main (int argc, char* argv[]) {
       cout << var.name() << " = " << rho[var].asKnown() << endl;
     }
   }
+  */
 
   parser -> free(parser);
   tokens -> free(tokens);
diff --git a/impl/systems/test.eqns b/impl/systems/test.eqns
index ee90a4b..a3b521d 100644
--- a/impl/systems/test.eqns
+++ b/impl/systems/test.eqns
@@ -1,14 +1,20 @@
-i-4[0] = max(-inf, 0)
-negi-4[0] = max(-inf, 0)
-negi-1-pre = max(-inf, guard(add(min(negi-4[0], inf), min(i-4[0], inf)), 0, negi-4[0]), guard(add(min(negi-2[0], inf), min(i-2[0], inf)), 0, negi-2[0]))
-i-1-pre = max(-inf, guard(add(min(negi-4[0], inf), min(i-4[0], inf)), 0, i-4[0]), guard(add(min(negi-2[0], inf), min(i-2[0], inf)), 0, i-2[0]))
-negi-3-pre = max(-inf, guard(add(min(negi-1-pre, inf), min(i-1-pre, 2)), 0, negi-1-pre))
-i-3-pre = max(-inf, guard(add(min(negi-1-pre, inf), min(i-1-pre, 2)), 0, min(2, i-1-pre)))
-negi-0-pre = max(-inf, guard(add(min(negi-1-pre, -3), min(i-1-pre, inf)), 0, min(-3, negi-1-pre)))
-i-0-pre = max(-inf, guard(add(min(negi-1-pre, -3), min(i-1-pre, inf)), 0, i-1-pre))
-i-3[0] = max(-inf, add(1, i-3-pre))
-negi-3[0] = max(-inf, add(-1, negi-3-pre))
-negi-2-pre = max(-inf, guard(add(min(negi-3[0], inf), min(i-3[0], inf)), 0, negi-3[0]))
-i-2-pre = max(-inf, guard(add(min(negi-3[0], inf), min(i-3[0], inf)), 0, i-3[0]))
+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))
+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]))
+i-3[0] = max(-inf, 10)
+neg-i-3[0] = max(-inf, -10)
 i-2[0] = max(-inf, add(1, i-2-pre))
-negi-2[0] = max(-inf, add(-1, negi-2-pre))
+neg-i-2[0] = max(-inf, add(-1, neg-i-2-pre))
diff --git a/tex/thesis/Makefile b/tex/thesis/Makefile
index 1ccb5c4..8609c3a 100644
--- a/tex/thesis/Makefile
+++ b/tex/thesis/Makefile
@@ -3,7 +3,7 @@ PROJ = thesis
 
 .PHONY: all pdf wc clean
 
-all: pdf
+all: pdf clean
 
 pdf:
 	pdflatex $(PROJ)
@@ -26,4 +26,3 @@ clean:
 	rm -f `find . -name '*.lot'`
 	rm -f `find . -name '*.out'`
 	rm -f `find . -name '*~'`
-										
diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex
new file mode 100644
index 0000000..6d4aeca
--- /dev/null
+++ b/tex/thesis/contribution/contribution.tex
@@ -0,0 +1,423 @@
+\floatname{algorithm}{Listing}
+
+\newcommand\stable{\mathsf{stable}}
+\newcommand\eval{\mathsf{\textsc{eval}}}
+\newcommand\solve{\mathsf{\textsc{solve}}}
+\newcommand\system{\mathsf{system}}
+\algblockx[Globals]{Globals}{EndGlobals}{\textbf{Globals:\\}}{} 
+\algblockx[Assume]{Assumptions}{EndAssumptions}{\textbf{Assume:\\}}{} 
+
+
+\chapter{Contribution} \label{chap:contribution}
+
+The main theoretical contribution of this paper is an improvement on a
+$\max$-strategy improvement algorithm for solving fixpoint equations
+over the integers with monotonic
+operators\cite{Gawlitza:2007:PFC:1762174.1762203}. The original
+algorithm is presented in Section \ref{section:basic-algorithm}. We
+employ the ideas of Seidl, et al. to design an algorithm which runs in
+considerably less time than the existing solver.
+
+In this chapter we will begin by presenting the Work-list Depth First
+Search (W-DFS) fixpoint algorithm developed by Seidl, et
+al.\cite{DBLP:tr/trier/MI96-11}. We will then present a modification
+to the algorithm to allow it to perform $\max$-strategy iteration
+rather than fixpoint iteration. The chapter will then conclude with
+our Local Demand-driven Strategy Improvement (LDSI) algorithm.
+
+The existing algorithm as presented in Section
+\ref{section:basic-algorithm} consists of two iterative operations:
+fixpoint iteration and max-strategy iteration. Each of these
+operations consists of naively ``evaluating'' the system repeatedly
+until a further evaluation yields no change. It is shown by Gawlitza,
+et al. that these iterations must converge in a finite number of
+steps\cite{Gawlitza:2007:PFC:1762174.1762203}, but in practice this
+naive approach performs many more operations than are necessary, in
+many cases merely re-calculating results which are already known.
+
+By making use of some data-dependencies within the equation systems it
+is possible to reduce the amount of work that is to be done quite
+considerably.
+
+In order to aid our explanation of these algorithms we will now define
+a few terms and notations. All variables are taken from the set $X$
+and all values from the set $\D$.
+
+\begin{definition}
+  \textbf{Variable Assignments:} $X \to \D$. A function from a
+  variable to a value in our domain. An underlined value
+  (eg. $\underline{\infty}$) indicates a variable assignment mapping
+  everything to that value. Variable assignments may be combined with
+  $\oplus$ in the following way:
+  \begin{align*}
+    \rho \oplus \varrho = \left\{\begin{array}{lc}
+        \varrho(x) & x \in \mathsf{domain}(\varrho) \\
+        \rho(x) & \mbox{otherwise}
+      \end{array}\right.
+  \end{align*}
+\end{definition}
+
+\begin{definition}
+  \textbf{Expressions:} For the purposes of this discussion we will
+  consider expressions, $e \in E$, as $e : (X \to \D) \to \D$, a
+  mapping from a variable assignment to the expression's value in that
+  assignment.
+\end{definition}
+
+\begin{definition}
+  \textbf{Equation System:} $\{ x = e_x \mid x \in X, e_x \in E \}$. An
+  equation system can also be considered as a function $\varepsilon :
+  (X \to D) \to (X \to D)$; $\varepsilon[\rho](x) = e_x(\rho)$.
+\end{definition}
+
+\begin{definition}
+  \textbf{Dependencies:} A variable $x$ is said to \emph{depend on}
+  $y$ if a change to the value of $y$ induces a change in the value of
+  $x$.
+\end{definition}
+
+\section{Fixpoint Iteration}
+\subsection{Kleene Iteration}
+
+A simple approach to fixpoint iteration over monotonic equations is to
+simply iterate over the system repeatedly until a reevaluation results
+in no change to the values of any variables. This approach will always
+reach the least/greatest solution if there is one to be found, but it
+will often perform many more evaluations than are necessary. This
+algorithm is presented in Listing \ref{algo:kleene}.
+
+\begin{algorithm}
+  \begin{algorithmic}
+    \Assumptions
+      \begin{tabularx}{0.9\textwidth}{rX}
+        $\rho $:&$ X \to \D$, a variable assignment \\
+        $\varepsilon $:&$ (X \to \D) \to (X \to \D)$, an equation system
+      \end{tabularx}
+    \EndAssumptions
+
+    \State $n = 0$
+    \State $\rho_0 = \underline{\infty}$
+    \Repeat
+      \State $\rho_{n+1} = \varepsilon[ \rho_{n} ]$
+      \State $n = n + 1$
+    \Until {$\rho_{n-1} = \rho_n$}
+    \State \Return $\rho_n$
+  \end{algorithmic}
+  \caption{The Kleene iteration algorithm for solving fixpoint
+    equations for their greatest solutions.}
+  \label{algo:kleene}
+\end{algorithm}
+
+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 and thus an approach which can
+evaluate smaller portions of the system in each iteration would be a
+sensible improvement.
+
+\subsection{W-DFS algorithm}
+
+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
+ability to leave portions of the system unevaluated when it is certain
+that those values have not changed.
+
+\begin{algorithm}
+  \begin{algorithmic}
+    \Globals
+    \begin{tabularx}{0.9\textwidth}{rX}
+      $D : X \to \D$ & a mapping from variables to their current values, starting
+      at $\{ x \mapsto \infty | \forall x \in X \}$ \\ 
+      I & A mapping from a variable to the variables which depend on
+      it in their evaluation \\
+      stable & The set of all variables whose values have stabilised \\ 
+      system & The equation system, a mapping from a variable to its
+      associated function \\
+    \end{tabularx}
+    \EndGlobals
+    something something
+  \end{algorithmic}
+
+  \begin{algorithmic}
+    \Function {eval} {$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\}$
+      \State \Return $D[y]$
+    \EndFunction 
+  \end{algorithmic}
+
+  \begin{algorithmic}
+    \Function {solve} {$x$}
+    \Comment{Solve a specific variable and place its value in $D$}
+    \If {$x \not \in \stable$}
+      \State $f = \system[x]$
+      \State $\stable = \stable \cup \{x\}$
+      \State $v = f( \lambda y . \eval(x, y) )$
+      \If {$v \ne D[x]$}
+        \State $D = \{ x \mapsto v, \alpha \mapsto D[\alpha] \}
+        \forall \alpha \ne x$
+        \State $W = I[x]$
+        \State $I(x) = \emptyset$
+        \State $\stable = \stable \backslash W$
+        \For {$v \in W$}
+          \State $\solve(v)$
+        \EndFor
+      \EndIf
+    \EndIf
+    \EndFunction
+  \end{algorithmic}
+
+  \caption{The W-DFS alluded to in \cite{DBLP:tr/trier/MI96-11} and
+    presented in \cite{fixpoint-slides}, modified to find
+    greatest-fixpoints of monotonic fixpoint equations}
+  \label{algo:w-dfs}
+\end{algorithm}
+
+
+
+\section{$\max$-strategy Iteration}
+\subsection{Naive approach}
+
+TODO: Explanation of the naive approach
+
+\subsection{Adapted W-DFS algorithm}
+
+The $\max$-strategy iteration can be viewed as a fixpoint problem. We
+are attempting to find a strategy, $\sigma: E_{\max} \to E$ that will
+result in the greatest value for each $e \in E_{\max}$. Therefore if
+we consider our ``variables'' to be $\max$-expressions, our ``values''
+to be their subexpressions and our ``comparison'' to be carried out
+using the result of evaluating the system with that strategy.
+
+This, then, allows us to use the W-DFS algorithm to re-evaluate only
+those parts of the strategy which have changed. Listing
+\ref{algo:w-dfs-max} presents this variation on W-DFS.
+
+\begin{algorithm}
+  \begin{algorithmic}
+    \Globals
+    \begin{tabularx}{0.9\textwidth}{rX}
+      $\sigma$ & A mapping from $\max$-expressions to their current
+      sub-expressions, starting by mapping to the first
+      sub-expression \\
+      I & A mapping from a $\max$-expression to the sub-expressions
+      which depend on it in their evaluation \\
+      stable & The set of all $\max$-expressions whose strategies have
+      stabilised \\
+      system & The equation system, a mapping from a variable to its
+      associated function \\
+      bestStrategy & A function $(E_{\max}, (X \to D)) \to E$ mapping
+      from an expression and a variable \\& assignment to the greatest
+      subexpression in that context
+    \end{tabularx}
+    \EndGlobals
+
+    \Function {eval} {$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\}$
+      \State \Return $\sigma[y]$
+    \EndFunction
+
+    \Function {solve} {$x$}
+    \Comment{Solve a specific expression and place its value in $\sigma$}
+    \If {$x \not \in \stable$}
+      \State $f = \system[x]$
+      \State $\stable = \stable \cup \{x\}$
+      \State $v = bestStrategy(x, \lambda y . \eval(x, y))$
+      \If {$v \ne \sigma[x]$}
+        \State $\sigma = \{ x \mapsto v, \alpha \mapsto \sigma[\alpha]
+        \} \forall \alpha \ne x $
+        \State $W = I[x]$
+        \State $I(x) = \emptyset$
+        \State $\stable = \stable \backslash W$
+        \For {$v \in W$}
+        \State $\solve(v)$
+        \EndFor
+      \EndIf
+    \EndIf
+    \EndFunction
+  \end{algorithmic}
+
+  \caption{W-DFS, this time modified to find the best $\max$-strategy.}
+  \label{algo:w-dfs-max}
+\end{algorithm}
+
+
+\section{Combined W-DFS}
+
+W-DFS can be used to speed up both the $\max$-strategy iteration and
+the fixpoint iteration as two independent processes, but each
+fixpoint-iteration step still requires at least one complete
+evaluation of the equation system per $\max$-strategy improvement
+step. Ideally we would be able to adapt the W-DFS algorithm so that
+the fixpoint-iteration and $\max$-strategy iteration steps could
+provide some information to each other about what values have changed
+so that at each step only a subset of the entire system would have to
+be evaluated.
+
+The new algorithm, \emph{Combined W-DFS} seeks to do this. By adding
+an ``invalidate'' method to both W-DFS instances we provide an
+interface for the two sides of the algorithm to indicate which values
+have changed. This gives the other side enough information to avoid
+evaluating irrelevant portions of the equation system.
+
+This algorithm is presented in two parts. Listing
+\ref{algo:combined-fixpoint} presents the fixpoint-iteration portion
+of the algorithm, while Listing \ref{algo:combined-max} presents the
+$\max$-strategy portion.  The correctness of this new algorithm is
+argued in \ref{sec:combined-correctness}.
+
+
+\begin{algorithm}
+  \begin{algorithmic}
+    \Globals
+    \begin{tabularx}{0.9\textwidth}{rX}
+      D & A mapping from variables to their current values, starting
+      at $\{ x \mapsto \infty \}$ \\ 
+      I & A mapping from a variable to the variables which depend on
+      it in their evaluation \\
+      stable & The set of all variables whose values have stabilised \\ 
+      system & The equation system, a mapping from a variable to its
+      associated function \\
+    \end{tabularx}
+    \EndGlobals
+
+    \Function {eval} {$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\}$
+      \State \Return $D[y]$
+    \EndFunction
+
+    \Function {invalidate} {$x$}
+    \If {$x \in \stable$}
+      \State $\stable = \stable \backslash \{x\}$
+      \State $D[x] = \infty$
+      \State $W = I[x]$
+      \State $I[x] = \emptyset$
+      \For {$v \in W$}
+        invalidate(v)
+      \EndFor
+    \EndIf
+    \EndFunction
+
+    \Function {solve} {$x$}
+    \Comment{Solve a specific expression and place its value in $D$}
+    \If {$x \not \in \stable$}
+      \State $f = \system[x]$
+      \State $\stable = \stable \cup \{x\}$
+      \State $v = f( \lambda y . \eval(x, y) )$
+      \If {$v \ne D[x]$}
+        \State $D = \{ x \mapsto v, \alpha \mapsto D[\alpha] \}
+        \forall \alpha \ne x$
+        \State $W = I[x]$
+        \State $I(x) = \emptyset$
+        \State strategy::invalidate($x$)
+        \State $\stable = \stable \backslash W$
+        \For {$v \in W$}
+        \State $\solve(v)$
+        \EndFor
+      \EndIf
+    \EndIf
+    \EndFunction
+  \end{algorithmic}
+
+  \caption{The fixpoint portion of the Combined W-DFS.}
+  \label{algo:combined-fixpoint}
+\end{algorithm}
+
+
+\begin{algorithm}
+  \begin{algorithmic}
+    \Globals
+    \begin{tabularx}{0.9\textwidth}{rX}
+      $\sigma$ & A mapping from $\max$-expressions to their current
+      sub-expressions, starting by \\& mapping to the first
+      sub-expression \\
+      D & A \emph{dynamic} variable assignment which will stay updated
+      as $\sigma$ changes \\
+      $I$ & A mapping from a $\max$-expression to the sub-expressions
+      which depend on it \\& in their evaluation \\
+      $I_V$ & A mapping from a variable to the $\max-$ expressions which
+      depend on it in their \\& evaluation \\
+      stable & The set of all $\max$-expressions whose strategies have
+      stabilised \\
+      system & The equation system, a mapping from a variable to its
+      associated function \\
+      bestStrategy & A function $(E_{\max}, (X \to D)) \to E$ mapping
+      from an expression and a variable \\& assignment to the greatest
+      subexpression in that context
+    \end{tabularx}
+    \EndGlobals
+
+    \Function {eval} {$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\}$
+      \State \Return $\sigma[y]$
+    \EndFunction
+
+    \Function {invalidate} {$x \in X$} \Comment{X is vars}
+      \State $\stable = \stable \backslash I[x]$
+      \State $W = I_v[x]$
+      \State $I_V = \emptyset$
+      \For {$v \in W$}
+        \State solve(v)
+      \EndFor
+    \EndFunction
+
+    \Function {solve} {$x$}
+    \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(x,
+                               \lambda y . \eval(x, y))$
+      \If {$v \ne \sigma[x]$}
+        \State $\sigma = \{ x \mapsto v, \alpha \mapsto \sigma[\alpha]
+        \} \forall \alpha \ne x $
+        \State $W = I[x]$
+        \State $I(x) = \emptyset$
+        \State fixpoint::invalidate$(\mathsf{lookupVarFor}(x))$
+        \State $\stable = \stable \backslash W$
+        \For {$v \in W$}
+          \State $\solve(v)$
+        \EndFor
+      \EndIf
+    \EndIf
+    \EndFunction
+  \end{algorithmic}
+
+  \caption{The $\max$-strategy portion of the Combined W-DFS.}
+  \label{algo:combined-max}
+\end{algorithm}
+
+
+\subsection{Correctness} \label{sec:combined-correctness}
+
+This algorithm relies on the correctness of the underlying W-DFS
+algorithm. This algorithm was presented in
+\cite{DBLP:tr/trier/MI96-11}.
+
+If we assume that W-DFS is correct then we only have to prove that the
+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}
diff --git a/tex/thesis/references.bib b/tex/thesis/references.bib
index d03c67a..e743703 100644
--- a/tex/thesis/references.bib
+++ b/tex/thesis/references.bib
@@ -134,4 +134,10 @@
   publisher = {OCG},
   OPTnote = {},
   OPTannote = {}
+}
+@misc{fixpoint-slides,
+  author = {Helmut Seidl},
+  title = {Lecture Slides in Program Optimisation},
+  url = {http://www2.in.tum.de/~seidl/Courses/WS2011/Optimierung/all2011.pdf},
+  year = {2011}
 }
\ No newline at end of file
diff --git a/tex/thesis/thesis.tex b/tex/thesis/thesis.tex
index 6983d79..8f64c07 100644
--- a/tex/thesis/thesis.tex
+++ b/tex/thesis/thesis.tex
@@ -37,6 +37,7 @@
 \usepackage{xcolor}
 \usepackage{xspace}
 \usepackage{stmaryrd,tikz}
+\usepackage{tabularx}
 
 \usepackage{float}
 \floatstyle{boxed} 
@@ -44,6 +45,8 @@
 
 \lstset{language={Python}, literate={<=}{$\le$}{1}}%, frame=tlrb}
 \usetikzlibrary{arrows}
+
+\newcommand\D{\mathbb{D}}
 \newcommand\R{\mathbb{R}}
 \newcommand\Z{\mathbb{Z}}
 \newcommand\CZ{\overline{\Z}}
@@ -136,6 +139,7 @@
 
 \input{introduction/introduction.tex}
 \input{litreview/litreview.tex}
+\input{contribution/contribution.tex}
 \input{evaluation/evaluation.tex}
 \input{experiments/experiments.tex}
 \input{results/results.tex}
@@ -146,7 +150,7 @@
 % End
 
 % Bibliography
-\bibliographystyle{style/mybibstyle}
+\bibliographystyle{abbrvnat} %style/mybibstyle}
 {
 \setstretch{1.25}
 \cleardoublepage
diff --git a/tex/thesis/usydthesis.cls b/tex/thesis/usydthesis.cls
index e18eb53..5b1a4d4 100644
--- a/tex/thesis/usydthesis.cls
+++ b/tex/thesis/usydthesis.cls
@@ -32,7 +32,8 @@
 \usepackage{amssymb,amsmath}
 \newcommand{\theHalgorithm}{\arabic{algorithm}}
 \usepackage[ruled]{algorithm}
-\usepackage{algorithmic}
+\usepackage{algorithmicx}
+\usepackage{algpseudocode}
 
 % Fancy footnotes
 \usepackage[stable]{style/footmisc}