#include <iostream>
#include <fstream>
#include <cstring>
#include "cudd.h"

void toDot(DdManager*, DdNode**, int, char**, char**, const char*);

DdNode* createTautology(DdManager*);
DdNode* createFunctionF(DdManager*);
DdNode* createFunctionF_x(DdManager*);
DdNode* createFunctionG(DdManager*);
DdNode* createFunctionH(DdManager*);
DdNode* createFunctionG_E(DdManager*);
DdNode* createAndIte(DdManager*);

int main(int argc, char** argv)
{
	short numVars=0;  // num of vars; if unknown set to 0
	short numVarsZ=0; // num of vars for ZBDDs; if unknown set to 0
	int numSlots=CUDD_UNIQUE_SLOTS; // default for CUDD package
	int cacheSize=CUDD_CACHE_SLOTS; // default for CUDD package
	int maxCacheSize=0; // unlimited

	// creating the manager    
	DdManager *ddman = Cudd_Init(numVars, numVarsZ, numSlots, cacheSize, maxCacheSize);

	// variables identifiers
	char** inputNames = new char*[9];
	strcpy(inputNames[0] = new char[2],"x");
	strcpy(inputNames[1] = new char[2],"y");
	strcpy(inputNames[2] = new char[2],"A" );
	strcpy(inputNames[3] = new char[2],"B");
	strcpy(inputNames[4] = new char[2],"C");
	strcpy(inputNames[5] = new char[2],"D");
	strcpy(inputNames[6] = new char[2],"a");
	strcpy(inputNames[7] = new char[2],"b");
	strcpy(inputNames[8] = new char[2],"c");

	// function identifiers
	char** outputNames;

	// printing the F,G,H functions to a dot file
	DdNode **outputs = new DdNode*[3];
	outputs[0] = createFunctionF(ddman); 
	outputs[1] = createFunctionG(ddman); 
	outputs[2] = createFunctionH(ddman); 

	outputNames = new char*[3];
	strcpy(outputNames[0] = new char[2],"F");
	strcpy(outputNames[1] = new char[2],"G");
	strcpy(outputNames[2] = new char[2],"H");

	toDot(ddman,outputs, 3, inputNames, outputNames, "F_G_H.dot");
	delete outputs;
	delete outputNames;

	// printing the Tautology to a dot file
	outputs = new DdNode*[1];
	outputs[0] = createTautology(ddman);

	outputNames = new char*[1];
	strcpy(outputNames[0] = new char[4], "Tau");

	toDot(ddman,outputs, 1, inputNames, outputNames, "tautology.dot");

	delete outputs;
	delete outputNames;

	// printing F and F_x to a dot file

	outputs = new DdNode*[2];
	outputs[0] = createFunctionF(ddman);
	outputs[1] = createFunctionF_x(ddman);

	outputNames = new char*[2];
	strcpy(outputNames[0] = new char[2], "F");
	strcpy(outputNames[1] = new char[4], "F_x");

	toDot(ddman,outputs, 2, inputNames, outputNames, "F_x.dot");

	delete outputs;
	delete outputNames;

	// printing G_E to a dot file

	outputs = new DdNode*[1];
	outputs[0] = createFunctionG_E(ddman);

	outputNames = new char*[1];
	strcpy(outputNames[0] = new char[8],"G_exist");

	toDot(ddman,outputs, 1, inputNames, outputNames, "G_exists.dot");

	delete outputs;
	delete outputNames;

	// printing AndIte to a dot file

	outputs = new DdNode*[1];
	outputs[0] = createAndIte(ddman);

	outputNames = new char*[1];
	strcpy(outputNames[0] = new char[8], "And_Ite");

	toDot(ddman,outputs, 1, inputNames, outputNames, "ite.dot");

	delete outputs;
	delete outputNames;
	// deleting the manager

	Cudd_Quit(ddman);
	return 0;
}

DdNode* createTautology(DdManager *manager)
{
	DdNode* x_var = Cudd_bddIthVar(manager,0);

	DdNode* tau = Cudd_bddOr(manager,x_var,Cudd_Not(x_var));
	Cudd_Ref(tau);

	return tau;
}

