#include "../include/Mgr.h"
#include "../CUDD/include/dddmp.h"

using namespace std;

Mgr m;

BDD Mgr::bddVar() const { return mgr.bddVar(); }

BDD Mgr::bddVar(int i) const { return mgr.bddVar(i); }

BDD Mgr::bddZero() const { return mgr.bddZero(); }

BDD Mgr::bddOne() const { return mgr.bddOne(); }

BDD Mgr::bddConstant(bool v) const { return v ? mgr.bddOne() : mgr.bddZero(); }

void Mgr::setMaxMemory(unsigned long maxMemory)
{
	mgr.SetMaxMemory(maxMemory);
}

void Mgr::storeBDD(const BDD& bdd, char filename[])
{
	Dddmp_cuddBddStore(
		mgr.getManager(),
		NULL,
		bdd.getNode(),
		NULL,
		NULL,
		DDDMP_MODE_TEXT,
		DDDMP_VARIDS,
		filename,
		NULL
	);
}

void Mgr::storeCNF(const BDD& bdd, char filename[])
{
	int clauses, news;

	Dddmp_cuddBddStoreCnf(
		mgr.getManager(),
		bdd.getNode(),
		DDDMP_CNF_MODE_MAXTERM,
		false,
		NULL,
		NULL,
		NULL,
		NULL,
		mgr.ReadNodeCount(),
		-1,
		-1,
		filename,
		NULL,
		&clauses,
		&news
	);
}

BDD Mgr::loadBDD(const string& path)
{
	char* filename = new char[path.length() + 1];
	strcpy(filename, path.c_str());
	
	DdNode* node = Dddmp_cuddBddLoad(
		mgr.getManager(),
		DDDMP_VAR_MATCHIDS,
		NULL,
		NULL,
		NULL,
		DDDMP_MODE_TEXT,
		filename,
		NULL
	);
	
	return BDD(mgr, node);
}

BDD Mgr::loadCNF(const string& path)
{
	char* filename = new char[path.length() + 1];
	strcpy(filename, path.c_str());
	
	DdNode** roots;
	int nRoots;
	
	Dddmp_cuddBddLoadCnf(
		mgr.getManager(),
		DDDMP_VAR_MATCHIDS,
		NULL,
		NULL,
		NULL,
		2,
		filename,
		NULL,
		&roots,
		&nRoots
	);
	
	return BDD(mgr, roots[0]);
}

void Mgr::dumpDot(const BDD& b, FILE* fp) const
{
	vector<BDD> single(1); single[0] = b;
	mgr.DumpDot(single, NULL, NULL, fp);
}

void Mgr::dumpDot(const BDD& b) const
{
	dumpDot(b, stdout);
}

void Mgr::dumpDot(const BDD& b, const string& dotPath) const
{
	FILE* fp = fopen(dotPath.c_str(), "a");
	
	dumpDot(b, fp);
	
	fclose(fp);
}

void Mgr::dumpDot(const vector<BDD>& roots, FILE* fp) const
{
	mgr.DumpDot(roots, NULL, NULL, fp);
}

void Mgr::dumpDot(const vector<BDD>& roots) const
{
	dumpDot(roots, stdout);
}

void Mgr::dumpDot(const vector<BDD>& roots, const string& dotPath) const
{
	FILE* fp = fopen(dotPath.c_str(), "a");
	
	dumpDot(roots, fp);
	
	fclose(fp);
}

int Mgr::nodeCount(const vector<BDD>& roots) const
{
	return mgr.nodeCount(roots);
}

void Mgr::debug(BDD b) const
{
	dumpDot(b, "../debug/bdd.dot");
}

void Mgr::debug(const vector<BDD>& roots) const
{
	dumpDot(roots, "../debug/bdds.dot");
}