#include "Implementation.h"

#include <vector>
#include <functional>

using QEMethod = std::function<BDD(int, const BDD&)>;

BDD defaultOne(int x, const BDD& b);

BDD defaultZero(int x, const BDD& b);

BDD shannonExpansion(int x, const BDD& b);

BDD selfSubstitution(int x, const BDD& b);

BDD negSelfSubstitution(int x, const BDD& b);

Implementation realizability(
	const BDD& spec,
	const std::vector<int>& outputIndex,
	const QEMethod& qe);