
/*                                                                          */
/*                      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 : ../../....     */
/*                                                                          */
/****************************************************************************/

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

int num1,num2;

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

if (optim == 1)		/* calcul de la profondeur */
   {
   int profE1,profE2;

   profE1 = syf_profExprFact(expr1);
   profE2 = syf_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);
   }
}

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

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

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

if (high == zero)	/* F = (and (not a) L) */
   return(createBinExpr(AND,syf_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,syf_bdd2Abl(low,tabName,optim),a));
      }
   else
      {
      expr1 = syf_bdd2Abl(low,tabName,optim);
      expr2 = syf_bdd2Abl(high,tabName,optim);

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

		/* H est inclu dans L */

if (pBdd == high)
   {

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

      expr2 = createBinExpr(OR,
                 syf_bdd2Abl(high,tabName,optim),
                 createBinExpr(AND,
                         syf_bdd2Abl(simplifDcOneBdd(low,high),tabName,optim),
                         notExpr(a))); 

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

      expr1 = createBinExpr(AND,
                 syf_bdd2Abl(low,tabName,optim),
		 createBinExpr(OR,
                         syf_bdd2Abl(simplifDcZeroBdd(high,notBdd(low)),tabName,optim),
                         notExpr(copyExpr(a)))); 
      return(syf_bestExpr(expr2,expr1,optim));
      }
   else

      {
      expr1 = syf_bdd2Abl(low,tabName,optim);
      expr2 = syf_bdd2Abl(high,tabName,optim);
      
      if (syf_profExprFact(expr1) > syf_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)
      {
      expr2 = createBinExpr(OR,
                 syf_bdd2Abl(low,tabName,optim),
                 createBinExpr(AND,
                         syf_bdd2Abl(simplifDcOneBdd(high,low),tabName,optim),
                         copyExpr(a))); 

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

      expr1 = createBinExpr(AND,
                 syf_bdd2Abl(high,tabName,optim),
		 createBinExpr(OR,
                         syf_bdd2Abl(simplifDcZeroBdd(low,notBdd(high)),tabName,optim),
                         copyExpr(a))); 

      return(syf_bestExpr(expr2,expr1,optim));
      }
   else
      {
      expr1 = syf_bdd2Abl(low,tabName,optim);
      expr2 = syf_bdd2Abl(high,tabName,optim);
      
      if (syf_profExprFact(expr1) > syf_profExprFact(expr2))
         {
		/* F = L + a.H */

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

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

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


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

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

		/* cas general */

if (!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)));
   }


		/* FDD */

if (RULES_FDD)
   {
		/* F = L xor (L xor H).a  */

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

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

   return(syf_bestExpr(expr1p,expr1,optim));
   }

if (!RULES_DC)
   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 = syf_bdd2Abl(pt1,tabName,optim);
   expr2p = syf_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,syf_bdd2Abl(pt1,tabName,optim));
   return(syf_bestExpr(expr1p,expr1,optim));
   }
else
   return(expr1);
}

