#include <mut315.h>
#include <log200.h>
main()
{
pNode nodeA, nodeB, nodeC;
pNode res;
int nNode ;

printf("TEST DE DISPLAYBDD\n") ;
fflush(stdout) ;
initializeBdd(SMALL_BDD);

nodeA = createNodeTermBdd(2);
nodeB = createNodeTermBdd(3);
nodeC = createNodeTermBdd(4);

res = applyBinBdd(OR,applyBinBdd(AND,nodeB,nodeC),applyBinBdd(AND,nodeB,nodeA));

nNode = numberNodeBdd(res) + 1  ;
markBdd(res,0) ;
markXBdd(nNode,res) ;

/* Ca c'est un (or(and b c)a) -> b.c + a */

/*displayBdd(res,1);
displayBdd(res,0);*/
displayXBdd(res->index,res) ;

destroyBdd(1);
}

displayXBdd(level,bdd)
int level ;
pNode bdd ;
{
int i;

if(bdd == one || bdd == zero)
	return;


/*
if(bdd == one)
	{
	printf("one\n") ;
	printf("(%d)%d\n",bdd->mark,bdd->index) ;
	return ;
	}
if(bdd == zero)
	{
 	printf("zero\n") ; 
	printf("(%d)%d\n",bdd->mark,bdd->index) ;
	return ;
	}

*/



if(bdd != one && bdd != zero)
	{
	displayXBdd(level,bdd->high) ;
	printBdd(level,bdd);
	displayXBdd(level,bdd->low) ;
	}
}


printBdd(level,bdd)
pNode bdd ;
int level;
{
int i;

for(i = 0; i < level - bdd->index; i++)
	printf("\t") ;
printf("(%d %d %d %d)\n",bdd->mark,bdd->high->mark,bdd->low->mark,bdd->index) ;
printf("\n");
}

markXBdd(nNode,bdd)
int nNode ;
pNode bdd ;
{
 if(bdd->mark > 0)
	return ;
 if(bdd != one && bdd != zero)
	{
	markXBdd(nNode -1, bdd->high) ;
	markXBdd(nNode - 2, bdd->low) ;
	bdd->mark = nNode ;
	}
else
	{
	if(bdd == zero)
	bdd->mark = 0  ;	
	if(bdd == one)
	bdd->mark =  1 ;
	}

}

