/*******************************************************************************
*	fichier des fonctions pour la factorisation .			       *
*	version du MARDI 26 MARS 91					       *
*******************************************************************************/
#include <stdio.h>
#include  MUT_H
#include  LOG_H
#include"fact.h"

/*------------------------------------------------------------------------------
factorise0		:	test de possibilite de factorisation et 
				factorisation .
--------------------------------------------------------------
parametres	:	factorTab : table de hash pour les facteurs .
			g	  : le diviseur .
			m	  : = f(g = 1) .
			r	  : = f(g = 0) .
--------------------------------------------------------------
return		:	pointeur sur la structure facteur .
------------------------------------------------------------------------------*/
pFact factorise0(pC,factorTab,f1,f0,g,divRecom)
pCircuit pC ;
pTabFact factorTab ;
pNode g,f1,f0 ;
pNode *divRecom ;
{
pNode h, R2 ;
pFact hFact, rFact, factM1,factM2, factM3 ;
pNode andRM,M1,M2,M3 ;
chain_list *abl ;

/*
printf("bdd \n") ;
displayBdd(0,bdd) ;
printf("g \n") ;
displayBdd(0,g) ;
printf("f0 \n") ;
displayBdd(0,f0) ;
printf("f1 \n") ;
displayBdd(0,f1) ;
*/
andRM = applyBinBdd(AND,f0,f1) ;
/*
printf("g : \n") ;
abl = bddToAbl(g,pC->pNameI) ;
displayExpr(abl) ;
printf("f1 : \n") ;
abl = bddToAbl(f1,pC->pNameI) ;
displayExpr(abl) ;
printf("f0 : \n") ;
abl = bddToAbl(f0,pC->pNameI) ;
displayExpr(abl) ;
printf("andRM : \n") ;
abl = bddToAbl(andRM,pC->pNameI) ;
displayExpr(abl) ;
printf("\n") ;
*/
if(andRM == f0)	/* expression factorisable */
	{
	h = simplifDcOneBdd(f1, f0) ;
	/*
	printf("*************  f1\n") ;
	displayExpr(bddToAbl(f1,pC->pNameI)) ;
	printf("\n*************  h\n") ;
	displayExpr(bddToAbl(h,pC->pNameI)) ;
	printf("\n") ;
	*/
	if(h->index >= 2)
		hFact = factorise3(pC,factorTab,h,divRecom) ;
	else
		hFact = oneFact ; /* sinon ne peut etre que one */
		
	if(f0->index >= 2)
		rFact = factorise3(pC,factorTab,f0,divRecom) ;
	else
		rFact = zeroFact ; /* sinon ne peut etre que zero */

	return(initFact(factorTab,g,hFact,rFact)) ;
	}

if(andRM == f1)	/* expression factorisable */
	{
	h = simplifDcOneBdd(f0, f1) ;
	if(h->index >= 2)
		hFact = factorise3(pC,factorTab,h,divRecom) ;
	else
		hFact = oneFact ; /* sinon ne peut etre que one */
		
	if(f1->index >= 2)
		rFact = factorise3(pC,factorTab,f1,divRecom) ;
	else
		rFact = zeroFact ; /* sinon ne peut etre que zero */

	return(initFact(factorTab,notBdd(g),hFact,rFact)) ;
	}

else /* fact = M1 * h + M2 * f0 + M3 */
	{
	M1 = simplifDcOneBdd(f1,andRM) ;
	M2 = simplifDcOneBdd(f0,andRM) ;
	M3 = simplifDcOneBdd(andRM,applyBinBdd(AND,M1,M2)) ;
	/*M3 = simplifDc(M3,applyBinBdd(AND,M2,andRM)) ;*/
	if(M1 != zero && M1 != one)
		factM1 = factorise3(pC,factorTab,M1,divRecom) ;
	else
		{
		printf("factorise0 : M1 = zero ou one\n") ;
		exit(-1) ;
		}
	if(M2 != zero && M2 != one)
		factM2 = factorise3(pC,factorTab,M2,divRecom) ;
	else
		{
		printf("factorise0 : M2 = zero ou one\n") ;
		exit(-1) ;
		}
	if(M3 == zero)
		factM3 = zeroFact ;
	else
		factM3 = factorise3(pC,factorTab,M3,divRecom) ;
/*
	M1 = simplifDcOneBddOneBddZeroBdd(f1,f0) ;
	M2 = simplifDcOneBddOneBddZeroBdd(f0,f1) ;
	M3 = simplifDcOneBddOneBddZeroBdd(M1,f1) ;
	printf("*************  F(g = 0)\n") ;
	displayExpr(bddToAbl(f0,pC->pNameI)) ;
	printf("*************  F(g = 1)\n") ;
	displayExpr(bddToAbl(f1,pC->pNameI)) ;
	printf("\n*************  M1\n") ;
	displayExpr(bddToAbl(M1,pC->pNameI)) ;
	printf("\n") ;
	printf("*************  M2\n") ;
	displayExpr(bddToAbl(M2,pC->pNameI)) ;
	printf("\n*************  M3\n") ;
	displayExpr(bddToAbl(M3,pC->pNameI)) ;
	printf("\n*************  andRM\n") ;
	displayExpr(bddToAbl(andRM,pC->pNameI)) ;
	printf("\n") ;
*/
/*	R2 = simplifDcOneBdd(R2,applyBinBdd(OR,h,f0)) ;*/
/*	R2 = simplifDcOneBddOneBddZeroBdd(R2,f0) ;*/
	return(initFact(factorTab, g, factM1,
			 initFact(factorTab,notBdd(g),factM2, factM3))) ;
	}
}



