#ifndef EQUATION_SYSTEM_HPP
#define EQUATION_SYSTEM_HPP

#include <map>

template<typename T>
struct EquationSystem;

#include "IdSet.hpp"
#include "Expression.hpp"
#include "FixpointAlgorithm.hpp"

template<typename T>
struct MaxStrategy;

template<typename T>
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];
    }
  }
  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;
    }
  }
  const std::vector<Variable<T>*> vars() const {
    return _vars;
  }
  const Variable<T>* getVar(unsigned int i) const {
    return _vars[i];
  }
  unsigned int varCount() const {
    return _vars.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;
  }

  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;
  }
  unsigned int maxCount() const {
    return _max_expressions.count();
  }
  const MaxExpression<T>* getMax(unsigned int i) const {
    return _max_expressions[i];
  }

  MaxStrategy<T> strategy() const {
    return MaxStrategy<T>(_max_expressions.size());
  }

  VariableAssignment<T> assignment() const {
    return VariableAssignment<T>(_vars.size());
  }

  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()];
  }

  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;
  }

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

  VariableAssignment<T> maxFixpoint(const MaxStrategy<T>& strat, const FixpointAlgorithm<T>& algo) const {
    return algo.maxFixpoint(strat, *this);
  }

  VariableAssignment<T> minFixpoint(const FixpointAlgorithm<T>& algo) const {
    VariableAssignment<T> rho = assignment();
    VariableAssignment<T> lastRho = assignment();
    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;
};

#include "MaxStrategy.hpp"

#endif