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

7 files changed, 161 insertions, 103 deletions

diff --git a/impl/Expression.hpp b/impl/Expression.hpp
index c005fd6..dcf7201 100644
--- a/impl/Expression.hpp
+++ b/impl/Expression.hpp
@@ -4,6 +4,7 @@
 #include <string>
 #include <vector>
 #include <sstream>
+#include <set>
 #include "IdMap.hpp"
 #include "Operator.hpp"
 
@@ -33,6 +34,10 @@ struct Expression {
 
   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);
   }
@@ -40,6 +45,9 @@ struct Expression {
   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;
 };
 
@@ -100,6 +108,16 @@ struct OperatorExpression : public Expression<Domain> {
     return _operator.eval(argumentValues);
   }
 
+  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();
@@ -130,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();
@@ -161,27 +187,33 @@ struct MaxExpression : public OperatorExpression<Domain> {
     return this;
   }
 
+  virtual Domain eval(VariableAssignment<Domain>& rho, const MaxStrategy<Domain>& strat) const {
+    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 {
+    log::strategy << "const MaxExpression eval" << std::endl;
     return this->_arguments[strat.get(*this)]->eval(rho, strat);
   }
 
   unsigned int bestStrategy(VariableAssignment<Domain>& rho, MaxStrategy<Domain>& strat) const {
-    Domain bestValue = this->eval(rho, strat);
-    unsigned int bestIndex = strat.get(*this);
+    unsigned int bestIndex = const_cast<const MaxStrategy<Domain>&>(strat).get(*this);
+    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]->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;
@@ -190,6 +222,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/impl/Makefile b/impl/Makefile
index 6fc6f3b..ca0b37d 100644
--- a/impl/Makefile
+++ b/impl/Makefile
@@ -2,7 +2,7 @@ CC=gcc
 CPP=g++
 BUILD=build
 PARSER=parser
-FLAGS=-Wall -Werror -Wextra -pedantic -lantlr3c -fno-exceptions
+FLAGS=-Wall -Werror -Wextra -pedantic -lantlr3c -fno-exceptions -lrt
 NORMAL_FLAGS=$(FLAGS) -g -pg
 OPTIMISED_FLAGS=$(FLAGS) -O3
 
diff --git a/impl/MaxStrategy.hpp b/impl/MaxStrategy.hpp
index d908c7b..5534597 100644
--- a/impl/MaxStrategy.hpp
+++ b/impl/MaxStrategy.hpp
@@ -9,7 +9,10 @@
 template<typename Domain>
 struct MaxStrategy {
   virtual ~MaxStrategy() { }
-  virtual unsigned int get(const MaxExpression<Domain>& e) = 0;
+  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;
 };
 
 unsigned int stack_depth = 1;
@@ -39,44 +42,60 @@ struct DynamicMaxStrategy : public MaxStrategy<Domain> {
                  IdSet<MaxExpression<Domain> >(system.maxExpressionCount())),
       _var_influence(system.variableCount(),
                      IdSet<MaxExpression<Domain> >(system.maxExpressionCount())),
-      _frozen(false)
+      _changed(false)
   {}
 
-  void freeze() {
-    _frozen = true;
+  void setRho(DynamicVariableAssignment<Domain>& rho) {
+    _rho = &rho;
   }
 
-  void thaw() {
-    _frozen = false;
+  void hasChanged(bool c) {
+    _changed = c;
   }
 
-  bool is_frozen() {
-    return _frozen;
+  bool hasChanged() const {
+    return _changed;
   }
 
-  void setRho(DynamicVariableAssignment<Domain>& rho) {
-    _rho = &rho;
+  unsigned int get(const MaxExpression<Domain>& e) const {
+    log::strategy << indent() << "Look up " << e << std::endl;
+    return _values[e];
   }
 
   unsigned int get(const MaxExpression<Domain>& e) {
-    if (!_frozen)
-      solve(e);
+    log::strategy << indent() << "Solve for " << e << std::endl;
+    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]);
+    //log::debug << indent() << "  var-influence sets " << _var_influence << std::endl;
 
     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));
+      invalidate(_system.maxExpression(*it));
+    }
+  }
+
+  void invalidate(const MaxExpression<Domain>& v) {
+    if (_stable.contains(v)) {
+      log::strategy << indent() << "Invalidating " << v << std::endl; 
+      //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));
+      }
     }
   }
 
@@ -96,16 +115,13 @@ private:
         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->thaw();
