/****************************************************************************/
/*                                                                          */
/*                      Chaine de CAO & VLSI   Alliance                     */
/*                                                                          */
/*    Produit : librairie BDD - Gestion de BDD				    */
/*    Fichier : bdd0.c                                                     */
/*                                                                          */
/*    (c) copyright 1991 Laboratoire MASI equipe CAO & VLSI                 */
/*    Tous droits reserves                                                  */
/*    Support : e-mail cao-vlsi@masi.ibp.fr                                 */
/*                                                                          */
/*    Auteur(s) :   Burgun Luc                          le : 07/01/92       */
/*                                                                          */
/*    Modifie par :                                     le : ../../....     */
/*    Modifie par :                                     le : ../../....     */
/*    Modifie par :                                     le : ../../....     */
/*                                                                          */
/****************************************************************************/

#include<stdio.h>
#include MUT_H
#include "log200.h"

#undef NAME_ATOM
#undef MIN_OPER
#undef MAX_OPER
#define MIN_OPER 0
#define MAX_OPER 7

#define NAME_ATOM createAtom(*(tabName + pt->index - 2)) 

/*------------------------------------------------------------------------------
initVertexBdd 	 :cree un noeud BDD . 
-------------------------------------------------------
parametres 	 :index de la variable.
		  pointeurs sur les noeuds fils.
-------------------------------------------------------
return 		 :pointeur sur le noeud cree.
------------------------------------------------------------------------------*/

pNode initVertexBdd(index,high,low)
int index;
pNode high,low;
{
pNode pt;


if ((pt = searchTableBdd(sysBdd.pRT,index,high,low)) != NULL)
   if (pt != BDDTABLE_PLEINE)
      return(pt);
   else
      {
      sysBdd.pRT = reAllocTableBdd(sysBdd.pRT);
      return(initVertexBdd(index,high,low));
      }

if (high == low)            /* noeud eliminable */
   return(high);

if (sysBdd.indiceAT == MAX_PACK)
   {
   sysBdd.pAT = (pNode) mbkalloc (MAX_PACK * sizeof (struct node));
   sysBdd.indiceAT = 1;
   sysBdd.lpAT = addchain(sysBdd.lpAT,(void *)sysBdd.pAT) ;
   }
else
  {
  sysBdd.pAT++;
  sysBdd.indiceAT++;
  }

pt = sysBdd.pAT;
pt->index = index;
pt->high = high;
pt->low = low;
pt->mark = 0;
if (index > 1)
   if (addTableBdd(sysBdd.pRT,pt) == TABLE_PLEINE)   /* table pleine */
      {
      sysBdd.pRT = reAllocTableBdd(sysBdd.pRT);
      return(initVertexBdd(index,high,low));
      }
return(pt);
}

/*------------------------------------------------------------------------------
createNodeTermBdd  :cree un noeud variable . 
-------------------------------------------------------
parametres 	 :index de la variable.
-------------------------------------------------------
return 		 :pointeur sur le noeud cree.
------------------------------------------------------------------------------*/

pNode createNodeTermBdd(index)
short index;
{
pNode pt ;

if (index <= 1)
   {
   printf("createNodeTermBdd : error index <= 1\n");
   exit(-1);
   }
else
   {
   pt = initVertexBdd(index,one,zero);
   return(pt);
   }
}

/*------------------------------------------------------------------------------
initializeBdd: Initialise le systeme de la boite a outils des BDD.
-------------------------------------------------------
parametres 	 :rien .
-------------------------------------------------------
return 		 :rien.
------------------------------------------------------------------------------*/

void initializeBdd(size)
int size ;
{
switch(size)
	{
	case 0 :
		sysBdd.pRT = createTableBdd(SMALL);
		break ;
	case 1 :
		sysBdd.pRT = createTableBdd(MEDIUM);
		break ;
	case 2 :
		sysBdd.pRT = createTableBdd(LARGE);
		break ;
	default :
		printf("initializeBdd : size out of bound\n") ;
		exit(-1) ;
	}	

sysBdd.pMC = createTabLoc(MEDIUM);
sysBdd.indiceAT = MAX_PACK;
sysBdd.lpAT = NULL;

zero = initVertexBdd(0,(pNode)0,(pNode)1);
one  = initVertexBdd(1,(pNode)0,(pNode)1);
}

/*------------------------------------------------------------------------------
destroyBdd        :desalloue le systeme de la boite a outils des BDD.
-------------------------------------------------------
parametres 	 :niveau de desallocation .
-------------------------------------------------------
return 		 :rien.
------------------------------------------------------------------------------*/

void destroyBdd(level)
int level;
{
chain_list *pt;

if(level == 1)
	{
	pt = sysBdd.lpAT ;
	while(pt != NULL)	/* desallocation des pages de noeuds */
		{
		mbkfree((pNode)pt->DATA) ;
		pt = pt->NEXT ;
		}
	freechain(sysBdd.lpAT) ;
	sysBdd.lpAT = NULL ;
	}
else
	{
	freechain(sysBdd.lpAT) ;
 	sysBdd.lpAT = NULL;
	}
destroyTableBdd(sysBdd.pRT);              /* les tables de hachage */
destroyTabLoc(sysBdd.pMC);
}

/*------------------------------------------------------------------------------
resetBdd        :vide le systeme de la boite a outils des BDD.
-------------------------------------------------------
parametres 	 :rien
-------------------------------------------------------
return 		 :rien.
------------------------------------------------------------------------------*/

void resetBdd()
{
int i ;
pNode *pBdd ;
chain_list *pt ;

pt = sysBdd.lpAT ;
while(pt)	/*vide la liste d'allocation par paquet */
	{
	mbkfree((pNode)pt->DATA) ;
	pt = pt->NEXT ;
	}
freechain(sysBdd.lpAT) ;
sysBdd.lpAT = NULL ;

videTabLoc(sysBdd.pMC);

pBdd = (sysBdd.pRT)->pBdd;
for(i=0;i < sysBdd.pRT->lenTableBdd;i++)   /* vide la table de reduction */
	{
   	*pBdd = NULL;
   	pBdd++;
   	}
(sysBdd.pRT)->compteur = 0;
sysBdd.indiceAT = MAX_PACK;

zero = initVertexBdd(0,(pNode)0,(pNode)1);
one  = initVertexBdd(1,(pNode)0,(pNode)1);
}

/*------------------------------------------------------------------------------
numberNodeAllBdd :compte le nombre de noeud utilise dans le systeme. 
-------------------------------------------------------
return 		 :le nombre de noeud.
------------------------------------------------------------------------------*/

