Make the recursive solver work properly.

If you ignore the intermediate results for the strategy iteration phase
then you're in the clear! I think!

18 files changed, 182 insertions, 42 deletions

diff --git a/.gitignore b/.gitignore
index 3b01757..0173d7a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,14 @@
 /impl/build/*
 /impl/parser/*
+*.log
+*.dvi
+*.ps
+*.aux
+*.blg
+*.bbl
+*.toc
+*.lof
+*.lot
+*.out
+*~
+gmon.out
diff --git a/impl/Complete.hpp b/impl/Complete.hpp
index 8c5559a..38b637e 100644
--- a/impl/Complete.hpp
+++ b/impl/Complete.hpp
@@ -7,23 +7,38 @@
 
 template<typename T>
 T infinity() { }
+template<typename T>
+T unknown(const T&) { }
 
 template<typename T>
 struct Complete {
   Complete()
-    : _value(0), _infinity(false) { }
+    : _value(0), _infinity(false), _unknown(false) { }
   Complete(const T& value)
-    : _value(value), _infinity(false) { }
+    : _value(value), _infinity(false), _unknown(false) { }
   Complete(const T& value, const bool& infinity)
-    : _value(value), _infinity(infinity) {
+    : _value(value), _infinity(infinity), _unknown(false) {
     assert(value != 0 || infinity == false);
   }
   Complete(const Complete& other)
-    : _value(other._value), _infinity(other._infinity) { }
+    : _value(other._value), _infinity(other._infinity), _unknown(other._unknown) { }
+  Complete(const Complete& other, bool unknown)
+    : _value(other._value), _infinity(other._infinity), _unknown(unknown) { }
+
+  Complete asUnknown() const {
+    return Complete(*this, true);
+  }
+  Complete asKnown() const {
+    return Complete(*this, false);
+  }
+  bool isUnknown() const {
+    return _unknown;
+  }
 
   Complete& operator=(const Complete& other) {
     _value = other._value;
     _infinity = other._infinity;
+    _unknown = other._unknown;
     return *this;
   }
   Complete& operator+=(const Complete& other) {
@@ -98,6 +113,7 @@ struct Complete {
   private:
   T _value;
   bool _infinity;
+  bool _unknown;
 };
 
 template<typename Z>
@@ -110,6 +126,8 @@ std::istream& operator>>(std::istream& cin, Complete<Z>& num) {
 
 template<typename Z>
 std::ostream& operator<<(std::ostream& cout, const Complete<Z>& num) {
+  if (num._unknown)
+    cout << "(unknown)";
   if (num._infinity) {
     cout << (num._value > 0 ? "inf" : "-inf");
   } else {
@@ -122,5 +140,9 @@ template<>
 Complete<int> infinity() {
   return Complete<int>(1, true);
 }
+template<>
+Complete<int> unknown(const Complete<int>& x) {
+  return Complete<int>(x, true);
+}
 
 #endif
diff --git a/impl/EquationSystem.hpp b/impl/EquationSystem.hpp
index 2fd24bd..a0ba8a1 100644
--- a/impl/EquationSystem.hpp
+++ b/impl/EquationSystem.hpp
@@ -31,7 +31,7 @@ struct EquationSystem {
     delete _expr_to_var;
   }
 
-  MaxExpression<Domain>& maxExpression(const std::vector<Expression<Domain>*>& arguments) {
+  MaxExpression<Domain>& maxExpression(const std::vector<Expression<Domain>*> arguments) {
     unsigned int id = _max_expressions.size();
     Maximum<Domain>* max = new Maximum<Domain>();
     MaxExpression<Domain>* expr = new MaxExpression<Domain>(id, *max, arguments);
diff --git a/impl/Expression.hpp b/impl/Expression.hpp
index 00bc9cd..0f3717f 100644
--- a/impl/Expression.hpp
+++ b/impl/Expression.hpp
@@ -143,7 +143,7 @@ struct OperatorExpression : public Expression<Domain> {
 template<typename Domain>
 struct MaxExpression : public OperatorExpression<Domain> {
   MaxExpression(const unsigned int& id, const Maximum<Domain>& op, const std::vector<Expression<Domain>*>& arguments)
-    : OperatorExpression<Domain>(op, arguments), _id(id) { }
+    : OperatorExpression<Domain>(op, arguments), _id(id) {}
 
   const MaxExpression* toMaxExpression() const {
     return this;
@@ -161,9 +161,11 @@ struct MaxExpression : public OperatorExpression<Domain> {
          i < length;
          ++i) {
       const Domain value = this->_arguments[i]->eval(rho, strat);
-      if (bestValue < value) {
-        bestValue = value;
-        bestIndex = i;
+      if (!value.isUnknown()) {
+        if (bestValue < value) {
+          bestValue = value;
+          bestIndex = i;
+        }
       }
     }
     return bestIndex;
diff --git a/impl/MaxStrategy.hpp b/impl/MaxStrategy.hpp
index 96aeef4..96d0492 100644
--- a/impl/MaxStrategy.hpp
+++ b/impl/MaxStrategy.hpp
@@ -31,7 +31,8 @@ template<typename Domain>
 struct DynamicMaxStrategy : public MaxStrategy<Domain> {
   DynamicMaxStrategy(
     const EquationSystem<Domain>& system
-  ) : _system(system),
+  ) : _frozen(false),
+      _system(system),
       _rho(NULL),
       _values(system.maxExpressionCount(), 0),
       _stable(system.maxExpressionCount()),
@@ -46,23 +47,26 @@ struct DynamicMaxStrategy : public MaxStrategy<Domain> {
   }
 
   unsigned int get(const MaxExpression<Domain>& e) const {
-    solve(e);
+    if (!_frozen)
+      solve(e);
     return _values[e];
   }
 
   void invalidate(const Variable<Domain>& v) const {
     log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl;
-    _stable.filter(_var_influence[v]);
-
-    IdSet<MaxExpression<Domain> > infl = _var_influence[v];
-    _var_influence[v].clear();
-
-    for (typename IdSet<MaxExpression<Domain> >::iterator
-           it = infl.begin(),
-           end = infl.end();
-         it != end;
-         ++it) {
-      solve(_system.maxExpression(*it));
+    if (_system[v] && _stable.contains(*_system[v])) {
+      _stable.remove(*_system[v]);
+      _stable.filter(_var_influence[v]);
+      
+      IdSet<MaxExpression<Domain> > infl = _var_influence[v];
+      _var_influence[v].clear();
+      for (typename IdSet<MaxExpression<Domain> >::iterator
+             it = infl.begin(),
+             end = infl.end();
+           it != end;
+           ++it) {
+        solve(_system.maxExpression(*it));
+      }
     }
   }
 
@@ -78,6 +82,7 @@ private:
       stack_depth--;
 
       if (val != _values[x]) {
+
         log::strategy << x << " => " << *x.arguments()[val] << std::endl;
 
         IdSet<MaxExpression<Domain> > oldInfluence = _influence[x];
@@ -105,6 +110,16 @@ private:
     }
   }
 
+  const DynamicMaxStrategy& freeze() const {
+    _frozen = true;
+    return *this;
+  }
+
+  const DynamicMaxStrategy& thaw() const {
+    _frozen = false;
+    return *this;
+  }
+
   struct DependencyAssignment : public VariableAssignment<Domain>{
     DependencyAssignment(const DynamicMaxStrategy& strat,
                          VariableAssignment<Domain>& rho,
@@ -123,6 +138,30 @@ private:
     const MaxExpression<Domain>& _expr;
   };
 
+  struct InvalidatingAssignment : public VariableAssignment<Domain>{
+    InvalidatingAssignment(DynamicVariableAssignment<Domain>& rho)
+      : _rho(rho) {
+    }
+    ~InvalidatingAssignment() {
+      for (typename std::set<const Variable<Domain>*>::iterator
+             it = seen.begin(),
+             ei = seen.end();
+           it != ei;
+           ++it) {
+        if (!_old_stable.contains(**it))
+          _rho.invalidate(**it);
+      }
+    }
+    const Domain& operator[](const Variable<Domain>& var) const {
+      seen.insert(&var);
+      return _rho[var];
+    }
+  private:
+    DynamicVariableAssignment<Domain>& _rho;
+    IdSet<Variable<Domain> > _old_stable;
+    mutable std::set<const Variable<Domain>*> seen;
+  };
+
   struct DependencyStrategy : public MaxStrategy<Domain> {
     DependencyStrategy(const DynamicMaxStrategy& strat, const MaxExpression<Domain>& expr)
       : _strat(strat),
@@ -141,6 +180,7 @@ private:
   };
 
 private:
+  mutable bool _frozen;
   const EquationSystem<Domain>& _system;
   mutable DynamicVariableAssignment<Domain>* _rho;
   mutable IdMap<MaxExpression<Domain>,unsigned int> _values;
diff --git a/impl/VariableAssignment.hpp b/impl/VariableAssignment.hpp
index ae5efd7..a1f0b5b 100644
--- a/impl/VariableAssignment.hpp
+++ b/impl/VariableAssignment.hpp
@@ -22,7 +22,7 @@ struct DynamicVariableAssignment : public VariableAssignment<Domain> {
     const DynamicMaxStrategy<Domain>& strat
   ) : _system(system),
       _strategy(strat),
-      _values(system.variableCount(), infinity<Domain>()),
+      _values(system.variableCount(), unknown(infinity<Domain>())),
       _stable(system.variableCount()),
       _influence(system.variableCount(),
                  IdSet<Variable<Domain> >(system.variableCount()))
@@ -37,9 +37,20 @@ struct DynamicVariableAssignment : public VariableAssignment<Domain> {
     log::fixpoint << indent() << "Invalidating " << x << std::endl;
     if (_stable.contains(x)) {
       _stable.remove(x);
-      _values[x] = infinity<Domain>();
+      _values[x] = unknown(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));
+      }
+      */
     }
   }
 
