/****************************************************************************/
/*                                                                          */
/*                      Chaine de CAO & VLSI   Alliance                     */
/*                                                                          */
/*    Produit :  Synthetiseur Logique                                       */
/*    Fichier :  optim.c                                                    */
/*                                                                          */
/*    (c) copyright 1991 Laboratoire MASI equipe CAO & VLSI                 */
/*    Tous droits reserves                                                  */
/*    Support : e-mail cao-vlsi@masi.ibp.fr                                 */
/*                                                                          */
/*    Auteur(s) :  L. Burgun                            le : 08/01/1991     */
/*                                                                          */
/*    Modifie par :                                     le : 15/03/92       */
/*    Modifie par :                                     le : 06/04/92       */
/*    Modifie par :                                     le : 06/07/93       */
/*                                                                          */
/****************************************************************************/

#include <math.h>
#include MUT_H
#include LOG_H
#include BEH_H
#include "optim.h"
#include "sl_facto.h"
      
/*------------------------------------------------------------------------------
bestExpr         :determine la meilleure expression parmi expr1 et expr2.
-------------------------------------------------------
parametres 	 : Deux pointeurs de CHAIN_LIST.
-------------------------------------------------------
return 		 :une pointeur de CHAIN_LIST.
------------------------------------------------------------------------------*/
chain_list *bestExpr(expr1,expr2,optim)
chain_list *expr1,*expr2;
int optim;
{

int num1,num2;

num1 = numberAtomExpr(expr1);
num2 = numberAtomExpr(expr2);

if (optim == 1)	
   {
   int profE1,profE2;

   profE1 = profExprFact(expr1);
   profE2 = profExprFact(expr2);

   if (profE1*profE1 + num1 > profE2*profE2 + num2)
      {
      freeExpr(expr1);
      return(expr2);
      }
   else
      {
      freeExpr(expr2);
      return(expr1);
      }
   }


if (num1 > num2)
   {
   freeExpr(expr1);
   return(expr2);
   }
else
   {
   freeExpr(expr2);
   return(expr1);
   }
}

/*------------------------------------------------------------------------------
mux2Abl          : 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 *mux2Abl(high,low,a,tabName,optim)
pNode high,low;
chain_list *a;
char **tabName;
int optim;
{
pNode pBdd;
chain_list *expr1,*expr2;
chain_list *expr1p,*expr2p;
pNode pt1,pt2;

	/*--------- 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,bdd2Abl(high,tabName,optim),notExpr(a)));

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

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

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


pBdd = applyBinBdd(AND,high,low);

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

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

      return(createBinExpr(XOR,bdd2Abl(low,tabName,optim),a));
      }
   else
      {
      expr1 = bdd2Abl(low,tabName,optim);
      expr2 = bdd2Abl(high,tabName,optim);

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

		/* FDD */

      if (RULES_FDD)
         {
	 printf("FDD: ");

		/* F = L xor (L xor H).a  */

   	 expr1p = bdd2Abl(applyBinBdd(XOR,low,high),tabName,optim);
   	 expr2p = bdd2Abl(low,tabName,optim);

   	 expr2 = createBinExpr(XOR,expr1p,createBinExpr(AND,expr2p,copyExpr(a)) );

         displayExpr(expr2);
         return(bestExpr(expr2,expr1,optim));
   	 }
      else
         return(expr1);
      }
   }

		/* H est inclu dans L */

