Bit more work. maxFixpoint should be working now.

1 files changed, 79 insertions, 0 deletions

diff --git a/impl/EquationSystem.hpp b/impl/EquationSystem.hpp
new file mode 100644
index 0000000..065a1a2
--- /dev/null
+++ b/impl/EquationSystem.hpp
@@ -0,0 +1,79 @@
+#ifndef EQUATION_SYSTEM_HPP
+#define EQUATION_SYSTEM_HPP
+
+#include "Expression.hpp"
+
+template<typename T>
+struct EquationSystem {
+  EquationSystem ()
+    : _max_id(0) { }
+  virtual ~EquationSystem() {
+    for (int i = 0, size = _vars.size(); i < size; ++i) {
+      delete _vars[i];
+    }
+  }
+  Variable<T>* newVariable(const std::string&) {
+    _vars.push_back(new Variable<T>(_vars.size()));
+    return _vars[_vars.size()-1];
+  }
+  unsigned int varCount() const {
+    return _vars.size();
+  }
+  MaxExpression<T>* newMaxExpression(const std::vector<Expression<T>*>& args) {
+    MaxExpression<T>* expr = new MaxExpression<T>(args);
+    expr->id(_max_id++);
+    return expr;
+  }
+  unsigned int maxCount() const {
+    return _max_id;
+  }
+
+  Expression<T>*& operator[] (const Variable<T>& v) {
+    if (_expressions.size() <= v.id()) {
+      _expressions.resize(v.id()+1);
+    }
+    return _expressions[v.id()];
+  }
+  const Expression<T>*& operator[] (const Variable<T>& v) const {
+    if (_expressions.size() <= v.id()) {
+      throw "Out of range";
+    }
+    return _expressions[v.id()];
+  }
+
+  template<typename F>
+  VariableAssignment<T> foreach(F op, const VariableAssignment<T>& v) {
+    VariableAssignment<T> result(_vars.size());
+    for (unsigned int i = 0, size = _vars.size(); i < size; ++i) {
+      result[_vars[i]] = op(_expressions[i], v);
+    }
+  }
+
+  VariableAssignment<T> operator() (const VariableAssignment<T>& rho) {
+    VariableAssignment<T> result(_vars.size());
+    for (unsigned int i = 0, size = _vars.size(); i < size; ++i) {
+      result[*_vars[i]] = (*_expressions[i])(rho);
+    }
+    return result;
+  }
+
+  VariableAssignment<T> maxFixpoint() {
+    unsigned int size = _vars.size();
+    VariableAssignment<T> result(size, infinity<T>());
+    for (unsigned int i = 0; i < size; ++i) {
+      result = (*this)(result);
+    }
+    result = result.expand((*this)(result), -infinity<T>());
+    for (unsigned int i = 0; i < size-1; ++i) {
+      result = (*this)(result);
+    }
+    return result;
+  }
+  private:
+  unsigned int _max_id;
+  std::vector<Variable<T>*> _vars;
+  std::vector<Expression<T>*> _expressions;
+};
+
+
+#endif