int numberNodeAllBdd()
{
return ((sysBdd.pRT)->compteur);
}

/*------------------------------------------------------------------------------
numberNodeBdd       :compte le nombre de noeud reduits d'un graphe.
-------------------------------------------------------
parametres 	 :un pointeur de Node.
-------------------------------------------------------
return 		 :le nombre de noeud.
------------------------------------------------------------------------------*/

int numberNodeBdd(pBdd)
pNode pBdd;
{
int val;

markBdd(pBdd,-1);
markBdd(pBdd,0);
val = countNode(pBdd);
markBdd(pBdd,0);
return(val);
}

/*------------------------------------------------------------------------------
countNode        : calcul du nombre de noeuds BDD 
-------------------------------------------------------
parametres 	 : une pNode
-------------------------------------------------------
return 		 : int
------------------------------------------------------------------------------*/
int countNode(pt)
pNode pt;
{
if (pt->index > 1)
   {
   if (pt->mark == 0)
      {
      pt->mark = 1;
      return(countNode(pt->high) + countNode(pt->low) + 1);
      }
   }
return(0);
}

/*------------------------------------------------------------------------------
countNodeTdg     : calcul du nombre de noeuds equivalent TDG sur un BDD 
-------------------------------------------------------
parametres 	 : une pNode
-------------------------------------------------------
return 		 : int
------------------------------------------------------------------------------*/
int countNodeTdg(pt)
pNode pt;
{
if (pt->index > 1)
   {
   if (pt->mark == 0)
      {
      int val;
      pt->mark = 1;
      val = countNodeTdg(pt->high) + countNodeTdg(pt->low) + 1;
      markBdd(notBdd(pt),1);
      return val;
      }
   }
return(0);
}

/*------------------------------------------------------------------------------
muxAbl          : realise le multiplexeur a.H + a'.L
-------------------------------------------------------
parametres 	 : Deux pointeurs de Node et un pointeur de CHAIN_LIST.
-------------------------------------------------------
return 		 :une pointeur de CHAIN_LIST.
------------------------------------------------------------------------------*/
chain_list *muxAbl(high,low,a,tabName)
pNode high,low;
chain_list *a;
char **tabName;
{
pNode pBdd;
chain_list *expr1,*expr2;

	/*--------- multiplexeur terminal ---------*/

if (low->index < 2 && high->index < 2)
   {
   if (low == one)	   	/* not de la variable */
      return(notExpr(a));
   else 			/* variable directe */
      return(a);
   }

	/*--------- multiplexeur semi-terminal ---------*/

if (low == one)	/* F = (or (not a) H) */
    return(createBinExpr(OR,bddToAbl(high,tabName),notExpr(a)));

if (low == zero)	/* F = (and a H) */
   return(createBinExpr(AND,bddToAbl(high,tabName),a));

if (high == one)	/* F = (or a L) */
   return(createBinExpr(OR,bddToAbl(low,tabName),a));

if (high == zero)	/* F = (and (not a) L) */
   return(createBinExpr(AND,bddToAbl(low,tabName),notExpr(a)));


pBdd = applyBinBdd(AND,high,low);

if (pBdd == zero && applyBinBdd(OR,low,high) == one)

      		/* (xor a L) */
   {
		/* choix L ou H ? */

   return(createBinExpr(XOR,bddToAbl(low,tabName),a));
   }

		/* H est inclu dans L */

if (pBdd == high)
   {

   expr2 = createBinExpr(OR,
                 bddToAbl(high,tabName),
                 createBinExpr(AND,
                         bddToAbl(low,tabName),
                         notExpr(a))); 

   return(expr2);
   }

		/* L est inclu dans H */

if (pBdd == low)
   {

   expr2 = createBinExpr(OR,
                 bddToAbl(low,tabName),
                 createBinExpr(AND,
                         bddToAbl(high,tabName),
                         copyExpr(a))); 

   return(expr2);
   }

		/* cas general */

expr1 = bddToAbl(low,tabName);
expr2 = bddToAbl(high,tabName);

expr1 = createBinExpr(OR,
             createBinExpr(AND,expr1,notExpr(a)),
             createBinExpr(AND,expr2,copyExpr(a)));

return(expr1);
}

/*------------------------------------------------------------------------------
bddToAbl        :traduit un BDD en ABL d'une maniere simplifie. Cette fonction
                 recupere des noms de variables que l'on a empile par index
                 croissant dans une table.
-------------------------------------------------------
parametres 	 :un pointeur de NODE.
-------------------------------------------------------
return 		 :une pointeur de CHAIN_LIST.
------------------------------------------------------------------------------*/
chain_list *bddToAbl(pt,tabName)
pNode pt;
char **tabName;
{
chain_list *expr1;
pNode pBdd;
chain_list *res = NULL;

	/*----------------- noeud ONE ou ZERO ------------------*/

if (pt->index < 2)
   {
   if (pt->index == 0)
      res = createAtom("'0'");
   else
      res = createAtom("'1'");
   return(res);
   }

	/*----------------- variable terminale -----------------*/

if ((pt->low)->index < 2 || (pt->high)->index < 2)
   {
   if ((pt->low)->index < 2 && (pt->high)->index < 2)
      {
      if (pt->low == one)   	/* not de la variable */
	 res = notExpr(NAME_ATOM);
      else 			/* variable directe */
	 res = NAME_ATOM;
      }
   else		/* variable semi-terminale */
      {
      if (pt->low == one)	/* F = (or (not a) H) */
         res = createBinExpr(OR,bddToAbl(pt->high,tabName),notExpr(NAME_ATOM));

      if (pt->low == zero)	/* F = (and a H) */
         res = createBinExpr(AND,bddToAbl(pt->high,tabName),NAME_ATOM);

      if (pt->high == one)	/* F = (or a L) */
         res = createBinExpr(OR,bddToAbl(pt->low,tabName),NAME_ATOM);

      if (pt->high == zero)	/* F = (and (not a) L) */
         res = createBinExpr(AND,bddToAbl(pt->low,tabName),notExpr(NAME_ATOM));
      }
   return(res);
   }
else
   {

	/*---------------- variable non-terminale ----------------*/

       /* recherche de noyaux non-atomique pour le multiplexeur */

		/* noyaux a double polarite */

   if (pt->high == (pt->low)->high || pt->high == (pt->low)->low)
      {
      expr1 = createExpr(OR);
      pBdd = pt;		/* sauvegarde de pt */
      while (pt->high == pBdd->high || pt->low == pBdd->high)
         {
         if (pt->high == pBdd->high)
	    {
            addQExpr(expr1,NAME_ATOM); 
            pt = pt->low;
   	    }
      	 else
	    {
            addQExpr(expr1,notExpr(NAME_ATOM)); 
	    pt = pt->high;
 	    }
         }
      res = muxAbl(pBdd->high,pt,expr1,tabName);
      pt = pBdd;
      return(res);
      }
   else
      {
      if (pt->low == (pt->high)->low || pt->low == (pt->high)->high)
	 {
         expr1 = createExpr(AND);
         pBdd = pt;		/* sauvegarde de pt */
         while (pt->low == pBdd->low || pt->high == pBdd->low)
            {
            if (pt->low == pBdd->low)
	       {
               addQExpr(expr1,NAME_ATOM); 
               pt = pt->high;
	       }
            else
	       {
               addQExpr(expr1,notExpr(NAME_ATOM)); 
               pt = pt->low;
	       }
            }
	 res = muxAbl(pt,pBdd->low,expr1,tabName);
         pt = pBdd;
         return(res);
         }
      else
	 {

			/* noyaux XOR-NXOR */

	 if ((pt->high)->high == (pt->low)->low &&
             (pt->high)->low == (pt->low)->high &&
             (pt->high)->index == (pt->low)->index)
	    {
	    expr1 = createExpr(XOR);
            addQExpr(expr1,NAME_ATOM); 
	    pBdd = pt;
    	    pt = pt->low;
            addQExpr(expr1,NAME_ATOM); 
	    pt = pBdd;
            
	    res = muxAbl((pt->low)->high,(pt->low)->low,expr1,tabName);
            return(res);
            }
         }
      }
		/*  (or (and a H) (and (not a) L) */

   expr1 = muxAbl(pt->high,pt->low,NAME_ATOM,tabName);

   return(expr1);
   }
}

