1 files changed, 106 insertions, 102 deletions

diff --git a/impl/EquationSystem.hpp b/impl/EquationSystem.hpp
index 13319e0..50a0e45 100644
--- a/impl/EquationSystem.hpp
+++ b/impl/EquationSystem.hpp
@@ -1,141 +1,145 @@
 #ifndef EQUATION_SYSTEM_HPP
 #define EQUATION_SYSTEM_HPP
 
+#include <vector>
+#include <set>
 #include <map>
-
-template<typename T>
-struct EquationSystem;
-
-#include "IdSet.hpp"
+#include "Operator.hpp"
 #include "Expression.hpp"
-#include "FixpointAlgorithm.hpp"
+#include "VariableAssignment.hpp"
 
-template<typename T>
-struct MaxStrategy;
-
-template<typename T>
+template<typename Domain>
 struct EquationSystem {
-  virtual ~EquationSystem() {
-    for (int i = 0, size = _expressions.size(); i < size; ++i) {
-      delete _expressions[i];
-    }
-    for (int i = 0, size = _vars.size(); i < size; ++i) {
-      delete _vars[i];
+  virtual ~EquationSystem() { }
+  virtual const Expression<Domain>* operator[](const Variable<Domain>&) const = 0;
+  virtual VariableAssignment<Domain>* eval(const VariableAssignment<Domain>& rho) const = 0;
+  virtual unsigned int variableCount() const = 0;
+  virtual Variable<Domain>& variable(unsigned int) const = 0;
+  virtual StableVariableAssignment<Domain>* assignment(const Domain& value) const = 0;
+  virtual bool equalAssignments(const VariableAssignment<Domain>&, const VariableAssignment<Domain>&) const = 0;
+
+  virtual void print(std::ostream& cout) const = 0;
+};
+
+template<typename Domain>
+struct ConcreteEquationSystem : public EquationSystem<Domain> {
+  virtual ~ConcreteEquationSystem() {
+    for (typename std::set<Expression<Domain>*>::iterator it = _expressions.begin();
+         it != _expressions.end();
+         ++it) {
+      delete *it;
     }
-  }
-  Variable<T>* newVariable(const std::string& name) {
-    typename std::map<const std::string, Variable<T>*>::iterator it = _var_names.find(name);
-    if (it == _var_names.end()) {
-      Variable<T>* newVar = new Variable<T>(_vars.size(), name);
-      _vars.push_back(newVar);
-      _var_names[name] = newVar;
-      return _vars[_vars.size()-1];
-    } else {
-      return it->second;
+    for (typename std::set<Operator<Domain>*>::iterator it = _operators.begin();
+         it != _operators.end();
+         ++it) {
+      delete *it;
     }
   }
-  const std::vector<Variable<T>*> vars() const {
-    return _vars;
+
+  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);
+    _operators.insert(max);
+    _max_expressions.push_back(expr);
+    _expressions.insert(expr);
+    return *expr;
   }
-  const Variable<T>* getVar(unsigned int i) const {
-    return _vars[i];
+  MaxExpression<Domain>& maxExpression(unsigned int i) const {
+    return *_max_expressions[i];
   }
-  unsigned int varCount() const {
-    return _vars.size();
+  unsigned int maxExpressionCount() const {
+    return _max_expressions.size();
   }
 
-  Expression<T>* newExpression(Operator<T>* op, const std::vector<Expression<T>*>& args=std::vector<Expression<T>*>()) {
-    Expression<T>* expr = new Expression<T>(op, args);
-    _expressions.push_back(expr);
-    return expr;
+  Expression<Domain>& expression(Operator<Domain>* op, const std::vector<Expression<Domain>*>& arguments) {
+    Expression<Domain>* expr = new OperatorExpression<Domain>(*op, arguments);
+    _operators.insert(op);
+    _expressions.insert(expr);
+    return *expr;
   }
 
-  MaxExpression<T>* newMaxExpression(const std::vector<Expression<T>*>& args) {
-    MaxExpression<T>* expr = new MaxExpression<T>(args);
-    expr->id(_max_expressions.size());
-    _max_expressions.push_back(expr);
-    _expressions.push_back(expr);
-    return expr;
+  Variable<Domain>& variable(const std::string& name) {
+    if (_variable_names.find(name) == _variable_names.end()) {
+      // not found - create a new variable and whatnot
+      unsigned int id = _variables.size();
+      Variable<Domain>* var = new Variable<Domain>(id, name);
+      _variables.push_back(var);
+      _right_sides.push_back(NULL);
+      _expressions.insert(var);
+      _variable_names[name] = var;
+      return *var;
+    } else {
+      return *_variable_names[name];
+    }
   }
-  unsigned int maxCount() const {
-    return _max_expressions.count();
+  Variable<Domain>& variable(unsigned int id) const {
+    return *_variables[id];
   }
-  const MaxExpression<T>* getMax(unsigned int i) const {
-    return _max_expressions[i];
+  unsigned int variableCount() const {
+    return _variables.size();
   }
 
-  MaxStrategy<T> strategy() const {
-    return MaxStrategy<T>(_max_expressions.size());
+  Constant<Domain>& constant(const Domain& value) {
+    Constant<Domain>* constant = new Constant<Domain>(value);
+    _expressions.insert(constant);
+    return *constant;
   }
 
-  VariableAssignment<T> assignment() const {
-    return VariableAssignment<T>(_vars.size());
+  Expression<Domain>* operator[](const Variable<Domain>& var) const {
+    return _right_sides[var.id()];
   }
-
-  Expression<T>*& operator[] (const Variable<T>& v) {
-    if (_right_expressions.size() <= v.id()) {
-      _right_expressions.resize(v.id()+1);
-    }
-    return _right_expressions[v.id()];
-  }
-  const Expression<T>* operator[] (const Variable<T>& v) const {
-    if (_right_expressions.size() <= v.id()) {
-      throw "Out of range";
-    }
-    return _right_expressions[v.id()];
+  Expression<Domain>*& operator[](const Variable<Domain>& var) {
+    return _right_sides[var.id()];
   }
 
-  template<typename F>
-  VariableAssignment<T> foreach(F op, const VariableAssignment<T>& rho) const {
-    VariableAssignment<T> result(_vars.size());
-    for (unsigned int i = 0, size = _vars.size(); i < size; ++i) {
-      result[*_vars[i]] = op(*_right_expressions[i], rho);
-    }
-    return result;
+  StableVariableAssignment<Domain>* assignment(const Domain& value) const {
+    return new StableVariableAssignment<Domain>(_variables.size(), value);
   }
-
-  VariableAssignment<T> operator() (const VariableAssignment<T>& rho) const {
-    VariableAssignment<T> result(_vars.size());
-    for (unsigned int i = 0, size = _vars.size(); i < size; ++i) {
-      result[*_vars[i]] = (*_right_expressions[i])(rho);
+  VariableAssignment<Domain>* eval(const VariableAssignment<Domain>& rho) const {
+    StableVariableAssignment<Domain>* result = this->assignment(-infinity<Domain>());
+    for (unsigned int i = 0, length = _variables.size();
+         i < length;
+         ++i) {
+      const Variable<Domain>& var = *_variables[i];
+      const Expression<Domain>& expr = * (*this)[var];
+      (*result)[var] = expr.eval(rho);
     }
     return result;
   }
 
-  VariableAssignment<T> maxFixpoint() const {
-    unsigned int size = _vars.size();
-    VariableAssignment<T> newResult(size, infinity<T>());
-    VariableAssignment<T> result(0);
-    do {
-      result = newResult;
-      newResult = (*this)(result);
-    } while (newResult != result);
-    return result;
+  virtual bool equalAssignments(const VariableAssignment<Domain>& l, const VariableAssignment<Domain>& r) const {
+    for (unsigned int i = 0, length = _variables.size();
+         i < length;
+         ++i) {
+      const Variable<Domain>& var = *_variables[i];
+      if (l[var] != r[var])
+        return false;
+    }
+    return true;
   }
 
-  VariableAssignment<T> maxFixpoint(const MaxStrategy<T>& strat, const FixpointAlgorithm<T>& algo) const {
-    return algo.maxFixpoint(strat, *this);
+  void print(std::ostream& cout) const {
+    for (unsigned int i = 0, length = _variables.size();
+         i < length;
+         ++i) {
+      cout << *_variables[i] << " = " << *_right_sides[i] << std::endl;
+    }
   }
 
-  VariableAssignment<T> minFixpoint(const FixpointAlgorithm<T>& algo) const {
-    VariableAssignment<T> rho = assignment();
-    VariableAssignment<T> lastRho(0);
-    MaxStrategy<T> strat = strategy();
-    do {
-      lastRho = rho;
-      strat = strat.improve(*this, rho);
-      rho = maxFixpoint(strat, algo);
-    } while(lastRho != rho);
-    return rho;
-  }
   private:
-  std::map<const std::string, Variable<T>*> _var_names;
-  std::vector<Variable<T>*> _vars;
-  std::vector<MaxExpression<T>*> _max_expressions;
-  std::vector<Expression<T>*> _expressions;
-  std::vector<Expression<T>*> _right_expressions;
+  std::set<Operator<Domain>*> _operators;
+  std::set<Expression<Domain>*> _expressions;
+  std::vector<Variable<Domain>*> _variables;
+  std::map<std::string, Variable<Domain>*> _variable_names;
+  std::vector<MaxExpression<Domain>*> _max_expressions;
+  std::vector<Expression<Domain>*> _right_sides;
 };
 
-#include "MaxStrategy.hpp"
+template<typename T>
+std::ostream& operator<<(std::ostream& cout, const EquationSystem<T>& system) {
+  system.print(cout);
+  return cout;
+}
 
 #endif