if (pBdd == high)
   {

   if (RULES_DC)
      {
      pNode ptSimplif1,ptSimplif2;

		/* F = H + a'.L(H=*) */


      ptSimplif1 = simplifDcOneBdd(low,high);

		/* ptSimplif1 et high existe deja */

      if (optim == 0 && searchTH(pTabExpr,ptSimplif1) != EMPTYTH &&
          searchTH(pTabExpr,high) != EMPTYTH)
         {
         expr2 = createBinExpr(OR,
                 copyExpr((chain_list *) searchTH(pTabExpr,high)),
                 createBinExpr(AND,
                         copyExpr((chain_list *) searchTH(pTabExpr,ptSimplif1)),
                         notExpr(a))); 
         return(expr2);
         }



		/* F = L.(H(L'=*) + a') */

      if (RULES_BEST)
         {
         ptSimplif2 = simplifDcZeroBdd(high,notBdd(low));

		/* ptSimplif2 et low existe deja */

         if (optim == 0 && searchTH(pTabExpr,ptSimplif2) != EMPTYTH &&
             searchTH(pTabExpr,low) != EMPTYTH)
            {
            expr1 = createBinExpr(AND,
                    copyExpr((chain_list *) searchTH(pTabExpr,low)),
		    createBinExpr(OR,
                         copyExpr((chain_list *) searchTH(pTabExpr,ptSimplif2)),
                         notExpr(copyExpr(a)))); 

            return(expr1);
            }
		/* low et high existe deja */

         if (optim == 0 && searchTH(pTabExpr,high) != EMPTYTH &&
             searchTH(pTabExpr,low) != EMPTYTH)
            {
            expr2 = createBinExpr(OR,
                    copyExpr((chain_list *) searchTH(pTabExpr,high)),
                    createBinExpr(AND,
                         copyExpr((chain_list *) searchTH(pTabExpr,low)),
                         notExpr(a))); 
            return(expr2);
            }

		/* si aucun n'a deja ete traite ... on cree les expressions et on prends
                    la meilleure */

         expr2 = createBinExpr(OR,
                    bdd2Abl(high,tabName,optim),
                    createBinExpr(AND,
                         bdd2Abl(ptSimplif1,tabName,optim),
                         notExpr(a))); 
         
         expr1 = createBinExpr(AND,
                    bdd2Abl(low,tabName,optim),
		    createBinExpr(OR,
                         bdd2Abl(ptSimplif2,tabName,optim),
                         notExpr(copyExpr(a)))); 

         return(bestExpr(expr2,expr1,optim));
         }
      else
         {
         expr2 = createBinExpr(OR,
                    bdd2Abl(high,tabName,optim),
                    createBinExpr(AND,
                         bdd2Abl(ptSimplif1,tabName,optim),
                         notExpr(a))); 
         return(expr2);
         }
      }
   else

      {
      expr1 = bdd2Abl(low,tabName,optim);
      expr2 = bdd2Abl(high,tabName,optim);
      
      if (optim && (profExprFact(expr1) > profExprFact(expr2)))
         {
		/* F = L.(H + a') */

         return(createBinExpr(AND,
                expr1,createBinExpr(OR,expr2,notExpr(copyExpr(a))))); 
         }
      else
         {

		/* F = H + a'.L */

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

		/* L est inclu dans H */

if (pBdd == low)
   {

		/* F = L + a.H(L=*) */

   if (RULES_DC)
      {
      pNode ptSimplif1,ptSimplif2;


      ptSimplif1 = simplifDcOneBdd(high,low);

		/* ptSimplif1 existe deja */

      if (optim == 0 && searchTH(pTabExpr,ptSimplif1) != EMPTYTH &&
          searchTH(pTabExpr,low) != EMPTYTH)
         {
         expr2 = createBinExpr(OR,
                 copyExpr((chain_list *) searchTH(pTabExpr,low)),
                 createBinExpr(AND,
                         copyExpr((chain_list *) searchTH(pTabExpr,ptSimplif1)),
                         copyExpr(a))); 
         return(expr2);
         }

		/* F = H.(L(H'=*) + a) */

      if (RULES_BEST)
         {
         ptSimplif2 = simplifDcZeroBdd(low,notBdd(high));

		/* ptSimplif2 existe deja */

         if (optim == 0 && searchTH(pTabExpr,ptSimplif2) != EMPTYTH &&
             searchTH(pTabExpr,high) != EMPTYTH)
            {
            expr1 = createBinExpr(AND,
                    copyExpr((chain_list *) searchTH(pTabExpr,high)),
		    createBinExpr(OR,
                         copyExpr((chain_list *) searchTH(pTabExpr,ptSimplif2)),
                         copyExpr(a))); 

            return(expr1);
            }

         if (optim == 0 && searchTH(pTabExpr,high) != EMPTYTH &&
             searchTH(pTabExpr,low) != EMPTYTH)
            {
            expr2 = createBinExpr(OR,
                    copyExpr((chain_list *) searchTH(pTabExpr,low)),
                    createBinExpr(AND,
                         copyExpr((chain_list *) searchTH(pTabExpr,high)),
                         copyExpr(a))); 
            return(expr2);
            }

         expr2 = createBinExpr(OR,
                    bdd2Abl(low,tabName,optim),
                    createBinExpr(AND,
                         bdd2Abl(ptSimplif1,tabName,optim),
                         copyExpr(a))); 

         expr1 = createBinExpr(AND,
                    bdd2Abl(high,tabName,optim),
		    createBinExpr(OR,
                         bdd2Abl(ptSimplif2,tabName,optim),
                         copyExpr(a))); 

         return(bestExpr(expr2,expr1,optim));
         }
      else
         {
         expr2 = createBinExpr(OR,
                    bdd2Abl(low,tabName,optim),
                    createBinExpr(AND,
                         bdd2Abl(ptSimplif1,tabName,optim),
                         copyExpr(a))); 
         return(expr2);
         }
      }
   else
      {
      expr1 = bdd2Abl(low,tabName,optim);
      expr2 = bdd2Abl(high,tabName,optim);
      
      if (optim && (profExprFact(expr1) < profExprFact(expr2)))
         {
		/* F = H.(L + a) */

         return(createBinExpr(AND,
                expr2,createBinExpr(OR,expr1,copyExpr(a)))); 
         }
      else
         {
		/* F = L + a.H */

         return(createBinExpr(OR,
                expr1,createBinExpr(AND,expr2,copyExpr(a)))); 
         }
      }
   }


		/* F = a'.L + a.H  */

expr1 = bdd2Abl(low,tabName,optim);
expr2 = bdd2Abl(high,tabName,optim);

		/* cas general */

if (optim && (!ATOM(expr1) || !ATOM(expr2)))
   {
   int num_OR=0,num_AND=0;

   if (!ATOM(expr1))
      {
      if (OPER(expr1) == OR)
         num_OR = num_OR + lengthExpr(expr1);
      if (OPER(expr1) == AND)
         num_AND = num_AND + lengthExpr(expr1);
      }

   if (!ATOM(expr2))
      {
      if (OPER(expr2) == OR)
         num_OR = num_OR + lengthExpr(expr2);
      if (OPER(expr2) == AND)
         num_AND = num_AND + lengthExpr(expr2);
      }

   if (num_AND < num_OR)	/* (a + L).(a' + H) */
      {
      expr1 = createBinExpr(AND,
                createBinExpr(OR,expr2,notExpr(a)),
                createBinExpr(OR,expr1,copyExpr(a)));
      }
   else				/*  a'.L + a.H  */
      {
      expr1 = createBinExpr(OR,
                createBinExpr(AND,expr1,notExpr(a)),
                createBinExpr(AND,expr2,copyExpr(a)));
      }
   }
else   
   {
   expr1 = createBinExpr(OR,
                createBinExpr(AND,expr1,notExpr(a)),
                createBinExpr(AND,expr2,copyExpr(a)));
   }



if (!RULES_DC || !RULES_BEST)
   return (expr1);

		/* low et high existe deja */

if (optim == 0 && searchTH(pTabExpr,high) != EMPTYTH &&
    searchTH(pTabExpr,low) != EMPTYTH)
   {
   return(expr1);
   }


		/* F = a'.L(H.L=*) + a.H(H.L=*) + H.L(PHL=*) 	   
		    avec PHL = L(H.L=*).H(H.L=*) 		 */

pt1 = simplifDcOneBdd(low,pBdd);
pt2 = simplifDcOneBdd(high,pBdd);

if (pt1 != low && pt2 != high)
   {
   expr1p = bdd2Abl(pt1,tabName,optim);
   expr2p = bdd2Abl(pt2,tabName,optim);

   pt1 = simplifDcOneBdd(pBdd,applyBinBdd(AND,pt1,pt2));

   expr1p = createBinExpr(OR,
                createBinExpr(AND,expr1p,notExpr(copyExpr(a))),
                createBinExpr(AND,expr2p,copyExpr(a)));

   expr1p = createBinExpr(OR,expr1p,bdd2Abl(pt1,tabName,optim));
   return(bestExpr(expr1p,expr1,optim));
   }
else
   return(expr1);
}

/*------------------------------------------------------------------------------
bdd2Abl        :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 *bdd2Abl(pt,tabName,optim)
pNode pt;
char **tabName;
int optim;
{
chain_list *expr1,*expr2;
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,bdd2Abl(pt->high,tabName,optim),notExpr(NAME_ATOM));

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

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

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

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

	/* recherche dans la table de hachage */

   if (searchTH(pTabExpr,pt) != EMPTYTH)
      {
      return(copyExpr((chain_list *) searchTH(pTabExpr,pt)));
      }

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

   if (ITE)
      { 


      if (pt->high == (pt->low)->high || pt->high == (pt->low)->low ||
          pt->low == (pt->high)->low || pt->low == (pt->high)->high ||
          (RULES_XOR && ((pt->high)->index == (pt->low)->index) && 
           ((pt->high)->low == (pt->low)->high) && 
           ((pt->high)->high == (pt->low)->low)))
         {
         chain_list *exprint;
         pNode pLow, pHigh;

         pBdd = pt;		/* sauvegarde de pt */
         exprint = NAME_ATOM;   /* initialisation de la commande de mux avec la variable de pt */
         pHigh = pt->high;	/* initialisation pHigh et pLow */
         pLow  = pt->low;
         
         while ((pHigh->index > 1 && pLow->index > 1) &&
                ((pHigh == (pLow)->high || pHigh == (pLow)->low   ||
                pLow  == (pHigh)->low || pLow  == (pHigh)->high ||
                (RULES_XOR && (pHigh->index == pLow->index) && 
                 (pHigh->low == pLow->high) && (pHigh->high == pLow->low)))))
               {
				/* noyaux OU */

               if (pHigh == (pLow)->high || pHigh == (pLow)->low)
                  {
                  expr1 = createExpr(OR);
                  addQExpr(expr1,exprint); 
                  pt = pLow;

                  while (pt->high == pHigh || pt->low == pHigh)
                     {
                     if (pt->high == pHigh)
	                {
                        addQExpr(expr1,NAME_ATOM); 
                        pt = pt->low;
   	                }
      	             else
	                {
                        addQExpr(expr1,notExpr(NAME_ATOM)); 
	                pt = pt->high;
 	                }
                     }
                  pLow = pt;		/* mise a jour de pLow et exprint */
                  exprint = expr1;
                  }
				/* noyaux ET */

               if (pLow == (pHigh)->low || pLow == (pHigh)->high)
	          {
                  expr1 = createExpr(AND);
                  addQExpr(expr1,exprint); 
                  pt = pHigh;
   
                  while (pt->low == pLow || pt->high == pLow)
                     {     
                     if (pt->low == pLow)
	                {
                        addQExpr(expr1,NAME_ATOM); 
                        pt = pt->high;
	                }
                     else
	                {
                        addQExpr(expr1,notExpr(NAME_ATOM)); 
                        pt = pt->low;
	                }
                     }
                  pHigh = pt;		/* mise a jour de pHigh et exprint */
                  exprint = expr1;
                  }

			/* noyaux XOR-NXOR */

               if (RULES_XOR)
                  {
                  if ((pHigh)->index == (pLow)->index)
                     {
	             if ((pHigh->high == pLow->low) && (pLow->high == pHigh->low))
                        {
	                expr1 = createExpr(XOR);
                        addQExpr(expr1,exprint); 
                        pt = pLow;
                        addQExpr(expr1,NAME_ATOM); 
	                pHigh = pHigh->low;
	                pLow =  pLow->low;
                        exprint = expr1;
                        }
                     }
                 }
              }
			/* il n'existe plus de propriete ... */

         res = mux2Abl(pHigh,pLow,exprint,tabName,optim);
/*
         addTH(pTabExpr,pBdd,copyExpr(res));
*/
         return(res);
         }
      }

         	/* recherche de simplifications au 2eme niveau */

   if ((pt->high)->index == (pt->low)->index)
      {

		/* HL = LH */

      if ((pt->high)->low == (pt->low)->high && ((pt->high)->low)->index > 1)
         {
         pBdd = pt;


			/* carry de l'additionneur */

         if (RULES_CARRY)
            {
            if ((pt->high)->high == one && (pt->low)->low == zero)
               {
               res = bdd2Abl((pt->high)->low,tabName,optim);
               expr1 = createExpr(AND);
               expr2 = createExpr(OR);
               addQExpr(expr1,NAME_ATOM);		/* a */
               addQExpr(expr2,NAME_ATOM);
               pt = pt->high; 
               addQExpr(expr1,NAME_ATOM);		/* b */
               addQExpr(expr2,NAME_ATOM);
   
               if (!ATOM(res) && OPER(res) == OR)
                  {
			   /*  (a.b + HL).(a + b)  */
   
                  expr1 = createBinExpr(OR,res,expr1);
                  res = createExpr(AND);
                  addQExpr(res,expr1);
                  addQExpr(res,expr2);
                  }
               else
			   /*  a.b + (a + b).HL  */
                  {
                  expr2 = createBinExpr(AND,res,expr2);
                  res = createExpr(OR);
                  addQExpr(res,expr1);
                  addQExpr(res,expr2);
                  }
/*
               addTH(pTabExpr,pBdd,copyExpr(res));
*/
               return(res);
               }
			   /*  a'.b' + HL.(a' + b')  */
   
            if ((pt->high)->high == zero && (pt->low)->low == one)
               {
               res = bdd2Abl((pt->high)->low,tabName,optim);
               expr1 = createExpr(AND);
               expr2 = createExpr(OR);
               addQExpr(expr1,notExpr(NAME_ATOM));   /* not a */
               addQExpr(expr2,notExpr(NAME_ATOM));
               pt = pt->high; 
               addQExpr(expr1,notExpr(NAME_ATOM));  /* not b */
               addQExpr(expr2,notExpr(NAME_ATOM));

               if (!ATOM(res) && OPER(res) == OR)
                  {
			   /*  (a'.b' + HL).(a' + b')  */

                  expr1 = createBinExpr(OR,res,expr1);
                  res = createExpr(AND);
                  addQExpr(res,expr1);
                  addQExpr(res,expr2);
                  }
               else
			   /*  a'.b' + (a' + b').HL  */
                  {
                  expr2 = createBinExpr(AND,res,expr2);
                  res = createExpr(OR);
                  addQExpr(res,expr1);
                  addQExpr(res,expr2);
                  }
/*
               addTH(pTabExpr,pBdd,copyExpr(res));
*/
               return(res);
               }
            }			/* fin RULES_CARRY */

         if (optim && RULES_SON)
            {
			   /* a'.b'.LL + (a xor b).HL 
                              si HL inclus dans LL
                              a'.b'.LL(HL=*) + (a' + b').HL */
   
            if ((pt->high)->high == zero)
               {
               pNode ptAND = applyBinBdd(AND,(pt->high)->low,(pt->low)->low);
               pNode simplif;

               if (ptAND == (pBdd->high)->low)
                  expr1 = createExpr(OR);
               else
                  expr1 = createExpr(XOR);

               expr2 = createExpr(AND);
               if (ptAND == (pt->high)->low)
                  addQExpr(expr1,notExpr(NAME_ATOM));   /* not a */
               else
                  addQExpr(expr1,NAME_ATOM);   /* a */
               addQExpr(expr2,notExpr(NAME_ATOM));   /* not a */

               pt = pBdd->high;
               if (ptAND == (pBdd->high)->low)
                  addQExpr(expr1,notExpr(NAME_ATOM));   /* not b */
               else
                  addQExpr(expr1,NAME_ATOM);   /* b */
               addQExpr(expr2,notExpr(NAME_ATOM));	/* not b */

               if (RULES_DC && ptAND == (pBdd->high)->low)
                  simplif = simplifDcOneBdd((pBdd->low)->low,(pBdd->high)->low);
               else
                  simplif = (pBdd->low)->low; 
               addQExpr(expr2,bdd2Abl(simplif,tabName,optim));

               res = createBinExpr(OR,expr2,
                       createBinExpr(AND,expr1,bdd2Abl((pBdd->high)->low,tabName,optim))); ;
/*
               addTH(pTabExpr,pBdd,copyExpr(res));
*/
               return(res);
               }
			   /* a.b.HH + (a xor b).HL
                              si HL inclus dans HH
                              a.b.HH(HL=*) + (a + b).HL */
   
            if ((pt->low)->low == zero)
               {
               pNode ptAND = applyBinBdd(AND,(pt->high)->low,(pt->high)->high);
               pNode simplif;

               if (ptAND == (pBdd->high)->low)
                  expr1 = createExpr(OR);
               else
                  expr1 = createExpr(XOR);

               expr2 = createExpr(AND);
               addQExpr(expr1,NAME_ATOM);   /* a */
               addQExpr(expr2,NAME_ATOM);   /* a */
               pt = pBdd->high;
               addQExpr(expr1,NAME_ATOM);   /* b */
               addQExpr(expr2,NAME_ATOM);   /* b */

               if (RULES_DC && ptAND == (pBdd->high)->low)
                  simplif = simplifDcOneBdd((pBdd->high)->high,(pBdd->high)->low);
               else
                  simplif = (pBdd->high)->high; 
               addQExpr(expr2,bdd2Abl(simplif,tabName,optim));

               res = createBinExpr(OR,expr2,
                       createBinExpr(AND,expr1,bdd2Abl((pBdd->high)->low,tabName,optim))); ;
/*
               addTH(pTabExpr,pBdd,copyExpr(res));
*/
               return(res);
               }
			   /*  a'.b' + (a' + b').HL + a.b.HH */
   
            if ((pt->low)->low == one)
               {
               expr1 = createExpr(AND);
               addQExpr(expr1,notExpr(NAME_ATOM));   /* not a */
               pt = pBdd->high;
               addQExpr(expr1,notExpr(NAME_ATOM));	/* not b */
               res = createBinExpr(OR,expr1,bdd2Abl(initVertexBdd(pBdd->index,pBdd->high,pt->low),
                                      tabName,optim)); 
/*
               addTH(pTabExpr,pBdd,copyExpr(res));
*/
               return(res);
               }
			   /*  a.b + (a + b).HL + a'.b'.LL */
   
            if ((pt->high)->high == one)
               {
               expr1 = createExpr(AND);
               addQExpr(expr1,NAME_ATOM);   /* a */
               pt = pBdd->high;
               addQExpr(expr1,NAME_ATOM);	/* b */
               res = createBinExpr(OR,expr1,bdd2Abl(initVertexBdd(pBdd->index,pt->low,pBdd->low),
                                      tabName,optim)); 
/*
               addTH(pTabExpr,pBdd,copyExpr(res));
*/
               return(res);
               }
            }
         pt = pBdd;
         }

			/* HH = LL */

      if ((pt->high)->high == (pt->low)->low && ((pt->high)->high)->index > 1)
         {
         pBdd = pt;

			/* carry de l'additionneur */

         if (RULES_CARRY)
            {
			/*  a.b' + HH.(a + b')  */

            if ((pt->high)->low == one && (pt->low)->high == zero)
               {
               res = bdd2Abl((pt->high)->high,tabName,optim);
               expr1 = createExpr(AND);
               expr2 = createExpr(OR);
               addQExpr(expr1,NAME_ATOM);		/* a */
               addQExpr(expr2,NAME_ATOM);
               pt = pt->high; 
               addQExpr(expr1,notExpr(NAME_ATOM));  /* not b */
               addQExpr(expr2,notExpr(NAME_ATOM));
   
               if (!ATOM(res) && OPER(res) == OR)
                  {
			   /*  (a.b' + HH).(a + b')  */
   
                  expr1 = createBinExpr(OR,res,expr1);
                  res = createExpr(AND);
                  addQExpr(res,expr1);
                  addQExpr(res,expr2);
                  }
               else
			   /*  a.b' + (a + b').HH  */
                  {
                  expr2 = createBinExpr(AND,res,expr2);
                  res = createExpr(OR);
                  addQExpr(res,expr1);
                  addQExpr(res,expr2);
                  }
/*
               addTH(pTabExpr,pBdd,copyExpr(res));
*/
               return(res);
               }
			   /*  a'.b + HH.(a' + b)  */
   
            if ((pt->high)->low == zero && (pt->low)->high == one)
               {
               res = bdd2Abl((pt->high)->high,tabName,optim);
               expr1 = createExpr(AND);
               expr2 = createExpr(OR);
               addQExpr(expr1,notExpr(NAME_ATOM));   /* not a */
               addQExpr(expr2,notExpr(NAME_ATOM));
               pt = pt->high; 
               addQExpr(expr1,NAME_ATOM);  	/* b */
               addQExpr(expr2,NAME_ATOM);

               if (!ATOM(res) && OPER(res) == OR)
                  {
			   /*  (a'.b + HH).(a' + b)  */
   
                  expr1 = createBinExpr(OR,res,expr1);
                  res = createExpr(AND);
                  addQExpr(res,expr1);
                  addQExpr(res,expr2);
                  }
               else
			   /*  a'.b + (a' + b).HH  */
                  {
                  expr2 = createBinExpr(AND,res,expr2);
                  res = createExpr(OR);
                  addQExpr(res,expr1);
                  addQExpr(res,expr2);
                  }
/*
               addTH(pTabExpr,pBdd,copyExpr(res));
*/
               return(res);
               }
            }

         if (optim && RULES_SON)
            {
			   /* a'.b.LH + (a' xor b).LL
                              si LL inclus dans LH
                              a'.b.LH(LL=*) + (a' + b).LL */
   
            if ((pt->high)->low == zero)
               {
               pNode ptAND = applyBinBdd(AND,(pt->low)->low,(pt->low)->high);
               pNode simplif;

               if (ptAND == (pBdd->low)->low)
                  expr1 = createExpr(OR);
               else
                  expr1 = createExpr(XOR);
               expr2 = createExpr(AND);
               addQExpr(expr1,notExpr(NAME_ATOM));   /* not a */
               addQExpr(expr2,notExpr(NAME_ATOM));   /* not a */
               pt = pBdd->high;
               addQExpr(expr1,NAME_ATOM);   /* b */
               addQExpr(expr2,NAME_ATOM);   /* b */

               if (RULES_DC && ptAND == (pBdd->low)->low)
                  simplif = simplifDcOneBdd((pBdd->low)->high,(pBdd->low)->low);
               else
                  simplif = (pBdd->low)->high; 
               addQExpr(expr2,bdd2Abl(simplif,tabName,optim));

               res = createBinExpr(OR,expr2,
                       createBinExpr(AND,expr1,bdd2Abl((pBdd->low)->low,tabName,optim))); ;
/*
               addTH(pTabExpr,pBdd,copyExpr(res));
*/
               return(res);
               }
			   /* a.b'.HL + (a xor b').LL
                              si LL inclus dans HL
                              a.b'.HL(LL=*) + (a + b').LL */
   
            if ((pt->low)->high == zero)
               {
               pNode ptAND = applyBinBdd(AND,(pt->low)->low,(pt->high)->low);
               pNode simplif;

               if (ptAND == (pBdd->low)->low)
                  expr1 = createExpr(XOR);
               else
                  expr1 = createExpr(XOR);
               expr2 = createExpr(AND);
               addQExpr(expr1,NAME_ATOM);   /* a */
               addQExpr(expr2,NAME_ATOM);   /* a */
               pt = pBdd->high;
               addQExpr(expr1,notExpr(NAME_ATOM));   /* not b */
               addQExpr(expr2,notExpr(NAME_ATOM));   /* b */

               if (RULES_DC && ptAND == (pBdd->low)->low)
                  simplif = simplifDcOneBdd((pBdd->high)->low,(pBdd->low)->low);
               else
                  simplif = (pBdd->high)->low; 
               addQExpr(expr2,bdd2Abl(simplif,tabName,optim));

               res = createBinExpr(OR,expr2,
                       createBinExpr(AND,expr1,bdd2Abl((pBdd->low)->low,tabName,optim))); ;
/*
               addTH(pTabExpr,pBdd,copyExpr(res));
*/
               return(res);
               }
   
			   /*  a.b' + (a + b').HH + a'.b.LH */
   
            if ((pt->high)->low == one)
               {
               expr1 = createExpr(AND);
               addQExpr(expr1,NAME_ATOM);   		/* a */
               pt = pBdd->low;
               addQExpr(expr1,notExpr(NAME_ATOM));	/* not b */
               res = createBinExpr(OR,expr1,bdd2Abl(initVertexBdd(pBdd->index,pt->low,pBdd->low),
                                      tabName,optim)); 
/*
               addTH(pTabExpr,pBdd,copyExpr(res));
*/
               return(res);
               }
			   /*  a'.b + (a' + b).HH + a.b'.HL */
   
            if ((pt->low)->high == one)
               {
               expr1 = createExpr(AND);
               addQExpr(expr1,notExpr(NAME_ATOM));   /* not a */
               pt = pBdd->low;
               addQExpr(expr1,NAME_ATOM);	/* b */
               res = createBinExpr(OR,expr1,bdd2Abl(initVertexBdd(pBdd->index,pBdd->high,pt->low),
                                      tabName,optim)); 
/*
               addTH(pTabExpr,pBdd,copyExpr(res));
*/
               return(res);
               }
            }
         pt = pBdd;
         }
   
			   /* HH = LH */
   
      if ((pt->high)->high == (pt->low)->high && ((pt->high)->high)->index > 1)
         {
         pBdd = pt;
   
         if (RULES_CARRY)
            {
			   /*  a.b' + HH.b  */
   
            if ((pt->high)->low == one && (pt->low)->low == zero)
               {
               expr1 = createExpr(AND);
               addQExpr(expr1,NAME_ATOM);		/* a */
               pt = pt->high; 
               addQExpr(expr1,notExpr(NAME_ATOM));  /* not b */
               expr2 = createBinExpr(AND,NAME_ATOM,bdd2Abl(pt->high,tabName,optim));
               res = createExpr(OR);
               addQExpr(res,expr1);
               addQExpr(res,expr2);
/*
               addTH(pTabExpr,pBdd,copyExpr(res));
*/
               return(res);
               }
			   /*  a'.b' + HH.b  */
   
            if ((pt->high)->low == zero && (pt->low)->low == one)
               {
               expr1 = createExpr(AND);
               addQExpr(expr1,notExpr(NAME_ATOM));   /* not a */
               pt = pt->high; 
               addQExpr(expr1,notExpr(NAME_ATOM));   /* not b */
               expr2 = createBinExpr(AND,NAME_ATOM,bdd2Abl(pt->high,tabName,optim));
               res = createExpr(OR);
               addQExpr(res,expr1);
               addQExpr(res,expr2);
/*
               addTH(pTabExpr,pBdd,copyExpr(res));
*/
               return(res);
               }
            }
         pt = pBdd;
         }
   
			   /*  HL = LL */
   
      if ((pt->high)->low == (pt->low)->low && ((pt->high)->low)->index > 1)
	 {
         pBdd = pt;

         if (RULES_CARRY)
            {
			/*  a.b + HL.b'  */

            if ((pt->high)->high == one && (pt->low)->high == zero)
               {
               expr1 = createExpr(AND);
               addQExpr(expr1,NAME_ATOM);		/* a */
               pt = pt->high; 
               addQExpr(expr1,NAME_ATOM);  	/* b */
               expr2 = createBinExpr(AND,notExpr(NAME_ATOM),bdd2Abl(pt->low,tabName,optim));
               res = createExpr(OR);
               addQExpr(res,expr1);
               addQExpr(res,expr2);
/*
               addTH(pTabExpr,pBdd,copyExpr(res));
*/
               return(res);
               }
			   /*  a'.b + HL.b'  */

            if ((pt->high)->high == zero && (pt->low)->high == one)
               {
               expr1 = createExpr(AND);
               expr2 = createExpr(OR);
               addQExpr(expr1,notExpr(NAME_ATOM));   /* not a */
               pt = pt->high; 
               addQExpr(expr1,NAME_ATOM);		/* b */
               expr2 = createBinExpr(AND,notExpr(NAME_ATOM),bdd2Abl(pt->low,tabName,optim));
               res = createExpr(OR);
               addQExpr(res,expr1);
               addQExpr(res,expr2);
/*
               addTH(pTabExpr,pBdd,copyExpr(res));
*/
               return(res);
               }
            }
         pt = pBdd;
         }
      }

		/*  (or (and a H) (and (not a) L) */

   res =  mux2Abl(pt->high,pt->low,NAME_ATOM,tabName,optim);

/*
   addTH(pTabExpr,pt,copyExpr(res));
*/
   return(res);
   }
}
/*------------------------------------------------------------------------------
numberAtomFact  : calcule le nombre de litteraux resultant de l'appel bdd2abl
-------------------------------------------------------
parametres 	 :un pointeur de NODE.
-------------------------------------------------------
return 		 :un int 
------------------------------------------------------------------------------*/
int numberAtomFact(pt)
pNode pt;
{
pNode pBdd;
int cpt;
int numberAtomFacto2();

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

if (pt->index < 2)
   return(0);

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

if ((pt->low)->index < 2 || (pt->high)->index < 2)
   {
   if ((pt->low)->index < 2 && (pt->high)->index < 2)
      return(1);
   else		/* variable semi-terminale */
      {
      if (pt->low == one || pt->low == zero)	/* F = (or (not a) H) */
         return(1+numberAtomFact(pt->high));

      if (pt->high == one || pt->high == one)	/* F = (or a L) */
         return(1+numberAtomFact(pt->low));
      }
   }
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)
      {
      pBdd = pt;
      cpt = 0;
      while (pt->high == pBdd->high || pt->low == pBdd->high)
         {
         if (pt->high == pBdd->high)
	    {
            cpt++;
            pt = pt->low;
   	    }
      	 else
	    {
            cpt++;
	    pt = pt->high;
 	    }
         }
      cpt = numberAtomFacto2(pBdd->high,pt,cpt);
      return(cpt);
      }
   else
      {
      if (pt->low == (pt->high)->low || pt->low == (pt->high)->high)
	 {
         cpt = 0;
         pBdd = pt;		/* sauvegarde de pt */
         while (pt->low == pBdd->low || pt->high == pBdd->low)
            {
            if (pt->low == pBdd->low)
	       {
               cpt++;
               pt = pt->high;
	       }
            else
	       {
               cpt++;
               pt = pt->low;
	       }
            }
         cpt = numberAtomFacto2(pBdd->low,pt,cpt);
         return(cpt);
         }
      }
   }

         	/* recherche de simplifications au 2eme niveau */

   if ((pt->high)->index == (pt->low)->index)
      {

		/* HL = LH */

      if ((pt->high)->low == (pt->low)->high)
         {

			/* noyaux XOR-NXOR */

         if (RULES_XOR)
            {
	    if ((pt->high)->high == (pt->low)->low) 
               {
               cpt = numberAtomFacto2((pt->low)->high,(pt->low)->low,2);
               return(cpt);
               }
            }
			/* carry de l'additionneur */
			/*  a.b + HL.(a + b)  */

         if ((pt->high)->high == one && 
            (pt->low)->low == zero)
            {
            return(4 + numberAtomFact((pt->high)->low));
            }
			/*  a'.b' + HL.(a' + b')  */

         if ((pt->high)->high == zero && 
            (pt->low)->low == one)
            {
            return(4 + numberAtomFact((pt->high)->low));
            }

         }
			/* HH = LL */

      if ((pt->high)->high == (pt->low)->low)
         {

			/* carry de l'additionneur */
			/*  a.b' + HH.(a + b')  */

         if ((pt->high)->low == one && 
            (pt->low)->high == zero)
            {
            return(4 + numberAtomFact((pt->high)->high));
            }
			/*  a'.b + HH.(a' + b)  */

         if ((pt->high)->low == zero && 
            (pt->low)->high == one)
            {
            return(4 + numberAtomFact((pt->high)->high));
            }
         }

			/* HH = LH */

      if ((pt->high)->high == (pt->low)->high)
         {

			/* carry de l'additionneur */
			/*  a.b' + HH.b  */

         if ((pt->high)->low == one && 
            (pt->low)->low == zero)
            {
            return(3 + numberAtomFact((pt->high)->high));
            }
			/*  a'.b' + HH.b  */

         if ((pt->high)->low == zero && 
            (pt->low)->low == one)
            {
            return(3 + numberAtomFact((pt->high)->high));
            }

	 }

			/*  HL = LL */

      if ((pt->high)->low == (pt->low)->low) 
	 {

			/* carry de l'additionneur */
			/*  a.b + HL.b'  */

         if ((pt->high)->high == one && 
            (pt->low)->high == zero)
            {
            return(3 + numberAtomFact((pt->high)->low));
            }
			/*  a'.b + HL.b'  */

         if ((pt->high)->high == zero && 
            (pt->low)->high == one)
            {
            return(3 + numberAtomFact((pt->high)->low));
            }

         }
      }

		/*  (or (and a H) (and (not a) L) */

