#include "../include/Specification.h"
#include "../include/Base.h"
#include "../include/Mgr.h"

#include <stdexcept>
#include <functional>
#include <iostream>

using namespace std;

invalid_argument differentSizes(string where)
{
	return invalid_argument(where + ": Vectors of different size\n");
}

vector<BDD> add(const vector<BDD>& x, const vector<BDD>& y, const BDD& carryIn)
{
	if (x.size() != y.size()) throw differentSizes("Add");
			
	size_t n = x.size();
			
	vector<BDD> out(n + 1);
	BDD carry = carryIn;
		
	for (size_t i = 0; i < n; i++)
	{
		out[i] = x[i] ^ y[i] ^ carry;
		carry = (x[i] & y[i]) | (carry & (x[i] | y[i]));
	}
	
	out[n] = carry;
	
	return out;
}

vector<BDD> add(const vector<BDD>& x, const vector<BDD>& y) { return add(x, y, m.bddZero()); }

BDD equals(const vector<BDD>& x, const vector<BDD>& y)
{
	if (x.size() != y.size()) throw differentSizes("Equals");
			
	size_t n = x.size();
			
	BDD b = m.bddOne();
	
	for (size_t i = 0; i < n; i++) b &= x[i].Xnor(y[i]);
	
	return b;
}

BDD greaterOrEquals(const vector<BDD>& x, const vector<BDD>& y)
{
	if (x.size() != y.size()) throw differentSizes("Greater or Equals");
			
	size_t n = x.size();
			
	BDD b = m.bddOne();
	
	for (size_t i = 0; i < n; i++)
	{
		b &= x[i].Xnor(y[i]);
		b |= x[i] & !y[i];
	}
	
	return b;
}

BDD lessOrEquals(const vector<BDD>& x, const vector<BDD>& y)
{
	if (x.size() != y.size()) throw differentSizes("Less or Equals");
			
	size_t n = x.size();
			
	BDD b = m.bddOne();
	
	for (size_t i = 0; i < n; i++)
	{
		b &= x[i].Xnor(y[i]);
		b |= !x[i] & y[i];
	}
	
	return b;
}

BDD sorted(const vector<BDD>& a)
{
	int n = a.size();
	
	vector<BDD> allOnes(n + 1);
	
	allOnes[n] = m.bddOne();
	
	for (int i = n - 1; i >= 0; i--) allOnes[i] = allOnes[i + 1] & a[i];
	
	vector<BDD> sortedFrom(n + 1);
	
	sortedFrom[n] = m.bddOne();
	
	for (int i = n - 1; i >= 0; i--) sortedFrom[i] = allOnes[i] | (!a[i] & sortedFrom[i + 1]);
	
	return sortedFrom[0];
}

BDD sameWeight(const vector<BDD>& x, const vector<BDD>& y)
{
	if (x.size() != y.size()) throw differentSizes("Same weight");
			
	int n = x.size();
	
	vector<vector<BDD>> sameCount(n + 1, vector<BDD>(n + 1));
	
	sameCount[n][n] = m.bddOne();
	
	for (int i = n - 1; i >= 0; i--)
	{
		sameCount[i][n] = !x[i] & sameCount[i + 1][n];
		sameCount[n][i] = !y[i] & sameCount[n][i + 1];
	}
	
	for (int i = n - 1; i >= 0; i--)
	for (int j = n - 1; j >= 0; j--)
	{
		sameCount[i][j] =
			(x[i].Xnor(y[j]) & sameCount[i + 1][j + 1]) |
			(x[i] & !y[j] & sameCount[i][j + 1]) |
			(!x[i] & y[j] & sameCount[i + 1][j]);
	}
	
	return sameCount[0][0];
}

BDD subtractionSpec(const vector<BDD>& in1, const vector<BDD>& in2, const vector<BDD>& out)
{
	vector<BDD> aux = add(in2, out);
	aux.resize(in1.size());

	return equals(in1, aux);
}

BDD maxSpec(const vector<BDD>& in1, const vector<BDD>& in2, const vector<BDD>& out)
{
	return
		greaterOrEquals(out, in1) &
		greaterOrEquals(out, in2) &
		(equals(out, in1) | equals(out, in2));
}

BDD minSpec(const vector<BDD>& in1, const vector<BDD>& in2, const vector<BDD>& out)
{
	return
		lessOrEquals(out, in1) &
		lessOrEquals(out, in2) &
		(equals(out, in1) | equals(out, in2));
}

BDD averageSpec(const vector<BDD>& in1, const vector<BDD>& in2, const vector<BDD>& out)
{
	return equals(add(in1, in2), add(out, out));
}

BDD averageFloorSpec(const vector<BDD>& in1, const vector<BDD>& in2, const vector<BDD>& out)
{
	return averageSpec(in1, in2, out) | equals(add(in1, in2), add(out, out, m.bddOne()));
}

BDD averageCeilingSpec(const vector<BDD>& in1, const vector<BDD>& in2, const vector<BDD>& out)
{
	return averageSpec(in1, in2, out) | equals(add(in1, in2, m.bddOne()), add(out, out));
}

BDD sortingSpec(const vector<BDD>& in, const vector<BDD>& out)
{
	BDD s1 = sorted(out);
	BDD s2 = sameWeight(in, out);
	return s1 & s2;
}

BDD decompositionSpec(const vector<BDD>& in, const vector<BDD>& out1, const vector<BDD>& out2)
{
	vector<BDD> aux = add(out1, out2);
	aux.resize(in.size());

	return equals(in, aux);
}

BDD equalizationSpec(
	const vector<BDD>& in1, const vector<BDD>& in2,
	const vector<BDD>& out1, const vector<BDD>& out2)
{
	vector<BDD> aux1 = add(in1, out1);
	vector<BDD> aux2 = add(in2, out2);
	
	return equals(aux1, aux2);
}

BDD intermediateValueSpec(const vector<BDD>& in1, const vector<BDD>& in2, const vector<BDD>& out)
{
	return (greaterOrEquals(in1, out) & greaterOrEquals(out, in2))
		| (greaterOrEquals(in2, out) & greaterOrEquals(out, in1));
}