/*------------------------------------------------------------------------------
syf_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 *syf_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,syf_bdd2Abl(pt->high,tabName,optim),notExpr(NAME_ATOM));

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

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

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

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

	/* recherche dans la table de hachage */

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

       /* 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 = syf_mux2Abl(pBdd->high,pt,expr1,tabName,optim);
      pt = pBdd;
      addTH(pTabExpr,pt,copyExpr(res));
      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 = syf_mux2Abl(pt,pBdd->low,expr1,tabName,optim);
         pt = pBdd;
         addTH(pTabExpr,pt,copyExpr(res));
         return(res);
         }
      else
	 {
         	/* recherche de simplifications au 2eme niveau */

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

		/* HL = LH */

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

			/* noyaux XOR-NXOR */

               if (RULES_XOR)
                  {
	          if ((pt->high)->high == (pt->low)->low) 
                     {
	             expr1 = createExpr(XOR);
                     addQExpr(expr1,NAME_ATOM); 
    	             pt = pt->low;
                     addQExpr(expr1,NAME_ATOM); 
	             pt = pBdd;
	             res = syf_mux2Abl((pt->low)->high,(pt->low)->low,expr1,tabName,optim);
                     addTH(pTabExpr,pt,copyExpr(res));
                     return(res);
                     }
                  }

			/* carry de l'additionneur */

               if (RULES_CARRY)
                  {
                  if ((pt->high)->high == one && 
                      (pt->low)->low == zero)
                     {
                     res = syf_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)
                     {
                     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));
                     expr2 = createBinExpr(AND,expr2,
                                        syf_bdd2Abl(pt->low,tabName,optim));
                     res = createExpr(OR);
                     addQExpr(res,expr1);
                     addQExpr(res,expr2);
                     addTH(pTabExpr,pBdd,copyExpr(res));
                     return(res);
                     }
                  }

               if (RULES_SON)
                  {
			   /*  (a' + b')((a + b).HL + a'.b'.LL) */
   
                  if ((pt->high)->high == zero)
                     {
                     expr2 = createExpr(OR);
                     addQExpr(expr2,notExpr(NAME_ATOM));   /* not a */
                     pt = pBdd->high;
                     addQExpr(expr2,notExpr(NAME_ATOM));	/* not b */
                     res = createBinExpr(AND,expr2,
                              syf_bdd2Abl(initVertexBdd(pBdd->index,pt->low,pBdd->low),
                                      tabName,optim)); 
   /*
   printf("1 -- ");
   displayExpr(res);
   */
                     addTH(pTabExpr,pBdd,copyExpr(res));
                     return(res);
                     }
			   /*  (a + b)((a' + b').HL + a.b.HH) */
   
                  if ((pt->low)->low == zero)
                     {
                     expr2 = createExpr(OR);
                     addQExpr(expr2,NAME_ATOM);   /* a */
                     pt = pBdd->high;
                     addQExpr(expr2,NAME_ATOM);	/* b */
                     res = createBinExpr(AND,expr2,
                             syf_bdd2Abl(initVertexBdd(pBdd->index,pBdd->high,pt->low),
                                      tabName,optim)); 
   /*
   printf("2 -- ");
   displayExpr(res);
   */
                     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,
                             syf_bdd2Abl(initVertexBdd(pBdd->index,pBdd->high,pt->low),
                                      tabName,optim)); 
   /*
   printf("3 -- ");
   displayExpr(res);
   */
                     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,
                             syf_bdd2Abl(initVertexBdd(pBdd->index,pt->low,pBdd->low),
                                      tabName,optim)); 
   /*
   printf("4 -- ");
   displayExpr(res);
   */
                     addTH(pTabExpr,pBdd,copyExpr(res));
                     return(res);
                     }
			   /*  si HL inclu dans HH
                               a.b.HH(HL = *) + (a + b).HL + a'.b'.LL */
   
                  pt = pBdd->high;
                  if (applyBinBdd(AND,pt->high,pt->low) == pt->low)
                     {
                     expr1 = syf_bdd2Abl(initVertexBdd(pBdd->index,pt->low,pBdd->low),
                                         tabName,optim); 
                     pt= pBdd;
                     expr2 = createExpr(AND);
                     addQExpr(expr2,NAME_ATOM);
                     pt = pBdd->high;
                     addQExpr(expr2,NAME_ATOM);
                     res = createBinExpr(AND,
                                         syf_bdd2Abl(simplifDcOneBdd(pt->high,pt->low),
                                                 tabName,optim),expr2); 
                     res = createBinExpr(OR,expr1,res);
   /*
   printf("choix *3*\n");displayExpr(res);
   */
                     addTH(pTabExpr,pBdd,copyExpr(res));
                     return(res);
                     }
   
			   /*  si LH inclu dans LL
                               a'.b'.LL(HL = *) + (a' + b').HL + a.b.HH */
   
                  pt = pBdd->low;
   
                  if (applyBinBdd(AND,pt->high,pt->low) == pt->high)
                     {
                     expr1 = syf_bdd2Abl(initVertexBdd(pBdd->index,pBdd->high,pt->high),
                                         tabName,optim); 
                     pt= pBdd;
                     expr2 = createExpr(AND);
                     addQExpr(expr2,notExpr(NAME_ATOM));
                     pt = pBdd->low;
                     addQExpr(expr2,notExpr(NAME_ATOM));
                     res = createBinExpr(AND,
                                         syf_bdd2Abl(simplifDcOneBdd(pt->low,pt->high),
                                                 tabName,optim),expr2); 
                     res = createBinExpr(OR,expr1,res);
   /*
   printf("choix *4*\n");displayExpr(res);
   */
                     addTH(pTabExpr,pBdd,copyExpr(res));
                     return(res);
                     }
                  }
               pt = pBdd;
               }

			/* HH = LL */

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

			/* carry de l'additionneur */

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

                  if ((pt->high)->low == one && 
                      (pt->low)->high == zero)
                     {
                     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));
                     expr2 = createBinExpr(AND,expr2,
                                        syf_bdd2Abl(pt->high,tabName,optim));
                     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)
                     {
                     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);
                     expr2 = createBinExpr(AND,expr2,
                                        syf_bdd2Abl(pt->high,tabName,optim));
                     res = createExpr(OR);
                     addQExpr(res,expr1);
                     addQExpr(res,expr2);
                     addTH(pTabExpr,pBdd,copyExpr(res));
                     return(res);
                     }
                  }

               if (RULES_SON)
                  {

			/*  (a' + b)((a + b').LL + a'.b.HL) */

                  if ((pt->high)->low == zero)
                     {
                     expr2 = createExpr(OR);
                     addQExpr(expr2,notExpr(NAME_ATOM));   /* not a */
                     pt = pBdd->low;
                     addQExpr(expr2,NAME_ATOM);	/* b */
                     res = createBinExpr(AND,expr2,
                             syf_bdd2Abl(initVertexBdd(pBdd->index,pt->low,pBdd->low),
                                      tabName,optim)); 
   /*
   printf("5 -- ");
   displayExpr(res);
   */
                     addTH(pTabExpr,pBdd,copyExpr(res));
                     return(res);
                     }
			   /*  (a + b')((a' + b).HL + a.b.HH) */
   
                  if ((pt->low)->high == zero)
                     {
                     expr2 = createExpr(OR);
                     addQExpr(expr2,NAME_ATOM);   		/* a */
                     pt = pBdd->low;
                     addQExpr(expr2,notExpr(NAME_ATOM));	/* not b */
                     res = createBinExpr(AND,expr2,
                             syf_bdd2Abl(initVertexBdd(pBdd->index,pBdd->high,pt->low),
                                      tabName,optim)); 
   /*
   printf("6 -- ");
   displayExpr(res);
   */
                     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,
                            syf_bdd2Abl(initVertexBdd(pBdd->index,pt->low,pBdd->low),
                                      tabName,optim)); 
   /*
   printf("7 -- ");
   displayExpr(res);
   */
                     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,
                            syf_bdd2Abl(initVertexBdd(pBdd->index,pBdd->high,pt->low),
                                      tabName,optim)); 
   /*
   printf("8 -- ");
   displayExpr(res);
   */
                     addTH(pTabExpr,pBdd,copyExpr(res));
                     return(res);
                     }
                  
			   /*  si HH inclu dans HL
                               a.b'.HL(HH = *) + (a + b').HH + a'.b.LH */
   
                  pt = pBdd->high;
                  if (applyBinBdd(AND,pt->high,pt->low) == pt->high)
                     {
                     expr1 = syf_bdd2Abl(initVertexBdd(pBdd->index,pt->high,pBdd->low),
                                         tabName,optim); 
   
                     pt= pBdd;
                     expr2 = createExpr(AND);
                     addQExpr(expr2,NAME_ATOM);	
                     pt = pBdd->high;
                     addQExpr(expr2,notExpr(NAME_ATOM));
                     res = createBinExpr(AND,
                                         syf_bdd2Abl(simplifDcOneBdd(pt->low,pt->high),
                                                 tabName,optim),expr2); 
                     res = createBinExpr(OR,expr1,res);
   /*
   printf("choix *1*\n");displayExpr(res);
   */
                     addTH(pTabExpr,pBdd,copyExpr(res));
                     return(res);
                     }
   
   
             	      /*  si LL inclu dans LH
                          a'.b.LH(HH = *) + (a' + b).HH + a.b'.HL */
   
                  pt = pBdd->low;
                  if (applyBinBdd(AND,pt->high,pt->low) == pt->low)
                     {
                     expr1 = syf_bdd2Abl(initVertexBdd(pBdd->index,pBdd->high,pt->low),
                                         tabName,optim); 
   
                     pt= pBdd;
                     expr2 = createExpr(AND);
                     addQExpr(expr2,notExpr(NAME_ATOM));
                     pt = pBdd->low;
                     addQExpr(expr2,NAME_ATOM);
                     res = createBinExpr(AND,
                                         syf_bdd2Abl(simplifDcOneBdd(pt->high,pt->low),
                                                 tabName,optim),expr2); 
                     res = createBinExpr(OR,expr1,res);
   /*
   printf("choix *2*\n");displayExpr(res);
   */
                     addTH(pTabExpr,pBdd,copyExpr(res));
                     return(res);
                     }
                  }
               pt = pBdd;
               }
   
			   /* HH = LH */
   
            if ((pt->high)->high == (pt->low)->high)
               {
               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,
                                        syf_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,
                                        syf_bdd2Abl(pt->high,tabName,optim));
                     res = createExpr(OR);
                     addQExpr(res,expr1);
                     addQExpr(res,expr2);
                     addTH(pTabExpr,pBdd,copyExpr(res));
                     return(res);
                     }
                  }
   
               if (RULES_SON)
                  {
			   /*  b'.(a'.LL + a.HL) + b.HH  */
                           /* a'.LL + a.HL = constraintBdd(pBdd,b=0) */
                     
                  pt = pt->high;
                  res = syf_mux2Abl(pt->high,constraintBdd(pBdd,notBdd(createNodeTermBdd(pt->index))),NAME_ATOM,tabName,optim);
                  pt = pBdd;
                  addTH(pTabExpr,pBdd,copyExpr(res));
                  return(res);
	          }
               }
   
			   /*  HL = LL */
   
            if ((pt->high)->low == (pt->low)->low) 
	       {
               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),
                                        syf_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),
                                        syf_bdd2Abl(pt->low,tabName,optim));
                     res = createExpr(OR);
                     addQExpr(res,expr1);
                     addQExpr(res,expr2);
                     addTH(pTabExpr,pBdd,copyExpr(res));
                     return(res);
                     }
                  }

               if (RULES_SON)
                  {
			/*  b.(a'.LH + a.HH) + b'.HL  */
                        /* a'.LH + a.HH = constraintBdd(pBdd,b=1) */
                  
                  pt = pt->high;
                  res = syf_mux2Abl(constraintBdd(pBdd,createNodeTermBdd(pt->index)),pt->low,NAME_ATOM,tabName,optim);
                  pt = pBdd;
                  addTH(pTabExpr,pBdd,copyExpr(res));
                  return(res);
                  }
               }
            }
         }
      }

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

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

   addTH(pTabExpr,pt,copyExpr(res));
   return(res);
   }
}
/*------------------------------------------------------------------------------
syf_numberAtomFact  : calcule le nombre de litteraux resultant de l'appel bdd2abl
-------------------------------------------------------
parametres 	 :un pointeur de NODE.
-------------------------------------------------------
return 		 :un int 
------------------------------------------------------------------------------*/
int syf_numberAtomFact(pt)
pNode pt;
{
pNode pBdd;
int cpt;
int syf_syf_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+syf_numberAtomFact(pt->high));

      if (pt->high == one || pt->high == one)	/* F = (or a L) */
         return(1+syf_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 = syf_syf_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 = syf_syf_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 = syf_syf_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 + syf_numberAtomFact((pt->high)->low));
            }
			/*  a'.b' + HL.(a' + b')  */

         if ((pt->high)->high == zero && 
            (pt->low)->low == one)
            {
            return(4 + syf_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 + syf_numberAtomFact((pt->high)->high));
            }
			/*  a'.b + HH.(a' + b)  */

         if ((pt->high)->low == zero && 
            (pt->low)->high == one)
            {
            return(4 + syf_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 + syf_numberAtomFact((pt->high)->high));
            }
			/*  a'.b' + HH.b  */

         if ((pt->high)->low == zero && 
            (pt->low)->low == one)
            {
            return(3 + syf_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 + syf_numberAtomFact((pt->high)->low));
            }
			/*  a'.b + HL.b'  */

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

         }
      }

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

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