-	this->freeze();
-	_rho->stabilise();
-	_rho->freeze();
-	this->thaw();
+        
+	//_rho->stabilise();
 
         _stable.filter(oldInfluence);
 
@@ -136,15 +152,11 @@ private:
 	_current(strat._system.variableCount()) {
     }
     const Domain operator[](const Variable<Domain>& var) {
+      // solve the strategy for this variable, too
+      _strat.solve(*_strat._system[var]);
       _strat._var_influence[var].insert(_expr);
-      if (_current.contains(var)) {
-	return _rho[var];
-      } else {
-	_current.insert(var);
-	Domain val = _strat._system[var]->eval(_rho, _strat);
-	_current.remove(var);
-	return val;
-      }
+      _strat._influence[*_strat._system[var]].insert(_expr);
+      return _rho[var];
     }
   private:
     DynamicMaxStrategy& _strat;
@@ -158,11 +170,13 @@ private:
       : _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:
@@ -177,7 +191,7 @@ private:
   IdSet<MaxExpression<Domain> > _stable;
   IdMap<MaxExpression<Domain>,IdSet<MaxExpression<Domain> > > _influence;
   IdMap<Variable<Domain>,IdSet<MaxExpression<Domain> > > _var_influence;
-  bool _frozen;
+  bool _changed;
 };
 
 