@@ -97,7 +108,9 @@ private:
   const EquationSystem<Domain>& _system;
   const DynamicMaxStrategy<Domain>& _strategy;
   mutable IdMap<Variable<Domain>, Domain> _values;
+public:
   mutable IdSet<Variable<Domain> > _stable;
+private:
   mutable IdMap<Variable<Domain>,IdSet<Variable<Domain> > > _influence;
 };
 
diff --git a/impl/gmon.out b/impl/gmon.out
deleted file mode 100644
index aff812c..0000000
--- a/impl/gmon.out
+++ /dev/null
diff --git a/impl/main.cpp b/impl/main.cpp
index e3e0ae3..b547c48 100644
--- a/impl/main.cpp
+++ b/impl/main.cpp
@@ -147,13 +147,14 @@ int main (int argc, char* argv[]) {
   if (variables.size() > 0) {
     for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
       Variable<ZBar>& var = system.variable(i);
-      if (variables.find(var.name()) != variables.end())
-        cout << var.name() << " = " << rho[var] << endl;
+      if (variables.find(var.name()) != variables.end()) {
+        cout << var.name() << " = " << rho[var].asKnown() << endl;
+      }
     }
   } else {
     for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
       Variable<ZBar>& var = system.variable(i);
-      cout << var.name() << " = " << rho[var] << endl;
+      cout << var.name() << " = " << rho[var].asKnown() << endl;
     }
   }
 