cpt = numberAtomFacto2(pt->high,pt->low,1);
return(cpt);
}

/*------------------------------------------------------------------------------
numberAtomFacto2  : renvoie le nombre de litteraux realisant le multiplexeur
                    a.H + a'.L
-------------------------------------------------------
parametres 	 : Deux pNode et le nombre de litteraux de la commande 
-------------------------------------------------------
return 		 : un int
------------------------------------------------------------------------------*/
int numberAtomFacto2(high,low,cpt)
pNode high,low;
int cpt;
{
pNode pBdd;

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

if (low->index < 2 && high->index < 2)
   return(cpt);

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

if (low == one || low == zero)	/* F = (or (not a) H) */
    return(cpt + numberAtomFact(high));

if (high == one || high == zero)	/* F = (or a L) */
    return(cpt + numberAtomFact(low));


pBdd = applyBinBdd(AND,high,low);

if (RULES_XOR && pBdd == zero)		/* F = (xor a L) */
   if (applyBinBdd(OR,low,high) == one)
      return(cpt + numberAtomFact(high));

		/* H est inclu dans L */

if (pBdd == high)
		/* F = H + a'.L(H=*) */

   return(cpt + numberAtomFact(high) + 
                numberAtomFact(simplifDcOneBdd(low,high)));


		/* L est inclu dans H */

if (pBdd == low)

		/* F = L + a.H(L=*) */

   return(cpt + numberAtomFact(low) + 
                numberAtomFact(simplifDcOneBdd(high,low)));

		/* cas general */

		/* F = a'.L + a.H  */

return(2*cpt + numberAtomFact(low) + numberAtomFact(high));
}

