source: icGREP/icgrep-devel/cudd-2.5.1/dddmp/dddmpDdNodeCnf.c @ 4597

Last change on this file since 4597 was 4597, checked in by nmedfort, 4 years ago

Upload of the CUDD library.

File size: 24.9 KB
Line 
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
57static int DddmpWriteNodeIndexCnf(DdNode *f, int *cnfIds, int id);
58static int DddmpReadNodeIndexCnf(DdNode *f);
59static int DddmpClearVisitedCnfRecur(DdNode *f);
60static int DddmpVisitedCnf(DdNode *f);
61static void DddmpSetVisitedCnf(DdNode *f);
62static void DddmpClearVisitedCnf(DdNode *f);
63static int NumberNodeRecurCnf(DdNode *f, int *cnfIds, int id);
64static void DddmpDdNodesCheckIncomingAndScanPath(DdNode *f, int pathLengthCurrent, int edgeInTh, int pathLengthTh);
65static int DddmpDdNodesNumberEdgesRecur(DdNode *f, int *cnfIds, int id);
66static int DddmpDdNodesResetCountRecur(DdNode *f);
67static int DddmpDdNodesCountEdgesRecur(DdNode *f);
68static void RemoveFromUniqueRecurCnf(DdManager *ddMgr, DdNode *f);
69static void RestoreInUniqueRecurCnf(DdManager *ddMgr, DdNode *f);
70static 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
99int
100DddmpNumberDdNodesCnf (
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
137int
138DddmpDdNodesCountEdgesAndNumber (
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
256void
257DddmpUnnumberDdNodesCnf(
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
284int
285DddmpPrintBddAndNext (
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
319int
320DddmpWriteNodeIndexCnfBis (
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
354static int
355DddmpWriteNodeIndexCnf (
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
389static int
390DddmpReadNodeIndexCnf (
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
413static int
414DddmpClearVisitedCnfRecur (
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
450static int
451DddmpVisitedCnf (
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
472static void
473DddmpSetVisitedCnf (
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
496static void
497DddmpClearVisitedCnf (
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
523static int
524NumberNodeRecurCnf(
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
563static void
564DddmpDdNodesCheckIncomingAndScanPath (
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
625static int
626DddmpDdNodesNumberEdgesRecur (
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
674static int
675DddmpDdNodesResetCountRecur (
676  DdNode */*  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
712static int
713DddmpDdNodesCountEdgesRecur (
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
758static void
759RemoveFromUniqueRecurCnf (
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
824static void
825RestoreInUniqueRecurCnf (
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
902static int
903DddmpPrintBddAndNextRecur (
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
Note: See TracBrowser for help on using the repository browser.