/*------------------------------------------------------------------------------
syf_syf_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 syf_syf_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 + syf_numberAtomFact(high));

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


pBdd = applyBinBdd(AND,high,low);

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

		/* H est inclu dans L */

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

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


		/* L est inclu dans H */

if (pBdd == low)

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

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

		/* cas general */

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

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

/*------------------------------------------------------------------------------
syf_profFact  : calcule la profondeur d'un abl. 
-------------------------------------------------------
parametres 	 :un pointeur de NODE.
-------------------------------------------------------
return 		 :un int 
------------------------------------------------------------------------------*/
int syf_profFact(pt,ptHash)
pNode pt;
pTH ptHash;
{
pNode pBdd;
int cpt;
int syf_syf_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)) != VIDETH)
      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 = syf_syf_profFact2(pBdd->high,pt,syf_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 = syf_syf_profFact2(pBdd->low,pt,syf_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 = syf_syf_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 + syf_profFact((pt->high)->low,ptHash));
            }
			/*  a'.b' + HL.(a' + b')  */

         if ((pt->high)->high == zero && 
            (pt->low)->low == one)
            {
            return(2 + syf_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 + syf_profFact((pt->high)->high,ptHash));
            }
			/*  a'.b + HH.(a' + b)  */

         if ((pt->high)->low == zero && 
            (pt->low)->high == one)
            {
            return(2 + syf_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 + syf_profFact((pt->high)->high,ptHash));
            }
			/*  a'.b' + HH.b  */

         if ((pt->high)->low == zero && 
            (pt->low)->low == one)
            {
            return(2 + syf_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 + syf_profFact((pt->high)->low,ptHash));
            }
			/*  a'.b + HL.b'  */

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

         }
      }

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

   cpt = syf_syf_profFact2(pt->high,pt->low,0,ptHash);
   addTH(ptHash,pt,cpt);
   return(cpt);
   }
}
/*------------------------------------------------------------------------------
syf_syf_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 syf_syf_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,syf_profFact(high,ptHash)));

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

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

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


pBdd = applyBinBdd(AND,high,low);

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

		/* H est inclu dans L */

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

   int profHigh = 1 + syf_profFact(high,ptHash);
   int profLow  = 2 + MAX(cpt,syf_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 + syf_profFact(low,ptHash);
   int profHigh  = 2 + MAX(cpt,syf_profFact(simplifDcOneBdd(high,low),ptHash));

   return(MAX(profHigh,profLow));
   }

		/* cas general */

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

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

   return(MAX(profHigh,profLow));

   }
}

