distrib/sources/bdd/log_bdd1.c

   1 /*
   2  * This file is part of the Alliance CAD System
   3  * Copyright (C) Laboratoire LIP6 - Département ASIM
   4  * Universite Pierre et Marie Curie
   5  *
   6  * Home page          : http://www-asim.lip6.fr/alliance/
   7  * E-mail support     : mailto:alliance-support@asim.lip6.fr
   8  *
   9  * This progam is  free software; you can redistribute it  and/or modify it
  10  * under the  terms of the GNU  General Public License as  published by the
  11  * Free Software Foundation;  either version 2 of the License,  or (at your
  12  * option) any later version.
  13  *
  14  * Alliance VLSI  CAD System  is distributed  in the hope  that it  will be
  15  * useful, but WITHOUT  ANY WARRANTY; without even the  implied warranty of
  16  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
  17  * Public License for more details.
  18  *
  19  * You should have received a copy  of the GNU General Public License along
  20  * with the GNU C Library; see the  file COPYING. If not, write to the Free
  21  * Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
  22  */
  23
  24 /*
  25  * Tool    : ABL, BDD, HT Librarie
  26  * Date    : 1991,92
  27  * Author  : Luc Burgun
  28  * Modified by Czo <Olivier.Sirol@lip6.fr> 1996,97
  29  */
  30
  31
  32
  33
  34 #ident "$Id: log_bdd1.c,v 1.18 2008/03/03 14:27:54 gregoire Exp $"
  35
  36
  37 /****************************************************************************/
  38 /*    Produit : librairie BDD - Gestion de BDD                              */
  39 /****************************************************************************/
  40
  41 #include<stdio.h>
  42 #include<stdlib.h>
  43 #include<string.h>
  44 #include<limits.h>
  45 #include MUT_H
  46 #include LOG_H
  47 #include AVT_H
  48
  49 /*------------------------------------------------------------------------------
  50 initializeCct          :cree un circuit .
  51 -------------------------------------------------------
  52 parametres          :nom du circuit, nombre d'entrees et nombre de sorties .
  53 -------------------------------------------------------
  54 return                  :pointeur de circuit.
  55 ------------------------------------------------------------------------------*/
  56 pCircuit
  57 initializeCct (name, nbI, nbO)
  58      char *name;
  59      int nbI, nbO;
  60 {
  61   pCircuit pC;
  62   char **pt;
  63   int i;
  64   /* on assure ... */
  65   nbI++;
  66   nbO++;
  67
  68   pC = (pCircuit) mbkalloc (sizeof (struct circuit));
  69   pC->countI = 2;
  70   pC->pTI = createTH (2 * nbI);
  71   pC->pTO = createTH (2 * nbO);
  72   pC->pNameI = (char **) mbkalloc (sizeof (char *) * 2 * nbI);
  73   pt = pC->pNameI;
  74   for (i = 0; i < 2 * nbI; i++)
  75     {
  76       *pt = NULL;
  77       pt++;
  78     }
  79   pC->name = name;
  80   return (pC);
  81 }
  82 /*------------------------------------------------------------------------------
  83 resetCct          :vide un circuit .
  84 -------------------------------------------------------
  85 parametres          :pointeur de circuit.
  86 -------------------------------------------------------
  87 return                  :rien.
  88 ------------------------------------------------------------------------------*/
  89 void
  90 resetCct (pC)
  91      pCircuit pC;
  92 {
  93   pElemTH pEl;
  94   short i;
  95   char **pt;
  96
  97   pEl = (pC->pTI)->pElem;
  98   for (i = 0; i < (pC->pTI)->length; i++)
  99     {
 100       pEl->value = EMPTYTH;
 101       pEl++;
 102     }
 103   pEl = (pC->pTO)->pElem;
 104   for (i = 0; i < (pC->pTO)->length; i++)
 105     {
 106       pEl->value = EMPTYTH;
 107       pEl++;
 108     }
 109   pt = pC->pNameI;
 110   for (i = 0; i < (pC->pTI)->length; i++)
 111     {
 112       *pt = NULL;
 113       pt++;
 114     }
 115   pC->countI = 2;
 116 }
 117
 118 /*------------------------------------------------------------------------------
 119 destroyCct          :desalloue un circuit .
 120 -------------------------------------------------------
 121 parametres          :pointeur de circuit.
 122 -------------------------------------------------------
 123 return                  :rien.
 124 ------------------------------------------------------------------------------*/
 125 void
 126 destroyCct (pC)
 127      pCircuit pC;
 128 {
 129   destroyTH (pC->pTI);
 130   destroyTH (pC->pTO);
 131   mbkfree (pC->pNameI);
 132   mbkfree (pC);
 133 }
 134 /*------------------------------------------------------------------------------
 135 searchOutputCct         :recherche le GDB associe a une sortie .
 136 -------------------------------------------------------
 137 parametres          :un pointeur sur le circuit, et le nom de la sortie.
 138 -------------------------------------------------------
 139 return                  :pointeur de GDB ou null.
 140 ------------------------------------------------------------------------------*/
 141 pNode
 142 searchOutputCct_no_NA (pC, name)
 143      pCircuit pC;
 144      char *name;
 145 {
 146   long res;
 147 #if TEST_IT
 148   if (name!=namefind(name)) exit(10);
 149 #endif
 150   if ((res = searchTH (pC->pTO, name)) != EMPTYTH)
 151     return ((pNode) res);
 152   else
 153     return (NULL);
 154 }
 155
 156 pNode
 157 searchOutputCct (pC, name)
 158      pCircuit pC;
 159      char *name;
 160 {
 161   return searchOutputCct_no_NA (pC, namealloc (name));
 162 }
 163 /*------------------------------------------------------------------------------
 164 addOutputCct         :ajoute un GDB associe a une sortie .
 165 -------------------------------------------------------
 166 parametres          :un pointeur sur le GDB,un pointeur de circuit, et le nom
 167                   de la sortie.
 168 -------------------------------------------------------
 169 return                  :rien.
 170 ------------------------------------------------------------------------------*/
 171 void
 172 addOutputCct_no_NA (pC, name, pt)
 173      pCircuit pC;
 174      char *name;
 175      pNode pt;
 176 {
 177 #if TEST_IT
 178   if (name!=namefind(name)) exit(10);
 179 #endif
 180   addTH (pC->pTO, name, (long)pt);
 181 }
 182
 183 void
 184 addOutputCct (pC, name, pt)
 185      pCircuit pC;
 186      char *name;
 187      pNode pt;
 188 {
 189   addOutputCct_no_NA (pC, namealloc(name), pt);
 190 }
 191 /*------------------------------------------------------------------------------
 192 searchIndexCct         :recherche entree associe a un index .
 193 -------------------------------------------------------
 194 parametres          :un pointeur sur le circuit, et l'index
 195 -------------------------------------------------------
 196 return                  : NULL ou le pointeur namealloc
 197 ------------------------------------------------------------------------------*/
 198 char *
 199 searchIndexCct (pC, index)
 200      pCircuit pC;
 201      short index;
 202 {
 203   if (index <= pC->countI)
 204     return (*(pC->pNameI + index - 2));
 205   else
 206     return (NULL);
 207 }
 208 /*------------------------------------------------------------------------------
 209 searchInputCct         :recherche index associe a une entree .
 210 -------------------------------------------------------
 211 parametres          :un pointeur sur le circuit, et le nom de l' entree.
 212 -------------------------------------------------------
 213 return                  :index ou EMPTYTH.
 214 ------------------------------------------------------------------------------*/
 215 short
 216 searchInputCct_no_NA (pC, name)
 217      pCircuit pC;
 218      char *name;
 219 {
 220   int reallocTH;
 221   int resul;
 222
 223 #if TEST_IT
 224   if (name!=namefind(name)) exit(10);
 225 #endif
 226   reallocTH = (pC->pTI)->length;
 227   resul = searchTH (pC->pTI, name);
 228
 229   /* on doit reallouer pNameI */
 230
 231   if (reallocTH != (pC->pTI)->length)
 232     {
 233       int i, j;
 234       char **pOldName = pC->pNameI;
 235       char **pOldSave = pC->pNameI;
 236       char **pt;
 237
 238       pC->pNameI = (char **) mbkalloc (sizeof (char *) * (pC->pTI)->length);
 239       pt = pC->pNameI;
 240       for (i = 0; i < reallocTH && *pOldName != NULL; i++)
 241         {
 242           *pt = *pOldName;
 243           pt++;
 244           pOldName++;
 245         }
 246
 247       /* mise a null du reste de la table */
 248
 249       for (j = i; j < (pC->pTI)->length; j++)
 250         {
 251           *pt = NULL;
 252           pt++;
 253         }
 254       mbkfree (pOldSave);
 255     }
 256   return (resul);
 257 }
 258
 259 short
 260 searchInputCct (pC, name)
 261      pCircuit pC;
 262      char *name;
 263 {
 264    return searchInputCct_no_NA (pC, namealloc(name));
 265 }
 266 /*------------------------------------------------------------------------------
 267 addInputCct         :ajoute une entree dans la table des var_index.
 268 -------------------------------------------------------
 269 parametres          :un pointeur de circuit, et le nom de la variable
 270 -------------------------------------------------------
 271 return                  :index.
 272 ------------------------------------------------------------------------------*/
 273 short
 274 addInputCct_no_NA (pC, name)
 275      pCircuit pC;
 276      char *name;
 277 {
 278   short index;
 279   char **ptName;
 280
 281 #if TEST_IT
 282   if (name!=namefind(name)) exit(10);
 283 #endif
 284   if ((index = searchInputCct_no_NA (pC, name)) != EMPTYTH)
 285     {
 286       createNodeTermBdd (index);
 287       return (index);
 288     }
 289   else
 290     {
 291       int reallocTH;
 292
 293       index = pC->countI;
 294       reallocTH = (pC->pTI)->length;
 295       addTH (pC->pTI, name, index);
 296
 297       /* on doit reallouer pNameI */
 298
 299       if (reallocTH != (pC->pTI)->length)
 300         {
 301           int i, j;
 302           char **pOldName = pC->pNameI;
 303           char **pOldSave = pC->pNameI;
 304           char **pt;
 305
 306           pC->pNameI = (char **) mbkalloc (sizeof (char *) * (pC->pTI)->length);
 307           pt = pC->pNameI;
 308           for (i = 0; i < (pC->pTI)->length && *pOldName != NULL; i++)
 309             {
 310               *pt = *pOldName;
 311               pt++;
 312               pOldName++;
 313             }
 314
 315           /* mise a null du reste de la table */
 316
 317           for (j = i; j < (pC->pTI)->length; j++)
 318             {
 319               *pt = NULL;
 320               pt++;
 321             }
 322           mbkfree (pOldSave);
 323         }
 324       ptName = pC->pNameI + pC->countI - 2;        /* ajout du nom d'INPUT */
 325       *ptName = name;
 326       if (pC->countI == SHRT_MAX) {
 327         avt_errmsg(LOG_ERRMSG,"001",AVT_FATAL);
 328 //          fprintf(stderr, "[LOG ERR] Maximum number of variables for BDDs reached\n");
 329 //          EXIT(1);
 330       }
 331       pC->countI++;
 332       createNodeTermBdd (index);
 333       return (index);
 334     }
 335 }
 336
 337 short
 338 addInputCct (pC, name)
 339      pCircuit pC;
 340      char *name;
 341 {
 342   return addInputCct_no_NA (pC, namealloc(name));
 343 }
 344 /*------------------------------------------------------------------------------
 345 delInputCct         :detruit une entree dans la table des var_index.
 346 -------------------------------------------------------
 347 parametres          :un pointeur de circuit, et le nom de la variable
 348 -------------------------------------------------------
 349 return                  : void.
 350 ------------------------------------------------------------------------------*/
 351 void
 352 delInputCct (pC, name)
 353      pCircuit pC;
 354      char *name;
 355 {
 356   deleteTH (pC->pTI, name);
 357 }
 358
 359 /*------------------------------------------------------------------------------
 360 displayCct         :visualise le circuit .
 361 -------------------------------------------------------
 362 parametres          :un pointeur de circuit.
 363 -------------------------------------------------------
 364 return                  :rien.
 365 ------------------------------------------------------------------------------*/
 366 void
 367 displayCct (pCircuit pC, int mode)
 368 {
 369   pElemTH pEl;
 370   int i, cpt = 0;
 371   chain_list *tempabl;
 372
 373   pEl = (pC->pTI)->pElem;
 374   printf("\n");
 375   printf("******* DISPLAY %s *******\n", pC->name);
 376   for (i = 0; i < (pC->pTI)->length; i++)
 377     {
 378       if (pEl->value != EMPTYTH && pEl->value != DELETETH)
 379         printf("INPUT = %s        INDEX = %ld\n",(char*) pEl->key, pEl->value);
 380       pEl++;
 381     }
 382   printf("\n");
 383   printf("-------------  NUMBER OF INPUTS : %d\n\n", (pC->countI) - 2);
 384   pEl = (pC->pTO)->pElem;
 385   for (i = 0; i < (pC->pTO)->length; i++)
 386     {
 387       if (pEl->value != EMPTYTH && pEl->value != DELETETH)
 388         markBdd ((pNode)pEl->value, 0);
 389       pEl++;
 390     }
 391   pEl = (pC->pTO)->pElem;
 392   for (i = 0; i < (pC->pTO)->length; i++)
 393     {
 394       if (pEl->value != EMPTYTH && pEl->value != DELETETH)
 395         {
 396           cpt++;
 397           printf("OUTPUT = %s",(char*) pEl->key);
 398           if (mode == 0)
 399             {
 400               printf("        BDD = %ld\n", pEl->value);
 401               displayBddName (TRUE, (pNode)pEl->value, pC->pNameI);
 402             }
 403           else
 404             {
 405               printf("\n");
 406               printf("%s = ",(char*) pEl->key);
 407               displayExpr (tempabl=bddToAbl ((pNode)pEl->value, pC->pNameI));
 408               freeExpr(tempabl);
 409             }
 410           printf("\n");
 411         }
 412       pEl++;
 413     }
 414   pEl = (pC->pTO)->pElem;
 415   for (i = 0; i < (pC->pTO)->length; i++)
 416     {
 417       if (pEl->value != EMPTYTH && pEl->value != DELETETH)
 418         markBdd ((pNode)pEl->value, 0);
 419       pEl++;
 420     }
 421   printf("-------------  NUMBER OF OUTPUTS : %d\n", cpt);
 422   printf("**************************************\n\n");
 423 }
 424
 425 void
 426 displayCctLog (int lib, int loglevel, pCircuit pC, int mode)
 427 {
 428   pElemTH pEl;
 429   int i, cpt = 0;
 430   chain_list *tempabl;
 431
 432   pEl = (pC->pTI)->pElem;
 433   avt_log(lib,loglevel,"\n");
 434   avt_log(lib,loglevel,"******* DISPLAY %s *******\n", pC->name);
 435   for (i = 0; i < (pC->pTI)->length; i++)
 436     {
 437       if (pEl->value != EMPTYTH && pEl->value != DELETETH)
 438         avt_log(lib,loglevel,"INPUT = %s        INDEX = %ld\n",(char*) pEl->key, pEl->value);
 439       pEl++;
 440     }
 441   avt_log(lib,loglevel,"\n");
 442   avt_log(lib,loglevel,"-------------  NUMBER OF INPUTS : %d\n\n", (pC->countI) - 2);
 443   pEl = (pC->pTO)->pElem;
 444   for (i = 0; i < (pC->pTO)->length; i++)
 445     {
 446       if (pEl->value != EMPTYTH && pEl->value != DELETETH)
 447         markBdd ((pNode)pEl->value, 0);
 448       pEl++;
 449     }
 450   pEl = (pC->pTO)->pElem;
 451   for (i = 0; i < (pC->pTO)->length; i++)
 452     {
 453       if (pEl->value != EMPTYTH && pEl->value != DELETETH)
 454         {
 455           cpt++;
 456           avt_log(lib,loglevel,"OUTPUT = %s",(char*) pEl->key);
 457           if (mode == 0)
 458             {
 459               avt_log(lib,loglevel,"        BDD = %ld\n", pEl->value);
 460               displayBddNameLog (lib, loglevel, TRUE, (pNode)pEl->value, pC->pNameI);
 461             }
 462           else
 463             {
 464               avt_log(lib,loglevel,"\n");
 465               avt_log(lib,loglevel,"%s = ",(char*) pEl->key);
 466               displayExprLog(lib, loglevel, tempabl=bddToAbl ((pNode)pEl->value, pC->pNameI));
 467               freeExpr(tempabl);
 468             }
 469           avt_log(lib,loglevel,"\n");
 470         }
 471       pEl++;
 472     }
 473   pEl = (pC->pTO)->pElem;
 474   for (i = 0; i < (pC->pTO)->length; i++)
 475     {
 476       if (pEl->value != EMPTYTH && pEl->value != DELETETH)
 477         markBdd ((pNode)pEl->value, 0);
 478       pEl++;
 479     }
 480   avt_log(lib,2,"-------------  NUMBER OF OUTPUTS : %d\n", cpt);
 481   avt_log(lib,2,"**************************************\n\n");
 482 }
 483
 484 /*------------------------------------------------------------------------------
 485 composeCct         :compose tous les GDB de pC en expansant l'entree name .
 486 -------------------------------------------------------
 487 parametres          :un pointeur de circuit,nom d'entree,le GDB associe.
 488 -------------------------------------------------------
 489 return                  :rien .
 490 ------------------------------------------------------------------------------*/
 491 void
 492 composeCct (pC, name, pt)
 493      pCircuit pC;
 494      char *name;
 495      pNode pt;
 496 {
 497   int i;
 498   short index;
 499   pElemTH pEl;
 500
 501   pEl = (pC->pTO)->pElem;        /* pointeur courant de la table pTI */
 502   index = searchInputCct (pC, name);
 503   if (index == EMPTYTH)
 504     {
 505       avt_errmsg(LOG_ERRMSG,"000",AVT_FATAL,"178");
 506 //      printf ("bdd1-composeCct : la variable a expanser n'est pas une entree\n");
 507 //      EXIT (-1);
 508     }
 509   for (i = 0; i < (pC->pTO)->length; i++)
 510     {
 511       if (pEl->value != EMPTYTH && pEl->value != DELETETH)
 512         pEl->value = (long) composeBdd ((pNode)pEl->value, pt, index);
 513       pEl++;
 514     }
 515   deleteTH (pC->pTI, name);        /* on elimine name des INPUT */
 516 }
 517
 518 /*------------------------------------------------------------------------------
 519 constraintCct         :contraint tous les GDB de pC avec le GDB pointe par pt .
 520 -------------------------------------------------------
 521 parametres          :un pointeur de circuit,le GDB .
 522 -------------------------------------------------------
 523 return                  :rien .
 524 ------------------------------------------------------------------------------*/
 525 void
 526 constraintCct (pC, pt)
 527      pCircuit pC;
 528      pNode pt;
 529 {
 530   int i;
 531   pElemTH pEl;
 532
 533   pEl = (pC->pTO)->pElem;        /* pointeur courant de la table pTO */
 534   for (i = 0; i < (pC->pTO)->length; i++)
 535     {
 536       if (pEl->value != EMPTYTH && pEl->value != DELETETH)
 537         pEl->value = (long) constraintBdd ((pNode)pEl->value, pt);
 538       pEl++;
 539     }
 540 }
 541 /*------------------------------------------------------------------------------
 542 proofCct         :preuve formelle de circuits .
 543 -------------------------------------------------------
 544 parametres          :deux pointeurs de circuits .
 545 -------------------------------------------------------
 546 return                  :rien .
 547 ------------------------------------------------------------------------------*/
 548 void
 549 proofCct (pC1, pC2)
 550      pCircuit pC1, pC2;
 551 {
 552   pElemTH pEl;
 553   pNode noeudCC2;
 554   int i;
 555   short indexCC2;
 556   chain_list *expr;
 557
 558   printf("\n\n*******  PROOF between %s & %s *******\n", pC1->name, pC2->name);
 559   pEl = (pC1->pTI)->pElem;        /* pointeur courant de la table pTI */
 560   for (i = 0; i < (pC1->pTI)->length; i++)
 561     {
 562       if (pEl->value != EMPTYTH && pEl->value != DELETETH)
 563         {
 564           /* recherche dans CC2 */
 565
 566           indexCC2 = searchTH (pC2->pTI, pEl->key);
 567
 568
 569           if (pEl->value != indexCC2)
 570             {
 571               printf("INDEX (%s) differents pour les deux circuits\n",(char*) pEl->key);
 572               printf("**********  END OF PROOF **********\n\n");
 573               break;
 574             }
 575         }
 576     }
 577
 578   pEl = (pC1->pTO)->pElem;        /* pointeur courant de la table CC1 */
 579
 580   for (i = 0; i < (pC1->pTO)->length; i++)
 581     {
 582       if (pEl->value != EMPTYTH && pEl->value != DELETETH)
 583         {
 584           /* recherche dans CC2 */
 585
 586           noeudCC2 = (pNode) searchTH (pC2->pTO, pEl->key);
 587
 588
 589           if (noeudCC2 != (pNode) EMPTYTH)
 590             {
 591               printf("OUTPUT %s ",(char*) pEl->key);
 592               if (noeudCC2 == (pNode) pEl->value)
 593                     printf("is equal\n");
 594               else
 595                 {
 596                   printf("is different\n");
 597                   printf("%s = ",(char*) pEl->key);
 598                   expr = bddToAbl ((pNode) pEl->value, pC1->pNameI);
 599                   if (numberAtomExpr (expr) < 50)
 600                     displayExpr (expr);
 601                   else
 602                     printf("too small...");
 603                   printf("\n");
 604                   printf("%s = ",(char*) pEl->key);
 605                   expr = bddToAbl (noeudCC2, pC2->pNameI);
 606                   if (numberAtomExpr (expr) < 50)
 607                     displayExpr (expr);
 608                   else
 609                     printf("too small...");
 610                   printf("\n");
 611                 }
 612             }
 613         }
 614       pEl++;
 615     }
 616   printf("**********  END OF PROOF **********\n\n");
 617 }
 618
 619 /*------------------------------------------------------------------------------
 620 ablToBddCct         :traduit la forme prefixee ABL en un GDB .
 621 -------------------------------------------------------
 622 parametres          : un circuit et un pointeur d'ABL .
 623 -------------------------------------------------------
 624 return                  :GDB .
 625 ------------------------------------------------------------------------------*/
 626 pNode
 627 ablToBddCct (pC, expr)
 628      pCircuit pC;
 629      chain_list *expr;
 630 {
 631   short oper;
 632   pNode pt;
 633   chain_list *lstGdb;
 634
 635   if (ATOM (expr))
 636     {
 637       if ((pt = searchOutputCct_no_NA (pC, VALUE_ATOM (expr))) != NULL)
 638         return (pt);
 639       else
 640         {
 641           if (!strcmp (VALUE_ATOM (expr), "'0'"))
 642             return (BDD_zero);
 643           if (!strcmp (VALUE_ATOM (expr), "'d'"))
 644             return (BDD_zero);
 645           if (!strcmp (VALUE_ATOM (expr), "'1'"))
 646             return (BDD_one);
 647           pt = createNodeTermBdd (addInputCct_no_NA (pC, VALUE_ATOM (expr)));
 648           return (pt);
 649         }
 650     }
 651   else
 652     {
 653       oper = OPER (expr);
 654       lstGdb = NULL;
 655       while ((expr = CDR (expr)))
 656         lstGdb = addListBdd (lstGdb, ablToBddCct (pC, CAR (expr)));
 657       pt = applyBdd (oper, lstGdb);
 658       freechain (lstGdb);
 659       return (pt);
 660     }
 661 }
 662 /*------------------------------------------------------------------------------
 663 cpOrderCct         :copie la table des index de CC1 dans CC2 .
 664 -------------------------------------------------------
 665 parametres          :deux pointeurs de circuits.
 666                   de la sortie.
 667 -------------------------------------------------------
 668 return                  :rien.
 669 ------------------------------------------------------------------------------*/
 670 void
 671 cpOrderCct (CC1, CC2)
 672      pCircuit CC1, CC2;
 673 {
 674   int i;
 675   pElemTH pEl1;
 676   pElemTH pEl2;
 677   char **pt1, **pt2;
 678   pTH tab;
 679
 680   if (CC2->pTI->length != CC1->pTI->length)
 681     {
 682       tab = createTH ((CC1->pTI->length));
 683       destroyTH (CC2->pTI);
 684       CC2->pTI = tab;
 685     }
 686   pEl1 = (CC1->pTI)->pElem;
 687   pEl2 = (CC2->pTI)->pElem;
 688   for (i = 0; i < (CC1->pTI)->length; i++)
 689     {
 690       pEl2->value = pEl1->value;
 691       pEl2->key = pEl1->key;
 692       pEl1++;
 693       pEl2++;
 694     }
 695   CC2->pTI->count = CC1->pTI->count;
 696   CC2->countI = CC1->countI;
 697   pt1 = CC1->pNameI;
 698   pt2 = CC2->pNameI;
 699   for (i = 0; i < CC1->countI; i++)
 700     {
 701       *pt2 = *pt1;
 702       pt1++;
 703       pt2++;
 704     }
 705 }
 706
 707 /*-------------------------------------------------------------------------
 708 upVarCct         : remontee d'une variable dans un circuit
 709 ---------------------------------------------------------------------------
 710 retour                : un void.
 711 ---------------------------------------------------------------------------*/
 712
 713 void
 714 upVarCct (pC, ptOldIndex, newIndex)
 715      pCircuit pC;
 716      pNode ptOldIndex;
 717      short newIndex;
 718 {
 719   int i;
 720   pElemTH pEl;
 721
 722   pEl = (pC->pTO)->pElem;
 723   for (i = 0; i < (pC->pTO)->length; i++)
 724     {
 725       if (pEl->value != EMPTYTH && pEl->value != DELETETH)
 726         pEl->value = (long) upVarBdd ((pNode)pEl->value, ptOldIndex, newIndex);
 727       pEl++;
 728     }
 729   deleteTH (pC->pTI, *(pC->pNameI + newIndex - 2));
 730   *(pC->pNameI + newIndex - 2) = *(pC->pNameI + ptOldIndex->index - 2);
 731   addTH (pC->pTI, *(pC->pNameI + ptOldIndex->index - 2), newIndex);
 732 }
 733
 734 /*-------------------------------------------------------------------------
 735 numberNodeCct         : calcule le nombre de noeud d'un circuit
 736 ---------------------------------------------------------------------------
 737 retour                : un entier.
 738 ---------------------------------------------------------------------------*/
 739
 740 int
 741 numberNodeCct (pC)
 742      pCircuit pC;
 743 {
 744   pElemTH pEl;
 745   int i, number_node;
 746
 747   number_node = 0;
 748   markAllBdd (0);
 749   pEl = (pC->pTO)->pElem;
 750   for (i = 0; i < (pC->pTO)->length; i++)
 751     {
 752       if (pEl->value != EMPTYTH && pEl->value != DELETETH)
 753         {
 754           number_node = number_node + countNode ((pNode) pEl->value);
 755         }
 756       pEl++;
 757     }
 758   markAllBdd (0);
 759   return (number_node);
 760 }
 761
 762 /*-------------------------------------------------------------------------
 763 numberNodeTdgCct : calcule le nombre de noeud equivalent TDG d'un circuit
 764 ---------------------------------------------------------------------------
 765 retour                    : un entier.
 766 ---------------------------------------------------------------------------*/
 767
 768 int
 769 numberNodeTdgCct (pC)
 770      pCircuit pC;
 771 {
 772   pElemTH pEl;
 773   int i, number_node;
 774
 775   number_node = 0;
 776   markAllBdd (0);
 777   pEl = (pC->pTO)->pElem;
 778   for (i = 0; i < (pC->pTO)->length; i++)
 779     {
 780       if (pEl->value != EMPTYTH && pEl->value != DELETETH)
 781         {
 782           number_node = number_node + countNodeTdg ((pNode) pEl->value);
 783         }
 784       pEl++;
 785     }
 786   markAllBdd (0);
 787   return (number_node);
 788 }
 789
 790 /*------------------------------------------------------------------------------
 791 bddToAblCct      :traduit un BDD en ABL d'une maniere simplifie.
 792 -------------------------------------------------------
 793 parametres          :un pointeur de NODE.
 794 -------------------------------------------------------
 795 return                  :une pointeur de CHAIN_LIST.
 796 ------------------------------------------------------------------------------*/
 797 chain_list *
 798 bddToAblCct (pC, pBdd)
 799      pCircuit pC;
 800      pNode pBdd;
 801 {
 802   return (bddToAbl (pBdd, pC->pNameI));
 803 }
 804
 805 /*------------------------------------------------------------------------------
 806 gcNodeCct         :effectue un garbage collecteur sur tous les noeuds de systeme
 807                   en sauvegardant les noeuds pointes par les pNode(s) du circuit.
 808 -------------------------------------------------------
 809 parametres          : pointeur de chain_list.
 810 -------------------------------------------------------
 811 return                  : 1 si ok ;
 812                    0 si erreur .
 813 ------------------------------------------------------------------------------*/
 814 void
 815 gcNodeCct (pC)
 816      pCircuit pC;
 817 {
 818   struct systemBdd sysBddAux;
 819   pNode zeroAux, oneAux;
 820   pTH pTHNode;
 821   pElemTH pEl;
 822   int j;
 823
 824   pTHNode = createTH (MEDIUM);
 825   sysBddAux.pRT = createTableBdd (MEDIUM);
 826   sysBddAux.pMC = createTabLoc (MEDIUM);
 827   sysBddAux.indiceAT = MAX_PACK;
 828   sysBddAux.lpAT = NULL;
 829   zeroAux = initVertexBddAux (0, (pNode) 0, (pNode) 1, &sysBddAux);
 830   oneAux = initVertexBddAux (1, (pNode) 0, (pNode) 1, &sysBddAux);
 831   addTH (pTHNode, (char *)BDD_zero, (long) zeroAux);
 832   addTH (pTHNode, (char *)BDD_one, (long) oneAux);
 833
 834
 835   /* on regenere les graphes */
 836
 837   pEl = (pC->pTO)->pElem;
 838   for (j = 0; j < (pC->pTO)->length; j++)
 839     {
 840       if (pEl->value != EMPTYTH && pEl->value != DELETETH)
 841         pEl->value = (long) regenereBdd ((pNode) pEl->value, &sysBddAux, pTHNode);
 842       pEl++;
 843     }
 844
 845   destroyBdd (1);
 846   destroyTH (pTHNode);
 847   sysBdd.pRT = sysBddAux.pRT;
 848   sysBdd.pMC = sysBddAux.pMC;
 849   sysBdd.indiceAT = sysBddAux.indiceAT;
 850   sysBdd.lpAT = sysBddAux.lpAT;
 851   sysBdd.pAT = sysBddAux.pAT;
 852   BDD_zero = zeroAux;
 853   BDD_one = oneAux;
 854 }
 855
 856 chain_list *supportChain_listBddExpr(pCircuit circuit, pNode bdd)
 857 {
 858   chain_list *cl, *ch=NULL, *abl;
 859   char *var;
 860   if (bdd!=BDD_zero && bdd!=BDD_one)
 861     {
 862       cl=supportIndexBdd(bdd, 0);
 863       while (cl!=NULL)
 864         {
 865           var=searchIndexCct(circuit, (short)(long)cl->DATA);
 866           ch=addchain(ch, var);
 867           cl=delchain(cl,cl);
 868         }
 869     }
 870   return ch;
 871 }
 872