#include <iostream>
#include <vector>
#include <math.h>

#include "Operator.hpp"
#include "Expression.hpp"
#include "MaxStrategy.hpp"
#include "EquationSystem.hpp"

using namespace std;

typedef std::vector<Expression<float>*> Args;
typedef Expression<float> E;
typedef Constant<float> C;
typedef Addition<float> A;
typedef Minimum<float> Min;

std::vector< Expression<float>* > empty;
int main () {
  {
  EquationSystem<float> sys;
  Variable<float>* x = sys.newVariable("x");
  Variable<float>* y = sys.newVariable("y");
  Variable<float>* z = sys.newVariable("z");

  Args xPlusArgs;
  xPlusArgs.push_back(sys.newExpression(x, empty));

  Args xMinArgs;
  xMinArgs.push_back(sys.newExpression(new A(-1), xPlusArgs));
  xMinArgs.push_back(sys.newExpression(y, empty));

  Args xMaxArgs;
  xMaxArgs.push_back(sys.newExpression(new C(0), empty));
  xMaxArgs.push_back(sys.newExpression(new Min(), xMinArgs));

  sys[*x] = sys.newMaxExpression(xMaxArgs);
  // x = max(0, min(x-1, y))


  Args yPlusArgs;
  yPlusArgs.push_back(sys.newExpression(x, empty));

  Args yMaxArgs;
  yMaxArgs.push_back(sys.newExpression(new C(0), empty));
  yMaxArgs.push_back(sys.newExpression(new A(5), yPlusArgs));
  yMaxArgs.push_back(sys.newExpression(x, empty));

  sys[*y] = sys.newMaxExpression(yMaxArgs);
  // y = max(0, x+5, x)


  Args zPlusArgs1;
  zPlusArgs1.push_back(sys.newExpression(z, empty));

  Args zPlusArgs2;
  zPlusArgs2.push_back(sys.newExpression(x, empty));

  Args zMaxArgs;
  zMaxArgs.push_back(sys.newExpression(new C(0), empty));
  zMaxArgs.push_back(sys.newExpression(new A(1), zPlusArgs1));
  zMaxArgs.push_back(sys.newExpression(new A(0), zPlusArgs2));

  sys[*z] = sys.newMaxExpression(zMaxArgs);
  // z = max(0, z+1, x)



  // x = max(0, min(x-1, y))
  // y = max(0, x+5, x)
  // z = max(0, z+1, x)
  // => x: 0, y: 5, z: inf
  VariableAssignment<float> fixpoint = sys.minFixpoint();
  cout << "x = " << fixpoint[*x] << endl;
  cout << "y = " << fixpoint[*y] << endl;
  cout << "z = " << fixpoint[*z] << endl;
  }

  return 0;
}