
/****************************************************************************/
/*                                                                          */
/*                      Chaine de CAO & VLSI   Alliance                     */
/*                                                                          */
/*    Produit : bibliotheques logiques                                      */
/*    Fichier : log120.h                                                    */
/*                                                                          */
/*    (c) copyright 1991 Laboratoire MASI equipe CAO & VLSI                 */
/*    Tous droits reserves                                                  */
/*    Support : e-mail cao-vlsi@masi.ibp.fr                                 */
/*                                                                          */
/*    Auteur(s) : Burgun L.                             le : 26/01/92       */
/*                                                                          */
/*    Modifie par :                                     le : ../../....     */
/*    Modifie par :                                     le : ../../....     */
/*    Modifie par :                                     le : ../../....     */
/*                                                                          */
/****************************************************************************/

/* ==============================================================
   La bibliotheque des graphes de decision binaires version 06/09/91
   Burgun L.
   Structures de donnees
   ==============================================================*/

#undef OUI
#undef NON
#undef TRUE
#undef FALSE
#undef INPUT
#undef OUTPUT
#undef SMALL
#undef MEDIUM
#undef LARGE

#undef VIDE
#undef DELETE
#undef TABLE_PLEINE
#undef BDDDELETE
#undef BDDTABLE_PLEINE
#undef MAX_SIZE_BDD

#undef DONTCARE0
#undef DONTCARE1
#undef DONTCARE2


#define OUI 1
#define NON 0
#define TRUE 1
#define FALSE 0
#define INPUT 0
#define OUTPUT 1
#define SMALL 999
#define MEDIUM 9999
#define LARGE 99999
#define SMALL_BDD 0
#define MEDIUM_BDD 1
#define LARGE_BDD 2

#define VIDE -1
#define DELETE -2
#define TABLE_PLEINE -3
#define BDDDELETE (pNode) DELETE
#define BDDTABLE_PLEINE (pNode) TABLE_PLEINE
#define MAX_SIZE_BDD 50000000    /* 50 Mega de noeuds Bdd */

#define DONTCARE0 8
#define DONTCARE1 9
#define DONTCARE2 10



/*---------------- structure d'un noeud de BDD -------------------*/

typedef struct node 
    {
    struct node *high,*low;		/* les noeuds fils */
    short index;			/* index de la variable */
    short mark ;			/* nombre de peres pointant le noeud */
    } *pNode;


/*--------------- La table de hachage pour des BDD ------------ */

/* table de hachage qui retourne des pointeurs de BDD
   lenTableBdd est la longueur de la table,
   pBddT le pointeur sur le debut de table,
   compteur le nombre d'elements deja rentres. */

typedef struct tableBdd
    {
    int lenTableBdd;
    pNode * pBdd;    
    int compteur;           
    } * pTableBdd;



/*------ les structures pour la table de hachage local -----*/

typedef struct vertexLoc
    {
    pNode high,low,father;
    short oper;
    } *pVertexLoc;

/* table de hachage pour la recuperation d'operation locale. 
   lenTable est la longueur de la table,
   pElemT le pointeur sur le debut de table,
   compteur le nombre d'elements deja rentres. */

typedef struct tableLoc
    {
    int lenTabLoc;
    pVertexLoc pLoc;    
    } * pTableLoc;

/*------------- structure pour les circuits -------------*/

typedef struct circuit
	{
	pTH pTI ;
	pTH pTO ;
	short countI ;
	char **pNameI;
	char *name;
	} *pCircuit ;

#define MAX_PACK 1000

/* structure systeme pour la generation de GDB .*/

struct systemBdd
	{
	chain_list *lpAT ;
	pTableBdd pRT ;
	pNode pAT ;
	int indiceAT ;
	pTableLoc pMC ;
	}sysBdd ;

pNode one,zero;

/**************** DECLARATION DES FONCTIONS *******/

/******* COUCHE 0 *******/

void initializeBdd() ;
void destroyBdd() ;
void displayBdd() ;
void resetBdd() ;
pNode createNodeTermBdd() ;
pNode notBdd() ;
pNode applyBinBdd() ;
pNode applyBdd() ;
chain_list *addListBdd() ;
pNode constraintBdd() ;
pNode simplifDcOneBdd() ;
pNode simplifPlusDcOneBdd() ;
pNode simplifDcZeroBdd() ;
pNode composeBdd() ;
int oneBdd();
int zeroBdd();
int equalBdd();
int numberNodeAllBdd();
int numberNodeBdd();
void markAllBdd() ;
void markBdd();
pNode upVarBdd();
chain_list *supportChain_listBdd();
void gcNodeBdd();

pNode initVertexBdd();
chain_list *bddToAbl() ;

/******* COUCHE 1 *******/

pCircuit initializeCct() ;
void destroyCct() ;
pNode searchOutputCct() ;
void addOutputCct() ;
short searchInputCct() ;
short addInputCct() ;
void displayCct() ;
void composeCct() ;
void constraintCct() ;
void proofCct() ;
pNode ablToBddCct() ;
void cpOrderCct() ;
chain_list *bddToAblCct() ;
int numberNodeCct();
void upVarCct();
void gcNodeCct();

pNode initVertexBddAux();
pNode regenereBdd();


/************** fonctions internes *************/
pNode searchTableBdd() ;
pTableBdd createTableBdd() ;
void destroyTableBdd() ;
void destroyTabLoc() ;
void videTabLoc() ;
pTableBdd reAllocTableBdd() ;
int addTableBdd() ;

int countNode() ;
int countNodeTdg() ;
int addTabLoc() ;
void destroyTH() ;
void displayBddName() ;

pNode searchTabLoc() ;
pTableLoc createTabLoc() ;

