#ifndef EQUATION_SYSTEM_HPP
#define EQUATION_SYSTEM_HPP

#include "Expression.hpp"
template<typename T>
struct MaxStrategy;

template<typename T>
struct EquationSystem {
  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_expressions.size());
    _max_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 (_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>& rho) const {
    VariableAssignment<T> result(_vars.size());
    for (unsigned int i = 0, size = _vars.size(); i < size; ++i) {
      result[*_vars[i]] = op(*_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]] = (*_expressions[i])(rho);
    }
    return result;
  }

  VariableAssignment<T> maxFixpoint() const {
    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;
  }

  VariableAssignment<T> maxFixpoint(const MaxStrategy<T>& strat) const {
    unsigned int size = _vars.size();
    VariableAssignment<T> result(size, infinity<T>());
    for (unsigned int i = 0; i < size; ++i) {
      result = strat(*this, result);
    }
    result = result.expand(strat(*this, result), -infinity<T>());
    for (unsigned int i = 0; i < size-1; ++i) {
      result = strat(*this, result);
    }
    return result;
  }

  VariableAssignment<T> minFixpoint() const {
    VariableAssignment<T> rho = assignment();
    VariableAssignment<T> lastRho = assignment();
    MaxStrategy<T> strat = strategy();
    do {
      lastRho = rho;
      strat = strat.improve(*this, rho);
      rho = maxFixpoint(strat);
    } while(lastRho != rho);
    return rho;
  }
  private:
  std::vector<Variable<T>*> _vars;
  std::vector<MaxExpression<T>*> _max_expressions;
  std::vector<Expression<T>*> _expressions;
};

#include "MaxStrategy.hpp"

#endif