/*------------------------------------------------------------------------------
profFact  : calcule la profondeur d'un abl. 
-------------------------------------------------------
parametres 	 :un pointeur de NODE.
-------------------------------------------------------
return 		 :un int 
------------------------------------------------------------------------------*/
int profFact(pt,ptHash)
pNode pt;
pTH ptHash;
{
pNode pBdd;
int cpt;
int profFact2();

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

if (pt->index < 2)
   return(0);

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

if ((pt->low)->index < 2 && (pt->high)->index < 2)
   return(0);
else
   {

   if ((cpt = searchTH(ptHash,pt)) != EMPTYTH)
      return(cpt);

	/*---------------- 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)
      {
      pBdd = pt;
      cpt = 0;
      while (pt->high == pBdd->high || pt->low == pBdd->high)
         {
         if (pt->high == pBdd->high)
	    {
            cpt++;
            pt = pt->low;
   	    }
      	 else
	    {
            cpt++;
	    pt = pt->high;
 	    }
         }
      cpt = profFact2(pBdd->high,pt,logsup2(cpt),ptHash);
      addTH(ptHash,pBdd,cpt);
      return(cpt);
      }
   else
      {
      if (pt->low == (pt->high)->low || pt->low == (pt->high)->high)
	 {
         cpt = 0;
         pBdd = pt;		/* sauvegarde de pt */
         while (pt->low == pBdd->low || pt->high == pBdd->low)
            {
            if (pt->low == pBdd->low)
	       {
               cpt++;
               pt = pt->high;
	       }
            else
	       {
               cpt++;
               pt = pt->low;
	       }
            }
         cpt = profFact2(pBdd->low,pt,logsup2(cpt),ptHash);
         addTH(ptHash,pBdd,cpt);
         return(cpt);
         }
      }
         	/* recherche de simplifications au 2eme niveau */

   if ((pt->high)->index == (pt->low)->index)
      {

		/* HL = LH */

      if ((pt->high)->low == (pt->low)->high)
         {

			/* noyaux XOR-NXOR */

	 if ((pt->high)->high == (pt->low)->low) 
            {
            cpt = profFact2((pt->low)->high,(pt->low)->low,1,ptHash);
            return(cpt);
            }
			/* carry de l'additionneur */
			/*  a.b + HL.(a + b)  */

         if ((pt->high)->high == one && 
            (pt->low)->low == zero)
            {
            return(2 + profFact((pt->high)->low,ptHash));
            }
			/*  a'.b' + HL.(a' + b')  */

         if ((pt->high)->high == zero && 
            (pt->low)->low == one)
            {
            return(2 + profFact((pt->high)->low,ptHash));
            }

         }
			/* HH = LL */

      if ((pt->high)->high == (pt->low)->low)
         {

			/* carry de l'additionneur */
			/*  a.b' + HH.(a + b')  */

         if ((pt->high)->low == one && 
            (pt->low)->high == zero)
            {
            return(2 + profFact((pt->high)->high,ptHash));
            }
			/*  a'.b + HH.(a' + b)  */

         if ((pt->high)->low == zero && 
            (pt->low)->high == one)
            {
            return(2 + profFact((pt->high)->high,ptHash));
            }
         }

			/* HH = LH */

      if ((pt->high)->high == (pt->low)->high)
         {

			/* carry de l'additionneur */
			/*  a.b' + HH.b  */

         if ((pt->high)->low == one && 
            (pt->low)->low == zero)
            {
            return(2 + profFact((pt->high)->high,ptHash));
            }
			/*  a'.b' + HH.b  */

         if ((pt->high)->low == zero && 
            (pt->low)->low == one)
            {
            return(2 + profFact((pt->high)->high,ptHash));
            }

	 }

			/*  HL = LL */

      if ((pt->high)->low == (pt->low)->low) 
	 {

			/* carry de l'additionneur */
			/*  a.b + HL.b'  */

         if ((pt->high)->high == one && 
            (pt->low)->high == zero)
            {
            return(2 + profFact((pt->high)->low,ptHash));
            }
			/*  a'.b + HL.b'  */

         if ((pt->high)->high == zero && 
            (pt->low)->high == one)
            {
            return(2 + profFact((pt->high)->low,ptHash));
            }

         }
      }

		/*  (or (and a H) (and (not a) L) */

   cpt = profFact2(pt->high,pt->low,0,ptHash);
   addTH(ptHash,pt,cpt);
   return(cpt);
   }
}
/*------------------------------------------------------------------------------
profFact2  : renvoie la profondeur de l'expression realisant le multiplexeur
                    a.H + a'.L
-------------------------------------------------------
parametres 	 : Deux pNodes et la profondeur de la commande 
-------------------------------------------------------
return 		 : un int
------------------------------------------------------------------------------*/
int profFact2(high,low,cpt,ptHash)
pNode high,low;
int cpt;
pTH ptHash;
{
pNode pBdd;

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

if (low->index < 2 && high->index < 2)
   return(cpt);

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

if (low == one) 	/* F = (or (not a) H) */
    return(1 + MAX(cpt,profFact(high,ptHash)));

if (high == one)	/* F = (or a L) */
    return(1 + MAX(cpt,profFact(low,ptHash)));

if (low == zero) 	/* F = (and (not a) H) */
    return(1 + MAX(cpt,profFact(high,ptHash)));

if (high == zero)	/* F = (and a L) */
    return(1 + MAX(cpt,profFact(low,ptHash)));


pBdd = applyBinBdd(AND,high,low);

if (pBdd == zero)
   if (applyBinBdd(OR,low,high) == one)
      return(2 + profFact(high,ptHash));

		/* H est inclu dans L */

if (pBdd == high)
		/* F = H + a'.L(H=*) */
   {

   int profHigh = 1 + profFact(high,ptHash);
   int profLow  = 2 + MAX(cpt,profFact(simplifDcOneBdd(low,high),ptHash));

   return(MAX(profHigh,profLow));
   }


		/* L est inclu dans H */

if (pBdd == low)

		/* F = L + a.H(L=*) */
   {
   int profLow  = 1 + profFact(low,ptHash);
   int profHigh  = 2 + MAX(cpt,profFact(simplifDcOneBdd(high,low),ptHash));

   return(MAX(profHigh,profLow));
   }

		/* cas general */

		/* F = a'.L + a.H  */

   {
   int profLow  = 2 + profFact(low,ptHash);
   int profHigh = 2 + profFact(high,ptHash);

   return(MAX(profHigh,profLow));

   }
}

