source: vis_dev/glu-2.3/src/cuBdd/cuddZddUtil.c @ 100

Last change on this file since 100 was 13, checked in by cecile, 13 years ago

library glu 2.3

File size: 30.1 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddZddUtil.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Utility functions for ZDDs.]
8
9  Description [External procedures included in this module:
10                    <ul>
11                    <li> Cudd_zddPrintMinterm()
12                    <li> Cudd_zddPrintCover()
13                    <li> Cudd_zddPrintDebug()
14                    <li> Cudd_zddFirstPath()
15                    <li> Cudd_zddNextPath()
16                    <li> Cudd_zddCoverPathToString()
17                    <li> Cudd_zddDumpDot()
18                    </ul>
19               Internal procedures included in this module:
20                    <ul>
21                    <li> cuddZddP()
22                    </ul>
23               Static procedures included in this module:
24                    <ul>
25                    <li> zp2()
26                    <li> zdd_print_minterm_aux()
27                    <li> zddPrintCoverAux()
28                    </ul>
29              ]
30
31  SeeAlso     []
32
33  Author      [Hyong-Kyoon Shin, In-Ho Moon, Fabio Somenzi]
34
35  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
36
37  All rights reserved.
38
39  Redistribution and use in source and binary forms, with or without
40  modification, are permitted provided that the following conditions
41  are met:
42
43  Redistributions of source code must retain the above copyright
44  notice, this list of conditions and the following disclaimer.
45
46  Redistributions in binary form must reproduce the above copyright
47  notice, this list of conditions and the following disclaimer in the
48  documentation and/or other materials provided with the distribution.
49
50  Neither the name of the University of Colorado nor the names of its
51  contributors may be used to endorse or promote products derived from
52  this software without specific prior written permission.
53
54  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
55  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
56  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
57  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
58  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
59  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
60  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
61  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
62  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
63  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
64  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
65  POSSIBILITY OF SUCH DAMAGE.]
66
67******************************************************************************/
68
69#include "util.h"
70#include "cuddInt.h"
71
72/*---------------------------------------------------------------------------*/
73/* Constant declarations                                                     */
74/*---------------------------------------------------------------------------*/
75
76
77/*---------------------------------------------------------------------------*/
78/* Stucture declarations                                                     */
79/*---------------------------------------------------------------------------*/
80
81
82/*---------------------------------------------------------------------------*/
83/* Type declarations                                                         */
84/*---------------------------------------------------------------------------*/
85
86
87/*---------------------------------------------------------------------------*/
88/* Variable declarations                                                     */
89/*---------------------------------------------------------------------------*/
90
91#ifndef lint
92static char rcsid[] DD_UNUSED = "$Id: cuddZddUtil.c,v 1.27 2009/03/08 02:49:02 fabio Exp $";
93#endif
94
95/*---------------------------------------------------------------------------*/
96/* Macro declarations                                                        */
97/*---------------------------------------------------------------------------*/
98
99
100/**AutomaticStart*************************************************************/
101
102/*---------------------------------------------------------------------------*/
103/* Static function prototypes                                                */
104/*---------------------------------------------------------------------------*/
105
106static int zp2 (DdManager *zdd, DdNode *f, st_table *t);
107static void zdd_print_minterm_aux (DdManager *zdd, DdNode *node, int level, int *list);
108static void zddPrintCoverAux (DdManager *zdd, DdNode *node, int level, int *list);
109
110/**AutomaticEnd***************************************************************/
111
112
113/*---------------------------------------------------------------------------*/
114/* Definition of exported functions                                          */
115/*---------------------------------------------------------------------------*/
116
117
118/**Function********************************************************************
119
120  Synopsis    [Prints a disjoint sum of product form for a ZDD.]
121
122  Description [Prints a disjoint sum of product form for a ZDD. Returns 1
123  if successful; 0 otherwise.]
124
125  SideEffects [None]
126
127  SeeAlso     [Cudd_zddPrintDebug Cudd_zddPrintCover]
128
129******************************************************************************/
130int
131Cudd_zddPrintMinterm(
132  DdManager * zdd,
133  DdNode * node)
134{
135    int         i, size;
136    int         *list;
137
138    size = (int)zdd->sizeZ;
139    list = ALLOC(int, size);
140    if (list == NULL) {
141        zdd->errorCode = CUDD_MEMORY_OUT;
142        return(0);
143    }
144    for (i = 0; i < size; i++) list[i] = 3; /* bogus value should disappear */
145    zdd_print_minterm_aux(zdd, node, 0, list);
146    FREE(list);
147    return(1);
148
149} /* end of Cudd_zddPrintMinterm */
150
151
152/**Function********************************************************************
153
154  Synopsis    [Prints a sum of products from a ZDD representing a cover.]
155
156  Description [Prints a sum of products from a ZDD representing a cover.
157  Returns 1 if successful; 0 otherwise.]
158
159  SideEffects [None]
160
161  SeeAlso     [Cudd_zddPrintMinterm]
162
163******************************************************************************/
164int
165Cudd_zddPrintCover(
166  DdManager * zdd,
167  DdNode * node)
168{
169    int         i, size;
170    int         *list;
171
172    size = (int)zdd->sizeZ;
173    if (size % 2 != 0) return(0); /* number of variables should be even */
174    list = ALLOC(int, size);
175    if (list == NULL) {
176        zdd->errorCode = CUDD_MEMORY_OUT;
177        return(0);
178    }
179    for (i = 0; i < size; i++) list[i] = 3; /* bogus value should disappear */
180    zddPrintCoverAux(zdd, node, 0, list);
181    FREE(list);
182    return(1);
183
184} /* end of Cudd_zddPrintCover */
185
186
187/**Function********************************************************************
188
189  Synopsis [Prints to the standard output a ZDD and its statistics.]
190
191  Description [Prints to the standard output a DD and its statistics.
192  The statistics include the number of nodes and the number of minterms.
193  (The number of minterms is also the number of combinations in the set.)
194  The statistics are printed if pr &gt; 0.  Specifically:
195  <ul>
196  <li> pr = 0 : prints nothing
197  <li> pr = 1 : prints counts of nodes and minterms
198  <li> pr = 2 : prints counts + disjoint sum of products
199  <li> pr = 3 : prints counts + list of nodes
200  <li> pr &gt; 3 : prints counts + disjoint sum of products + list of nodes
201  </ul>
202  Returns 1 if successful; 0 otherwise.
203  ]
204
205  SideEffects [None]
206
207  SeeAlso     []
208
209******************************************************************************/
210int
211Cudd_zddPrintDebug(
212  DdManager * zdd,
213  DdNode * f,
214  int  n,
215  int  pr)
216{
217    DdNode      *empty = DD_ZERO(zdd);
218    int         nodes;
219    double      minterms;
220    int         retval = 1;
221
222    if (f == empty && pr > 0) {
223        (void) fprintf(zdd->out,": is the empty ZDD\n");
224        (void) fflush(zdd->out);
225        return(1);
226    }
227
228    if (pr > 0) {
229        nodes = Cudd_zddDagSize(f);
230        if (nodes == CUDD_OUT_OF_MEM) retval = 0;
231        minterms = Cudd_zddCountMinterm(zdd, f, n);
232        if (minterms == (double)CUDD_OUT_OF_MEM) retval = 0;
233        (void) fprintf(zdd->out,": %d nodes %g minterms\n",
234                       nodes, minterms);
235        if (pr > 2)
236            if (!cuddZddP(zdd, f)) retval = 0;
237        if (pr == 2 || pr > 3) {
238            if (!Cudd_zddPrintMinterm(zdd, f)) retval = 0;
239            (void) fprintf(zdd->out,"\n");
240        }
241        (void) fflush(zdd->out);
242    }
243    return(retval);
244
245} /* end of Cudd_zddPrintDebug */
246
247
248
249/**Function********************************************************************
250
251  Synopsis    [Finds the first path of a ZDD.]
252
253  Description [Defines an iterator on the paths of a ZDD
254  and finds its first path. Returns a generator that contains the
255  information necessary to continue the enumeration if successful; NULL
256  otherwise.<p>
257  A path is represented as an array of literals, which are integers in
258  {0, 1, 2}; 0 represents an else arc out of a node, 1 represents a then arc
259  out of a node, and 2 stands for the absence of a node.
260  The size of the array equals the number of variables in the manager at
261  the time Cudd_zddFirstCube is called.<p>
262  The paths that end in the empty terminal are not enumerated.]
263
264  SideEffects [The first path is returned as a side effect.]
265
266  SeeAlso     [Cudd_zddForeachPath Cudd_zddNextPath Cudd_GenFree
267  Cudd_IsGenEmpty]
268
269******************************************************************************/
270DdGen *
271Cudd_zddFirstPath(
272  DdManager * zdd,
273  DdNode * f,
274  int ** path)
275{
276    DdGen *gen;
277    DdNode *top, *next, *prev;
278    int i;
279    int nvars;
280
281    /* Sanity Check. */
282    if (zdd == NULL || f == NULL) return(NULL);
283
284    /* Allocate generator an initialize it. */
285    gen = ALLOC(DdGen,1);
286    if (gen == NULL) {
287        zdd->errorCode = CUDD_MEMORY_OUT;
288        return(NULL);
289    }
290
291    gen->manager = zdd;
292    gen->type = CUDD_GEN_ZDD_PATHS;
293    gen->status = CUDD_GEN_EMPTY;
294    gen->gen.cubes.cube = NULL;
295    gen->gen.cubes.value = DD_ZERO_VAL;
296    gen->stack.sp = 0;
297    gen->stack.stack = NULL;
298    gen->node = NULL;
299
300    nvars = zdd->sizeZ;
301    gen->gen.cubes.cube = ALLOC(int,nvars);
302    if (gen->gen.cubes.cube == NULL) {
303        zdd->errorCode = CUDD_MEMORY_OUT;
304        FREE(gen);
305        return(NULL);
306    }
307    for (i = 0; i < nvars; i++) gen->gen.cubes.cube[i] = 2;
308
309    /* The maximum stack depth is one plus the number of variables.
310    ** because a path may have nodes at all levels, including the
311    ** constant level.
312    */
313    gen->stack.stack = ALLOC(DdNodePtr, nvars+1);
314    if (gen->stack.stack == NULL) {
315        zdd->errorCode = CUDD_MEMORY_OUT;
316        FREE(gen->gen.cubes.cube);
317        FREE(gen);
318        return(NULL);
319    }
320    for (i = 0; i <= nvars; i++) gen->stack.stack[i] = NULL;
321
322    /* Find the first path of the ZDD. */
323    gen->stack.stack[gen->stack.sp] = f; gen->stack.sp++;
324
325    while (1) {
326        top = gen->stack.stack[gen->stack.sp-1];
327        if (!cuddIsConstant(Cudd_Regular(top))) {
328            /* Take the else branch first. */
329            gen->gen.cubes.cube[Cudd_Regular(top)->index] = 0;
330            next = cuddE(Cudd_Regular(top));
331            gen->stack.stack[gen->stack.sp] = Cudd_Not(next); gen->stack.sp++;
332        } else if (Cudd_Regular(top) == DD_ZERO(zdd)) {
333            /* Backtrack. */
334            while (1) {
335                if (gen->stack.sp == 1) {
336                    /* The current node has no predecessor. */
337                    gen->status = CUDD_GEN_EMPTY;
338                    gen->stack.sp--;
339                    goto done;
340                }
341                prev = Cudd_Regular(gen->stack.stack[gen->stack.sp-2]);
342                next = cuddT(prev);
343                if (next != top) { /* follow the then branch next */
344                    gen->gen.cubes.cube[prev->index] = 1;
345                    gen->stack.stack[gen->stack.sp-1] = next;
346                    break;
347                }
348                /* Pop the stack and try again. */
349                gen->gen.cubes.cube[prev->index] = 2;
350                gen->stack.sp--;
351                top = gen->stack.stack[gen->stack.sp-1];
352            }
353        } else {
354            gen->status = CUDD_GEN_NONEMPTY;
355            gen->gen.cubes.value = cuddV(Cudd_Regular(top));
356            goto done;
357        }
358    }
359
360done:
361    *path = gen->gen.cubes.cube;
362    return(gen);
363
364} /* end of Cudd_zddFirstPath */
365
366
367/**Function********************************************************************
368
369  Synopsis    [Generates the next path of a ZDD.]
370
371  Description [Generates the next path of a ZDD onset,
372  using generator gen. Returns 0 if the enumeration is completed; 1
373  otherwise.]
374
375  SideEffects [The path is returned as a side effect. The
376  generator is modified.]
377
378  SeeAlso     [Cudd_zddForeachPath Cudd_zddFirstPath Cudd_GenFree
379  Cudd_IsGenEmpty]
380
381******************************************************************************/
382int
383Cudd_zddNextPath(
384  DdGen * gen,
385  int ** path)
386{
387    DdNode *top, *next, *prev;
388    DdManager *zdd = gen->manager;
389
390    /* Backtrack from previously reached terminal node. */
391    while (1) {
392        if (gen->stack.sp == 1) {
393            /* The current node has no predecessor. */
394            gen->status = CUDD_GEN_EMPTY;
395            gen->stack.sp--;
396            goto done;
397        }
398        top = gen->stack.stack[gen->stack.sp-1];
399        prev = Cudd_Regular(gen->stack.stack[gen->stack.sp-2]);
400        next = cuddT(prev);
401        if (next != top) { /* follow the then branch next */
402            gen->gen.cubes.cube[prev->index] = 1;
403            gen->stack.stack[gen->stack.sp-1] = next;
404            break;
405        }
406        /* Pop the stack and try again. */
407        gen->gen.cubes.cube[prev->index] = 2;
408        gen->stack.sp--;
409    }
410
411    while (1) {
412        top = gen->stack.stack[gen->stack.sp-1];
413        if (!cuddIsConstant(Cudd_Regular(top))) {
414            /* Take the else branch first. */
415            gen->gen.cubes.cube[Cudd_Regular(top)->index] = 0;
416            next = cuddE(Cudd_Regular(top));
417            gen->stack.stack[gen->stack.sp] = Cudd_Not(next); gen->stack.sp++;
418        } else if (Cudd_Regular(top) == DD_ZERO(zdd)) {
419            /* Backtrack. */
420            while (1) {
421                if (gen->stack.sp == 1) {
422                    /* The current node has no predecessor. */
423                    gen->status = CUDD_GEN_EMPTY;
424                    gen->stack.sp--;
425                    goto done;
426                }
427                prev = Cudd_Regular(gen->stack.stack[gen->stack.sp-2]);
428                next = cuddT(prev);
429                if (next != top) { /* follow the then branch next */
430                    gen->gen.cubes.cube[prev->index] = 1;
431                    gen->stack.stack[gen->stack.sp-1] = next;
432                    break;
433                }
434                /* Pop the stack and try again. */
435                gen->gen.cubes.cube[prev->index] = 2;
436                gen->stack.sp--;
437                top = gen->stack.stack[gen->stack.sp-1];
438            }
439        } else {
440            gen->status = CUDD_GEN_NONEMPTY;
441            gen->gen.cubes.value = cuddV(Cudd_Regular(top));
442            goto done;
443        }
444    }
445
446done:
447    if (gen->status == CUDD_GEN_EMPTY) return(0);
448    *path = gen->gen.cubes.cube;
449    return(1);
450
451} /* end of Cudd_zddNextPath */
452
453
454/**Function********************************************************************
455
456  Synopsis    [Converts a path of a ZDD representing a cover to a string.]
457
458  Description [Converts a path of a ZDD representing a cover to a
459  string.  The string represents an implicant of the cover.  The path
460  is typically produced by Cudd_zddForeachPath.  Returns a pointer to
461  the string if successful; NULL otherwise.  If the str input is NULL,
462  it allocates a new string.  The string passed to this function must
463  have enough room for all variables and for the terminator.]
464
465  SideEffects [None]
466
467  SeeAlso     [Cudd_zddForeachPath]
468
469******************************************************************************/
470char *
471Cudd_zddCoverPathToString(
472  DdManager *zdd                /* DD manager */,
473  int *path                     /* path of ZDD representing a cover */,
474  char *str                     /* pointer to string to use if != NULL */
475  )
476{
477    int nvars = zdd->sizeZ;
478    int i;
479    char *res;
480
481    if (nvars & 1) return(NULL);
482    nvars >>= 1;
483    if (str == NULL) {
484        res = ALLOC(char, nvars+1);
485        if (res == NULL) return(NULL);
486    } else {
487        res = str;
488    }
489    for (i = 0; i < nvars; i++) {
490        int v = (path[2*i] << 2) | path[2*i+1];
491        switch (v) {
492        case 0:
493        case 2:
494        case 8:
495        case 10:
496            res[i] = '-';
497            break;
498        case 1:
499        case 9:
500            res[i] = '0';
501            break;
502        case 4:
503        case 6:
504            res[i] = '1';
505            break;
506        default:
507            res[i] = '?';
508        }
509    }
510    res[nvars] = 0;
511
512    return(res);
513
514} /* end of Cudd_zddCoverPathToString */
515
516
517/**Function********************************************************************
518
519  Synopsis    [Writes a dot file representing the argument ZDDs.]
520
521  Description [Writes a file representing the argument ZDDs in a format
522  suitable for the graph drawing program dot.
523  It returns 1 in case of success; 0 otherwise (e.g., out-of-memory,
524  file system full).
525  Cudd_zddDumpDot does not close the file: This is the caller
526  responsibility. Cudd_zddDumpDot uses a minimal unique subset of the
527  hexadecimal address of a node as name for it.
528  If the argument inames is non-null, it is assumed to hold the pointers
529  to the names of the inputs. Similarly for onames.
530  Cudd_zddDumpDot uses the following convention to draw arcs:
531    <ul>
532    <li> solid line: THEN arcs;
533    <li> dashed line: ELSE arcs.
534    </ul>
535  The dot options are chosen so that the drawing fits on a letter-size
536  sheet.
537  ]
538
539  SideEffects [None]
540
541  SeeAlso     [Cudd_DumpDot Cudd_zddPrintDebug]
542
543******************************************************************************/
544int
545Cudd_zddDumpDot(
546  DdManager * dd /* manager */,
547  int  n /* number of output nodes to be dumped */,
548  DdNode ** f /* array of output nodes to be dumped */,
549  char ** inames /* array of input names (or NULL) */,
550  char ** onames /* array of output names (or NULL) */,
551  FILE * fp /* pointer to the dump file */)
552{
553    DdNode      *support = NULL;
554    DdNode      *scan;
555    int         *sorted = NULL;
556    int         nvars = dd->sizeZ;
557    st_table    *visited = NULL;
558    st_generator *gen;
559    int         retval;
560    int         i, j;
561    int         slots;
562    DdNodePtr   *nodelist;
563    long        refAddr, diff, mask;
564
565    /* Build a bit array with the support of f. */
566    sorted = ALLOC(int,nvars);
567    if (sorted == NULL) {
568        dd->errorCode = CUDD_MEMORY_OUT;
569        goto failure;
570    }
571    for (i = 0; i < nvars; i++) sorted[i] = 0;
572
573    /* Take the union of the supports of each output function. */
574    for (i = 0; i < n; i++) {
575        support = Cudd_Support(dd,f[i]);
576        if (support == NULL) goto failure;
577        cuddRef(support);
578        scan = support;
579        while (!cuddIsConstant(scan)) {
580            sorted[scan->index] = 1;
581            scan = cuddT(scan);
582        }
583        Cudd_RecursiveDeref(dd,support);
584    }
585    support = NULL; /* so that we do not try to free it in case of failure */
586
587    /* Initialize symbol table for visited nodes. */
588    visited = st_init_table(st_ptrcmp, st_ptrhash);
589    if (visited == NULL) goto failure;
590
591    /* Collect all the nodes of this DD in the symbol table. */
592    for (i = 0; i < n; i++) {
593        retval = cuddCollectNodes(f[i],visited);
594        if (retval == 0) goto failure;
595    }
596
597    /* Find how many most significant hex digits are identical
598    ** in the addresses of all the nodes. Build a mask based
599    ** on this knowledge, so that digits that carry no information
600    ** will not be printed. This is done in two steps.
601    **  1. We scan the symbol table to find the bits that differ
602    **     in at least 2 addresses.
603    **  2. We choose one of the possible masks. There are 8 possible
604    **     masks for 32-bit integer, and 16 possible masks for 64-bit
605    **     integers.
606    */
607
608    /* Find the bits that are different. */
609    refAddr = (long) f[0];
610    diff = 0;
611    gen = st_init_gen(visited);
612    while (st_gen(gen, &scan, NULL)) {
613        diff |= refAddr ^ (long) scan;
614    }
615    st_free_gen(gen);
616
617    /* Choose the mask. */
618    for (i = 0; (unsigned) i < 8 * sizeof(long); i += 4) {
619        mask = (1 << i) - 1;
620        if (diff <= mask) break;
621    }
622
623    /* Write the header and the global attributes. */
624    retval = fprintf(fp,"digraph \"ZDD\" {\n");
625    if (retval == EOF) return(0);
626    retval = fprintf(fp,
627        "size = \"7.5,10\"\ncenter = true;\nedge [dir = none];\n");
628    if (retval == EOF) return(0);
629
630    /* Write the input name subgraph by scanning the support array. */
631    retval = fprintf(fp,"{ node [shape = plaintext];\n");
632    if (retval == EOF) goto failure;
633    retval = fprintf(fp,"  edge [style = invis];\n");
634    if (retval == EOF) goto failure;
635    /* We use a name ("CONST NODES") with an embedded blank, because
636    ** it is unlikely to appear as an input name.
637    */
638    retval = fprintf(fp,\"CONST NODES\" [style = invis];\n");
639    if (retval == EOF) goto failure;
640    for (i = 0; i < nvars; i++) {
641        if (sorted[dd->invpermZ[i]]) {
642            if (inames == NULL) {
643                retval = fprintf(fp,"\" %d \" -> ", dd->invpermZ[i]);
644            } else {
645                retval = fprintf(fp,"\" %s \" -> ", inames[dd->invpermZ[i]]);
646            }
647            if (retval == EOF) goto failure;
648        }
649    }
650    retval = fprintf(fp,"\"CONST NODES\"; \n}\n");
651    if (retval == EOF) goto failure;
652
653    /* Write the output node subgraph. */
654    retval = fprintf(fp,"{ rank = same; node [shape = box]; edge [style = invis];\n");
655    if (retval == EOF) goto failure;
656    for (i = 0; i < n; i++) {
657        if (onames == NULL) {
658            retval = fprintf(fp,"\"F%d\"", i);
659        } else {
660            retval = fprintf(fp,"\"  %s  \"", onames[i]);
661        }
662        if (retval == EOF) goto failure;
663        if (i == n - 1) {
664            retval = fprintf(fp,"; }\n");
665        } else {
666            retval = fprintf(fp," -> ");
667        }
668        if (retval == EOF) goto failure;
669    }
670
671    /* Write rank info: All nodes with the same index have the same rank. */
672    for (i = 0; i < nvars; i++) {
673        if (sorted[dd->invpermZ[i]]) {
674            retval = fprintf(fp,"{ rank = same; ");
675            if (retval == EOF) goto failure;
676            if (inames == NULL) {
677                retval = fprintf(fp,"\" %d \";\n", dd->invpermZ[i]);
678            } else {
679                retval = fprintf(fp,"\" %s \";\n", inames[dd->invpermZ[i]]);
680            }
681            if (retval == EOF) goto failure;
682            nodelist = dd->subtableZ[i].nodelist;
683            slots = dd->subtableZ[i].slots;
684            for (j = 0; j < slots; j++) {
685                scan = nodelist[j];
686                while (scan != NULL) {
687                    if (st_is_member(visited,(char *) scan)) {
688                        retval = fprintf(fp,"\"%p\";\n", (void *)
689                                         ((mask & (ptrint) scan) /
690                                          sizeof(DdNode)));
691                        if (retval == EOF) goto failure;
692                    }
693                    scan = scan->next;
694                }
695            }
696            retval = fprintf(fp,"}\n");
697            if (retval == EOF) goto failure;
698        }
699    }
700
701    /* All constants have the same rank. */
702    retval = fprintf(fp,
703        "{ rank = same; \"CONST NODES\";\n{ node [shape = box]; ");
704    if (retval == EOF) goto failure;
705    nodelist = dd->constants.nodelist;
706    slots = dd->constants.slots;
707    for (j = 0; j < slots; j++) {
708        scan = nodelist[j];
709        while (scan != NULL) {
710            if (st_is_member(visited,(char *) scan)) {
711                retval = fprintf(fp,"\"%p\";\n", (void *)
712                                 ((mask & (ptrint) scan) / sizeof(DdNode)));
713                if (retval == EOF) goto failure;
714            }
715            scan = scan->next;
716        }
717    }
718    retval = fprintf(fp,"}\n}\n");
719    if (retval == EOF) goto failure;
720
721    /* Write edge info. */
722    /* Edges from the output nodes. */
723    for (i = 0; i < n; i++) {
724        if (onames == NULL) {
725            retval = fprintf(fp,"\"F%d\"", i);
726        } else {
727            retval = fprintf(fp,"\"  %s  \"", onames[i]);
728        }
729        if (retval == EOF) goto failure;
730        retval = fprintf(fp," -> \"%p\" [style = solid];\n",
731                         (void *) ((mask & (ptrint) f[i]) /
732                                          sizeof(DdNode)));
733        if (retval == EOF) goto failure;
734    }
735
736    /* Edges from internal nodes. */
737    for (i = 0; i < nvars; i++) {
738        if (sorted[dd->invpermZ[i]]) {
739            nodelist = dd->subtableZ[i].nodelist;
740            slots = dd->subtableZ[i].slots;
741            for (j = 0; j < slots; j++) {
742                scan = nodelist[j];
743                while (scan != NULL) {
744                    if (st_is_member(visited,(char *) scan)) {
745                        retval = fprintf(fp,
746                            "\"%p\" -> \"%p\";\n",
747                            (void *) ((mask & (ptrint) scan) / sizeof(DdNode)),
748                            (void *) ((mask & (ptrint) cuddT(scan)) /
749                                      sizeof(DdNode)));
750                        if (retval == EOF) goto failure;
751                        retval = fprintf(fp,
752                                         "\"%p\" -> \"%p\" [style = dashed];\n",
753                                         (void *) ((mask & (ptrint) scan)
754                                                   / sizeof(DdNode)),
755                                         (void *) ((mask & (ptrint)
756                                                    cuddE(scan)) /
757                                                   sizeof(DdNode)));
758                        if (retval == EOF) goto failure;
759                    }
760                    scan = scan->next;
761                }
762            }
763        }
764    }
765
766    /* Write constant labels. */
767    nodelist = dd->constants.nodelist;
768    slots = dd->constants.slots;
769    for (j = 0; j < slots; j++) {
770        scan = nodelist[j];
771        while (scan != NULL) {
772            if (st_is_member(visited,(char *) scan)) {
773                retval = fprintf(fp,"\"%p\" [label = \"%g\"];\n",
774                                 (void *) ((mask & (ptrint) scan) /
775                                           sizeof(DdNode)),
776                                 cuddV(scan));
777                if (retval == EOF) goto failure;
778            }
779            scan = scan->next;
780        }
781    }
782
783    /* Write trailer and return. */
784    retval = fprintf(fp,"}\n");
785    if (retval == EOF) goto failure;
786
787    st_free_table(visited);
788    FREE(sorted);
789    return(1);
790
791failure:
792    if (sorted != NULL) FREE(sorted);
793    if (visited != NULL) st_free_table(visited);
794    return(0);
795
796} /* end of Cudd_zddDumpBlif */
797
798
799/*---------------------------------------------------------------------------*/
800/* Definition of internal functions                                          */
801/*---------------------------------------------------------------------------*/
802
803
804/**Function********************************************************************
805
806  Synopsis [Prints a ZDD to the standard output. One line per node is
807  printed.]
808
809  Description [Prints a ZDD to the standard output. One line per node is
810  printed. Returns 1 if successful; 0 otherwise.]
811
812  SideEffects [None]
813
814  SeeAlso     [Cudd_zddPrintDebug]
815
816******************************************************************************/
817int
818cuddZddP(
819  DdManager * zdd,
820  DdNode * f)
821{
822    int retval;
823    st_table *table = st_init_table(st_ptrcmp, st_ptrhash);
824
825    if (table == NULL) return(0);
826
827    retval = zp2(zdd, f, table);
828    st_free_table(table);
829    (void) fputc('\n', zdd->out);
830    return(retval);
831
832} /* end of cuddZddP */
833
834
835/*---------------------------------------------------------------------------*/
836/* Definition of static functions                                            */
837/*---------------------------------------------------------------------------*/
838
839
840/**Function********************************************************************
841
842  Synopsis [Performs the recursive step of cuddZddP.]
843
844  Description [Performs the recursive step of cuddZddP. Returns 1 in
845  case of success; 0 otherwise.]
846
847  SideEffects [None]
848
849  SeeAlso     []
850
851******************************************************************************/
852static int
853zp2(
854  DdManager * zdd,
855  DdNode * f,
856  st_table * t)
857{
858    DdNode      *n;
859    int         T, E;
860    DdNode      *base = DD_ONE(zdd);
861
862    if (f == NULL)
863        return(0);
864
865    if (Cudd_IsConstant(f)) {
866        (void)fprintf(zdd->out, "ID = %d\n", (f == base));
867        return(1);
868    }
869    if (st_is_member(t, (char *)f) == 1)
870        return(1);
871
872    if (st_insert(t, (char *) f, NULL) == ST_OUT_OF_MEM)
873        return(0);
874
875#if SIZEOF_VOID_P == 8
876    (void) fprintf(zdd->out, "ID = 0x%lx\tindex = %u\tr = %u\t",
877        (ptruint)f / (ptruint) sizeof(DdNode), f->index, f->ref);
878#else
879    (void) fprintf(zdd->out, "ID = 0x%x\tindex = %hu\tr = %hu\t",
880        (ptruint)f / (ptruint) sizeof(DdNode), f->index, f->ref);
881#endif
882
883    n = cuddT(f);
884    if (Cudd_IsConstant(n)) {
885        (void) fprintf(zdd->out, "T = %d\t\t", (n == base));
886        T = 1;
887    } else {
888#if SIZEOF_VOID_P == 8
889        (void) fprintf(zdd->out, "T = 0x%lx\t", (ptruint) n /
890                       (ptruint) sizeof(DdNode));
891#else
892        (void) fprintf(zdd->out, "T = 0x%x\t", (ptruint) n /
893                       (ptruint) sizeof(DdNode));
894#endif
895        T = 0;
896    }
897
898    n = cuddE(f);
899    if (Cudd_IsConstant(n)) {
900        (void) fprintf(zdd->out, "E = %d\n", (n == base));
901        E = 1;
902    } else {
903#if SIZEOF_VOID_P == 8
904        (void) fprintf(zdd->out, "E = 0x%lx\n", (ptruint) n /
905                      (ptruint) sizeof(DdNode));
906#else
907        (void) fprintf(zdd->out, "E = 0x%x\n", (ptruint) n /
908                       (ptruint) sizeof(DdNode));
909#endif
910        E = 0;
911    }
912
913    if (E == 0)
914        if (zp2(zdd, cuddE(f), t) == 0) return(0);
915    if (T == 0)
916        if (zp2(zdd, cuddT(f), t) == 0) return(0);
917    return(1);
918
919} /* end of zp2 */
920
921
922/**Function********************************************************************
923
924  Synopsis    [Performs the recursive step of Cudd_zddPrintMinterm.]
925
926  Description []
927
928  SideEffects [None]
929
930  SeeAlso     []
931
932******************************************************************************/
933static void
934zdd_print_minterm_aux(
935  DdManager * zdd /* manager */,
936  DdNode * node /* current node */,
937  int  level /* depth in the recursion */,
938  int * list /* current recursion path */)
939{
940    DdNode      *Nv, *Nnv;
941    int         i, v;
942    DdNode      *base = DD_ONE(zdd);
943
944    if (Cudd_IsConstant(node)) {
945        if (node == base) {
946            /* Check for missing variable. */
947            if (level != zdd->sizeZ) {
948                list[zdd->invpermZ[level]] = 0;
949                zdd_print_minterm_aux(zdd, node, level + 1, list);
950                return;
951            }
952            /* Terminal case: Print one cube based on the current recursion
953            ** path.
954            */
955            for (i = 0; i < zdd->sizeZ; i++) {
956                v = list[i];
957                if (v == 0)
958                    (void) fprintf(zdd->out,"0");
959                else if (v == 1)
960                    (void) fprintf(zdd->out,"1");
961                else if (v == 3)
962                    (void) fprintf(zdd->out,"@");       /* should never happen */
963                else
964                    (void) fprintf(zdd->out,"-");
965            }
966            (void) fprintf(zdd->out," 1\n");
967        }
968    } else {
969        /* Check for missing variable. */
970        if (level != cuddIZ(zdd,node->index)) {
971            list[zdd->invpermZ[level]] = 0;
972            zdd_print_minterm_aux(zdd, node, level + 1, list);
973            return;
974        }
975
976        Nnv = cuddE(node);
977        Nv = cuddT(node);
978        if (Nv == Nnv) {
979            list[node->index] = 2;
980            zdd_print_minterm_aux(zdd, Nnv, level + 1, list);
981            return;
982        }
983
984        list[node->index] = 1;
985        zdd_print_minterm_aux(zdd, Nv, level + 1, list);
986        list[node->index] = 0;
987        zdd_print_minterm_aux(zdd, Nnv, level + 1, list);
988    }
989    return;
990
991} /* end of zdd_print_minterm_aux */
992
993
994/**Function********************************************************************
995
996  Synopsis    [Performs the recursive step of Cudd_zddPrintCover.]
997
998  Description []
999
1000  SideEffects [None]
1001
1002  SeeAlso     []
1003
1004******************************************************************************/
1005static void
1006zddPrintCoverAux(
1007  DdManager * zdd /* manager */,
1008  DdNode * node /* current node */,
1009  int  level /* depth in the recursion */,
1010  int * list /* current recursion path */)
1011{
1012    DdNode      *Nv, *Nnv;
1013    int         i, v;
1014    DdNode      *base = DD_ONE(zdd);
1015
1016    if (Cudd_IsConstant(node)) {
1017        if (node == base) {
1018            /* Check for missing variable. */
1019            if (level != zdd->sizeZ) {
1020                list[zdd->invpermZ[level]] = 0;
1021                zddPrintCoverAux(zdd, node, level + 1, list);
1022                return;
1023            }
1024            /* Terminal case: Print one cube based on the current recursion
1025            ** path.
1026            */
1027            for (i = 0; i < zdd->sizeZ; i += 2) {
1028                v = list[i] * 4 + list[i+1];
1029                if (v == 0)
1030                    (void) putc('-',zdd->out);
1031                else if (v == 4)
1032                    (void) putc('1',zdd->out);
1033                else if (v == 1)
1034                    (void) putc('0',zdd->out);
1035                else
1036                    (void) putc('@',zdd->out); /* should never happen */
1037            }
1038            (void) fprintf(zdd->out," 1\n");
1039        }
1040    } else {
1041        /* Check for missing variable. */
1042        if (level != cuddIZ(zdd,node->index)) {
1043            list[zdd->invpermZ[level]] = 0;
1044            zddPrintCoverAux(zdd, node, level + 1, list);
1045            return;
1046        }
1047
1048        Nnv = cuddE(node);
1049        Nv = cuddT(node);
1050        if (Nv == Nnv) {
1051            list[node->index] = 2;
1052            zddPrintCoverAux(zdd, Nnv, level + 1, list);
1053            return;
1054        }
1055
1056        list[node->index] = 1;
1057        zddPrintCoverAux(zdd, Nv, level + 1, list);
1058        list[node->index] = 0;
1059        zddPrintCoverAux(zdd, Nnv, level + 1, list);
1060    }
1061    return;
1062
1063} /* end of zddPrintCoverAux */
Note: See TracBrowser for help on using the repository browser.