#include "../include/QuantifierElimination.h"
#include "../include/Mgr.h"

using namespace std;

BDD defaultOne(int x, const BDD& b)
{
	return b.Compose(m.bddOne(), x);
}

BDD defaultZero(int x, const BDD& b)
{
	return !b.Compose(m.bddZero(), x);
}

BDD shannonExpansion(int x, const BDD& b)
{
	return b.Compose(m.bddOne(), x) | b.Compose(m.bddZero(), x);
}

BDD selfSubstitution(int x, const BDD& b)
{
	return b.Compose(defaultOne(x, b), x);
}

BDD negSelfSubstitution(int x, const BDD& b)
{
	return b.Compose(defaultZero(x, b), x);
}

Implementation realizability(
	const BDD& spec,
	const vector<int>& outputIndex,
	const QEMethod& qe)
{
	vector<BDD> b(outputIndex.size());
	
	BDD last = spec;
	
	for (size_t i = 0; i < outputIndex.size(); i++)
	{
		b[i] = last;
		last = qe(outputIndex[i], last);
	}

	return Implementation(last, b);
}