
/****************************************************************************/
/*                                                                          */
/*                      Chaine de CAO & VLSI   Alliance                     */
/*                                                                          */
/*    Produit : bibliotheques logiques                                      */
/*    Fichier : log200.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 : ../../....     */
/*                                                                          */
/****************************************************************************/


#undef OR
#undef AND
#undef XOR
#undef NOT
#undef NOR
#undef NAND
#undef NXOR
#undef CONTRAINT
#undef STABLE
#undef RESTRICT
#undef CNST 10

#define OR 0
#define AND 1
#define XOR 2 
#define NOT 3 
#define NOR 4 
#define NAND 5 
#define NXOR 6  
#define CONTRAINT 7  
#define STABLE 8  
#define RESTRICT 9  
#define CNST 10

/* ================================================================== 
   Gestion de table de hachage 			  Version du 16.07.91
   Les structures de donnees
   Burgun L. 
   ================================================================== */


#define EMPTYTH -1
#define VIDETH -1
#define DELETETH -2

/*------ les structures pour la table de hachage des entiers -----*/

typedef struct elemTH
    {
    char * key;
    int value;
    } *pElemTH;

/* table de hachage 
   length est la longueur de la table,
   pElemTH le pointeur sur le debut de table,
   count le nombre d'elements deja rentres. */

typedef struct tableTH
    {
    int length;
    pElemTH pElem;    
    int count;           
    } * pTH;

	/* ------- les fonctions de base ------ */

pTH createTH() ;
int searchTH() ;
int addTH() ;
int addExistTH() ;
void displayTH();
int deleteTH();
void reAllocTH();

/* ==============================================================
   La bibliotheque des Arbres binaires Lisp-like version 23/08/91
   Burgun L.
   Structures de donnees
   ==============================================================*/



/*-----------  Fonctions Lisp-Like de bas-niveau  -------------*/

#define CDR(expr) (expr->NEXT)
#define CAR(expr) ((chain_list *) expr->DATA)
#define CADR(expr) CAR(CDR(expr))
#define ATOM(expr) (!expr->NEXT)
#define VALUE_ATOM(expr) (char *) expr->DATA
#define OPER(expr) ((int)(CAR(expr))->DATA)


/*--  Declaration des fonctions et procedures de prefbib.c  --*/

/*-- fonctions de creation --*/

chain_list *createAtom();
chain_list *createExpr();
chain_list *createBinExpr();
chain_list *notExpr();
chain_list *charToExpr();
void addHExpr();
void addQExpr();
void freeExpr();

/*-- fonctions d'affichage --*/

char *operToChar();
short charToOper();
void displayExpr();
char *exprToChar();
char *identExpr();

/*-- fonctions de parcours --*/

void mapExpr();
chain_list *mapCarExpr();
int anyExpr();
int everyExpr();

/*-- fonctions de caracterisation --*/

int equalExpr();
int equalVarExpr();
int searchExpr();
int searchOperExpr();
int lengthExpr();
int profExpr();
int numberAtomExpr();
int numberOccExpr();
chain_list *supportChain_listExpr();
ptype_list *supportPtype_listExpr();

/*-- fonctions de modification physique ou de recopie --*/

chain_list *copyExpr();
chain_list *flatPolarityExpr();
chain_list *devXor2Expr();
chain_list *devXorExpr();
chain_list *substExpr();
void substPhyExpr();
void flatArityExpr();
chain_list *maxExpr();
chain_list *minExpr();
void sortExpr();
void normExpr();
chain_list *searchNumExpr();
void deleteNumExpr();
chain_list *simplifNotExpr();
chain_list *simplif10Expr();
int PMExpr();
void changeOperExpr();

/* ==============================================================
   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 11
#define DONTCARE1 12
#define DONTCARE2 13



/*---------------- 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() ;
pNode restrictBdd();
pNode cnstBdd();
void displayGraphicBdd();
int oneBdd();
int zeroBdd();
int equalBdd();
int numberNodeAllBdd();
int numberNodeBdd();
void markAllBdd() ;
void markBdd();
pNode upVarBdd();
chain_list *supportChain_listBdd();
chain_list *supportIndexBdd();
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() ;