/*------------------------------------------------------------------------------
displayBdd 	: visualise le BDD . 
-------------------------------------------------------
parametres 	 :niveau d'affichage ,pointeur sur le noeud tete de graphe.
-------------------------------------------------------
return 		 :rien.
------------------------------------------------------------------------------*/

void displayBddLoc(level,pt)
short level ;
pNode pt;
{

if (pt->mark == 1) return;
pt->mark = 1;
if (pt->index > 1) 
   {
   printf("%d\t INDEX = %d\t",(int)pt,(int)pt->index);
   if ((pt->high)->index == 0)
      printf(" HIGH = ZERO");
   else 
      if ((pt->high)->index == 1)
         printf(" HIGH = ONE");
      else
         printf(" HIGH = %d",(int)pt->high);

   if ((pt->low)->index == 0)
      printf("\t LOW = ZERO\n");
   else
      if ((pt->low)->index == 1)
         printf("\t LOW = ONE\n");
      else
         printf("\t LOW = %d\n",(int)pt->low);
   if(level == 1)
     {
     if((pt->low)->index > 1)
     	displayBddLoc(level,pt->low) ;
     if((pt->high)->index > 1)
     	displayBddLoc(level,pt->high) ;
     }
    }
else
   if (pt->index == 1)
      printf("ONE      INDEX = 1\n");
   else 
      printf("ZERO     INDEX = 0\n");
}

void displayBdd(pBdd,level)
pNode pBdd;
int level;
{
markBdd(pBdd,0);
displayBddLoc(level,pBdd);
markBdd(pBdd,0);
}

/*------------------------------------------------------------------------------
displayBddName :visualise le BDD en substituant l'index par son nom INPUT . 
-------------------------------------------------------
parametres 	 :niveau d'affichage ,pointeur sur le noeud tete de graphe et le
                  le pointeur de table de Name.
-------------------------------------------------------
return 		 :rien.
------------------------------------------------------------------------------*/

void displayBddName(level,pt,TabName)
short level ;
pNode pt;
char **TabName ;
{

if (pt->mark == 1) return;
pt->mark = 1;
if (pt->index > 1) 
   {
   printf("%d\t INPUT = %s\t",(int)pt,*(TabName + pt->index - 2));
   if ((pt->high)->index == 0)
      printf(" HIGH = ZERO");
   else 
      if ((pt->high)->index == 1)
         printf(" HIGH = ONE");
      else
         printf(" HIGH = %d",(int)pt->high);

   if ((pt->low)->index == 0)
      printf("\t LOW = ZERO\n");
   else
      if ((pt->low)->index == 1)
         printf("\t LOW = ONE\n");
      else
         printf("\t LOW = %d\n",(int)pt->low);
   if(level == 1)
     {
     if((pt->low)->index > 1)
     	displayBddName(level,pt->low,TabName) ;
     if((pt->high)->index > 1)
     	displayBddName(level,pt->high,TabName) ;
     }
    }
else
   if (pt->index == 1)
      printf("ONE      INDEX = 1\n");
   else 
      printf("ZERO     INDEX = 0\n");
}

/*------------------------------------------------------------------------------
notBdd           :inversion d'un arbre Bdd.
-------------------------------------------------------
parametres 	 :un pointeur de Bdd.
-------------------------------------------------------
return 		 :un pointeur de Bdd.
------------------------------------------------------------------------------*/

pNode notBdd(pBdd)
pNode pBdd;
{
pNode pBddLoc;

if (pBdd == zero) return(one);
if (pBdd == one)  return(zero);
pBddLoc =  searchTabLoc(sysBdd.pMC,pBdd,pBdd,NOT);
   if (pBddLoc != NULL) 
      return(pBddLoc);
pBddLoc = initVertexBdd(pBdd->index,notBdd(pBdd->high),notBdd(pBdd->low));
addTabLoc(sysBdd.pMC,pBdd,pBdd,pBddLoc,NOT);
return(pBddLoc);
}

/*------------------------------------------------------------------------------
applyTerm        :application d'un operateur sur un Bdd avec un noeud terminal.
-------------------------------------------------------
parametres 	 :un operateur,un index de noeud terminal,un pointeur de Bdd.
-------------------------------------------------------
return 		 :un pointeur de Bdd.
------------------------------------------------------------------------------*/

pNode applyTerm(oper,index,pBdd)
int oper;
short index; 
pNode pBdd;
{
                     /* noeud one */

if (index == 1) 
   if (oper == OR)
      return(one);
   else
      if (oper == NAND || oper == XOR)
         return(notBdd(pBdd));
      else
         if (oper == AND || oper == NXOR)
            return(pBdd);
         else
            return(zero);

                    /* noeud zero */

if (oper == AND)
   return(zero);
else
   if (oper == NOR || oper == NXOR)
      return(notBdd(pBdd));
   else
      if (oper == OR || oper == XOR)
         return(pBdd);
      else
         return(one);       /* c'est un "nand" */
}


