glu-2.2: src/cuBdd/cuddExport.c Source File

00001 
00065 #include "util.h"
00066 #include "cuddInt.h"
00067 
00068 /*---------------------------------------------------------------------------*/
00069 /* Constant declarations                                                     */
00070 /*---------------------------------------------------------------------------*/
00071 
00072 /*---------------------------------------------------------------------------*/
00073 /* Stucture declarations                                                     */
00074 /*---------------------------------------------------------------------------*/
00075 
00076 /*---------------------------------------------------------------------------*/
00077 /* Type declarations                                                         */
00078 /*---------------------------------------------------------------------------*/
00079 
00080 /*---------------------------------------------------------------------------*/
00081 /* Variable declarations                                                     */
00082 /*---------------------------------------------------------------------------*/
00083 
00084 #ifndef lint
00085 static char rcsid[] DD_UNUSED = "$Id: cuddExport.c,v 1.22 2009/03/08 02:49:02 fabio Exp $";
00086 #endif
00087 
00088 /*---------------------------------------------------------------------------*/
00089 /* Macro declarations                                                        */
00090 /*---------------------------------------------------------------------------*/
00091 
00094 /*---------------------------------------------------------------------------*/
00095 /* Static function prototypes                                                */
00096 /*---------------------------------------------------------------------------*/
00097 
00098 static int ddDoDumpBlif (DdManager *dd, DdNode *f, FILE *fp, st_table *visited, char **names, int mv);
00099 static int ddDoDumpDaVinci (DdManager *dd, DdNode *f, FILE *fp, st_table *visited, char **names, ptruint mask);
00100 static int ddDoDumpDDcal (DdManager *dd, DdNode *f, FILE *fp, st_table *visited, char **names, ptruint mask);
00101 static int ddDoDumpFactoredForm (DdManager *dd, DdNode *f, FILE *fp, char **names);
00102 
00106 /*---------------------------------------------------------------------------*/
00107 /* Definition of exported functions                                          */
00108 /*---------------------------------------------------------------------------*/
00109 
00110 
00131 int
00132 Cudd_DumpBlif(
00133   DdManager * dd /* manager */,
00134   int  n /* number of output nodes to be dumped */,
00135   DdNode ** f /* array of output nodes to be dumped */,
00136   char ** inames /* array of input names (or NULL) */,
00137   char ** onames /* array of output names (or NULL) */,
00138   char * mname /* model name (or NULL) */,
00139   FILE * fp /* pointer to the dump file */,
00140   int mv /* 0: blif, 1: blif-MV */)
00141 {
00142     DdNode      *support = NULL;
00143     DdNode      *scan;
00144     int         *sorted = NULL;
00145     int         nvars = dd->size;
00146     int         retval;
00147     int         i;
00148 
00149     /* Build a bit array with the support of f. */
00150     sorted = ALLOC(int,nvars);
00151     if (sorted == NULL) {
00152         dd->errorCode = CUDD_MEMORY_OUT;
00153         goto failure;
00154     }
00155     for (i = 0; i < nvars; i++) sorted[i] = 0;
00156 
00157     /* Take the union of the supports of each output function. */
00158     support = Cudd_VectorSupport(dd,f,n);
00159     if (support == NULL) goto failure;
00160     cuddRef(support);
00161     scan = support;
00162     while (!cuddIsConstant(scan)) {
00163         sorted[scan->index] = 1;
00164         scan = cuddT(scan);
00165     }
00166     Cudd_RecursiveDeref(dd,support);
00167     support = NULL; /* so that we do not try to free it in case of failure */
00168 
00169     /* Write the header (.model .inputs .outputs). */
00170     if (mname == NULL) {
00171         retval = fprintf(fp,".model DD\n.inputs");
00172     } else {
00173         retval = fprintf(fp,".model %s\n.inputs",mname);
00174     }
00175     if (retval == EOF) {
00176         FREE(sorted);
00177         return(0);
00178     }
00179 
00180     /* Write the input list by scanning the support array. */
00181     for (i = 0; i < nvars; i++) {
00182         if (sorted[i]) {
00183             if (inames == NULL) {
00184                 retval = fprintf(fp," %d", i);
00185             } else {
00186                 retval = fprintf(fp," %s", inames[i]);
00187             }
00188             if (retval == EOF) goto failure;
00189         }
00190     }
00191     FREE(sorted);
00192     sorted = NULL;
00193 
00194     /* Write the .output line. */
00195     retval = fprintf(fp,"\n.outputs");
00196     if (retval == EOF) goto failure;
00197     for (i = 0; i < n; i++) {
00198         if (onames == NULL) {
00199             retval = fprintf(fp," f%d", i);
00200         } else {
00201             retval = fprintf(fp," %s", onames[i]);
00202         }
00203         if (retval == EOF) goto failure;
00204     }
00205     retval = fprintf(fp,"\n");
00206     if (retval == EOF) goto failure;
00207 
00208     retval = Cudd_DumpBlifBody(dd, n, f, inames, onames, fp, mv);
00209     if (retval == 0) goto failure;
00210 
00211     /* Write trailer and return. */
00212     retval = fprintf(fp,".end\n");
00213     if (retval == EOF) goto failure;
00214 
00215     return(1);
00216 
00217 failure:
00218     if (sorted != NULL) FREE(sorted);
00219     if (support != NULL) Cudd_RecursiveDeref(dd,support);
00220     return(0);
00221 
00222 } /* end of Cudd_DumpBlif */
00223 
00224 
00247 int
00248 Cudd_DumpBlifBody(
00249   DdManager * dd /* manager */,
00250   int  n /* number of output nodes to be dumped */,
00251   DdNode ** f /* array of output nodes to be dumped */,
00252   char ** inames /* array of input names (or NULL) */,
00253   char ** onames /* array of output names (or NULL) */,
00254   FILE * fp /* pointer to the dump file */,
00255   int mv /* 0: blif, 1: blif-MV */)
00256 {
00257     st_table    *visited = NULL;
00258     int         retval;
00259     int         i;
00260 
00261     /* Initialize symbol table for visited nodes. */
00262     visited = st_init_table(st_ptrcmp, st_ptrhash);
00263     if (visited == NULL) goto failure;
00264 
00265     /* Call the function that really gets the job done. */
00266     for (i = 0; i < n; i++) {
00267         retval = ddDoDumpBlif(dd,Cudd_Regular(f[i]),fp,visited,inames,mv);
00268         if (retval == 0) goto failure;
00269     }
00270 
00271     /* To account for the possible complement on the root,
00272     ** we put either a buffer or an inverter at the output of
00273     ** the multiplexer representing the top node.
00274     */
00275     for (i = 0; i < n; i++) {
00276         if (onames == NULL) {
00277             retval = fprintf(fp,
00278 #if SIZEOF_VOID_P == 8
00279                 ".names %lx f%d\n", (ptruint) f[i] / (ptruint) sizeof(DdNode), i);
00280 #else
00281                 ".names %x f%d\n", (ptruint) f[i] / (ptruint) sizeof(DdNode), i);
00282 #endif
00283         } else {
00284             retval = fprintf(fp,
00285 #if SIZEOF_VOID_P == 8
00286                 ".names %lx %s\n", (ptruint) f[i] / (ptruint) sizeof(DdNode), onames[i]);
00287 #else
00288                 ".names %x %s\n", (ptruint) f[i] / (ptruint) sizeof(DdNode), onames[i]);
00289 #endif
00290         }
00291         if (retval == EOF) goto failure;
00292         if (Cudd_IsComplement(f[i])) {
00293             retval = fprintf(fp,"%s0 1\n", mv ? ".def 0\n" : "");
00294         } else {
00295             retval = fprintf(fp,"%s1 1\n", mv ? ".def 0\n" : "");
00296         }
00297         if (retval == EOF) goto failure;
00298     }
00299 
00300     st_free_table(visited);
00301     return(1);
00302 
00303 failure:
00304     if (visited != NULL) st_free_table(visited);
00305     return(0);
00306 
00307 } /* end of Cudd_DumpBlifBody */
00308 
00309 
00339 int
00340 Cudd_DumpDot(
00341   DdManager * dd /* manager */,
00342   int  n /* number of output nodes to be dumped */,
00343   DdNode ** f /* array of output nodes to be dumped */,
00344   char ** inames /* array of input names (or NULL) */,
00345   char ** onames /* array of output names (or NULL) */,
00346   FILE * fp /* pointer to the dump file */)
00347 {
00348     DdNode      *support = NULL;
00349     DdNode      *scan;
00350     int         *sorted = NULL;
00351     int         nvars = dd->size;
00352     st_table    *visited = NULL;
00353     st_generator *gen = NULL;
00354     int         retval;
00355     int         i, j;
00356     int         slots;
00357     DdNodePtr   *nodelist;
00358     long        refAddr, diff, mask;
00359 
00360     /* Build a bit array with the support of f. */
00361     sorted = ALLOC(int,nvars);
00362     if (sorted == NULL) {
00363         dd->errorCode = CUDD_MEMORY_OUT;
00364         goto failure;
00365     }
00366     for (i = 0; i < nvars; i++) sorted[i] = 0;
00367 
00368     /* Take the union of the supports of each output function. */
00369     support = Cudd_VectorSupport(dd,f,n);
00370     if (support == NULL) goto failure;
00371     cuddRef(support);
00372     scan = support;
00373     while (!cuddIsConstant(scan)) {
00374         sorted[scan->index] = 1;
00375         scan = cuddT(scan);
00376     }
00377     Cudd_RecursiveDeref(dd,support);
00378     support = NULL; /* so that we do not try to free it in case of failure */
00379 
00380     /* Initialize symbol table for visited nodes. */
00381     visited = st_init_table(st_ptrcmp, st_ptrhash);
00382     if (visited == NULL) goto failure;
00383 
00384     /* Collect all the nodes of this DD in the symbol table. */
00385     for (i = 0; i < n; i++) {
00386         retval = cuddCollectNodes(Cudd_Regular(f[i]),visited);
00387         if (retval == 0) goto failure;
00388     }
00389 
00390     /* Find how many most significant hex digits are identical
00391     ** in the addresses of all the nodes. Build a mask based
00392     ** on this knowledge, so that digits that carry no information
00393     ** will not be printed. This is done in two steps.
00394     **  1. We scan the symbol table to find the bits that differ
00395     **     in at least 2 addresses.
00396     **  2. We choose one of the possible masks. There are 8 possible
00397     **     masks for 32-bit integer, and 16 possible masks for 64-bit
00398     **     integers.
00399     */
00400 
00401     /* Find the bits that are different. */
00402     refAddr = (long) Cudd_Regular(f[0]);
00403     diff = 0;
00404     gen = st_init_gen(visited);
00405     if (gen == NULL) goto failure;
00406     while (st_gen(gen, &scan, NULL)) {
00407         diff |= refAddr ^ (long) scan;
00408     }
00409     st_free_gen(gen); gen = NULL;
00410 
00411     /* Choose the mask. */
00412     for (i = 0; (unsigned) i < 8 * sizeof(long); i += 4) {
00413         mask = (1 << i) - 1;
00414         if (diff <= mask) break;
00415     }
00416 
00417     /* Write the header and the global attributes. */
00418     retval = fprintf(fp,"digraph \"DD\" {\n");
00419     if (retval == EOF) return(0);
00420     retval = fprintf(fp,
00421         "size = \"7.5,10\"\ncenter = true;\nedge [dir = none];\n");
00422     if (retval == EOF) return(0);
00423 
00424     /* Write the input name subgraph by scanning the support array. */
00425     retval = fprintf(fp,"{ node [shape = plaintext];\n");
00426     if (retval == EOF) goto failure;
00427     retval = fprintf(fp,"  edge [style = invis];\n");
00428     if (retval == EOF) goto failure;
00429     /* We use a name ("CONST NODES") with an embedded blank, because
00430     ** it is unlikely to appear as an input name.
00431     */
00432     retval = fprintf(fp,"  \"CONST NODES\" [style = invis];\n");
00433     if (retval == EOF) goto failure;
00434     for (i = 0; i < nvars; i++) {
00435         if (sorted[dd->invperm[i]]) {
00436             if (inames == NULL || inames[dd->invperm[i]] == NULL) {
00437                 retval = fprintf(fp,"\" %d \" -> ", dd->invperm[i]);
00438             } else {
00439                 retval = fprintf(fp,"\" %s \" -> ", inames[dd->invperm[i]]);
00440             }
00441             if (retval == EOF) goto failure;
00442         }
00443     }
00444     retval = fprintf(fp,"\"CONST NODES\"; \n}\n");
00445     if (retval == EOF) goto failure;
00446 
00447     /* Write the output node subgraph. */
00448     retval = fprintf(fp,"{ rank = same; node [shape = box]; edge [style = invis];\n");
00449     if (retval == EOF) goto failure;
00450     for (i = 0; i < n; i++) {
00451         if (onames == NULL) {
00452             retval = fprintf(fp,"\"F%d\"", i);
00453         } else {
00454             retval = fprintf(fp,"\"  %s  \"", onames[i]);
00455         }
00456         if (retval == EOF) goto failure;
00457         if (i == n - 1) {
00458             retval = fprintf(fp,"; }\n");
00459         } else {
00460             retval = fprintf(fp," -> ");
00461         }
00462         if (retval == EOF) goto failure;
00463     }
00464 
00465     /* Write rank info: All nodes with the same index have the same rank. */
00466     for (i = 0; i < nvars; i++) {
00467         if (sorted[dd->invperm[i]]) {
00468             retval = fprintf(fp,"{ rank = same; ");
00469             if (retval == EOF) goto failure;
00470             if (inames == NULL || inames[dd->invperm[i]] == NULL) {
00471                 retval = fprintf(fp,"\" %d \";\n", dd->invperm[i]);
00472             } else {
00473                 retval = fprintf(fp,"\" %s \";\n", inames[dd->invperm[i]]);
00474             }
00475             if (retval == EOF) goto failure;
00476             nodelist = dd->subtables[i].nodelist;
00477             slots = dd->subtables[i].slots;
00478             for (j = 0; j < slots; j++) {
00479                 scan = nodelist[j];
00480                 while (scan != NULL) {
00481                     if (st_is_member(visited,(char *) scan)) {
00482                         retval = fprintf(fp,"\"%p\";\n",
00483                             (void *) ((mask & (ptrint) scan) /
00484                             sizeof(DdNode)));
00485                         if (retval == EOF) goto failure;
00486                     }
00487                     scan = scan->next;
00488                 }
00489             }
00490             retval = fprintf(fp,"}\n");
00491             if (retval == EOF) goto failure;
00492         }
00493     }
00494 
00495     /* All constants have the same rank. */
00496     retval = fprintf(fp,
00497         "{ rank = same; \"CONST NODES\";\n{ node [shape = box]; ");
00498     if (retval == EOF) goto failure;
00499     nodelist = dd->constants.nodelist;
00500     slots = dd->constants.slots;
00501     for (j = 0; j < slots; j++) {
00502         scan = nodelist[j];
00503         while (scan != NULL) {
00504             if (st_is_member(visited,(char *) scan)) {
00505                 retval = fprintf(fp,"\"%p\";\n",
00506                     (void *) ((mask & (ptrint) scan) / sizeof(DdNode)));
00507                 if (retval == EOF) goto failure;
00508             }
00509             scan = scan->next;
00510         }
00511     }
00512     retval = fprintf(fp,"}\n}\n");
00513     if (retval == EOF) goto failure;
00514 
00515     /* Write edge info. */
00516     /* Edges from the output nodes. */
00517     for (i = 0; i < n; i++) {
00518         if (onames == NULL) {
00519             retval = fprintf(fp,"\"F%d\"", i);
00520         } else {
00521             retval = fprintf(fp,"\"  %s  \"", onames[i]);
00522         }
00523         if (retval == EOF) goto failure;
00524         /* Account for the possible complement on the root. */
00525         if (Cudd_IsComplement(f[i])) {
00526             retval = fprintf(fp," -> \"%p\" [style = dotted];\n",
00527                 (void *) ((mask & (ptrint) f[i]) / sizeof(DdNode)));
00528         } else {
00529             retval = fprintf(fp," -> \"%p\" [style = solid];\n",
00530                 (void *) ((mask & (ptrint) f[i]) / sizeof(DdNode)));
00531         }
00532         if (retval == EOF) goto failure;
00533     }
00534 
00535     /* Edges from internal nodes. */
00536     for (i = 0; i < nvars; i++) {
00537         if (sorted[dd->invperm[i]]) {
00538             nodelist = dd->subtables[i].nodelist;
00539             slots = dd->subtables[i].slots;
00540             for (j = 0; j < slots; j++) {
00541                 scan = nodelist[j];
00542                 while (scan != NULL) {
00543                     if (st_is_member(visited,(char *) scan)) {
00544                         retval = fprintf(fp,
00545                             "\"%p\" -> \"%p\";\n",
00546                             (void *) ((mask & (ptrint) scan) /
00547                             sizeof(DdNode)),
00548                             (void *) ((mask & (ptrint) cuddT(scan)) /
00549                             sizeof(DdNode)));
00550                         if (retval == EOF) goto failure;
00551                         if (Cudd_IsComplement(cuddE(scan))) {
00552                             retval = fprintf(fp,
00553                                 "\"%p\" -> \"%p\" [style = dotted];\n",
00554                                 (void *) ((mask & (ptrint) scan) /
00555                                 sizeof(DdNode)),
00556                                 (void *) ((mask & (ptrint) cuddE(scan)) /
00557                                 sizeof(DdNode)));
00558                         } else {
00559                             retval = fprintf(fp,
00560                                 "\"%p\" -> \"%p\" [style = dashed];\n",
00561                                 (void *) ((mask & (ptrint) scan) /
00562                                 sizeof(DdNode)),
00563                                 (void *) ((mask & (ptrint) cuddE(scan)) /
00564                                 sizeof(DdNode)));
00565                         }
00566                         if (retval == EOF) goto failure;
00567                     }
00568                     scan = scan->next;
00569                 }
00570             }
00571         }
00572     }
00573 
00574     /* Write constant labels. */
00575     nodelist = dd->constants.nodelist;
00576     slots = dd->constants.slots;
00577     for (j = 0; j < slots; j++) {
00578         scan = nodelist[j];
00579         while (scan != NULL) {
00580             if (st_is_member(visited,(char *) scan)) {
00581                 retval = fprintf(fp,"\"%p\" [label = \"%g\"];\n",
00582                     (void *) ((mask & (ptrint) scan) / sizeof(DdNode)),
00583                     cuddV(scan));
00584                 if (retval == EOF) goto failure;
00585             }
00586             scan = scan->next;
00587         }
00588     }
00589 
00590     /* Write trailer and return. */
00591     retval = fprintf(fp,"}\n");
00592     if (retval == EOF) goto failure;
00593 
00594     st_free_table(visited);
00595     FREE(sorted);
00596     return(1);
00597 
00598 failure:
00599     if (sorted != NULL) FREE(sorted);
00600     if (support != NULL) Cudd_RecursiveDeref(dd,support);
00601     if (visited != NULL) st_free_table(visited);
00602     return(0);
00603 
00604 } /* end of Cudd_DumpDot */
00605 
00606 
00625 int
00626 Cudd_DumpDaVinci(
00627   DdManager * dd /* manager */,
00628   int  n /* number of output nodes to be dumped */,
00629   DdNode ** f /* array of output nodes to be dumped */,
00630   char ** inames /* array of input names (or NULL) */,
00631   char ** onames /* array of output names (or NULL) */,
00632   FILE * fp /* pointer to the dump file */)
00633 {
00634     DdNode        *support = NULL;
00635     DdNode        *scan;
00636     st_table      *visited = NULL;
00637     int           retval;
00638     int           i;
00639     st_generator  *gen;
00640     ptruint       refAddr, diff, mask;
00641 
00642     /* Initialize symbol table for visited nodes. */
00643     visited = st_init_table(st_ptrcmp, st_ptrhash);
00644     if (visited == NULL) goto failure;
00645 
00646     /* Collect all the nodes of this DD in the symbol table. */
00647     for (i = 0; i < n; i++) {
00648         retval = cuddCollectNodes(Cudd_Regular(f[i]),visited);
00649         if (retval == 0) goto failure;
00650     }
00651 
00652     /* Find how many most significant hex digits are identical
00653     ** in the addresses of all the nodes. Build a mask based
00654     ** on this knowledge, so that digits that carry no information
00655     ** will not be printed. This is done in two steps.
00656     **  1. We scan the symbol table to find the bits that differ
00657     **     in at least 2 addresses.
00658     **  2. We choose one of the possible masks. There are 8 possible
00659     **     masks for 32-bit integer, and 16 possible masks for 64-bit
00660     **     integers.
00661     */
00662 
00663     /* Find the bits that are different. */
00664     refAddr = (ptruint) Cudd_Regular(f[0]);
00665     diff = 0;
00666     gen = st_init_gen(visited);
00667     while (st_gen(gen, &scan, NULL)) {
00668         diff |= refAddr ^ (ptruint) scan;
00669     }
00670     st_free_gen(gen);
00671 
00672     /* Choose the mask. */
00673     for (i = 0; (unsigned) i < 8 * sizeof(ptruint); i += 4) {
00674         mask = (1 << i) - 1;
00675         if (diff <= mask) break;
00676     }
00677     st_free_table(visited);
00678 
00679     /* Initialize symbol table for visited nodes. */
00680     visited = st_init_table(st_ptrcmp, st_ptrhash);
00681     if (visited == NULL) goto failure;
00682 
00683     retval = fprintf(fp, "[");
00684     if (retval == EOF) goto failure;
00685     /* Call the function that really gets the job done. */
00686     for (i = 0; i < n; i++) {
00687         if (onames == NULL) {
00688             retval = fprintf(fp,
00689                              "l(\"f%d\",n(\"root\",[a(\"OBJECT\",\"f%d\")],",
00690                              i,i);
00691         } else {
00692             retval = fprintf(fp,
00693                              "l(\"%s\",n(\"root\",[a(\"OBJECT\",\"%s\")],",
00694                              onames[i], onames[i]);
00695         }
00696         if (retval == EOF) goto failure;
00697         retval = fprintf(fp, "[e(\"edge\",[a(\"EDGECOLOR\",\"%s\"),a(\"_DIR\",\"none\")],",
00698                          Cudd_IsComplement(f[i]) ? "red" : "blue");
00699         if (retval == EOF) goto failure;
00700         retval = ddDoDumpDaVinci(dd,Cudd_Regular(f[i]),fp,visited,inames,mask);
00701         if (retval == 0) goto failure;
00702         retval = fprintf(fp, ")]))%s", i == n-1 ? "" : ",");
00703         if (retval == EOF) goto failure;
00704     }
00705 
00706     /* Write trailer and return. */
00707     retval = fprintf(fp, "]\n");
00708     if (retval == EOF) goto failure;
00709 
00710     st_free_table(visited);
00711     return(1);
00712 
00713 failure:
00714     if (support != NULL) Cudd_RecursiveDeref(dd,support);
00715     if (visited != NULL) st_free_table(visited);
00716     return(0);
00717 
00718 } /* end of Cudd_DumpDaVinci */
00719 
00720 
00739 int
00740 Cudd_DumpDDcal(
00741   DdManager * dd /* manager */,
00742   int  n /* number of output nodes to be dumped */,
00743   DdNode ** f /* array of output nodes to be dumped */,
00744   char ** inames /* array of input names (or NULL) */,
00745   char ** onames /* array of output names (or NULL) */,
00746   FILE * fp /* pointer to the dump file */)
00747 {
00748     DdNode        *support = NULL;
00749     DdNode        *scan;
00750     int           *sorted = NULL;
00751     int           nvars = dd->size;
00752     st_table      *visited = NULL;
00753     int           retval;
00754     int           i;
00755     st_generator  *gen;
00756     ptruint       refAddr, diff, mask;
00757 
00758     /* Initialize symbol table for visited nodes. */
00759     visited = st_init_table(st_ptrcmp, st_ptrhash);
00760     if (visited == NULL) goto failure;
00761 
00762     /* Collect all the nodes of this DD in the symbol table. */
00763     for (i = 0; i < n; i++) {
00764         retval = cuddCollectNodes(Cudd_Regular(f[i]),visited);
00765         if (retval == 0) goto failure;
00766     }
00767 
00768     /* Find how many most significant hex digits are identical
00769     ** in the addresses of all the nodes. Build a mask based
00770     ** on this knowledge, so that digits that carry no information
00771     ** will not be printed. This is done in two steps.
00772     **  1. We scan the symbol table to find the bits that differ
00773     **     in at least 2 addresses.
00774     **  2. We choose one of the possible masks. There are 8 possible
00775     **     masks for 32-bit integer, and 16 possible masks for 64-bit
00776     **     integers.
00777     */
00778 
00779     /* Find the bits that are different. */
00780     refAddr = (ptruint) Cudd_Regular(f[0]);
00781     diff = 0;
00782     gen = st_init_gen(visited);
00783     while (st_gen(gen, &scan, NULL)) {
00784         diff |= refAddr ^ (ptruint) scan;
00785     }
00786     st_free_gen(gen);
00787 
00788     /* Choose the mask. */
00789     for (i = 0; (unsigned) i < 8 * sizeof(ptruint); i += 4) {
00790         mask = (1 << i) - 1;
00791         if (diff <= mask) break;
00792     }
00793     st_free_table(visited);
00794 
00795     /* Build a bit array with the support of f. */
00796     sorted = ALLOC(int,nvars);
00797     if (sorted == NULL) {
00798         dd->errorCode = CUDD_MEMORY_OUT;
00799         goto failure;
00800     }
00801     for (i = 0; i < nvars; i++) sorted[i] = 0;
00802 
00803     /* Take the union of the supports of each output function. */
00804     support = Cudd_VectorSupport(dd,f,n);
00805     if (support == NULL) goto failure;
00806     cuddRef(support);
00807     scan = support;
00808     while (!cuddIsConstant(scan)) {
00809         sorted[scan->index] = 1;
00810         scan = cuddT(scan);
00811     }
00812     Cudd_RecursiveDeref(dd,support);
00813     support = NULL; /* so that we do not try to free it in case of failure */
00814     for (i = 0; i < nvars; i++) {
00815         if (sorted[dd->invperm[i]]) {
00816             if (inames == NULL || inames[dd->invperm[i]] == NULL) {
00817                 retval = fprintf(fp,"v%d", dd->invperm[i]);
00818             } else {
00819                 retval = fprintf(fp,"%s", inames[dd->invperm[i]]);
00820             }
00821             if (retval == EOF) goto failure;
00822         }
00823         retval = fprintf(fp,"%s", i == nvars - 1 ? "\n" : " * ");
00824         if (retval == EOF) goto failure;
00825     }
00826     FREE(sorted);
00827     sorted = NULL;
00828 
00829     /* Initialize symbol table for visited nodes. */
00830     visited = st_init_table(st_ptrcmp, st_ptrhash);
00831     if (visited == NULL) goto failure;
00832 
00833     /* Call the function that really gets the job done. */
00834     for (i = 0; i < n; i++) {
00835         retval = ddDoDumpDDcal(dd,Cudd_Regular(f[i]),fp,visited,inames,mask);
00836         if (retval == 0) goto failure;
00837         if (onames == NULL) {
00838             retval = fprintf(fp, "f%d = ", i);
00839         } else {
00840             retval = fprintf(fp, "%s = ", onames[i]);
00841         }
00842         if (retval == EOF) goto failure;
00843         retval = fprintf(fp, "n%p%s\n",
00844                          (void *) (((ptruint) f[i] & mask) /
00845                          (ptruint) sizeof(DdNode)),
00846                          Cudd_IsComplement(f[i]) ? "'" : "");
00847         if (retval == EOF) goto failure;
00848     }
00849 
00850     /* Write trailer and return. */
00851     retval = fprintf(fp, "[");
00852     if (retval == EOF) goto failure;
00853     for (i = 0; i < n; i++) {
00854         if (onames == NULL) {
00855             retval = fprintf(fp, "f%d", i);
00856         } else {
00857             retval = fprintf(fp, "%s", onames[i]);
00858         }
00859         retval = fprintf(fp, "%s", i == n-1 ? "" : " ");
00860         if (retval == EOF) goto failure;
00861     }
00862     retval = fprintf(fp, "]\n");
00863     if (retval == EOF) goto failure;
00864 
00865     st_free_table(visited);
00866     return(1);
00867 
00868 failure:
00869     if (sorted != NULL) FREE(sorted);
00870     if (support != NULL) Cudd_RecursiveDeref(dd,support);
00871     if (visited != NULL) st_free_table(visited);
00872     return(0);
00873 
00874 } /* end of Cudd_DumpDDcal */
00875 
00876 
00897 int
00898 Cudd_DumpFactoredForm(
00899   DdManager * dd /* manager */,
00900   int  n /* number of output nodes to be dumped */,
00901   DdNode ** f /* array of output nodes to be dumped */,
00902   char ** inames /* array of input names (or NULL) */,
00903   char ** onames /* array of output names (or NULL) */,
00904   FILE * fp /* pointer to the dump file */)
00905 {
00906     int         retval;
00907     int         i;
00908 
00909     /* Call the function that really gets the job done. */
00910     for (i = 0; i < n; i++) {
00911         if (onames == NULL) {
00912             retval = fprintf(fp, "f%d = ", i);
00913         } else {
00914             retval = fprintf(fp, "%s = ", onames[i]);
00915         }
00916         if (retval == EOF) return(0);
00917         if (f[i] == DD_ONE(dd)) {
00918             retval = fprintf(fp, "CONST1");
00919             if (retval == EOF) return(0);
00920         } else if (f[i] == Cudd_Not(DD_ONE(dd)) || f[i] == DD_ZERO(dd)) {
00921             retval = fprintf(fp, "CONST0");
00922             if (retval == EOF) return(0);
00923         } else {
00924             retval = fprintf(fp, "%s", Cudd_IsComplement(f[i]) ? "!(" : "");
00925             if (retval == EOF) return(0);
00926             retval = ddDoDumpFactoredForm(dd,Cudd_Regular(f[i]),fp,inames);
00927             if (retval == 0) return(0);
00928             retval = fprintf(fp, "%s", Cudd_IsComplement(f[i]) ? ")" : "");
00929             if (retval == EOF) return(0);
00930         }
00931         retval = fprintf(fp, "%s", i == n-1 ? "" : "\n");
00932         if (retval == EOF) return(0);
00933     }
00934 
00935     return(1);
00936 
00937 } /* end of Cudd_DumpFactoredForm */
00938 
00939 
00940 /*---------------------------------------------------------------------------*/
00941 /* Definition of internal functions                                          */
00942 /*---------------------------------------------------------------------------*/
00943 
00944 
00945 /*---------------------------------------------------------------------------*/
00946 /* Definition of static functions                                            */
00947 /*---------------------------------------------------------------------------*/
00948 
00949 
00964 static int
00965 ddDoDumpBlif(
00966   DdManager * dd,
00967   DdNode * f,
00968   FILE * fp,
00969   st_table * visited,
00970   char ** names,
00971   int mv)
00972 {
00973     DdNode      *T, *E;
00974     int         retval;
00975 
00976 #ifdef DD_DEBUG
00977     assert(!Cudd_IsComplement(f));
00978 #endif
00979 
00980     /* If already visited, nothing to do. */
00981     if (st_is_member(visited, (char *) f) == 1)
00982         return(1);
00983 
00984     /* Check for abnormal condition that should never happen. */
00985     if (f == NULL)
00986         return(0);
00987 
00988     /* Mark node as visited. */
00989     if (st_insert(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
00990         return(0);
00991 
00992     /* Check for special case: If constant node, generate constant 1. */
00993     if (f == DD_ONE(dd)) {
00994 #if SIZEOF_VOID_P == 8
00995         retval = fprintf(fp, ".names %lx\n1\n",(ptruint) f / (ptruint) sizeof(DdNode));
00996 #else
00997         retval = fprintf(fp, ".names %x\n1\n",(ptruint) f / (ptruint) sizeof(DdNode));
00998 #endif
00999         if (retval == EOF) {
01000             return(0);
01001         } else {
01002             return(1);
01003         }
01004     }
01005 
01006     /* Check whether this is an ADD. We deal with 0-1 ADDs, but not
01007     ** with the general case.
01008     */
01009     if (f == DD_ZERO(dd)) {
01010 #if SIZEOF_VOID_P == 8
01011         retval = fprintf(fp, ".names %lx\n%s",
01012                          (ptruint) f / (ptruint) sizeof(DdNode),
01013                          mv ? "0\n" : "");
01014 #else
01015         retval = fprintf(fp, ".names %x\n%s",
01016                          (ptruint) f / (ptruint) sizeof(DdNode),
01017                          mv ? "0\n" : "");
01018 #endif
01019         if (retval == EOF) {
01020             return(0);
01021         } else {
01022             return(1);
01023         }
01024     }
01025     if (cuddIsConstant(f))
01026         return(0);
01027 
01028     /* Recursive calls. */
01029     T = cuddT(f);
01030     retval = ddDoDumpBlif(dd,T,fp,visited,names,mv);
01031     if (retval != 1) return(retval);
01032     E = Cudd_Regular(cuddE(f));
01033     retval = ddDoDumpBlif(dd,E,fp,visited,names,mv);
01034     if (retval != 1) return(retval);
01035 
01036     /* Write multiplexer taking complement arc into account. */
01037     if (names != NULL) {
01038         retval = fprintf(fp,".names %s", names[f->index]);
01039     } else {
01040 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
01041         retval = fprintf(fp,".names %u", f->index);
01042 #else
01043         retval = fprintf(fp,".names %hu", f->index);
01044 #endif
01045     }
01046     if (retval == EOF)
01047         return(0);
01048 
01049 #if SIZEOF_VOID_P == 8
01050     if (mv) {
01051         if (Cudd_IsComplement(cuddE(f))) {
01052             retval = fprintf(fp," %lx %lx %lx\n.def 0\n1 1 - 1\n0 - 0 1\n",
01053                 (ptruint) T / (ptruint) sizeof(DdNode),
01054                 (ptruint) E / (ptruint) sizeof(DdNode),
01055                 (ptruint) f / (ptruint) sizeof(DdNode));
01056         } else {
01057             retval = fprintf(fp," %lx %lx %lx\n.def 0\n1 1 - 1\n0 - 1 1\n",
01058                 (ptruint) T / (ptruint) sizeof(DdNode),
01059                 (ptruint) E / (ptruint) sizeof(DdNode),
01060                 (ptruint) f / (ptruint) sizeof(DdNode));
01061         }
01062     } else {
01063         if (Cudd_IsComplement(cuddE(f))) {
01064             retval = fprintf(fp," %lx %lx %lx\n11- 1\n0-0 1\n",
01065                 (ptruint) T / (ptruint) sizeof(DdNode),
01066                 (ptruint) E / (ptruint) sizeof(DdNode),
01067                 (ptruint) f / (ptruint) sizeof(DdNode));
01068         } else {
01069             retval = fprintf(fp," %lx %lx %lx\n11- 1\n0-1 1\n",
01070                 (ptruint) T / (ptruint) sizeof(DdNode),
01071                 (ptruint) E / (ptruint) sizeof(DdNode),
01072                 (ptruint) f / (ptruint) sizeof(DdNode));
01073         }
01074     }
01075 #else
01076     if (mv) {
01077         if (Cudd_IsComplement(cuddE(f))) {
01078             retval = fprintf(fp," %x %x %x\n.def 0\n1 1 - 1\n0 - 0 1\n",
01079                 (ptruint) T / (ptruint) sizeof(DdNode),
01080                 (ptruint) E / (ptruint) sizeof(DdNode),
01081                 (ptruint) f / (ptruint) sizeof(DdNode));
01082         } else {
01083             retval = fprintf(fp," %x %x %x\n.def 0\n1 1 - 1\n0 - 1 1\n",
01084                 (ptruint) T / (ptruint) sizeof(DdNode),
01085                 (ptruint) E / (ptruint) sizeof(DdNode),
01086                 (ptruint) f / (ptruint) sizeof(DdNode));
01087         }
01088     } else {
01089         if (Cudd_IsComplement(cuddE(f))) {
01090             retval = fprintf(fp," %x %x %x\n11- 1\n0-0 1\n",
01091                 (ptruint) T / (ptruint) sizeof(DdNode),
01092                 (ptruint) E / (ptruint) sizeof(DdNode),
01093                 (ptruint) f / (ptruint) sizeof(DdNode));
01094         } else {
01095             retval = fprintf(fp," %x %x %x\n11- 1\n0-1 1\n",
01096                 (ptruint) T / (ptruint) sizeof(DdNode),
01097                 (ptruint) E / (ptruint) sizeof(DdNode),
01098                 (ptruint) f / (ptruint) sizeof(DdNode));
01099         }
01100     }
01101 #endif
01102     if (retval == EOF) {
01103         return(0);
01104     } else {
01105         return(1);
01106     }
01107 
01108 } /* end of ddDoDumpBlif */
01109 
01110 
01125 static int
01126 ddDoDumpDaVinci(
01127   DdManager * dd,
01128   DdNode * f,
01129   FILE * fp,
01130   st_table * visited,
01131   char ** names,
01132   ptruint mask)
01133 {
01134     DdNode  *T, *E;
01135     int     retval;
01136     ptruint id;
01137 
01138 #ifdef DD_DEBUG
01139     assert(!Cudd_IsComplement(f));
01140 #endif
01141 
01142     id = ((ptruint) f & mask) / sizeof(DdNode);
01143 
01144     /* If already visited, insert a reference. */
01145     if (st_is_member(visited, (char *) f) == 1) {
01146         retval = fprintf(fp,"r(\"%p\")", (void *) id);
01147         if (retval == EOF) {
01148             return(0);
01149         } else {
01150             return(1);
01151         }
01152     }
01153 
01154     /* Check for abnormal condition that should never happen. */
01155     if (f == NULL)
01156         return(0);
01157 
01158     /* Mark node as visited. */
01159     if (st_insert(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
01160         return(0);
01161 
01162     /* Check for special case: If constant node, generate constant 1. */
01163     if (Cudd_IsConstant(f)) {
01164         retval = fprintf(fp,
01165                          "l(\"%p\",n(\"constant\",[a(\"OBJECT\",\"%g\")],[]))",
01166                          (void *) id, cuddV(f));
01167         if (retval == EOF) {
01168             return(0);
01169         } else {
01170             return(1);
01171         }
01172     }
01173 
01174     /* Recursive calls. */
01175     if (names != NULL) {
01176         retval = fprintf(fp,
01177                          "l(\"%p\",n(\"internal\",[a(\"OBJECT\",\"%s\"),",
01178                          (void *) id, names[f->index]);
01179     } else {
01180         retval = fprintf(fp,
01181 #if SIZEOF_VOID_P == 8
01182                          "l(\"%p\",n(\"internal\",[a(\"OBJECT\",\"%u\"),",
01183 #else
01184                          "l(\"%p\",n(\"internal\",[a(\"OBJECT\",\"%hu\"),",
01185 #endif
01186                          (void *) id, f->index);
01187     }
01188     retval = fprintf(fp, "a(\"_GO\",\"ellipse\")],[e(\"then\",[a(\"EDGECOLOR\",\"blue\"),a(\"_DIR\",\"none\")],");
01189     if (retval == EOF) return(0);
01190     T = cuddT(f);
01191     retval = ddDoDumpDaVinci(dd,T,fp,visited,names,mask);
01192     if (retval != 1) return(retval);
01193     retval = fprintf(fp, "),e(\"else\",[a(\"EDGECOLOR\",\"%s\"),a(\"_DIR\",\"none\")],",
01194                      Cudd_IsComplement(cuddE(f)) ? "red" : "green");
01195     if (retval == EOF) return(0);
01196     E = Cudd_Regular(cuddE(f));
01197     retval = ddDoDumpDaVinci(dd,E,fp,visited,names,mask);
01198     if (retval != 1) return(retval);
01199 
01200     retval = fprintf(fp,")]))");
01201     if (retval == EOF) {
01202         return(0);
01203     } else {
01204         return(1);
01205     }
01206 
01207 } /* end of ddDoDumpDaVinci */
01208 
01209 
01224 static int
01225 ddDoDumpDDcal(
01226   DdManager * dd,
01227   DdNode * f,
01228   FILE * fp,
01229   st_table * visited,
01230   char ** names,
01231   ptruint mask)
01232 {
01233     DdNode  *T, *E;
01234     int     retval;
01235     ptruint id, idT, idE;
01236 
01237 #ifdef DD_DEBUG
01238     assert(!Cudd_IsComplement(f));
01239 #endif
01240 
01241     id = ((ptruint) f & mask) / sizeof(DdNode);
01242 
01243     /* If already visited, do nothing. */
01244     if (st_is_member(visited, (char *) f) == 1) {
01245         return(1);
01246     }
01247 
01248     /* Check for abnormal condition that should never happen. */
01249     if (f == NULL)
01250         return(0);
01251 
01252     /* Mark node as visited. */
01253     if (st_insert(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
01254         return(0);
01255 
01256     /* Check for special case: If constant node, assign constant. */
01257     if (Cudd_IsConstant(f)) {
01258         if (f != DD_ONE(dd) && f != DD_ZERO(dd))
01259             return(0);
01260         retval = fprintf(fp, "n%p = %g\n", (void *) id, cuddV(f));
01261         if (retval == EOF) {
01262             return(0);
01263         } else {
01264             return(1);
01265         }
01266     }
01267 
01268     /* Recursive calls. */
01269     T = cuddT(f);
01270     retval = ddDoDumpDDcal(dd,T,fp,visited,names,mask);
01271     if (retval != 1) return(retval);
01272     E = Cudd_Regular(cuddE(f));
01273     retval = ddDoDumpDDcal(dd,E,fp,visited,names,mask);
01274     if (retval != 1) return(retval);
01275     idT = ((ptruint) T & mask) / sizeof(DdNode);
01276     idE = ((ptruint) E & mask) / sizeof(DdNode);
01277     if (names != NULL) {
01278         retval = fprintf(fp, "n%p = %s * n%p + %s' * n%p%s\n",
01279                          (void *) id, names[f->index],
01280                          (void *) idT, names[f->index],
01281                          (void *) idE, Cudd_IsComplement(cuddE(f)) ? "'" : "");
01282     } else {
01283 #if SIZEOF_VOID_P == 8
01284         retval = fprintf(fp, "n%p = v%u * n%p + v%u' * n%p%s\n",
01285 #else
01286         retval = fprintf(fp, "n%p = v%hu * n%p + v%hu' * n%p%s\n",
01287 #endif
01288                          (void *) id, f->index,
01289                          (void *) idT, f->index,
01290                          (void *) idE, Cudd_IsComplement(cuddE(f)) ? "'" : "");
01291     }
01292     if (retval == EOF) {
01293         return(0);
01294     } else {
01295         return(1);
01296     }
01297 
01298 } /* end of ddDoDumpDDcal */
01299 
01300 
01318 static int
01319 ddDoDumpFactoredForm(
01320   DdManager * dd,
01321   DdNode * f,
01322   FILE * fp,
01323   char ** names)
01324 {
01325     DdNode      *T, *E;
01326     int         retval;
01327 
01328 #ifdef DD_DEBUG
01329     assert(!Cudd_IsComplement(f));
01330     assert(!Cudd_IsConstant(f));
01331 #endif
01332 
01333     /* Check for abnormal condition that should never happen. */
01334     if (f == NULL)
01335         return(0);
01336 
01337     /* Recursive calls. */
01338     T = cuddT(f);
01339     E = cuddE(f);
01340     if (T != DD_ZERO(dd)) {
01341         if (E != DD_ONE(dd)) {
01342             if (names != NULL) {
01343                 retval = fprintf(fp, "%s", names[f->index]);
01344             } else {
01345 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
01346                 retval = fprintf(fp, "x%u", f->index);
01347 #else
01348                 retval = fprintf(fp, "x%hu", f->index);
01349 #endif
01350             }
01351             if (retval == EOF) return(0);
01352         }
01353         if (T != DD_ONE(dd)) {
01354             retval = fprintf(fp, "%s(", E != DD_ONE(dd) ? " * " : "");
01355             if (retval == EOF) return(0);
01356             retval = ddDoDumpFactoredForm(dd,T,fp,names);
01357             if (retval != 1) return(retval);
01358             retval = fprintf(fp, ")");
01359             if (retval == EOF) return(0);
01360         }
01361         if (E == Cudd_Not(DD_ONE(dd)) || E == DD_ZERO(dd)) return(1);
01362         retval = fprintf(fp, " + ");
01363         if (retval == EOF) return(0);
01364     }
01365     E = Cudd_Regular(E);
01366     if (T != DD_ONE(dd)) {
01367         if (names != NULL) {
01368             retval = fprintf(fp, "!%s", names[f->index]);
01369         } else {
01370 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
01371             retval = fprintf(fp, "!x%u", f->index);
01372 #else
01373             retval = fprintf(fp, "!x%hu", f->index);
01374 #endif
01375         }
01376         if (retval == EOF) return(0);
01377     }
01378     if (E != DD_ONE(dd)) {
01379         retval = fprintf(fp, "%s%s(", T != DD_ONE(dd) ? " * " : "",
01380                          E != cuddE(f) ? "!" : "");
01381         if (retval == EOF) return(0);
01382         retval = ddDoDumpFactoredForm(dd,E,fp,names);
01383         if (retval != 1) return(retval);
01384         retval = fprintf(fp, ")");
01385         if (retval == EOF) return(0);
01386     }
01387     return(1);
01388 
01389 } /* end of ddDoDumpFactoredForm */