pFact initFact(factorTab,g,h,r)
pTabFact factorTab ;
pNode g ;
pFact h, r ;
{
pFact fact ;

if(g == zero && zeroFact != NULL)
	{
	printf("ERREUR : initFact : g = 0\n") ; 
	exit(-1) ;
	}
if(zeroFact != NULL && h == zeroFact)
	{
	printf("ERREUR .fact.c : initFact : diviseur = 0\n") ;
	exit(-1) ;
	}
if(oneFact != NULL && r == oneFact)
	{
	printf("ERREUR .fact.c : initFact : exp + 1\n") ;
	exit(-1) ;
	}

if((fact = searchTabFact(factorTab, g,h,r)) == NULL)
	fact = addTabFact(factorTab,g,h,r) ;
return(fact) ;
}
/*------------------------------------------------------------------------------
factorise3	:	calcule H,R pour toutes les variables d'entreesg
			F = gH + R, et appelle factorise2 . 
--------------------------------------------------------------
parametres	:	factorTab : table de hash pour les facteurs .
			bdd	  : bdd a factoriser .
			pC	  : circuit contenant les variables d'entrees .
--------------------------------------------------------------
return		:	pointeur sur la structure facteur .
------------------------------------------------------------------------------*/
pFact factorise3(pC,factorTab,bdd,divRecom)
pCircuit pC ;
pTabFact factorTab ;
pNode bdd ;
pNode *divRecom ;
{
int i ;
pNode *h ;
pNode *r ;
pNode *var ;
pNode *varN ;
int nbVar ;
pFact res ;

nbVar = pC->countI ;
if(bdd == zero)
	return(zeroFact) ;
if(bdd == one)
	return(oneFact) ;
h = (pNode *)mbkalloc(nbVar * sizeof(pNode)) ;
r = (pNode *)mbkalloc(nbVar * sizeof(pNode)) ;
var = (pNode *)mbkalloc(nbVar * sizeof(pNode)) ;
varN = (pNode *)mbkalloc(nbVar * sizeof(pNode)) ;

for(i = 0; i< nbVar; i++ )
	{
	h[i] = NULL ;
	r[i] = NULL ;
	var[i] = NULL ;
	varN[i] = NULL ;
	}

initTabVar(bdd,var) ;

for(i = 0;var[i] != NULL && i < nbVar; i++)
	{
	varN[i] = notBdd(var[i]) ;
	h[i] = constraintBdd(bdd,var[i]) ;
	r[i] = constraintBdd(bdd,varN[i]) ;
	/*displayBdd(0,h[i]) ;*/
	}
/*displayTabRH(pC->pNameI,h,r,var) ;*/
res = factorise2(pC,factorTab,h,r,var,varN,0,divRecom) ;
mbkfree(h) ;
mbkfree(r) ;
mbkfree(var) ;
mbkfree(varN) ;
return(res) ;
}
/*------------------------------------------------------------------------------
factorise2	:	traite les cas particulers, sinon appelle factorise1 .	
--------------------------------------------------------------
parametres	:	factorTab : table de hash pour les facteurs .
			h	  : pteur sur la table bdd represantant les h.
			r	  : pteur sur la table bdd represantant les r.
			var	  : pteur sur la table bdd represantant les var.
			varN	  : pter sur la table bdd represantant les varN.
			index	  : index de la variable diviseur .
--------------------------------------------------------------
return		:	pointeur sur la structure facteur .
------------------------------------------------------------------------------*/
pFact factorise2(pC,factorTab,h,r,var,varN,index,divRecom)
pCircuit pC ;
pTabFact factorTab ;
pNode *h, *r, *var, *varN, *divRecom ;
int index ;
{
int i ;
pFact hF, rF ;

switch((*(h + index))->index)
	{
	case 1 :	/* F = g + R */
		rF = factorise3(pC,factorTab,r[index],divRecom) ;
		return(initFact(factorTab,var[index],oneFact,rF)) ;
		break ;
	case 0 :	/* F = g'R */
		rF = factorise3(pC,factorTab,r[index],divRecom) ;
		return(initFact(factorTab,varN[index],rF,zeroFact)) ;	
		break ;
	default :
		switch((*(r + index))->index)
			{
			case 1 :	/* F = g' + H */
				hF = factorise3(pC,factorTab,h[index],divRecom) ;
				return(initFact(factorTab,varN[index],oneFact,hF)) ;
				break ;
			case 0 :	/* F = gH */
				hF = factorise3(pC,factorTab,h[index],divRecom) ;
				return(initFact(factorTab,var[index],hF,zeroFact)) ;
				break ;
			default :
				if(var[index + 1] != NULL)
					return(factorise2(pC,factorTab,h,r,var,
							      varN,index + 1,divRecom)) ;
						
				else /* les tables h,r,var sont intacts */
					return(factorise1(pC,factorTab,h,r,var,divRecom));
								
			}
	}
}
/*------------------------------------------------------------------------------
factorise1	:	traitement des cas generaux, recherche de bon diviseur.	
--------------------------------------------------------------
parametres	:	factorTab : table de hash pour les facteurs .
			bdd	  : pteur sur bdd a factoriser.
			h	  : pteur sur la table bdd represantant les h.
			r	  : pteur sur la table bdd represantant les r.
			var	  : pteur sur la table bdd represantant les var.
--------------------------------------------------------------
return		:	pointeur sur la structure facteur .
------------------------------------------------------------------------------*/
pFact factorise1(pC,factorTab,h,r,var,divRecom)
pCircuit pC ;
pTabFact factorTab ;
pNode *h, *r, *var,*divRecom ;
{
int size, index, i ;
int cptSizef0 ;
int cptSizef1 ;
pFact fact,hF,rF ;
chain_list *abl ;
pNode andRH ;
pNode newBdd, bestBdd, bestFact() ;

/*displayTabRH(pC->pNameI,h,r,var) ;*/

if(divRecom[0] != NULL)
	{
	for(i = 0; var[i] != NULL && var[i] != divRecom[0];i++) ;
	deletOnePTabBdd(divRecom) ;
	if(var[i] != NULL)
		{
		/*printf("factorise1 : diviseur recommande non trouver\n") ;*/
		fact = factorise0(pC,factorTab,h[i],r[i],var[i],divRecom) ;
		}
	else
		fact = factorise1(pC,factorTab,h,r,var,divRecom) ;
	}
else
	{

	size = 1000000 ;

	for(i = 0; var[i] != NULL; i++)
		{
	
		andRH = applyBinBdd(AND,r[i],h[i]) ;
		if(andRH == zero) /*priorite: h et r disjoints*/
			{
			index = i ;
			break ;
			}
		else
			{
	
			cptSizef0 = syf_numberAtomFact(simplifDcOneBdd(r[i],andRH));
			cptSizef1 = syf_numberAtomFact(simplifDcOneBdd(h[i],andRH));
			/*
			sizeBdd(r[i],&cptSizef0) ;
			sizeBdd(h[i],&cptSizef1) ;
			*/
			/*printf("**** index : %d, size :%d\n",var[i]->index,cptSize);*/
			if(cptSizef1 < size )
				{
				size = cptSizef1 ;
				index = i ;
				}
			if(cptSizef0 < size )
				{
				size = cptSizef0;
				index = i ;
				}
			if((cptSizef1 == size || cptSizef0 == size) && 
					     ((var[i]->index< var[index]->index)
					     ||(h[i]->index>h[index]->index &&
						h[i]->index>r[index]->index)
					     ||(r[i]->index>h[index]->index &&
						r[i]->index>r[index]->index)))
					{
					index = i ;
					}

/*
			if(cptSizef0 == size || cptSizef1 == size)
				{
				displayExpr(bddToAbl(var[i],pC->pNameI)) ;
				}
*/
/*			if(cptSizef0 == size || cptSizef1 == size)
				{
				if(cptSizef0 == size)
					newBdd = r[i] ;
				else
					newBdd = h[i] ;
				bestBdd = bestFact(pC,applyBinBdd(AND,
						h[index], r[index]), newBdd) ;
				if(bestBdd == newBdd)
					index = i ;
				}
*/	
			}
		}
	if(MODE == OUI)
		{
		printf("**************** MEILLEUR FACT : ") ;
		displayExpr(bddToAbl(var[index],pC->pNameI)) ;
		printf("\n") ;
		}
	for(i = 0; var[i] != NULL;i++)
		if(index != i && (h[index]== h[i] || h[index] == r[i] ||
				r[index] == h[i] || r[index] == r[i] ))
			{
			if(syf_numberAtomFact(r[i]) > 3 || syf_numberAtomFact(h[i])>3)
				addBddFSM(divRecom,var[i]) ;
			if(MODE == OUI)
				{
				printf("**************** ") ;
				displayExpr(bddToAbl(var[i],pC->pNameI)) ;
				printf(" a un fact commun avec diviseur elu\n");
				}
			}	
	fact = factorise0(pC,factorTab,h[index],r[index],var[index],divRecom) ;
	/*
	abl = bddToAbl(fact->h->g,pC->pNameI) ;
	displayExpr(abl) ;
	*/
	}
return(fact) ;
}
