distr/dddmp/dddmpNodeCnf.c

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