/*------------------------------------------------------------------------------
applyBinBdd  	:application d'un operateur sur deux Bdd.
-------------------------------------------------------
parametres 	 :un operateur,deux pointeurs de Bdd.
-------------------------------------------------------
return 		 :un pointeur de Bdd.
------------------------------------------------------------------------------*/

pNode applyBinBdd(oper,pBdd1,pBdd2)
short oper;
pNode pBdd1,pBdd2;
{

pNode pBddLoc;
short index1=pBdd1->index;
short index2=pBdd2->index;

if ((index1 < 2) || (index2 < 2))      /* il existe un noeud terminal */
   if ((index1 < 2) && (index2 < 2))   /* tous les deux sont terminaux */ 

     if (index1 != index2)          /* 01 ou 10 */
       if (oper == OR || oper == NAND || oper == XOR)
          return(one);
       else
          return(zero);
     else
      if (index1 == 0)              /* 00 */
        if (oper == NOR || oper == NAND || oper == NXOR)
          return(one);
        else
          return(zero);
      else                          /* 11 */
        if (oper == OR || oper == AND || oper == NXOR)
          return(one);
        else
          return(zero);
   else
      if (index1 < 2) return(applyTerm(oper,index1,pBdd2));
      else return(applyTerm(oper,index2,pBdd1));

   /* les index ne correspondent pas a des noeuds terminaux */


   /* recherche dans la table de hachage locale */

   if (pBdd1 > pBdd2)
      pBddLoc =  searchTabLoc(sysBdd.pMC,pBdd1,pBdd2,oper);
   else
      pBddLoc =  searchTabLoc(sysBdd.pMC,pBdd2,pBdd1,oper);

     /* operation deja calcule... */

   if (pBddLoc != NULL)
      return(pBddLoc);


if (index1 == index2)       /* deux noeuds de meme index */
   {
   if (pBdd1 == pBdd2)   /* egalite des pointeurs ==> simplification */
      {
      if (oper == OR || oper == AND)
         return(pBdd1);
      if (oper == NOR || oper == NAND)
         return(notBdd(pBdd1));
      if (oper == XOR)
         return(zero);
      else
         return(one);
      } 
   pBddLoc = initVertexBdd(index1,applyBinBdd(oper,pBdd1->high,pBdd2->high),
                                  applyBinBdd(oper,pBdd1->low,pBdd2->low));
   }
else
   if (index1 < index2)    /* deux noeuds d'index different */
      pBddLoc = initVertexBdd(index2,applyBinBdd(oper,pBdd1,pBdd2->high),
                                     applyBinBdd(oper,pBdd1,pBdd2->low));
   else
      pBddLoc = initVertexBdd(index1,applyBinBdd(oper,pBdd1->high,pBdd2),
                                     applyBinBdd(oper,pBdd1->low,pBdd2));

     /* ajout d'un noeud dans la table de hash locale */

   if (pBdd1 > pBdd2)
      addTabLoc(sysBdd.pMC,pBdd1,pBdd2,pBddLoc,oper);
   else
      addTabLoc(sysBdd.pMC,pBdd2,pBdd1,pBddLoc,oper);

return(pBddLoc);
}

/*------------------------------------------------------------------------------
applyBdd         :application d'un operateur sur une liste de Bdd.
-------------------------------------------------------
parametres 	 :un operateur,un pointeur de liste de Bdd.
-------------------------------------------------------
return 		 :un pointeur de Bdd.
------------------------------------------------------------------------------*/

pNode applyBdd(oper,pt)
short oper;
chain_list *pt;
{
short operateur_N=0;
pNode pBdd ;
pNode pBddResul,pBddInter;

if(oper > MAX_OPER || oper < MIN_OPER)
	{
	printf("applyBdd : error - unknown operator %d\n",oper);
	exit(-1) ;
	}
if (pt == NULL)
	{
	printf("applyBdd : error chained list is empty\n");
	exit(-1) ;
	} 

pBdd = (pNode)pt->DATA ;

if (pt->NEXT == NULL)                  /* operateur unaire NOT */
   {
   if (oper != NOT)
      {
      printf("applyBdd : error - bad operator %s\n",operToChar(oper));
      exit(-1);
      }
   return(notBdd(pBdd));
   }


if ((pt->NEXT)->NEXT == NULL)          /* operateur binaire */
   {
   pBddResul = applyBinBdd(oper,pBdd,(pNode) (pt->NEXT)->DATA);
   return(pBddResul);
   }

    /* operateur negatif d'arite superieure a trois */

if (oper == NXOR || oper == NAND || oper == NOR) 
   {
   operateur_N = 1;
   if (oper == NOR)
      oper = OR;
   else
      if (oper == NXOR)
         oper = XOR;
      else
         oper = AND;
   }

pBddInter = applyBdd(oper,pt->NEXT);
pBddResul = applyBinBdd(oper,pBdd,pBddInter);

if (operateur_N == 1)
   return(notBdd(pBddResul));
else
   return(pBddResul);
}

/*----------------------------------------------------------------------------
constraintBdd     :constrainte d'un graphe sur un autre.
------------------------------------------------------------------------------
parametres 	 :deux graphes Bdd.
-----------------------------------------------------------------------
return 		 :un pointeur de Bdd.
------------------------------------------------------------------------------*/