diff --git a/impl/systems/gmon.out b/impl/systems/gmon.out
deleted file mode 100644
index 3240978..0000000
--- a/impl/systems/gmon.out
+++ /dev/null
diff --git a/impl/systems/test.eqns b/impl/systems/test.eqns
index fb23f1e..ee90a4b 100644
--- a/impl/systems/test.eqns
+++ b/impl/systems/test.eqns
@@ -1,16 +1,14 @@
 i-4[0] = max(-inf, 0)
-neg-i4[0] = max(-inf, 0)
-neg-i1-pre = max(-inf, guard(add(min(neg-i4[0], inf), min(i-4[0], inf)), 0, neg-i4[0]), guard(add(min(neg-i2-pre, inf), min(i-2-pre, inf)), 0, neg-i2-pre))
-i-1-pre = max(-inf, guard(add(min(neg-i4[0], inf), min(i-4[0], inf)), 0, i-4[0]), guard(add(min(neg-i2-pre, inf), min(i-2-pre, inf)), 0, i-2-pre))
-neg-i3-pre = max(-inf, guard(add(min(neg-i1-pre, inf), min(i-1-pre, 2)), 0, neg-i1-pre))
-i-3-pre = max(-inf, guard(add(min(neg-i1-pre, inf), min(i-1-pre, 2)), 0, min(2, i-1-pre)))
-neg-i0-pre = max(-inf, guard(add(min(neg-i1-pre, -3), min(i-1-pre, inf)), 0, min(-3, neg-i1-pre)))
-i-0-pre = max(-inf, guard(add(min(neg-i1-pre, -3), min(i-1-pre, inf)), 0, i-1-pre))
-i-3[0] = max(-inf, add(0, i-3-pre))
-neg-i3[0] = max(-inf, add(0, neg-i3-pre))
-neg-i2-pre = max(-inf, guard(add(min(neg-i3[0], inf), min(i-3[0], inf)), 0, neg-i3[0]))
-i-2-pre = max(-inf, guard(add(min(neg-i3[0], inf), min(i-3[0], inf)), 0, i-3[0]))
-x = max(-inf, 0)
-y = max(-inf, x, z)
-z = max(-inf, y)
-
+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-2[0] = max(-inf, add(1, i-2-pre))
+negi-2[0] = max(-inf, add(-1, negi-2-pre))
diff --git a/impl/test/10.eqns b/impl/test/10.eqns
new file mode 100644
index 0000000..39598f4
--- /dev/null
+++ b/impl/test/10.eqns
@@ -0,0 +1,9 @@
+x = 0
+w = max(x,y,z,u,w)
+y = w
+z = w
+u = a
+a = b
+b = c
+c = d
+d = w
diff --git a/impl/test/10.soln b/impl/test/10.soln
new file mode 100644
index 0000000..20a47ca
--- /dev/null
+++ b/impl/test/10.soln
@@ -0,0 +1,9 @@
+x = 0
+w = 0
+y = 0
+z = 0
+u = 0
+a = 0
+b = 0
+c = 0
+d = 0
diff --git a/impl/test/7.eqns b/impl/test/7.eqns
new file mode 100644
index 0000000..1f69268
--- /dev/null
+++ b/impl/test/7.eqns
@@ -0,0 +1,8 @@
+x = 0
+y = max(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
diff --git a/impl/test/8.eqns b/impl/test/8.eqns
new file mode 100644
index 0000000..c9e9c4e
--- /dev/null
+++ b/impl/test/8.eqns
@@ -0,0 +1,4 @@
+x = 0
+w = max(x,y,z)
+y = w
+z = w
diff --git a/impl/test/8.soln b/impl/test/8.soln
new file mode 100644
index 0000000..1945057
--- /dev/null
+++ b/impl/test/8.soln
@@ -0,0 +1,4 @@
+x = 0
+w = 0
+y = 0
+z = 0
diff --git a/impl/test/9.eqns b/impl/test/9.eqns
new file mode 100644
index 0000000..b85e118
--- /dev/null
+++ b/impl/test/9.eqns
@@ -0,0 +1,5 @@
+x = 0
+w = max(x,y,z,u)
+y = w
+z = w
+u = w
diff --git a/impl/test/9.soln b/impl/test/9.soln
new file mode 100644
index 0000000..616c5e5
--- /dev/null
+++ b/impl/test/9.soln
@@ -0,0 +1,5 @@
+x = 0
+w = 0
+y = 0
+z = 0
+u = 0