Okay, the solver is now correct.

It runs in two separate passes:
 - improve strategy (for all)
 - evaluate fixpoint

Unfortunately this loses out on locality at the moment.

I really want a local solver, so I'll have to see what I can do about
that.

10 files changed, 170 insertions, 41 deletions

diff --git a/impl/Complete.hpp b/impl/Complete.hpp
index 8c5559a..e3ec15a 100644
--- a/impl/Complete.hpp
+++ b/impl/Complete.hpp
@@ -40,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/impl/Expression.hpp b/impl/Expression.hpp
index 0d48d70..9c4ac9f 100644
--- a/impl/Expression.hpp
+++ b/impl/Expression.hpp
@@ -110,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;
   }
@@ -141,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>
diff --git a/impl/MaxStrategy.hpp b/impl/MaxStrategy.hpp
index 96aeef4..f4026dd 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;
@@ -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 {
-    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,7 +88,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;
@@ -106,7 +127,7 @@ private:
   }
 
   struct DependencyAssignment : public VariableAssignment<Domain>{
-    DependencyAssignment(const DynamicMaxStrategy& strat,
+    DependencyAssignment(DynamicMaxStrategy& strat,
                          VariableAssignment<Domain>& rho,
                          const MaxExpression<Domain>& expr)
       : _strat(strat),
@@ -118,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) {
     }
@@ -136,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/impl/VariableAssignment.hpp b/impl/VariableAssignment.hpp
index a9247b5..2a63756 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(), 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 {
+  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);
@@ -53,7 +75,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;
@@ -90,7 +112,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];
@@ -98,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/impl/gmon.out b/impl/gmon.out
deleted file mode 100644
index f33c245..0000000
--- a/impl/gmon.out
+++ /dev/null
diff --git a/impl/main.cpp b/impl/main.cpp
index e3e0ae3..84f17dd 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);
@@ -156,6 +170,7 @@ int main (int argc, char* argv[]) {
       cout << var.name() << " = " << rho[var] << endl;
     }
   }
+  */
 
   parser -> free(parser);
   tokens -> free(tokens);
diff --git a/impl/systems/gmon.out b/impl/systems/gmon.out
deleted file mode 100644
index b5abe0e..0000000
--- a/impl/systems/gmon.out
+++ /dev/null
diff --git a/impl/systems/test.eqns b/impl/systems/test.eqns
index af18a57..a3b521d 100644
--- a/impl/systems/test.eqns
+++ b/impl/systems/test.eqns
@@ -1,12 +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-pre, inf), min(i-2-pre, inf)), 0, negi-2-pre))
-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-pre, inf), min(i-2-pre, inf)), 0, i-2-pre))
-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(0, i-3-pre))
-negi-3[0] = max(-inf, add(0, 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))
+neg-i-2[0] = max(-inf, add(-1, neg-i-2-pre))
diff --git a/impl/test/7.eqns b/impl/test/7.eqns
new file mode 100644
index 0000000..2789f0e
--- /dev/null
+++ b/impl/test/7.eqns
@@ -0,0 +1,8 @@
+x = 0
+y = max(-inf, x, a)
+a = b
+b = c
+c = d
+d = e
+e = f
+f = y
diff --git a/impl/test/7.soln b/impl/test/7.soln
new file mode 100644
index 0000000..0d85468
--- /dev/null
+++ b/impl/test/7.soln
@@ -0,0 +1,8 @@
+x = 0
+y = 0
+a = 0
+b = 0
+c = 0
+d = 0
+e = 0
+f = 0