/*******************************************************************************
*									       *
*									       *
*      fonctions pour la simplification utilisant les don't care, basees sur   *
*      expansion.							       *
*      la version du 13.06.91,		 changement : 2/03/92 .		       *
*									       *
*******************************************************************************/
#include<stdio.h>
#include<math.h>
#include MUT_H
#include LOG_H
#include"dc.h"

#define NB_VAR 190
/*------------------------------------------------------------------------------
simplifDcAbl 	: simplifie un ABL en utilisant un ABL don't care .
-------------------------------------------------------
parametres 	: deux pointeurs de ABL.
-------------------------------------------------------
return 		: un pointeur de ABL.
------------------------------------------------------------------------------*/
chain_list *simplifDcAbl(abl,ablDc)
chain_list *abl,*ablDc ;
{
pNode bdd, bddDc, bddSimpl ;
pCircuit pC;
chain_list *ablSimpl, *name, *nameDc ;

printf("abl : \n") ;
displayExpr(abl) ;
printf("ablDc : \n") ;
displayExpr(ablDc) ;
name = supportChain_listExpr(abl) ;
nameDc = supportChain_listExpr(ablDc) ;
initializeBdd(SMALL_BDD) ;
pC = initializeCct("dc",10,10) ;
while(name)
	{
	addInputCct(pC,name->DATA) ;
	name = name->NEXT ;
	}	
while(nameDc)
	{
	addInputCct(pC,nameDc->DATA) ;
	nameDc = nameDc->NEXT ;
	}	
bdd = ablToBddCct(pC,abl) ;
bddDc = ablToBddCct(pC,ablDc) ;
bddSimpl = simplifDc(bdd,bddDc) ;
ablSimpl = bddToAblCct(pC,bddSimpl) ;
printf("ablSimplif : \n") ;
displayExpr(ablSimpl) ;
destroyCct(pC) ;
destroyBdd(1) ;
return(ablSimpl) ;
}
/*------------------------------------------------------------------------------
simplifDc 	: simplifie un BDD avec un BDD correspondant a un Don't Care.
-------------------------------------------------------
parametres 	: deux pointeurs de NODE.
-------------------------------------------------------
return 		: un pointeur de NODE.
------------------------------------------------------------------------------*/
pNode simplifDc(bdd,bddDc)
pNode bdd,bddDc;
{
pNode *monomOn, *reduceMonom ;
pNode bddR, bddOn, bddOff ;
int i, nbLiteral = 0, sizeTabFunc ;
int *tabIndexOn ;

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

bddOn = applyBinBdd(AND,bdd,notBdd(bddDc)) ;
if(bddOn == zero || bddOn == one)
	return(bddOn) ;
bddOff = notBdd(applyBinBdd(OR,bdd,bddDc)) ;

if(!(tabIndexOn = (int *)malloc(NB_VAR * sizeof(int *))))
	{
	printf("simp.c : allocation impossible\n") ;
	exit(-1) ;
	}
for(i = 0;i < NB_VAR;i++)
	tabIndexOn[i] = (int)NULL ;

countLiteralBdd(bddOn,&nbLiteral,tabIndexOn) ;


sizeTabFunc = (int)pow(2.0,(double)nbLiteral)/4 + 2 ;

if(!(monomOn = (pNode *)malloc((sizeTabFunc * sizeof(pNode)) + 1)))
	{
	printf("allocation impossible\n") ;
	exit(-1) ;
	}
if(!(reduceMonom = (pNode *)malloc((sizeTabFunc * sizeof(pNode)) + 1)))
	{
	printf("allocation impossible\n") ;
	exit(-1) ;
	}

initializeTabPBdd(sizeTabFunc + 1,monomOn) ;
initializeTabPBdd(sizeTabFunc + 1,reduceMonom) ;

monomBdd(bddOn,monomOn,one) ;
syf_expanse(bddOff,monomOn,reduceMonom) ;

bddR = orMonom(reduceMonom) ;

return(bddR) ;
}
/*------------------------------------------------------------------------------
monomBdd 	: extrait les monomes a partir d'un BDD.
-------------------------------------------------------
parametres 	: monom : semi_monome deja trouve(par recursion) .
		  bdd	: bdd a faire explose .
		  tabMonom: pointeur sur la table des monomes, a remplir .
-------------------------------------------------------
return 		: void .
------------------------------------------------------------------------------*/
void monomBdd(bdd,tabMonom,monom)
pNode *tabMonom ;
pNode bdd, monom ;
{
pNode monomH, monomL ;
			/* branche HIGH */
if(bdd->high == one)
	{
	monomH = applyBinBdd(AND,monom,createNodeTermBdd(bdd->index)) ;
	addBdd(tabMonom,monomH) ;
	}
else
	if(bdd->high != zero)
		{
		monomH = applyBinBdd(AND,monom,createNodeTermBdd(bdd->index)) ;
		monomBdd(bdd->high,tabMonom,monomH) ;
		}
			/* branche LOW */
if(bdd->low == one)
	{
	monomL = applyBinBdd(AND,monom,notBdd(createNodeTermBdd(bdd->index))) ;
	addBdd(tabMonom,monomL) ;
	}
else
	if(bdd->low != zero)
	    {
	    monomL=applyBinBdd(AND,monom,notBdd(createNodeTermBdd(bdd->index)));
	    monomBdd(bdd->low,tabMonom,monomL) ;
	    }
}
/*------------------------------------------------------------------------------
syf_expanse 	: expanse les monomes (*monom), sans toucher a l'espace de xBdd.
-------------------------------------------------------
parametres 	: xBdd  : bdd dont l'intersection avec les monomes doit etre 0 .
		  monomTab : pointeur sur la table des monomes .
		  reduceMonom : pointeur sur la table des monomes reduits
		  (a remplir) .
-------------------------------------------------------
return 		: void .
------------------------------------------------------------------------------*/
void syf_expanse(xBdd,monomTab,reduceMonom)
pNode xBdd ;
pNode *monomTab,*reduceMonom ;
{
int i;

for(i = 0; monomTab[i] != NULL; i++)
	expanseMonom(xBdd,monomTab[i],reduceMonom,0) ;	
}
/*------------------------------------------------------------------------------
expanseMonom 	: expanse le monome (monom), sans toucher a l'espace de xBdd.
-------------------------------------------------------
parametres 	: xBdd  : bdd dont l'intersection avec les monomes doit etre 0 .
		  monom : monome a expanser .
		  reduceMonom : pointeur sur la table des monomes reduits
		  (a remplir) .
		  niveau : comme la fonction est recursive, represente le nbre
		  de literaux qui ont ete deja traites .
-------------------------------------------------------
return 		: void .
------------------------------------------------------------------------------*/
void expanseMonom(xBdd,monom,reduceMonom,niveau)
pNode xBdd, monom ;
pNode *reduceMonom ;
int niveau ;
{
pNode literal, nodeCur, bdd, inters, bddR ;
int i ;

if(monom == one || monom == zero)
	{
	printf("expansion zero ou one\n") ;
	exit(-1) ;
	}
/*printf("********expanseMonom : %d\n",monom) ;*/
bdd = monom ;
bddR = monom ;
nodeCur = monom ;

/*
for(i = 0;i<niveau; i++)
	if(nodeCur->low == zero)
		nodeCur = nodeCur->high ;
	else
		nodeCur = nodeCur->low ;
*/

while(nodeCur != one)
	{
	literal = createNodeTermBdd(nodeCur->index) ;
	if(nodeCur->low == zero)
		{
		bdd = constraintBdd(monom,literal) ;
		nodeCur = nodeCur->high ;
		}
	else	
		{
		bdd = constraintBdd(monom,notBdd(literal)) ;
		nodeCur = nodeCur->low ;
		}
	inters = applyBinBdd(AND,bdd,xBdd) ;
	niveau++ ;
	if(inters == zero)
		{
		bddR = bdd ;
		break ;
		}
	if(inters == xBdd) /* => bdd = one */
		bddR = monom ;
	}
if(nodeCur != one)
	expanseMonom(xBdd,bdd,reduceMonom,niveau) ;
else
	addBdd(reduceMonom,bddR) ;
}
/*------------------------------------------------------------------------------
orMonom		: effectue l`operation OR sur tous les elements de la table .
-------------------------------------------------------
parametres 	: pTabBdd .
-------------------------------------------------------
return 		: bdd resultant .
------------------------------------------------------------------------------*/
pNode orMonom(pTabBdd)
pNode *pTabBdd ;
{
int i ;
pNode bddR ;

bddR = zero ;
for(i = 0; pTabBdd[i] != NULL; i++)
	bddR = applyBinBdd(OR,bddR,pTabBdd[i]) ;
return(bddR) ;
}
/*------------------------------------------------------------------------------
initializeTabPBdd: initialise la table des Bdd .
-------------------------------------------------------
parametres 	: sizeTab  : la taille de la table .
		  pTabBdd: pointeur sur la table des Bdd .
-------------------------------------------------------
return 		: void .
------------------------------------------------------------------------------*/
void initializeTabPBdd(sizeTab,pTabBdd)
int sizeTab ;
pNode *pTabBdd ;
{
int i ;

for(i = 0; i < sizeTab; i++)
	pTabBdd[i] = NULL ;
}
/*------------------------------------------------------------------------------
addBdd		: ajoute un bdd dans la table des bdd.
-------------------------------------------------------
parametres 	: bdd  : bdd a ajouter .
		  pTabBdd: pointeur sur la table des Bdd .
-------------------------------------------------------
return 		: void .
------------------------------------------------------------------------------*/
void addBdd(pTabBdd,bdd)
pNode *pTabBdd, bdd ;
{
int i ;

for(i = 0; pTabBdd[i] != NULL; i++) ;
	pTabBdd[i] = bdd ;
}
/*------------------------------------------------------------------------------
countLiteralBdd	: compte le nbre de literaux d'un BDD .
-------------------------------------------------------
parametres 	: bdd .
		  nbLit : nbre de literaux(fonction recursive) .
		  tabIndex : pointe la table des index .
-------------------------------------------------------
return 		: void .
------------------------------------------------------------------------------*/
void countLiteralBdd(bdd,nbLit,tabIndex)
pNode bdd ;
int *nbLit, *tabIndex ;
{
int i ;

/*printf("incrementation\n") ;*/
if(bdd != zero && bdd != one)
	{
	for(i = 0; tabIndex[i] != (int)NULL && tabIndex[i] != (int)bdd->index ;i++) ;
	if(tabIndex[i] == (int)NULL)
		{
		/*printf("j'ajoute\n") ;*/
		*nbLit = (*nbLit) + 1 ;
		tabIndex[i] = bdd->index ;
		}
	countLiteralBdd(bdd->high,nbLit,tabIndex) ;
	countLiteralBdd(bdd->low,nbLit,tabIndex) ;
	}
/*printf("fin\n") ;*/
}