/*------------------------------------------------------------------------------
syf_syf_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 syf_syf_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 + syf_numberAtomRedFact(high));

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


pBdd = applyBinBdd(AND,high,low);

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

		/* H est inclu dans L */

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

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


		/* L est inclu dans H */

if (pBdd == low)

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

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

		/* cas general */

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

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

/*------------------------------------------------------------------------------
syf_numberAtomRedFact  : calcule le nombre de litteraux reduits
-------------------------------------------------------
parametres 	 :un pointeur de NODE.
-------------------------------------------------------
return 		 :un int 
------------------------------------------------------------------------------*/
int syf_numberAtomRedFact(pt)
pNode pt;
{
pNode pBdd;
int cpt;

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

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

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

                  /* premiere occurence */

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

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

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

pt->mark = 1;

	/*----------------- 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) */
         {
         cpt = 1+syf_numberAtomRedFact(pt->high);
         markBdd(notBdd(pt),1);
         return(cpt);
         }

      if (pt->high == one || pt->high == zero)	/* F = (or a L) */
         {
         cpt = 1+syf_numberAtomRedFact(pt->low);
         markBdd(notBdd(pt),1);
         return(cpt);
         }
      }
   }
else
   {

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


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

   cpt = syf_syf_numberAtomRedFacto2(pt->high,pt->low,1);
   markBdd(notBdd(pt),1); 
   return(cpt);
   }
}

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