pNode constraintBdd(pBdd1,pBddGc)
pNode pBdd1,pBddGc;
{
short index1 = pBdd1->index;
short indexGc  = pBddGc->index;
pNode pBddLoc;

if (index1 == 0) return(zero);
if (index1 == 1) return(one) ;
if (indexGc == 1) return(pBdd1);

if (pBdd1 == pBddGc) return(one);  /*  pBdd1 = pBddGc  ==>  ONE  */

pBddLoc = searchTabLoc(sysBdd.pMC,pBdd1,pBddGc,CONTRAINT);
if (pBddLoc != NULL) return(pBddLoc);

if (index1 == indexGc)
   {
   if (pBddGc->high == zero)
      pBddLoc = constraintBdd(pBdd1->low,pBddGc->low);
   else
      if (pBddGc->low == zero)
         pBddLoc = constraintBdd(pBdd1->high,pBddGc->high);
      else
         pBddLoc = initVertexBdd(indexGc,
                                 constraintBdd(pBdd1->high,pBddGc->high),
                                 constraintBdd(pBdd1->low,pBddGc->low));
   }
else
  if (index1 < indexGc)
     pBddLoc = initVertexBdd(indexGc,constraintBdd(pBdd1,pBddGc->high),
                                  constraintBdd(pBdd1,pBddGc->low));
  else
     pBddLoc = initVertexBdd(index1,constraintBdd(pBdd1->high,pBddGc),
                                   constraintBdd(pBdd1->low,pBddGc));
addTabLoc(sysBdd.pMC,pBdd1,pBddGc,pBddLoc,CONTRAINT);
return(pBddLoc);
}
/*------------------------------------------------------------------------------
simplifDcZeroBdd :simplifie un BDD avec un BDD correspondant a un Don't Care.
                  pGdc est inclu dans pGon';
-------------------------------------------------------
parametres 	 :deux pointeurs de NODE.
-------------------------------------------------------
return 		 :un pointeur de NODE.
------------------------------------------------------------------------------*/
pNode simplifDcZeroBdd(pGon,pGdc)
pNode pGon,pGdc;
{
pNode pBddLoc;
pNode pAOH,pAOL;

	/* simplification terminale */

if (pGdc == zero) return(pGon);
if (pGon->index < 2) return(pGon);

pBddLoc = searchTabLoc(sysBdd.pMC,pGon,pGdc,DONTCARE0);
if (pBddLoc != NULL) return(pBddLoc);

	/* noeuds de meme index */

if (pGdc->index == pGon->index)
   {
   	/* simplification terminales sur les fils */

   if (pGdc->high == one) return(simplifDcZeroBdd(pGon->low,pGdc->low));
   if (pGdc->low == one) return(simplifDcZeroBdd(pGon->high,pGdc->high));

   if (applyBinBdd(OR,pGon,pGdc) == one) return(one);

   if (pGon->high == zero && applyBinBdd(AND,pGon->low,pGdc->high) == pGon->low)
      return(pGon->low);

   if (pGon->low == zero && applyBinBdd(AND,pGon->high,pGdc->low) == pGon->high)
      return(pGon->high);

   pAOH = applyBinBdd(AND,pGon->high,applyBinBdd(OR,pGon->low,pGdc->low)); 
   pAOL = applyBinBdd(AND,pGon->low,applyBinBdd(OR,pGon->high,pGdc->high));

   if (pAOH == pGon->high && pAOL == pGon->low)
      {
      pBddLoc = simplifDcZeroBdd(applyBinBdd(OR,pGon->low,pGon->high),
                                 applyBinBdd(AND,pGdc->low,pGdc->high));
      }
   else
      {
	/* cas general */

      pBddLoc = initVertexBdd(pGon->index,
			      simplifDcZeroBdd(pGon->high,pGdc->high),
			      simplifDcZeroBdd(pGon->low,pGdc->low));

      }
   }
else
		/* index differents */

   if (pGon->index > pGdc->index)
      pBddLoc = initVertexBdd(pGon->index,simplifDcZeroBdd(pGon->high,pGdc),
				          simplifDcZeroBdd(pGon->low,pGdc));
   else
      pBddLoc = simplifDcZeroBdd(pGon,applyBinBdd(AND,pGdc->low,pGdc->high));

addTabLoc(sysBdd.pMC,pGon,pGdc,pBddLoc,DONTCARE0);
return(pBddLoc);
}
/*------------------------------------------------------------------------------
simplifPlusDcZeroBdd 
               :simplifie plus fortement un BDD avec un BDD correspondant
                a un Don't Care, pGdc est inclu dans pGon';
-------------------------------------------------------
parametres 	 :deux pointeurs de NODE.
-------------------------------------------------------
return 		 :un pointeur de NODE.
------------------------------------------------------------------------------*/
pNode simplifPlusDcZeroBdd(pGon,pGdc)
pNode pGon,pGdc;
{
pNode pBddLoc;
pNode pAOH,pAOL;

	/* simplification terminale */

if (pGdc == zero) return(pGon);
if (pGdc == one) return(one);
if (pGon == zero) return(zero);

pBddLoc = searchTabLoc(sysBdd.pMC,pGon,pGdc,DONTCARE2);
if (pBddLoc != NULL) return(pBddLoc);

	/* noeuds de meme index */

if (pGdc->index == pGon->index)
   {
   	/* simplification terminales sur les fils */

   if (pGdc->high == one) return(simplifPlusDcZeroBdd(pGon->low,pGdc->low));
   if (pGdc->low == one) return(simplifPlusDcZeroBdd(pGon->high,pGdc->high));

   if (applyBinBdd(OR,pGon,pGdc) == one) return(one);

   if (pGon->high == zero && applyBinBdd(AND,pGon->low,pGdc->high) == pGon->low)
      return(pGon->low);

   if (pGon->low == zero && applyBinBdd(AND,pGon->high,pGdc->low) == pGon->high)
      return(pGon->high);

   pAOH = applyBinBdd(AND,pGon->high,applyBinBdd(OR,pGon->low,pGdc->low)); 
   pAOL = applyBinBdd(AND,pGon->low,applyBinBdd(OR,pGon->high,pGdc->high));

   if (pAOH == pGon->high && pAOL == pGon->low)
      {
      pBddLoc = simplifPlusDcZeroBdd(applyBinBdd(OR,pGon->low,pGon->high),
                                 applyBinBdd(AND,pGdc->low,pGdc->high));
      }
   else
      {
      if (pAOL == pGon->low)    /* Lon inclu dans Hon+Hdc */
         {			/* on maintient la propriete d'inclusion */
         pNode HonRes;

         HonRes = simplifPlusDcZeroBdd(
                              applyBinBdd(OR,pGon->low,pGon->high),
                              applyBinBdd(AND,pGdc->high,notBdd(pGon->low)));
         pBddLoc = initVertexBdd(pGon->index,HonRes,
			      simplifPlusDcZeroBdd(pGon->low,
                                   applyBinBdd(AND,pGdc->low,HonRes)));
         }
      else
         {
         if (pAOH == pGon->high)    /* Hon inclu dans Lon+Ldc */
            {			    /* on maintient la propriete d'inclusion */
            pNode LonRes;

            LonRes = simplifPlusDcZeroBdd(
                              applyBinBdd(OR,pGon->low,pGon->high),
                              applyBinBdd(AND,pGdc->low,notBdd(pGon->high)));
            pBddLoc = initVertexBdd(pGon->index,
			      simplifPlusDcZeroBdd(pGon->high,
                                        applyBinBdd(AND,pGdc->high,LonRes)),
                              LonRes);
            } 
         else
            {

	/* cas general */

            pBddLoc = initVertexBdd(pGon->index,
   			      simplifPlusDcZeroBdd(pGon->high,pGdc->high),
			      simplifPlusDcZeroBdd(pGon->low,pGdc->low));

            }
         }
      }
   }
else
		/* index differents */

   if (pGon->index > pGdc->index)
      pBddLoc = initVertexBdd(pGon->index,simplifPlusDcZeroBdd(pGon->high,pGdc),
				          simplifPlusDcZeroBdd(pGon->low,pGdc));
   else
      pBddLoc = simplifPlusDcZeroBdd(pGon,applyBinBdd(AND,pGdc->low,pGdc->high));

addTabLoc(sysBdd.pMC,pGon,pGdc,pBddLoc,DONTCARE2);
return(pBddLoc);
}