/*------------------------------------------------------------------------------
numberAtomRedFacto2  : renvoie le nombre de litteraux reduit 
                       realisant le multiplexeur a.H + a'.L
-------------------------------------------------------
parametres 	 : Deux pNode et le nombre de litteraux de la commande 
-------------------------------------------------------
return 		 : un int
------------------------------------------------------------------------------*/
int numberAtomRedFacto2(high,low,cpt)
pNode high,low;
int cpt;
{
pNode pBdd;

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

if (low->index < 2 && high->index < 2)
   return(cpt);

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

if (low == one || low == zero)	/* F = (or (not a) H) */
    return(cpt + numberAtomRedFact(high));

if (high == one || high == zero)	/* F = (or a L) */
    return(cpt + numberAtomRedFact(low));


pBdd = applyBinBdd(AND,high,low);

if (pBdd == zero)	
   {
   if (RULES_XOR && applyBinBdd(OR,low,high) == one)
      return(cpt + numberAtomRedFact(high));
   else
      {
      if (cpt == 1)
         return(2 + numberAtomRedFact(low) + numberAtomRedFact(high));
      else
         return(cpt + 2 + numberAtomRedFact(low) + numberAtomRedFact(high));
      }
   }

		/* H est inclu dans L */

		/* F = H + a'.L(H=*) */

if (pBdd == high)
   {
   return(cpt + numberAtomRedFact(high) + 
                numberAtomRedFact(simplifDcOneBdd(low,high)));
   }


		/* L est inclu dans H */

		/* F = L + a.H(L=*) */

if (pBdd == low)
   {
   return(cpt + numberAtomRedFact(low) + 
                numberAtomRedFact(simplifDcOneBdd(high,low)));
   }

		/* cas general */

		/* F = a'.L + a.H  */

if (cpt == 1)
   return(2 + numberAtomRedFact(low) + numberAtomRedFact(high));
else
   return(cpt + 2 + numberAtomRedFact(low) + numberAtomRedFact(high));
}

