Merge branch 'master' of https://bitbucket.org/czan/honours

Conflicts:
	.gitignore
	impl/MaxStrategy.hpp
	impl/VariableAssignment.hpp
	impl/systems/test.eqns
	impl/test/7.eqns

6 files changed, 146 insertions, 33 deletions

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))