/*------------------------------------------------------------------------------
simplifDcOneBdd  :simplifie un BDD avec un BDD correspondant a un Don't Care.
		  pGdc est inclu dans pGon;
-------------------------------------------------------
parametres 	 :deux pointeurs de NODE.
-------------------------------------------------------
return 		 :un pointeur de NODE.
------------------------------------------------------------------------------*/
pNode simplifDcOneBdd(pGon,pGdc)
pNode pGon,pGdc;
{
pNode pBddLoc,ptEtOn;

	/* simplification terminale */

if (pGdc == zero) return(pGon);
if (pGon == pGdc) return(zero);
if (pGon->index < 2) return(pGon);

pBddLoc = searchTabLoc(sysBdd.pMC,pGon,pGdc,DONTCARE1);
if (pBddLoc != NULL) return(pBddLoc);

	/* noeuds de meme index */

if (pGdc->index == pGon->index)
   {
   	/* simplification terminales sur les fils */

   if (pGdc->high == one) return(simplifDcOneBdd(pGon->low,pGdc->low));
   if (pGdc->low == one) return(simplifDcOneBdd(pGon->high,pGdc->high));

   if (pGon->high == one &&
       applyBinBdd(AND,notBdd(pGdc->high),pGon->low) == notBdd(pGdc->high))
     return(simplifDcOneBdd(pGon->low,applyBinBdd(AND,pGdc->high,pGdc->low)));

   if (pGon->low == one &&
       applyBinBdd(AND,pGon->high,notBdd(pGdc->low)) == notBdd(pGdc->low))
     return(simplifDcOneBdd(pGon->high,applyBinBdd(AND,pGdc->high,pGdc->low)));

   ptEtOn = applyBinBdd(AND,pGon->high,pGon->low);

   if (applyBinBdd(AND,ptEtOn,notBdd(pGdc->low)) == 
       applyBinBdd(AND,pGon->low,notBdd(pGdc->low)) &&
       applyBinBdd(AND,ptEtOn,notBdd(pGdc->high)) == 
       applyBinBdd(AND,pGon->high,notBdd(pGdc->high)))
      {
      pBddLoc = simplifDcOneBdd(ptEtOn,applyBinBdd(AND,pGdc->low,pGdc->high));
      }
   else

	/* cas general */

     pBddLoc = initVertexBdd(pGon->index,simplifDcOneBdd(pGon->high,pGdc->high),
      				         simplifDcOneBdd(pGon->low,pGdc->low));
   }
else
		/* index differents */

   if (pGon->index > pGdc->index)
      pBddLoc = initVertexBdd(pGon->index,simplifDcOneBdd(pGon->high,pGdc),
				          simplifDcOneBdd(pGon->low,pGdc));
   else
      pBddLoc = simplifDcOneBdd(pGon,applyBinBdd(AND,pGdc->low,pGdc->high));

addTabLoc(sysBdd.pMC,pGon,pGdc,pBddLoc,DONTCARE1);
return(pBddLoc);
}

/*------------------------------------------------------------------------------
simplifDcOneFPGABdd  :simplifie un BDD avec un BDD correspondant a un Don't Care.
		  pGdc est inclu dans pGon;
-------------------------------------------------------
parametres 	 :deux pointeurs de NODE.
-------------------------------------------------------
return 		 :un pointeur de NODE.
------------------------------------------------------------------------------*/
pNode simplifDcOneFPGABdd(pGon,pGdc)
pNode pGon,pGdc;
{
pNode pBddLoc;

	/* simplification terminale */

if (pGdc == zero) return(pGon);
if (pGon == pGdc) return(zero);
if (pGon->index < 2) return(pGon);

pBddLoc = searchTabLoc(sysBdd.pMC,pGon,pGdc,DONTCARE1);
if (pBddLoc != NULL) return(pBddLoc);

	/* noeuds de meme index */

if (pGdc->index == pGon->index)
   {
   	/* simplification terminales sur les fils */

   if (pGdc->high == one) return(simplifDcOneFPGABdd(pGon->low,pGdc->low));
   if (pGdc->low == one) return(simplifDcOneFPGABdd(pGon->high,pGdc->high));

   if (pGon->high == one &&
       applyBinBdd(AND,notBdd(pGdc->high),pGon->low) == notBdd(pGdc->high))
     return(simplifDcOneFPGABdd(pGon->low,applyBinBdd(AND,pGdc->high,pGdc->low)));

   if (pGon->low == one &&
       applyBinBdd(AND,pGon->high,notBdd(pGdc->low)) == notBdd(pGdc->low))
     return(simplifDcOneFPGABdd(pGon->high,applyBinBdd(AND,pGdc->high,pGdc->low)));

	/* cas general */

   pBddLoc = initVertexBdd(pGon->index,simplifDcOneFPGABdd(pGon->high,pGdc->high),
      				         simplifDcOneFPGABdd(pGon->low,pGdc->low));
   }
else
		/* index differents */

   if (pGon->index > pGdc->index)
      pBddLoc = initVertexBdd(pGon->index,simplifDcOneFPGABdd(pGon->high,pGdc),
				          simplifDcOneFPGABdd(pGon->low,pGdc));
   else
      pBddLoc = simplifDcOneFPGABdd(pGon,applyBinBdd(AND,pGdc->low,pGdc->high));

addTabLoc(sysBdd.pMC,pGon,pGdc,pBddLoc,DONTCARE1);
return(pBddLoc);
}

