#include "../include/WitnessSelect.h"
#include "../include/Mgr.h"

using namespace std;

Implementation witnessSelect(
	const BDD& spec,
	const vector<int>& outputIndex,
	const QEMethod& qe,
	bool defaultValue)
{
	Implementation impl = realizability(spec, outputIndex, qe);
	
	for (int i = outputIndex.size() - 1; i >= 0; i--)
	{
		for (int j = outputIndex.size() - 1; j > i; j--)
		{
			impl[i] = impl[i].Compose(impl[j], outputIndex[j]);
		}
		
		BDD defaultConstant = m.bddConstant(defaultValue);
		
		impl[i] = impl[i].Compose(defaultConstant, outputIndex[i]).Xnor(defaultConstant);
	}
	
	return impl;
}