/*------------------------------------------------------------------------------
numberAtomRedFact  : calcule le nombre de litteraux reduits
                     fonction de cout pour l'ordonnancement
-------------------------------------------------------
parametres 	 :un pointeur de NODE.
-------------------------------------------------------
return 		 :un int 
------------------------------------------------------------------------------*/
int numberAtomRedFact(pt)
pNode pt;
{
pNode pBdd;
pNode ptNotBdd;
int cpt;
pNode pLow, pHigh;

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

if (pt->index < 2)
   return(0);

		  /* noeud atomique */

if ((pt->low)->index < 2 && (pt->high)->index < 2)
   return(1);

        /*------------------ deja traite -------------------------*/

                  /* premiere occurence */

if (pt->mark == 1)
   {
   pt->mark = 2;
   ptNotBdd = notBdd(pt); 
   ptNotBdd->mark = 2;
   return(2);
   }

		/* x-ieme occurence (x > 1) */

if (pt->mark == 2)
   return(1);

        /*------------------ non traite -------------------------*/

pt->mark = 1;

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

if ((pt->low)->index < 2 || (pt->high)->index < 2)
   {
   if (pt->low == one || pt->low == zero)	
      cpt = 1+numberAtomRedFact(pt->high);

   if (pt->high == one || pt->high == zero)
      cpt = 1+numberAtomRedFact(pt->low);

   ptNotBdd = notBdd(pt); 
   ptNotBdd->mark = 1;
   return(cpt);
   }

cpt = 1;
pHigh = pt->high;	/* initialisation pHigh et pLow */
pLow  = pt->low;

if (ITE)
   { 


   if (pt->high == (pt->low)->high || pt->high == (pt->low)->low ||
       pt->low == (pt->high)->low || pt->low == (pt->high)->high ||
       (RULES_XOR && ((pt->high)->index == (pt->low)->index) && 
       ((pt->high)->low == (pt->low)->high) && 
       ((pt->high)->high == (pt->low)->low)))
       {

       pBdd = pt;		/* sauvegarde de pt */
         
       while ((pHigh->index > 1 && pLow->index > 1) &&
                ((pHigh == (pLow)->high || pHigh == (pLow)->low   ||
                pLow  == (pHigh)->low || pLow  == (pHigh)->high ||
                (RULES_XOR && (pHigh->index == pLow->index) && 
                 (pHigh->low == pLow->high) && (pHigh->high == pLow->low)))))
               {
				/* noyaux OU */

               if (pHigh == (pLow)->high || pHigh == (pLow)->low)
                  {
                  pt = pLow;

                  while (pt->high == pHigh || pt->low == pHigh)
                     {
                     if (pt->high == pHigh)
	                {
                        cpt++; 
                        pt = pt->low;
   	                }
      	             else
	                {
                        cpt++; 
	                pt = pt->high;
 	                }
                     }
                  pLow = pt;		/* mise a jour de pLow */
                  }
				/* noyaux ET */

               if (pLow == (pHigh)->low || pLow == (pHigh)->high)
	          {
                  pt = pHigh;
   
                  while (pt->low == pLow || pt->high == pLow)
                     {     
                     if (pt->low == pLow)
	                {
                        cpt++; 
                        pt = pt->high;
	                }
                     else
	                {
                        cpt++; 
                        pt = pt->low;
	                }
                     }
                  pHigh = pt;		/* mise a jour de pHigh */
                  }

			/* noyaux XOR-NXOR */

               if (RULES_XOR)
                  {
                  if ((pHigh)->index == (pLow)->index)
                     {
	             if ((pHigh->high == pLow->low) && (pLow->high == pHigh->low))
                        {
                        cpt++; 
	                pHigh = pHigh->low;
	                pLow =  pLow->low;
                        }
                     }
                  }
               }

         pt = pBdd;	/* on recupere le pt initial */
         }
      }

         	/* recherche de simplifications au 2eme niveau */

   if (cpt == 1 && (pt->high)->index == (pt->low)->index)
      {

			/* HL = LH */

      if ((pt->high)->low == (pt->low)->high && ((pt->high)->low)->index > 1)
         {
         if (((pt->high)->high)->index < 2 && ((pt->low)->low)->index < 2)
            {
            return(4 + numberAtomRedFact((pt->high)->low));
            }
         }

			/* HH = LL */

      if ((pt->high)->high == (pt->low)->low && ((pt->high)->high)->index > 1)
         {
         if (((pt->high)->low)->index < 2 && ((pt->low)->high)->index < 2)
            {
            return(4 + numberAtomRedFact((pt->high)->high));
            }
         }
   
			   /* HH = LH */
   
      if ((pt->high)->high == (pt->low)->high && ((pt->high)->high)->index > 1)
         {
         if (((pt->high)->low)->index < 2 && ((pt->low)->low)->index < 2)
            {
            return(3 + numberAtomRedFact((pt->high)->high));
            }
         }
   
			   /*  HL = LL */
   
      if ((pt->high)->low == (pt->low)->low && ((pt->high)->low)->index > 1)
         {
         if (((pt->high)->high)->index < 2 && ((pt->low)->high)->index < 2)
            {
            return(3 + numberAtomRedFact((pt->high)->low));
            }
         }
      }

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


		/*  (or (and a H) (and (not a) L) */

cpt = numberAtomRedFacto2(pHigh,pLow,cpt);

ptNotBdd = notBdd(pt); 
ptNotBdd->mark = 1;

return(cpt);
}