@@ -193,19 +207,25 @@ struct Solver {
   Domain solve(Variable<Domain>& var) {
     MaxExpression<Domain>& rhs = *_system[var];
 
-    do {
-      _rho.has_changed(false);
+    // _rho automatically keeps up to date with changes made to the
+    // strategy, so you don't need to stabilise it
+
+    _strategy.get(rhs);
 
-      // improve strategy
-      _rho.freeze();
-      _strategy.thaw();
-      _strategy.get(rhs);
 
-      // iterate fixpoint
-      _strategy.freeze();
-      _rho.thaw();
+    /*
+    do {
+      _strategy.hasChanged(false);
+      
+      log::debug << "Stabilise assignment (toplevel)" << std::endl;
       _rho.stabilise();
-    } while (_rho.has_changed());
+      
+      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());
+    */
 
     return _rho[var];
   }
diff --git a/impl/VariableAssignment.hpp b/impl/VariableAssignment.hpp
index e074f6f..2e081e6 100644
--- a/impl/VariableAssignment.hpp
+++ b/impl/VariableAssignment.hpp
@@ -26,54 +26,31 @@ struct DynamicVariableAssignment : public VariableAssignment<Domain> {
       _values(system.variableCount(), value),
       _unstable(system.variableCount()),
       _influence(system.variableCount(),
-                 IdSet<Variable<Domain> >(system.variableCount())),
-      _frozen(false),
-      _changed(false)
-  {
-  }
-
-  void freeze() {
-    _frozen = true;
-  }
-
-  void thaw() {
-    _frozen = false;
-  }
-
-  bool is_frozen() const {
-    return _frozen;
-  }
-
-  void has_changed(bool c) {
-    _changed = c;
-  }
-
-  bool has_changed() const {
-    return _changed;
-  }
+                 IdSet<Variable<Domain> >(system.variableCount()))
+  { }
 
   const Domain operator[](const Variable<Domain>& var) {
-    if (!_frozen)
-      solve(var);
+    solve(var);
     return _values[var];
   }
 
-  void stabilise() {
+  /*void stabilise() {
     if (!_unstable.empty()) {
       Variable<Domain>& var = _system.variable(*_unstable.begin());
       solve(var);
     }
-  }
+    }*/
 
   void invalidate(const Variable<Domain>& x) {
-    log::fixpoint << indent() << "Invalidating " << x << std::endl;
     if (!_unstable.contains(x)) {
+      log::fixpoint << indent() << "Invalidating " << x << std::endl;
+ 
       _unstable.insert(x);
       _values[x] = infinity<Domain>();
-      _changed = true;
-     
+
       IdSet<Variable<Domain> > infl = _influence[x];
       _influence[x].clear();
+
       for (typename IdSet<Variable<Domain> >::iterator
 	     it = infl.begin(),
 	     ei = infl.end();
@@ -92,19 +69,21 @@ private:
       log::fixpoint << indent() << "Stabilise " << x << std::endl;
 
       stack_depth++;
+      // 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, _strategy);
+      Domain val = _system[x]->eval(assignment, const_strat);
       stack_depth--;
 
       if (val != _values[x]) {
         log::fixpoint << x << " = " << val << std::endl;
+ 
+        _strategy.invalidate(x);
 
         IdSet<Variable<Domain> > oldInfluence = _influence[x];
         _influence[x].clear();
         _values[x] = val;
-	_changed = true;
-
-        _strategy.invalidate(x);
 
         _unstable.absorb(oldInfluence);
 
@@ -141,8 +120,6 @@ private:
   IdMap<Variable<Domain>, Domain> _values;
   IdSet<Variable<Domain> > _unstable;
   IdMap<Variable<Domain>,IdSet<Variable<Domain> > > _influence;
-  bool _frozen;
-  bool _changed;
 };
 
 #endif
diff --git a/impl/main.cpp b/impl/main.cpp
index 94351ec..1fed389 100644
--- a/impl/main.cpp
+++ b/impl/main.cpp
@@ -1,5 +1,6 @@
 #include "Log.hpp"
 #include <iostream>
+#include <iomanip>
 #include <vector>
 #include <sstream>
 #include "Complete.hpp"
@@ -9,6 +10,8 @@
 #include "MaxStrategy.hpp"
 #include "VariableAssignment.hpp"
 
+#include <ctime>
+
 extern "C" {
 #include "parser/EquationSystemParser.h"
 #include "parser/EquationSystemLexer.h"
@@ -134,44 +137,58 @@ int main (int argc, char* argv[]) {
 
   EquationSystemParser_equation_system_return ret = parser -> equation_system(parser);
 
+  std::cerr << "Parse complete." << std::endl;
+
   EquationSystem<ZBar> system;
   treeToSystem<ZBar>(ret.tree, system);
 
   log::debug << system << endl;
   system.indexMaxExpressions(); // make reverse-lookup O(1) instead of O(n)
 
+  std::cerr << "System created and indexed." << std::endl;
+
   Solver<ZBar> solver(system); // local *and* lazy. I love it!
+
+  timespec start, finish;
+  clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &start);
   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() << " = " << solver.solve(var) << endl;
+    for (set<string>::iterator it = variables.begin(), ei = variables.end();
+         it != ei;
+         ++it) {
+      solver.solve(system.variable(*it));
     }
   } else {
     for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
       Variable<ZBar>& var = system.variable(i);
-      cout << var.name() << " = " << solver.solve(var) << endl;
+      solver.solve(var);
     }
   }
+  clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &finish);
 
-  /*
-  DynamicMaxStrategy<ZBar> strategy(system);
-  DynamicVariableAssignment<ZBar> rho(system, strategy);
-  strategy.setRho(rho);
+  std::cerr << "System solved." << std::endl;
 
   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;
+        cout << var.name() << " = " << solver.solve(var) << 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() << " = " << solver.solve(var) << endl;
     }
   }
-  */
+
+  timespec temp;
+  if ((finish.tv_nsec-start.tv_nsec)<0) {
+    temp.tv_sec = finish.tv_sec-start.tv_sec-1;
+    temp.tv_nsec = 1000000000+finish.tv_nsec-start.tv_nsec;
+  } else {
+    temp.tv_sec = finish.tv_sec-start.tv_sec;
+    temp.tv_nsec = finish.tv_nsec-start.tv_nsec;
+  }
+  cerr << "Time taken: " << temp.tv_sec << "." << setfill('0') << setw(9) << temp.tv_nsec << " seconds." << endl;
 
   parser -> free(parser);
   tokens -> free(tokens);
diff --git a/impl/systems/example.eqns b/impl/systems/example.eqns
index 71ee74a..dc59a01 100644
--- a/impl/systems/example.eqns
+++ b/impl/systems/example.eqns
@@ -1,3 +1,3 @@
-x1 = max(0, min(x1-1, x2))
+x1 = max(0, min(x1 - 1, x2))
 x2 = max(0, 5+x1, x1)
-x3 = max(0, 1+x3, 0+x1)
+x3 = max(0, 1 + x3, 0 + x1)
diff --git a/impl/test/run b/impl/test/run
index 0c1886d..169edda 100644
--- a/impl/test/run
+++ b/impl/test/run
@@ -7,7 +7,10 @@ FAILED=0
 echo "Testing binary: $1 in directory $DIR"
 while [ -f "$DIR/$NUM.eqns" ]
 do
-  OUTPUT=$($1 "$DIR/$NUM.eqns")
+  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")
   if [ ! -z "$DIFF" ]; then
     echo "=================="