distr/dddmp/dddmpDdNodeCnf.c

   1 /**CFile**********************************************************************
   2
   3   FileName     [dddmpDdNodeCnf.c]
   4
   5   PackageName  [dddmp]
   6
   7   Synopsis     [Functions to handle BDD node infos and numbering
   8     while storing a CNF formula from a BDD or an array of BDDs]
   9
  10   Description  [Functions to handle BDD node infos and numbering
  11     while storing a CNF formula from a BDD or an array of BDDs.
  12     ]
  13
  14   Author       [Gianpiero Cabodi and Stefano Quer]
  15
  16   Copyright    [
  17     Copyright (c) 2004 by Politecnico di Torino.
  18     All Rights Reserved. This software is for educational purposes only.
  19     Permission is given to academic institutions to use, copy, and modify
  20     this software and its documentation provided that this introductory
  21     message is not removed, that this software and its documentation is
  22     used for the institutions' internal research and educational purposes,
  23     and that no monies are exchanged. No guarantee is expressed or implied
  24     by the distribution of this code.
  25     Send bug-reports and/or questions to:
  26     {gianpiero.cabodi,stefano.quer}@polito.it.
  27     ]
  28
  29 ******************************************************************************/
  30
  31 #include "dddmpInt.h"
  32
  33 /*---------------------------------------------------------------------------*/
  34 /* Stucture declarations                                                     */
  35 /*---------------------------------------------------------------------------*/
  36
  37 /*---------------------------------------------------------------------------*/
  38 /* Type declarations                                                         */
  39 /*---------------------------------------------------------------------------*/
  40
  41 /*---------------------------------------------------------------------------*/
  42 /* Variable declarations                                                     */
  43 /*---------------------------------------------------------------------------*/
  44
  45 #define DDDMP_DEBUG_CNF 0
  46
  47 /*---------------------------------------------------------------------------*/
  48 /* Macro declarations                                                        */
  49 /*---------------------------------------------------------------------------*/
  50
  51 /**AutomaticStart*************************************************************/
  52
  53 /*---------------------------------------------------------------------------*/
  54 /* Static function prototypes                                                */
  55 /*---------------------------------------------------------------------------*/
  56
  57 static int DddmpWriteNodeIndexCnf(DdNode *f, int *cnfIds, int id);
  58 static int DddmpReadNodeIndexCnf(DdNode *f);
  59 static int DddmpClearVisitedCnfRecur(DdNode *f);
  60 static int DddmpVisitedCnf(DdNode *f);
  61 static void DddmpSetVisitedCnf(DdNode *f);
  62 static void DddmpClearVisitedCnf(DdNode *f);
  63 static int NumberNodeRecurCnf(DdNode *f, int *cnfIds, int id);
  64 static void DddmpDdNodesCheckIncomingAndScanPath(DdNode *f, int pathLengthCurrent, int edgeInTh, int pathLengthTh);
  65 static int DddmpDdNodesNumberEdgesRecur(DdNode *f, int *cnfIds, int id);
  66 static int DddmpDdNodesResetCountRecur(DdNode *f);
  67 static int DddmpDdNodesCountEdgesRecur(DdNode *f);
  68 static void RemoveFromUniqueRecurCnf(DdManager *ddMgr, DdNode *f);
  69 static void RestoreInUniqueRecurCnf(DdManager *ddMgr, DdNode *f);
  70 static int DddmpPrintBddAndNextRecur(DdManager *ddMgr, DdNode *f);
  71
  72 /**AutomaticEnd***************************************************************/
  73
  74 /*---------------------------------------------------------------------------*/
  75 /* Definition of exported functions                                          */
  76 /*---------------------------------------------------------------------------*/
  77
  78 /*---------------------------------------------------------------------------*/
  79 /* Definition of internal functions                                          */
  80 /*---------------------------------------------------------------------------*/
  81
  82 /**Function********************************************************************
  83
  84   Synopsis    [Removes nodes from unique table and numbers them]
  85
  86   Description [Node numbering is required to convert pointers to integers.
  87     Since nodes are removed from unique table, no new nodes should
  88     be generated before re-inserting nodes in the unique table
  89     (DddmpUnnumberDdNodesCnf()).
  90     ]
  91
  92   SideEffects [Nodes are temporarily removed from unique table]
  93
  94   SeeAlso     [RemoveFromUniqueRecurCnf(), NumberNodeRecurCnf(),
  95     DddmpUnnumberDdNodesCnf()]
  96
  97 ******************************************************************************/
  98
  99 int
 100 DddmpNumberDdNodesCnf (
 101   DdManager *ddMgr  /*  IN: DD Manager */,
 102   DdNode **f        /*  IN: array of BDDs */,
 103   int rootN         /*  IN: number of BDD roots in the array of BDDs */,
 104   int *cnfIds       /* OUT: CNF identifiers for variables */,
 105   int id            /* OUT: number of Temporary Variables Introduced */
 106   )
 107 {
 108   int i;
 109
 110   for (i=0; i<rootN; i++) {
 111     RemoveFromUniqueRecurCnf (ddMgr, f[i]);
 112   }
 113
 114   for (i=0; i<rootN; i++) {
 115     id = NumberNodeRecurCnf (f[i], cnfIds, id);
 116   }
 117
 118   return (id);
 119 }
 120
 121 /**Function********************************************************************
 122
 123   Synopsis    [Removes nodes from unique table and numbers each node according
 124     to the number of its incoming BDD edges.
 125     ]
 126
 127   Description [Removes nodes from unique table and numbers each node according
 128     to the number of its incoming BDD edges.
 129     ]
 130
 131   SideEffects [Nodes are temporarily removed from unique table]
 132
 133   SeeAlso     [RemoveFromUniqueRecurCnf()]
 134
 135 ******************************************************************************/
 136
 137 int
 138 DddmpDdNodesCountEdgesAndNumber (
 139   DdManager *ddMgr    /*  IN: DD Manager */,
 140   DdNode **f          /*  IN: Array of BDDs */,
 141   int rootN           /*  IN: Number of BDD roots in the array of BDDs */,
 142   int edgeInTh        /*  IN: Max # In-Edges, after a Insert Cut Point */,
 143   int pathLengthTh    /*  IN: Max Path Length (after, Insert a Cut Point) */,
 144   int *cnfIds         /* OUT: CNF identifiers for variables */,
 145   int id              /* OUT: Number of Temporary Variables Introduced */
 146   )
 147 {
 148   int retValue, i;
 149
 150   /*-------------------------- Remove From Unique ---------------------------*/
 151
 152   for (i=0; i<rootN; i++) {
 153     RemoveFromUniqueRecurCnf (ddMgr, f[i]);
 154   }
 155
 156   /*-------------------- Reset Counter and Reset Visited --------------------*/
 157
 158   for (i=0; i<rootN; i++) {
 159     retValue = DddmpDdNodesResetCountRecur (f[i]);
 160   }
 161
 162   /*  Here we must have:
 163    *    cnfIndex = 0
 164    *    visitedFlag = 0
 165    *  FOR ALL nodes
 166    */
 167
 168 #if DDDMP_DEBUG_CNF
 169   fprintf (stdout, "###---> BDDs After Count Reset:\n");
 170   DddmpPrintBddAndNext (ddMgr, f, rootN);
 171 #endif
 172
 173   /*----------------------- Count Incoming Edges ----------------------------*/
 174
 175   for (i=0; i<rootN; i++) {
 176     retValue = DddmpDdNodesCountEdgesRecur (f[i]);
 177   }
 178
 179   /*  Here we must have:
 180    *    cnfIndex = incoming edge count
 181    *    visitedFlag = 0 (AGAIN ... remains untouched)
 182    *  FOR ALL nodes
 183    */
 184
 185 #if DDDMP_DEBUG_CNF
 186   fprintf (stdout, "###---> BDDs After Count Recur:\n");
 187   DddmpPrintBddAndNext (ddMgr, f, rootN);
 188 #endif
 189
 190   /*------------------------- Count Path Length ----------------------------*/
 191
 192   for (i=0; i<rootN; i++) {
 193     DddmpDdNodesCheckIncomingAndScanPath (f[i], 0, edgeInTh,
 194       pathLengthTh);
 195   }
 196
 197   /* Here we must have:
 198    *   cnfIndex = 1 if we want to insert there a cut point
 199    *              0 if we do NOT want to insert there a cut point
 200    *    visitedFlag = 1
 201    *  FOR ALL nodes
 202    */
 203
 204 #if DDDMP_DEBUG_CNF
 205   fprintf (stdout, "###---> BDDs After Check Incoming And Scan Path:\n");
 206   DddmpPrintBddAndNext (ddMgr, f, rootN);
 207 #endif
 208
 209   /*-------------------- Number Nodes and Set Visited -----------------------*/
 210
 211   for (i=0; i<rootN; i++) {
 212     id = DddmpDdNodesNumberEdgesRecur (f[i], cnfIds, id);
 213   }
 214
 215   /*  Here we must have:
 216    *    cnfIndex = CNF auxiliary variable enumeration
 217    *    visitedFlag = 0
 218    *  FOR ALL nodes
 219    */
 220
 221 #if DDDMP_DEBUG_CNF
 222   fprintf (stdout, "###---> BDDs After Count Edges Recur:\n");
 223   DddmpPrintBddAndNext (ddMgr, f, rootN);
 224 #endif
 225
 226   /*---------------------------- Clear Visited ------------------------------*/
 227
 228 #if DDDMP_DEBUG_CNF
 229   for (i=0; i<rootN; i++) {
 230     retValue = DddmpClearVisitedCnfRecur (f[i]);
 231   }
 232
 233 #if DDDMP_DEBUG_CNF
 234   fprintf (stdout, "###---> BDDs After All Numbering Process:\n");
 235   DddmpPrintBddAndNext (ddMgr, f, rootN);
 236 #endif
 237 #endif
 238
 239   return (id);
 240 }
 241
 242 /**Function********************************************************************
 243
 244   Synopsis     [Restores nodes in unique table, loosing numbering]
 245
 246   Description  [Node indexes are no more needed. Nodes are re-linked in the
 247     unique table.
 248     ]
 249
 250   SideEffects  [None]
 251
 252   SeeAlso      [DddmpNumberDdNode()]
 253
 254 ******************************************************************************/
 255
 256 void
 257 DddmpUnnumberDdNodesCnf(
 258   DdManager *ddMgr   /* IN: DD Manager */,
 259   DdNode **f         /* IN: array of BDDs */,
 260   int rootN           /* IN: number of BDD roots in the array of BDDs */
 261   )
 262 {
 263   int i;
 264
 265   for (i=0; i<rootN; i++) {
 266     RestoreInUniqueRecurCnf (ddMgr, f[i]);
 267   }
 268
 269   return;
 270 }
 271
 272 /**Function********************************************************************
 273
 274   Synopsis     [Prints debug information]
 275
 276   Description  [Prints debug information for an array of BDDs on the screen]
 277
 278   SideEffects  [None]
 279
 280   SeeAlso      []
 281
 282 ******************************************************************************/
 283
 284 int
 285 DddmpPrintBddAndNext (
 286   DdManager *ddMgr   /* IN: DD Manager */,
 287   DdNode **f         /* IN: Array of BDDs to be displayed */,
 288   int rootN          /* IN: Number of BDD roots in the array of BDDs */
 289   )
 290 {
 291   int i;
 292
 293   for (i=0; i<rootN; i++) {
 294     fprintf (stdout, "---> Bdd %d:\n", i);
 295     fflush (stdout);
 296     DddmpPrintBddAndNextRecur (ddMgr, f[i]);
 297   }
 298
 299   return (DDDMP_SUCCESS);
 300 }
 301
 302 /**Function********************************************************************
 303
 304   Synopsis     [Write index to node]
 305
 306   Description  [The index of the node is written in the "next" field of
 307     a DdNode struct. LSB is not used (set to 0). It is used as
 308     "visited" flag in DD traversals.
 309     ]
 310
 311   SideEffects  [None]
 312
 313   SeeAlso      [DddmpReadNodeIndexCnf(), DddmpSetVisitedCnf (),
 314     DddmpVisitedCnf ()
 315     ]
 316
 317 ******************************************************************************/
 318
 319 int
 320 DddmpWriteNodeIndexCnfBis (
 321   DdNode *f   /* IN: BDD node */,
 322   int id      /* IN: index to be written */
 323   )
 324 {
 325   if (!Cudd_IsConstant (f)) {
 326     f->next = (struct DdNode *)((ptruint)((id)<<1));
 327   }
 328
 329   return (DDDMP_SUCCESS);
 330 }
 331
 332 /*---------------------------------------------------------------------------*/
 333 /* Definition of static functions                                            */
 334 /*---------------------------------------------------------------------------*/
 335
 336 /**Function********************************************************************
 337
 338   Synopsis     [Write index to node]
 339
 340   Description  [The index of the node is written in the "next" field of
 341     a DdNode struct. LSB is not used (set to 0). It is used as
 342     "visited" flag in DD traversals. The index corresponds to
 343     the BDD node variable if both the node's children are a
 344     constant node, otherwise a new CNF variable is used.
 345     ]
 346
 347   SideEffects  [None]
 348
 349   SeeAlso      [DddmpReadNodeIndexCnf(), DddmpSetVisitedCnf (),
 350     DddmpVisitedCnf ()]
 351
 352 *****************************************************************************/
 353
 354 static int
 355 DddmpWriteNodeIndexCnf (
 356   DdNode *f    /* IN: BDD node */,
 357   int *cnfIds  /* IN: possible source for the index to be written */,
 358   int id       /* IN: possible source for the index to be written */
 359   )
 360 {
 361   if (!Cudd_IsConstant (f)) {
 362     if (Cudd_IsConstant (cuddT (f)) && Cudd_IsConstant (cuddE (f))) {
 363       /* If Variable SET ID as Variable ID */
 364       f->next = (struct DdNode *)((ptruint)((cnfIds[f->index])<<1));
 365     } else {
 366       f->next = (struct DdNode *)((ptruint)((id)<<1));
 367       id++;
 368     }
 369   }
 370
 371   return(id);
 372 }
 373
 374 /**Function********************************************************************
 375
 376   Synopsis     [Reads the index of a node]
 377
 378   Description  [Reads the index of a node. LSB is skipped (used as visited
 379                 flag).
 380                ]
 381
 382   SideEffects  [None]
 383
 384   SeeAlso      [DddmpWriteNodeIndexCnf(), DddmpSetVisitedCnf (),
 385                 DddmpVisitedCnf ()]
 386
 387 ******************************************************************************/
 388
 389 static int
 390 DddmpReadNodeIndexCnf (
 391   DdNode *f     /* IN: BDD node */
 392   )
 393 {
 394   if (!Cudd_IsConstant (f)) {
 395     return ((int)(((ptruint)(f->next))>>1));
 396   } else {
 397     return (1);
 398   }
 399 }
 400
 401 /**Function********************************************************************
 402
 403   Synopsis     [Mark ALL nodes as not visited]
 404
 405   Description  [Mark ALL nodes as not visited (it recurs on the node children)]
 406
 407   SideEffects  [None]
 408
 409   SeeAlso      [DddmpVisitedCnf (), DddmpSetVisitedCnf ()]
 410
 411 ******************************************************************************/
 412
 413 static int
 414 DddmpClearVisitedCnfRecur (
 415   DdNode *f     /* IN: root of the BDD to be marked */
 416   )
 417 {
 418   int retValue;
 419
 420   f = Cudd_Regular(f);
 421
 422   if (cuddIsConstant (f)) {
 423     return (DDDMP_SUCCESS);
 424   }
 425
 426   if (!DddmpVisitedCnf (f)) {
 427     return (DDDMP_SUCCESS);
 428   }
 429
 430   retValue = DddmpClearVisitedCnfRecur (cuddT (f));
 431   retValue = DddmpClearVisitedCnfRecur (cuddE (f));
 432
 433   DddmpClearVisitedCnf (f);
 434
 435   return (DDDMP_SUCCESS);
 436 }
 437
 438 /**Function********************************************************************
 439
 440   Synopsis     [Returns true if node is visited]
 441
 442   Description  [Returns true if node is visited]
 443
 444   SideEffects  [None]
 445
 446   SeeAlso      [DddmpSetVisitedCnf (), DddmpClearVisitedCnf ()]
 447
 448 ******************************************************************************/
 449
 450 static int
 451 DddmpVisitedCnf (
 452   DdNode *f      /* IN: BDD node to be tested */
 453   )
 454 {
 455   f = Cudd_Regular(f);
 456
 457   return ((int)((ptruint)(f->next)) & (01));
 458 }
 459
 460 /**Function********************************************************************
 461
 462   Synopsis     [Marks a node as visited]
 463
 464   Description  [Marks a node as visited]
 465
 466   SideEffects  [None]
 467
 468   SeeAlso      [DddmpVisitedCnf (), DddmpClearVisitedCnf ()]
 469
 470 ******************************************************************************/
 471
 472 static void
 473 DddmpSetVisitedCnf (
 474   DdNode *f     /* IN: BDD node to be marked (as visited) */
 475   )
 476 {
 477   f = Cudd_Regular(f);
 478
 479   f->next = (DdNode *)(ptruint)((int)((ptruint)(f->next))|01);
 480
 481   return;
 482 }
 483
 484 /**Function********************************************************************
 485
 486   Synopsis     [Marks a node as not visited]
 487
 488   Description  [Marks a node as not visited]
 489
 490   SideEffects  [None]
 491
 492   SeeAlso      [DddmpVisitedCnf (), DddmpSetVisitedCnf ()]
 493
 494 ******************************************************************************/
 495
 496 static void
 497 DddmpClearVisitedCnf (
 498   DdNode *f     /* IN: BDD node to be marked (as not visited) */
 499   )
 500 {
 501   f = Cudd_Regular (f);
 502
 503   f->next = (DdNode *)(ptruint)((int)((ptruint)(f->next)) & (~01));
 504
 505   return;
 506 }
 507
 508 /**Function********************************************************************
 509
 510   Synopsis     [Number nodes recursively in post-order]
 511
 512   Description  [Number nodes recursively in post-order.
 513     The "visited" flag is used with inverse polarity, because all nodes
 514     were set "visited" when removing them from unique.
 515     ]
 516
 517   SideEffects  ["visited" flags are reset.]
 518
 519   SeeAlso      []
 520
 521 ******************************************************************************/
 522
 523 static int
 524 NumberNodeRecurCnf(
 525   DdNode *f        /*  IN: root of the BDD to be numbered */,
 526   int *cnfIds      /*  IN: possible source for numbering */,
 527   int id        /* IN/OUT: possible source for numbering */
 528   )
 529 {
 530   f = Cudd_Regular(f);
 531
 532   if (!DddmpVisitedCnf (f)) {
 533     return (id);
 534   }
 535
 536   if (!cuddIsConstant (f)) {
 537     id = NumberNodeRecurCnf (cuddT (f), cnfIds, id);
 538     id = NumberNodeRecurCnf (cuddE (f), cnfIds, id);
 539   }
 540
 541   id = DddmpWriteNodeIndexCnf (f, cnfIds, id);
 542   DddmpClearVisitedCnf (f);
 543
 544   return (id);
 545 }
 546
 547 /**Function********************************************************************
 548
 549   Synopsis     [Number nodes recursively in post-order]
 550
 551   Description  [Number nodes recursively in post-order.
 552     The "visited" flag is used with the right polarity.
 553     The node is assigned to a new CNF variable only if it is a "shared"
 554     node (i.e. the number of its incoming edges is greater than 1).
 555     ]
 556
 557   SideEffects  ["visited" flags are set.]
 558
 559   SeeAlso      []
 560
 561 ******************************************************************************/
 562
 563 static void
 564 DddmpDdNodesCheckIncomingAndScanPath (
 565   DdNode *f             /* IN: BDD node to be numbered */,
 566   int pathLengthCurrent /* IN: Current Path Length */,
 567   int edgeInTh          /* IN: Max # In-Edges, after a Insert Cut Point */,
 568   int pathLengthTh      /* IN: Max Path Length (after, Insert a Cut Point) */
 569   )
 570 {
 571   int retValue;
 572
 573   f = Cudd_Regular(f);
 574
 575   if (DddmpVisitedCnf (f)) {
 576     return;
 577   }
 578
 579   if (cuddIsConstant (f)) {
 580     return;
 581   }
 582
 583   pathLengthCurrent++;
 584   retValue = DddmpReadNodeIndexCnf (f);
 585
 586   if ( ((edgeInTh >= 0) && (retValue > edgeInTh)) ||
 587        ((pathLengthTh >= 0) && (pathLengthCurrent > pathLengthTh))
 588      ) {
 589     DddmpWriteNodeIndexCnfBis (f, 1);
 590     pathLengthCurrent = 0;
 591   } else {
 592     DddmpWriteNodeIndexCnfBis (f, 0);
 593   }
 594
 595   DddmpDdNodesCheckIncomingAndScanPath (cuddT (f), pathLengthCurrent,
 596     edgeInTh, pathLengthTh);
 597   DddmpDdNodesCheckIncomingAndScanPath (cuddE (f), pathLengthCurrent,
 598     edgeInTh, pathLengthTh);
 599
 600   DddmpSetVisitedCnf (f);
 601
 602   return;
 603 }
 604
 605 /**Function********************************************************************
 606
 607   Synopsis     [Number nodes recursively in post-order]
 608
 609   Description  [Number nodes recursively in post-order.
 610     The "visited" flag is used with the inverse polarity.
 611     Numbering follows the subsequent strategy:
 612     * if the index = 0 it remains so
 613     * if the index >= 1 it gets enumerated.
 614       This implies that the node is assigned to a new CNF variable only if
 615       it is not a terminal node otherwise it is assigned the index of
 616       the BDD variable.
 617     ]
 618
 619   SideEffects  ["visited" flags are reset.]
 620
 621   SeeAlso      []
 622
 623 ******************************************************************************/
 624
 625 static int
 626 DddmpDdNodesNumberEdgesRecur (
 627   DdNode *f      /*  IN: BDD node to be numbered */,
 628   int *cnfIds    /*  IN: possible source for numbering */,
 629   int id      /* IN/OUT: possible source for numbering */
 630   )
 631 {
 632   int retValue;
 633
 634   f = Cudd_Regular(f);
 635
 636   if (!DddmpVisitedCnf (f)) {
 637     return (id);
 638   }
 639
 640   if (cuddIsConstant (f)) {
 641     return (id);
 642   }
 643
 644   id = DddmpDdNodesNumberEdgesRecur (cuddT (f), cnfIds, id);
 645   id = DddmpDdNodesNumberEdgesRecur (cuddE (f), cnfIds, id);
 646
 647   retValue = DddmpReadNodeIndexCnf (f);
 648   if (retValue >= 1) {
 649     id = DddmpWriteNodeIndexCnf (f, cnfIds, id);
 650   } else {
 651     DddmpWriteNodeIndexCnfBis (f, 0);
 652   }
 653
 654   DddmpClearVisitedCnf (f);
 655
 656   return (id);
 657 }
 658
 659 /**Function********************************************************************
 660
 661   Synopsis     [Resets counter and visited flag for ALL nodes of a BDD]
 662
 663   Description  [Resets counter and visited flag for ALL nodes of a BDD (it
 664     recurs on the node children). The index field of the node is
 665     used as counter.
 666     ]
 667
 668   SideEffects  []
 669
 670   SeeAlso      []
 671
 672 ******************************************************************************/
 673
 674 static int
 675 DddmpDdNodesResetCountRecur (
 676   DdNode *f  /*  IN: root of the BDD whose counters are reset */
 677   )
 678 {
 679   int retValue;
 680
 681   f = Cudd_Regular (f);
 682
 683   if (!DddmpVisitedCnf (f)) {
 684     return (DDDMP_SUCCESS);
 685   }
 686
 687   if (!cuddIsConstant (f)) {
 688     retValue = DddmpDdNodesResetCountRecur (cuddT (f));
 689     retValue = DddmpDdNodesResetCountRecur (cuddE (f));
 690   }
 691
 692   DddmpWriteNodeIndexCnfBis (f, 0);
 693   DddmpClearVisitedCnf (f);
 694
 695   return (DDDMP_SUCCESS);
 696 }
 697
 698 /**Function********************************************************************
 699
 700   Synopsis     [Counts the number of incoming edges for each node of a BDD]
 701
 702   Description  [Counts (recursively) the number of incoming edges for each
 703     node of a BDD. This number is stored in the index field.
 704     ]
 705
 706   SideEffects  ["visited" flags remain untouched.]
 707
 708   SeeAlso      []
 709
 710 ******************************************************************************/
 711
 712 static int
 713 DddmpDdNodesCountEdgesRecur (
 714   DdNode *f    /* IN: root of the BDD */
 715   )
 716 {
 717   int indexValue, retValue;
 718
 719   f = Cudd_Regular (f);
 720
 721   if (cuddIsConstant (f)) {
 722     return (DDDMP_SUCCESS);
 723   }
 724
 725   if (Cudd_IsConstant (cuddT (f)) && Cudd_IsConstant (cuddE (f))) {
 726     return (DDDMP_SUCCESS);
 727   }
 728
 729   indexValue = DddmpReadNodeIndexCnf (f);
 730
 731   /* IF (first time) THEN recur */
 732   if (indexValue == 0) {
 733     retValue = DddmpDdNodesCountEdgesRecur (cuddT (f));
 734     retValue = DddmpDdNodesCountEdgesRecur (cuddE (f));
 735   }
 736
 737   /* Increment Incoming-Edge Count Flag */
 738   indexValue++;
 739   DddmpWriteNodeIndexCnfBis (f, indexValue);
 740
 741   return (DDDMP_SUCCESS);
 742 }
 743
 744 /**Function********************************************************************
 745
 746   Synopsis    [Removes a node from unique table]
 747
 748   Description [Removes a node from the unique table by locating the proper
 749     subtable and unlinking the node from it. It recurs on son nodes.
 750     ]
 751
 752   SideEffects [Nodes are left with the "visited" flag true.]
 753
 754   SeeAlso     [RestoreInUniqueRecurCnf()]
 755
 756 ******************************************************************************/
 757
 758 static void
 759 RemoveFromUniqueRecurCnf (
 760   DdManager *ddMgr  /*  IN: DD Manager */,
 761   DdNode *f         /*  IN: root of the BDD to be extracted */
 762   )
 763 {
 764   DdNode *node, *last, *next;
 765   DdNode *sentinel = &(ddMgr->sentinel);
 766   DdNodePtr *nodelist;
 767   DdSubtable *subtable;
 768   int pos, level;
 769
 770   f = Cudd_Regular (f);
 771
 772   if (DddmpVisitedCnf (f)) {
 773     return;
 774   }
 775
 776   if (!cuddIsConstant (f)) {
 777
 778     RemoveFromUniqueRecurCnf (ddMgr, cuddT (f));
 779     RemoveFromUniqueRecurCnf (ddMgr, cuddE (f));
 780
 781     level = ddMgr->perm[f->index];
 782     subtable = &(ddMgr->subtables[level]);
 783
 784     nodelist = subtable->nodelist;
 785
 786     pos = ddHash (cuddT (f), cuddE (f), subtable->shift);
 787     node = nodelist[pos];
 788     last = NULL;
 789     while (node != sentinel) {
 790       next = node->next;
 791       if (node == f) {
 792         if (last != NULL)
 793           last->next = next;
 794         else
 795           nodelist[pos] = next;
 796         break;
 797       } else {
 798         last = node;
 799         node = next;
 800       }
 801     }
 802
 803     f->next = NULL;
 804
 805   }
 806
 807   DddmpSetVisitedCnf (f);
 808
 809   return;
 810 }
 811
 812 /**Function********************************************************************
 813
 814   Synopsis     [Restores a node in unique table]
 815
 816   Description  [Restores a node in unique table (recursive)]
 817
 818   SideEffects  [Nodes are not restored in the same order as before removal]
 819
 820   SeeAlso      [RemoveFromUnique()]
 821
 822 ******************************************************************************/
 823
 824 static void
 825 RestoreInUniqueRecurCnf (
 826   DdManager *ddMgr  /*  IN: DD Manager */,
 827   DdNode *f         /*  IN: root of the BDD to be restored */
 828   )
 829 {
 830   DdNodePtr *nodelist;
 831   DdNode *T, *E, *looking;
 832   DdNodePtr *previousP;
 833   DdSubtable *subtable;
 834   int pos, level;
 835 #ifdef DDDMP_DEBUG
 836   DdNode *node;
 837   DdNode *sentinel = &(ddMgr->sentinel);
 838 #endif
 839
 840   f = Cudd_Regular(f);
 841
 842   if (!Cudd_IsComplement (f->next)) {
 843     return;
 844   }
 845
 846   if (cuddIsConstant (f)) {
 847     DddmpClearVisitedCnf (f);
 848     /*f->next = NULL;*/
 849     return;
 850   }
 851
 852   RestoreInUniqueRecurCnf (ddMgr, cuddT (f));
 853   RestoreInUniqueRecurCnf (ddMgr, cuddE (f));
 854
 855   level = ddMgr->perm[f->index];
 856   subtable = &(ddMgr->subtables[level]);
 857
 858   nodelist = subtable->nodelist;
 859
 860   pos = ddHash (cuddT (f), cuddE (f), subtable->shift);
 861
 862 #ifdef DDDMP_DEBUG
 863   /* verify uniqueness to avoid duplicate nodes in unique table */
 864   for (node=nodelist[pos]; node != sentinel; node=node->next)
 865     assert(node!=f);
 866 #endif
 867
 868   T = cuddT (f);
 869   E = cuddE (f);
 870   previousP = &(nodelist[pos]);
 871   looking = *previousP;
 872
 873   while (T < cuddT (looking)) {
 874     previousP = &(looking->next);
 875     looking = *previousP;
 876   }
 877
 878   while (T == cuddT (looking) && E < cuddE (looking)) {
 879     previousP = &(looking->next);
 880     looking = *previousP;
 881   }
 882   f->next = *previousP;
 883   *previousP = f;
 884
 885   return;
 886 }
 887
 888 /**Function********************************************************************
 889
 890   Synopsis     [Prints debug info]
 891
 892   Description  [Prints debug info for a BDD on the screen. It recurs on
 893     node's children.
 894     ]
 895
 896   SideEffects  []
 897
 898   SeeAlso      []
 899
 900 ******************************************************************************/
 901
 902 static int
 903 DddmpPrintBddAndNextRecur (
 904   DdManager *ddMgr   /* IN: DD Manager */,
 905   DdNode *f          /* IN: root of the BDD to be displayed */
 906   )
 907 {
 908   int retValue;
 909   DdNode *fPtr, *tPtr, *ePtr;
 910
 911   fPtr = Cudd_Regular (f);
 912
 913   if (Cudd_IsComplement (f)) {
 914     fprintf (stdout, "sign=- ptr=%ld ", ((long int) fPtr));
 915   } else {
 916     fprintf (stdout, "sign=+ ptr=%ld ", ((long int) fPtr));
 917   }
 918
 919   if (cuddIsConstant (fPtr)) {
 920     fprintf (stdout, "one\n");
 921     fflush (stdout);
 922     return (DDDMP_SUCCESS);
 923   }
 924
 925   fprintf (stdout,
 926     "thenPtr=%ld elsePtr=%ld BddId=%d CnfId=%d Visited=%d\n",
 927     ((long int) cuddT (fPtr)), ((long int) cuddE (fPtr)),
 928     fPtr->index, DddmpReadNodeIndexCnf (fPtr),
 929     DddmpVisitedCnf (fPtr));
 930
 931   tPtr  = cuddT (fPtr);
 932   ePtr = cuddE (fPtr);
 933   if (Cudd_IsComplement (f)) {
 934     tPtr  = Cudd_Not (tPtr);
 935     ePtr = Cudd_Not (ePtr);
 936   }
 937
 938   retValue = DddmpPrintBddAndNextRecur (ddMgr, tPtr);
 939   retValue = DddmpPrintBddAndNextRecur (ddMgr, ePtr);
 940
 941   return (DDDMP_SUCCESS);
 942 }
 943
 944