DdNode* createFunctionF_x(DdManager *manager)
{
	DdNode* func_f = createFunctionF(manager);
	DdNode* x_var = Cudd_bddIthVar(manager,0);

	DdNode* f_x = Cudd_Cofactor(manager, func_f, x_var);
	Cudd_Ref(f_x);

	return f_x;
}

DdNode* createFunctionF(DdManager *manager)
{
	DdNode* x_var = Cudd_bddIthVar(manager,0);
	DdNode* y_var = Cudd_bddIthVar(manager,1);
	DdNode* A_var = Cudd_bddIthVar(manager,2);
	DdNode* B_var = Cudd_bddIthVar(manager,3);
	DdNode* C_var = Cudd_bddIthVar(manager,4);
	DdNode* D_var = Cudd_bddIthVar(manager,5);

	DdNode* cube1 = Cudd_bddAnd(manager, Cudd_bddAnd(manager,x_var,y_var), A_var);
	Cudd_Ref(cube1);

	DdNode* cube2 = Cudd_bddAnd(manager, Cudd_bddAnd(manager,x_var,Cudd_Not(y_var)), B_var);
	Cudd_Ref(cube2);

	DdNode* cube3 = Cudd_bddAnd(manager, Cudd_bddAnd(manager,Cudd_Not(x_var),y_var), C_var);
	Cudd_Ref(cube3);

	DdNode* cube4 = Cudd_bddAnd(manager, Cudd_bddAnd(manager,Cudd_Not(x_var),Cudd_Not(y_var)), D_var);
	Cudd_Ref(cube4);

	DdNode* f = Cudd_bddOr(manager, Cudd_bddOr(manager, Cudd_bddOr(manager, cube1, cube2) , cube3), cube4);	
	Cudd_Ref(f);
	Cudd_RecursiveDeref(manager, cube1);
	Cudd_RecursiveDeref(manager, cube2);
	Cudd_RecursiveDeref(manager, cube3);
	Cudd_RecursiveDeref(manager, cube4);

	return f;
}

DdNode* createFunctionG(DdManager *manager)
{
	DdNode* x_var = Cudd_bddIthVar(manager,0);
	DdNode* y_var = Cudd_bddIthVar(manager,1);

	DdNode* g = Cudd_bddXor(manager,x_var,y_var);
	Cudd_Ref(g);

	return g;
}

DdNode* createFunctionH(DdManager *manager)
{
	DdNode* func_f = createFunctionF(manager);
	DdNode* func_g = createFunctionG(manager);

	DdNode* h = Cudd_bddCompose(manager, func_f, func_g, 0);
	Cudd_Ref(h);

	return h;
}

DdNode* createFunctionG_E(DdManager *manager)
{
	DdNode* a_var = Cudd_bddIthVar(manager, 6);
	DdNode* b_var = Cudd_bddIthVar(manager, 7);
	DdNode* c_var = Cudd_bddIthVar(manager, 8);

	DdNode* and1 = Cudd_bddAnd(manager, a_var, b_var);
	DdNode* cube1 = Cudd_bddAnd(manager,b_var,c_var);

	DdNode* g_e = Cudd_bddExistAbstract(manager, and1, cube1);
	Cudd_Ref(g_e);

	return g_e;
}

DdNode* createAndIte(DdManager * manager)
{
	DdNode* x_var = Cudd_bddIthVar(manager, 0);
	DdNode* y_var = Cudd_bddIthVar(manager, 1);

	DdNode* andIte = Cudd_bddIte(manager, x_var,y_var, Cudd_Not(Cudd_ReadOne(manager)));
	Cudd_Ref(andIte);

	return andIte;
}

void toDot(DdManager *manager, DdNode **outputs, int numOutputs, char** inames, char** onames, const char* filename)
{

	FILE *f = fopen(filename,"w");

	// manager	: The cudd manager
	// numOutputs	: The number of outputs
	// outputs	: An array of outputs (DdNode*)
	// inames	: Maps input nodes to their names
	// onames	: Maps output nodes to their names
	// f		: The file to write to

	Cudd_DumpDot(manager, numOutputs, outputs,inames, onames,f);
	fclose(f);
}