int syf_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 + syf_numberAtomRedFact((pNode) pEl->value);
       }
    pEl++;
    }
markAllBdd(0);
return(numAtomRed);
}
/*------------------------------------------------------------------
  IDENT : syf_profExprFact
  ------------------------------------------------------------------
  FUNCTION : calcule la profondeur d'une expression.
  ------------------------------------------------------------------*/

int syf_profExprFact(expr)
chain_list *expr;
{
if (ATOM(expr))
   return(0);
else
   {
   int max=0,profCar;
   int arity;
   short oper;

   oper = OPER(expr);
   if (oper == NOT)
      return(syf_profExprFact(CADR(expr)));

   arity = lengthExpr(expr);
   while (expr = CDR(expr))
      {
      profCar = syf_profExprFact(CAR(expr));
      if (profCar >max)
         max = profCar;
      }
   if (oper == XOR)
      return(max +2*syf_logsup2(arity));
   else
      return(max +syf_logsup2(arity));
   }
}
/*------------------------------------------------------------------------------
syf_logsup2 		: calcule le log a base 2 d'un int 
------------------------------------------------------
parametres  	: un int 
-------------------------------------------------------
return 		: un int
------------------------------------------------------------------------------*/
int syf_logsup2(val)
int val;
{
int co;
int sup;

if (val < 1)
   {
   printf("warning : syf_logsup2 domain error\n");
   return(0);
   }

sup = 0;
co =  0;
while (val > 1)
   {
   if (val & 1)
      sup = 1;
   co++;
   val = (val >> 1);
   }
return(co + sup);
}