/*----------------------------------------------------------------------------
composeBdd       :Composition de deux graphes
------------------------------------------------------------------------------
soient index l'index de la variable de decomposition,
       G1 le graphe BDD a recalculer et G2 le graphe de V

on calcule G = G1(V(index)=0).not(G2(V)) + G1(V(index)=1).G2(V)
-----------------------------------------------------------------------
parametres 	 :un operateur,un pointeur de liste de Bdd.
-----------------------------------------------------------------------
return 		 :un pointeur de Bdd.
------------------------------------------------------------------------------*/

pNode composeBdd(pBdd1,pBdd2,index)
pNode pBdd1,pBdd2 ;
int index;
{
pNode r1,r2,resul;

r1 = constraintBdd(pBdd1,initVertexBdd(index,one,zero));

if (r1 == pBdd1)    /* V n'apparaissait pas dans pBdd1 */
   return(pBdd1);

r2 = constraintBdd(pBdd1,initVertexBdd(index,zero,one));

resul = applyBinBdd(OR,applyBinBdd(AND,pBdd2,r1),
                       applyBinBdd(AND,notBdd(pBdd2),r2));

return(resul);
}

/*------------------------------------------------------------------------------
addListBdd  : 	ajoute un nouveau noeud dans la liste des noeuds.
-------------------------------------------------------
parametres   :	pointeur sur le debut de la liste.
-------------------------------------------------------
return 	     :	nouveau pointeur debut de la liste.
------------------------------------------------------------------------------*/

chain_list *addListBdd(pt, pBdd)
chain_list *pt ;
pNode pBdd ;
{
chain_list *new_lstGdb,*pCur,*pCurSup;
int index;


index = pBdd->index;

new_lstGdb = addchain(NULL,(void *) pBdd);

       /* l'insertion par index decroissant */

if (pt == NULL)
   return(new_lstGdb);

pCur = pt;
pCurSup = pCur;
while(pCur->NEXT != NULL && index < ((pNode) (pCur->NEXT)->DATA)->index)
   {
   pCurSup = pCur;
   pCur = pCur->NEXT; 
   }

if (index < ((pNode) pCur->DATA)->index)     /* ajout apres */
   {
   new_lstGdb->NEXT = pCur->NEXT ;
   pCur->NEXT = new_lstGdb;
   }
else                                             /* ajout avant */
   {
   new_lstGdb->NEXT = pCur ;
   if (pt == pCur)                /* ajout devant la liste */
      return(new_lstGdb);
   pCurSup->NEXT = new_lstGdb; 
   }
return(pt) ;
}
/*----------------------------------------------------------------------------
oneBdd       :tautologie
------------------------------------------------------------------------------
renvoie 1 si le graphe est une tautologie
-----------------------------------------------------------------------
parametres 	 :un pointeur de Bdd.
-----------------------------------------------------------------------
return 		 :un int.
------------------------------------------------------------------------------*/

int oneBdd(pBdd)
pNode pBdd ;
{
if (pBdd == one)
   return(1);
else
   return(0);
}
/*----------------------------------------------------------------------------
zeroBdd       :antilogie
------------------------------------------------------------------------------
renvoie 1 si le graphe est une antilogie
-----------------------------------------------------------------------
parametres 	 :un pointeur de Bdd.
-----------------------------------------------------------------------
return 		 :un int.
------------------------------------------------------------------------------*/

int zeroBdd(pBdd)
pNode pBdd ;
{
if (pBdd == zero)
   return(1);
else
   return(0);
}
/*----------------------------------------------------------------------------
equalBdd       :egalite de Bdd
------------------------------------------------------------------------------
renvoie 1 si Bdd1 = Bdd2 
-----------------------------------------------------------------------
parametres 	 :deux pointeurs de Bdd.
-----------------------------------------------------------------------
return 		 :un short.
------------------------------------------------------------------------------*/

int equalBdd(pBdd1,pBdd2)
pNode pBdd1,pBdd2 ;
{
if (pBdd1 == pBdd2)
   return(1);
else
   return(0);
}

/*------------------------------------------------------------------------------
markBdd         :met a jour les marques d'un BDD.
-------------------------------------------------------
parametres 	:un pointeur de Bdd,la valeur du marquage.
-------------------------------------------------------
return 		:rien.
------------------------------------------------------------------------------*/
void markBdd(pBdd,value)
pNode pBdd;
short value;
{
if (pBdd->index > 1)
   {
   if (pBdd->mark != value)     /* noeud non encore marque */
      {
      pBdd->mark = value;
      markBdd(pBdd->high,value);
      markBdd(pBdd->low,value);
      }            
   }
}

/*-------------------------------------------------------------------------
upVarBdd 	: remonte une variable dans un BDD a l'index i. 
---------------------------------------------------------------------------
retour		: un pNode.
---------------------------------------------------------------------------*/
pNode upVarBdd(pF,pFoldIndex,newIndex)
pNode pF,pFoldIndex;
short newIndex;
{
pNode pBddLoc;

pBddLoc =searchTabLoc(sysBdd.pMC,pF,pFoldIndex,newIndex+10);
if (pBddLoc != NULL) return(pBddLoc);

if (pF->index < pFoldIndex->index)
   return(pF);
if (pF->index > newIndex)
   pBddLoc = initVertexBdd(pF->index,upVarBdd(pF->high,pFoldIndex,newIndex),
                                  upVarBdd(pF->low,pFoldIndex,newIndex));
else
		/* pF->index < newIndex */

   pBddLoc = initVertexBdd(newIndex,
                     constraintBdd(pF,pFoldIndex),
		     constraintBdd(pF,notBdd(pFoldIndex)));
addTabLoc(sysBdd.pMC,pF,pFoldIndex,pBddLoc,newIndex+10);
return(pBddLoc);
}
/*-------------------------------------------------------------------------
markAllBdd 	: marque tous les noeuds BDDs dans la table de reduction . 
---------------------------------------------------------------------------
retour		: void.
---------------------------------------------------------------------------*/
void markAllBdd(value)
short value ;
{
pNode pBdd,*ppBdd ;
int i ;

ppBdd = (sysBdd.pRT)->pBdd ;

for(i = 0; i < sysBdd.pRT->lenTableBdd; i++)
	{
	pBdd = *ppBdd ;
	if(pBdd != NULL)
		pBdd->mark = value ;
	ppBdd++ ;
	}
}

/*-------------------------------------------------------------------------
supportChain_listBdd 	: calcule le support en noeud d'un graphe.
---------------------------------------------------------------------------
retour		: une liste chainee
---------------------------------------------------------------------------*/
void supportBddInt(pt,ppCL)
pNode pt;
chain_list **ppCL;
{
if (pt->index > 1)
   if (pt->mark == 0)
      {
      *ppCL = addchain(*ppCL,(void *)pt);
      supportBddInt(pt->high,ppCL);
      supportBddInt(pt->low,ppCL);
      pt->mark = 1;
      }
}