/*-------------------------------------------------------------------------
numberAtomRedCct 	: calcule le nombre d'atome reduit d'un circuit 
---------------------------------------------------------------------------
retour		: un entier.
---------------------------------------------------------------------------*/

int numberAtomRedCct(pC)
pCircuit pC;
{
pElemTH pEl;
int i,numAtomRed;

numAtomRed = 0;
markAllBdd(0);
pEl = (pC->pTO)->pElem;
for (i=0; i<(pC->pTO)->length ; i++)
    {
    if (pEl->value != EMPTYTH && pEl->value != DELETETH)
       {
       numAtomRed = numAtomRed + numberAtomRedFact((pNode) pEl->value);
       }
    pEl++;
    }
markAllBdd(0);
return(numAtomRed);
}

/*-------------------------------------------------------------------------
numberAtomRedBeh 	: calcule le nombre d'atome reduit d'une befig 
---------------------------------------------------------------------------
retour		: un entier.
---------------------------------------------------------------------------*/

int numberAtomRedBeh(beh)
befig_list *beh;
{
int i,numAtomRed;
beout_list *out;
beaux_list *aux;
bereg_list *reg;
bebus_list *bus;
bebux_list *bux;
binode_list *binode;

numAtomRed = 0;
markAllBdd(0);

out = beh->BEOUT;
while (out)
   {
   if (out->NODE)
      numAtomRed = numAtomRed + numberAtomRedFact(out->NODE);
   out = out->NEXT;
   }

aux = beh->BEAUX;
while (aux)
   {
   if (aux->NODE)
      numAtomRed = numAtomRed + numberAtomRedFact(aux->NODE);
   aux = aux->NEXT;
   }

reg = beh->BEREG;
while (reg)
   {
   binode = reg->BINODE;
   while (binode)
      {
      if (binode->CNDNODE)
         numAtomRed = numAtomRed + numberAtomRedFact(binode->CNDNODE);
      if (binode->VALNODE)
         numAtomRed = numAtomRed + numberAtomRedFact(binode->VALNODE);
      binode = binode->NEXT;
      }
   reg = reg->NEXT;
   }

bus = beh->BEBUS;
while (bus)
   {
   binode = bus->BINODE;
   while (binode)
      {
      if (binode->CNDNODE)
         numAtomRed = numAtomRed + numberAtomRedFact(binode->CNDNODE);
      if (binode->VALNODE)
         numAtomRed = numAtomRed + numberAtomRedFact(binode->VALNODE);
      binode = binode->NEXT;
      }
   bus = bus->NEXT;
   }

bux = beh->BEBUX;
while (bux)
   {
   binode = bux->BINODE;
   while (binode)
      {
      if (binode->CNDNODE)
         numAtomRed = numAtomRed + numberAtomRedFact(binode->CNDNODE);
      if (binode->VALNODE)
         numAtomRed = numAtomRed + numberAtomRedFact(binode->VALNODE);
      binode = binode->NEXT;
      }
   bux = bux->NEXT;
   }



markAllBdd(0);
return(numAtomRed);
}
