source: icGREP/icgrep-devel/cudd-2.5.1/dddmp/dddmpNodeCnf.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.6 KB
Line 
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
57static int DddmpWriteNodeIndexCnfWithTerminalCheck(DdNode *f, int *cnfIds, int id);
58static int DddmpClearVisitedCnfRecur(DdNode *f);
59static void DddmpClearVisitedCnf(DdNode *f);
60static int NumberNodeRecurCnf(DdNode *f, int *cnfIds, int id);
61static void DddmpDdNodesCheckIncomingAndScanPath(DdNode *f, int pathLengthCurrent, int edgeInTh, int pathLengthTh);
62static int DddmpDdNodesNumberEdgesRecur(DdNode *f, int *cnfIds, int id);
63static int DddmpDdNodesResetCountRecur(DdNode *f);
64static int DddmpDdNodesCountEdgesRecur(DdNode *f);
65static void RemoveFromUniqueRecurCnf(DdManager *ddMgr, DdNode *f);
66static void RestoreInUniqueRecurCnf(DdManager *ddMgr, DdNode *f);
67static 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
96int
97DddmpNumberDdNodesCnf (
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
134int
135DddmpDdNodesCountEdgesAndNumber (
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
240void
241DddmpUnnumberDdNodesCnf(
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
268int
269DddmpPrintBddAndNext (
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
303int
304DddmpWriteNodeIndexCnf (
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
328int
329DddmpVisitedCnf (
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
350void
351DddmpSetVisitedCnf (
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
377int
378DddmpReadNodeIndexCnf (
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
411static int
412DddmpWriteNodeIndexCnfWithTerminalCheck (
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
443static int
444DddmpClearVisitedCnfRecur (
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
480static void
481DddmpClearVisitedCnf (
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
507static int
508NumberNodeRecurCnf(
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
547static void
548DddmpDdNodesCheckIncomingAndScanPath (
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
609static int
610DddmpDdNodesNumberEdgesRecur (
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
658static int
659DddmpDdNodesResetCountRecur (
660  DdNode */*  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
696static int
697DddmpDdNodesCountEdgesRecur (
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
743static void
744RemoveFromUniqueRecurCnf (
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
809static void
810RestoreInUniqueRecurCnf (
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
890static int
891DddmpPrintBddAndNextRecur (
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
Note: See TracBrowser for help on using the repository browser.