#include "../include/TrimSubstitute.h"
#include "../include/Mgr.h"

using namespace std;

BDD tsStep(int x, const BDD& b, bool defaultValue, unordered_map<DdNode*, BDD>& table)
{
	if (b.IsZero())
	{
		return m.bddConstant(!defaultValue);
	}
	else if (b.IsOne())
	{
		return m.bddConstant(defaultValue);
	}
	else
	{
		int j = b.NodeReadIndex();
		
		if (j < x)
		{
			BDD posCofactor = b.Compose(m.bddOne(), j);
			BDD negCofactor = b.Compose(m.bddZero(), j);
			
			BDD newPos = tsRec(x, posCofactor, defaultValue, table);
			BDD newNeg = tsRec(x, negCofactor, defaultValue, table);
			
			return m.bddVar(j).Ite(newPos, newNeg);
		}
		else if (j == x && b.Compose(m.bddConstant(defaultValue), j).IsZero())
		{
			return m.bddConstant(!defaultValue);
		}
		else
		{
			return m.bddConstant(defaultValue);
		}
	} 
}

BDD tsRec(int x, const BDD& b, bool defaultValue, unordered_map<DdNode*, BDD>& table)
{
	DdNode* node = b.getNode();

	unordered_map<DdNode*, BDD>::const_iterator it = table.find(node);
	
	if (it != table.end())
	{
		return it->second;
	}
	else
	{
		BDD result = tsStep(x, b, defaultValue, table);
	
		table.emplace(node, result);
		
		return result;
	}
}

BDD tsRun(int x, const BDD& b, bool defaultValue)
{
	unordered_map<DdNode*, BDD> table;

	return tsStep(x, b, defaultValue, table);
}

Implementation trimSubstitute(const BDD& spec, const vector<int>& outputIndex, bool defaultValue)
{
	BDD b = spec;
	vector<BDD> witness(outputIndex.size());
	
	for (size_t i = 0; i < outputIndex.size(); i++)
	{
		int x = outputIndex[i];
		
		witness[i] = tsRun(x, b, defaultValue);
		
		b = b.Compose(witness[i], x);
	}
	
	return Implementation(b, witness);
}