chain_list *supportChain_listBdd(pBdd)
pNode pBdd;
{
chain_list *res;

res = NULL;
markBdd(pBdd,0);
supportBddInt(pBdd,&res);
markBdd(pBdd,0);
return(res);
}

/*------------------------------------------------------------------------------
initVertexBddAux : creation d'un noeud dans la structure sysCible. 
-------------------------------------------------------
parametres 	 : index,high,low et system cible. 
-------------------------------------------------------
return 		 : le noeud cree. 
------------------------------------------------------------------------------*/
pNode initVertexBddAux(index,high,low,sysCible)
short index;
pNode high;
pNode low;
struct systemBdd *sysCible;
{
pNode pt;


if ((pt = searchTableBdd(sysCible->pRT,index,high,low)) != NULL)
   if (pt != BDDTABLE_PLEINE)
      return(pt);
   else
      {
      sysCible->pRT = reAllocTableBdd(sysCible->pRT);
      return(initVertexBddAux(index,high,low,sysCible));
      }

if (high == low)
   {
   printf("gcNode : error - there's a node that isn't reduced\n");
   exit(-1);
   }

if (sysCible->indiceAT == MAX_PACK)
   {
   sysCible->pAT = (pNode) mbkalloc (MAX_PACK * sizeof (struct node));
   sysCible->indiceAT = 1;
   sysCible->lpAT = addchain(sysCible->lpAT,(void *)sysCible->pAT) ;
   }
else
  {
  sysCible->pAT++;
  sysCible->indiceAT++;
  }

pt = sysCible->pAT;
pt->index = index;
pt->high = high;
pt->low = low;
pt->mark = 0;
if (index > 1)
   if (addTableBdd(sysCible->pRT,pt) == TABLE_PLEINE)   /* table pleine */
      {
      sysCible->pRT = reAllocTableBdd(sysCible->pRT);
      return(initVertexBddAux(index,high,low,sysCible));
      }
return(pt);
}

/*------------------------------------------------------------------------------
regenereBdd	 : regnere un Bdd dans une structure systeme cible.
-------------------------------------------------------
parametres 	 : pointeur Bdd et une structure cible. 
-------------------------------------------------------
return 		 : le pointeur dans la structure system cible.
------------------------------------------------------------------------------*/
pNode regenereBdd(pBdd,sysCible,pTHNode)
pNode pBdd;
struct systemBdd *sysCible;
pTH pTHNode;
{
int resul;

if ((resul = searchTH(pTHNode,pBdd)) != EMPTYTH)
   return((pNode) resul);
else
   {
   if (pBdd->index < 2)
      {
      printf("gcNode : error - bad index %d\n",pBdd->index);
      exit(-1);
      }
   resul = (int) initVertexBddAux(pBdd->index,
                                  regenereBdd(pBdd->high,sysCible,pTHNode),   
                                  regenereBdd(pBdd->low,sysCible,pTHNode),
                                  sysCible);
   addTH(pTHNode,pBdd,resul);
   return((pNode) resul);
   }
}
/*------------------------------------------------------------------------------
gcNodeBdd	 :effectue un garbage collecteur sur tous les noeuds de systeme
		  en sauvegardant les noeuds pointes par les pNode de la liste 
		  chainee pChain. 
-------------------------------------------------------
parametres 	 : pointeur de chain_list. 
-------------------------------------------------------
return 		 : 1 si ok ;
		   0 si erreur .
------------------------------------------------------------------------------*/
void gcNodeBdd(pt)
chain_list *pt ;
{
struct systemBdd sysBddAux ;
pNode zeroAux, oneAux ;
pTH pTHNode;

pTHNode = createTH(MEDIUM);
sysBddAux.pRT = createTableBdd(MEDIUM);
sysBddAux.pMC = createTabLoc(MEDIUM);
sysBddAux.indiceAT = MAX_PACK ;
sysBddAux.lpAT = NULL ;
zeroAux = initVertexBddAux(0,(pNode)0,(pNode)1,&sysBddAux) ;
oneAux = initVertexBddAux(1,(pNode)0,(pNode)1,&sysBddAux) ;
addTH(pTHNode,zero,(int) zeroAux);
addTH(pTHNode,one,(int) oneAux);

while(pt)
  {
  pNode ptNode;
  ptNode =  regenereBdd((pNode) pt->DATA,&sysBddAux,pTHNode);
  pt->DATA = ((void *) ptNode);
  pt = pt->NEXT;
  }

destroyBdd(1) ;
destroyTH(pTHNode);
sysBdd.pRT = sysBddAux.pRT ;
sysBdd.pMC = sysBddAux.pMC ;
sysBdd.indiceAT = sysBddAux.indiceAT ;
sysBdd.lpAT = sysBddAux.lpAT ;
sysBdd.pAT = sysBddAux.pAT ;
zero = zeroAux ;
one = oneAux ;
}
/*------------------------------------------------------------------------------
supportIndexBdd	 : calcule le support d'un BDD 
                   index decroissant : sens = 1
                   index croissant :   sens = 0
-------------------------------------------------------
parametres 	 : pNode 
-------------------------------------------------------
return 		 : une liste chainee d'index 
------------------------------------------------------------------------------*/

			/* fonction interne */

void rempTabIndex(pt, tabIndex)
pNode pt;
char *tabIndex;
{
if (pt->index > 1 && pt->mark == 0)
   {
   tabIndex[pt->index - 2] = 'O';
   pt->mark = 1;
   rempTabIndex(pt->high,tabIndex);
   rempTabIndex(pt->low,tabIndex);
   }
}


chain_list *supportIndexBdd(pt,sens)
pNode pt;
int sens;
{
char *tabIndex;
int i;
chain_list *ret;

		/*  initialisation du tableau d'index utilises */ 

tabIndex = (char *) mbkalloc (pt->index - 1);
for (i=0; i<= pt->index - 2; i++)
   tabIndex[i] = 'N';

rempTabIndex(pt,tabIndex);
markBdd(pt,0);

ret = NULL;

if (sens == 1)			/* index decroissant */
   {
   for (i=0; i<= pt->index - 2; i++)
      if (tabIndex[i] == 'O')
         ret = addchain(ret,i+2);
   }
else
   {
   for (i=pt->index - 2; i >= 0; i--)
      if (tabIndex[i] == 'O')
         ret = addchain(ret,i+2);
   }
mbkfree(tabIndex);
return ret;
}


