source: icGREP/icgrep-devel/cudd-2.5.1/nanotrav/main.c

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

Upload of the CUDD library.

File size: 43.4 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [main.c]
4
5  PackageName [ntr]
6
7  Synopsis    [Main program for the nanotrav program.]
8
9  Description []
10
11  SeeAlso     []
12
13  Author      [Fabio Somenzi]
14
15  Copyright   [Copyright (c) 1995-2012, Regents of the University of Colorado
16
17  All rights reserved.
18
19  Redistribution and use in source and binary forms, with or without
20  modification, are permitted provided that the following conditions
21  are met:
22
23  Redistributions of source code must retain the above copyright
24  notice, this list of conditions and the following disclaimer.
25
26  Redistributions in binary form must reproduce the above copyright
27  notice, this list of conditions and the following disclaimer in the
28  documentation and/or other materials provided with the distribution.
29
30  Neither the name of the University of Colorado nor the names of its
31  contributors may be used to endorse or promote products derived from
32  this software without specific prior written permission.
33
34  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
35  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
36  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
37  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
38  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
39  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
40  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
41  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
42  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
43  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
44  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
45  POSSIBILITY OF SUCH DAMAGE.]
46
47******************************************************************************/
48
49#include "ntr.h"
50#include "cuddInt.h"
51
52/*---------------------------------------------------------------------------*/
53/* Constant declarations                                                     */
54/*---------------------------------------------------------------------------*/
55
56#define NTR_VERSION\
57    "Nanotrav Version #0.12, Release date 2003/12/31"
58
59#define BUFLENGTH 8192
60
61/*---------------------------------------------------------------------------*/
62/* Stucture declarations                                                     */
63/*---------------------------------------------------------------------------*/
64
65/*---------------------------------------------------------------------------*/
66/* Type declarations                                                         */
67/*---------------------------------------------------------------------------*/
68
69/*---------------------------------------------------------------------------*/
70/* Variable declarations                                                     */
71/*---------------------------------------------------------------------------*/
72
73#ifndef lint
74static char rcsid[] UTIL_UNUSED = "$Id: main.c,v 1.41 2012/02/05 01:53:01 fabio Exp fabio $";
75#endif
76
77static  char    buffer[BUFLENGTH];
78#ifdef DD_DEBUG
79extern  st_table *checkMinterms (BnetNetwork *net, DdManager *dd, st_table *previous);
80#endif
81
82/*---------------------------------------------------------------------------*/
83/* Macro declarations                                                        */
84/*---------------------------------------------------------------------------*/
85
86/**AutomaticStart*************************************************************/
87
88/*---------------------------------------------------------------------------*/
89/* Static function prototypes                                                */
90/*---------------------------------------------------------------------------*/
91
92static NtrOptions * mainInit ();
93static void ntrReadOptions (int argc, char **argv, NtrOptions *option);
94static void ntrReadOptionsFile (char *name, char ***argv, int *argc);
95static char* readLine (FILE *fp);
96static FILE * open_file (char *filename, const char *mode);
97static int reorder (BnetNetwork *net, DdManager *dd, NtrOptions *option);
98static void freeOption (NtrOptions *option);
99static DdManager * startCudd (NtrOptions *option, int nvars);
100static int ntrReadTree (DdManager *dd, char *treefile, int nvars);
101
102/**AutomaticEnd***************************************************************/
103
104/*---------------------------------------------------------------------------*/
105/* Definition of exported functions                                          */
106/*---------------------------------------------------------------------------*/
107
108/**Function********************************************************************
109
110  Synopsis    [Main program for ntr.]
111
112  Description [Main program for ntr. Performs initialization. Reads command
113  line options and network(s). Builds BDDs with reordering, and optionally
114  does reachability analysis. Prints stats.]
115
116  SideEffects [None]
117
118  SeeAlso     []
119
120******************************************************************************/
121int
122main(
123  int  argc,
124  char ** argv)
125{
126    NtrOptions  *option;        /* options */
127    FILE        *fp1;           /* first network file pointer */
128    BnetNetwork *net1 = NULL;   /* first network */
129    FILE        *fp2;           /* second network file pointer */
130    BnetNetwork *net2 = NULL;   /* second network */
131    DdManager   *dd;            /* pointer to DD manager */
132    int         exitval;        /* return value of Cudd_CheckZeroRef */
133    int         ok;             /* overall return value from main() */
134    int         result;         /* stores the return value of functions */
135    BnetNode    *node;          /* auxiliary pointer to network node */
136    int         i;              /* loop index */
137    int         j;              /* loop index */
138    double      *signatures;    /* array of signatures */
139    int         pr;             /* verbosity level */
140    int         reencoded;      /* linear transformations attempted */
141
142    /* Initialize. */
143    option = mainInit();
144    ntrReadOptions(argc,argv,option);
145    pr = option->verb;
146    reencoded = option->reordering == CUDD_REORDER_LINEAR ||
147                option->reordering == CUDD_REORDER_LINEAR_CONVERGE ||
148                option->autoMethod == CUDD_REORDER_LINEAR ||
149                option->autoMethod == CUDD_REORDER_LINEAR_CONVERGE;
150    /* Currently traversal requires global BDDs. Override whatever
151    ** was specified for locGlob.
152    */
153    if (option->traverse == TRUE || option->envelope == TRUE ||
154        option->scc == TRUE) {
155        option->locGlob = BNET_GLOBAL_DD;
156    }
157
158    /* Read the first network... */
159    fp1 = open_file(option->file1, "r");
160    net1 = Bnet_ReadNetwork(fp1,pr);
161    (void) fclose(fp1);
162    if (net1 == NULL) {
163        (void) fprintf(stderr,"Syntax error in %s.\n",option->file1);
164        exit(2);
165    }
166    /* ... and optionally echo it to the standard output. */
167    if (pr > 2) {
168        Bnet_PrintNetwork(net1);
169    }
170
171    /* Read the second network... */
172    if (option->verify == TRUE || option->second == TRUE ||
173        option->clip > 0.0 || option->dontcares) {
174        fp2 = open_file(option->file2, "r");
175        net2 = Bnet_ReadNetwork(fp2,pr);
176        (void) fclose(fp2);
177        if (net2 == NULL) {
178            (void) fprintf(stderr,"Syntax error in %s.\n",option->file2);
179            exit(2);
180        }
181        /* ... and optionally echo it to the standard output. */
182        if (pr > 2) {
183            Bnet_PrintNetwork(net2);
184        }
185    }
186
187    /* Initialize manager. We start with 0 variables, because
188    ** Ntr_buildDDs will create new variables rather than using
189    ** whatever already exists.
190    */
191    dd = startCudd(option,net1->ninputs);
192    if (dd == NULL) { exit(2); }
193
194    /* Build the BDDs for the nodes of the first network. */
195    result = Ntr_buildDDs(net1,dd,option,NULL);
196    if (result == 0) { exit(2); }
197
198    /* Build the BDDs for the nodes of the second network if requested. */
199    if (option->verify == TRUE || option->second == TRUE ||
200        option->clip > 0.0 || option->dontcares == TRUE) {
201        char *nodesave = option->node;
202        option->node = NULL;
203        result = Ntr_buildDDs(net2,dd,option,net1);
204        option->node = nodesave;
205        if (result == 0) { exit(2); }
206    }
207
208    if (option->noBuild == TRUE) {
209        Bnet_FreeNetwork(net1);
210        if (option->verify == TRUE || option->second == TRUE ||
211            option->clip > 0.0) {
212            Bnet_FreeNetwork(net2);
213        }
214        freeOption(option);
215        exit(0);
216    }
217    if (option->locGlob != BNET_LOCAL_DD) {
218        /* Print the order before the final reordering. */
219        (void) printf("Order before final reordering\n");
220        result = Bnet_PrintOrder(net1,dd);
221        if (result == 0) exit(2);
222    }
223
224    /* Perform final reordering */
225    if (option->zddtest == FALSE) {
226        result = reorder(net1,dd,option);
227        if (result == 0) exit(2);
228
229        /* Print final order. */
230        if ((option->reordering != CUDD_REORDER_NONE || option->gaOnOff) &&
231            option->locGlob != BNET_LOCAL_DD) {
232            (void) printf("New order\n");
233            result = Bnet_PrintOrder(net1,dd);
234            if (result == 0) exit(2);
235        }
236
237        /* Print the re-encoded inputs. */
238        if (pr >= 1 && reencoded == 1) {
239            for (i = 0; i < net1->npis; i++) {
240                if (!st_lookup(net1->hash,net1->inputs[i],&node)) {
241                    exit(2);
242                }
243                (void) fprintf(stdout,"%s:",node->name);
244                Cudd_PrintDebug(dd,node->dd,Cudd_ReadSize(dd),pr);
245            }
246            for (i = 0; i < net1->nlatches; i++) {
247                if (!st_lookup(net1->hash,net1->latches[i][1],&node)) {
248                    exit(2);
249                }
250                (void) fprintf(stdout,"%s:",node->name);
251                Cudd_PrintDebug(dd,node->dd,Cudd_ReadSize(dd),pr);
252            }
253            if (pr >= 3) {
254                result = Cudd_PrintLinear(dd);
255                if (result == 0) exit(2);
256            }
257        }
258    }
259
260    /* Verify (combinational) equivalence. */
261    if (option->verify == TRUE) {
262        result = Ntr_VerifyEquivalence(dd,net1,net2,option);
263        if (result == 0) {
264            (void) printf("Verification abnormally terminated\n");
265            exit(2);
266        } else if (result == -1) {
267            (void) printf("Combinational verification failed\n");
268        } else {
269            (void) printf("Verification succeeded\n");
270        }
271    }
272
273    /* Traverse if requested and if the circuit is sequential. */
274    result = Ntr_Trav(dd,net1,option);
275    if (result == 0) exit(2);
276
277    /* Traverse with trasitive closure. */
278    result = Ntr_ClosureTrav(dd,net1,option);
279    if (result == 0) exit(2);
280
281    /* Compute outer envelope if requested and if the circuit is sequential. */
282    if (option->envelope == TRUE && net1->nlatches > 0) {
283        NtrPartTR *T;
284        T = Ntr_buildTR(dd,net1,option,option->image);
285        result = Ntr_Envelope(dd,T,NULL,option);
286        Ntr_freeTR(dd,T);
287    }
288
289    /* Compute SCCs if requested and if the circuit is sequential. */
290    result = Ntr_SCC(dd,net1,option);
291    if (result == 0) exit(2);
292
293    /* Test Constrain Decomposition. */
294    if (option->partition == TRUE && net1->nlatches > 0) {
295        NtrPartTR *T;
296        DdNode *product;
297        DdNode **decomp;
298        int sharingSize;
299        T = Ntr_buildTR(dd,net1,option,NTR_IMAGE_MONO);
300        decomp = Cudd_bddConstrainDecomp(dd,T->part[0]);
301        if (decomp == NULL) exit(2);
302        sharingSize = Cudd_SharingSize(decomp, Cudd_ReadSize(dd));
303        (void) fprintf(stdout, "Decomposition Size: %d components %d nodes\n",
304                       Cudd_ReadSize(dd), sharingSize);
305        product = Cudd_ReadOne(dd);
306        Cudd_Ref(product);
307        for (i = 0; i < Cudd_ReadSize(dd); i++) {
308            DdNode *intermediate = Cudd_bddAnd(dd, product, decomp[i]);
309            if (intermediate == NULL) {
310                exit(2);
311            }
312            Cudd_Ref(intermediate);
313            Cudd_IterDerefBdd(dd, product);
314            product = intermediate;
315        }
316        if (product != T->part[0])
317            exit(2);
318        Cudd_IterDerefBdd(dd, product);
319        for (i = 0; i < Cudd_ReadSize(dd); i++) {
320            Cudd_IterDerefBdd(dd, decomp[i]);
321        }
322        FREE(decomp);
323        Ntr_freeTR(dd,T);
324    }
325
326    /* Test char-to-vect conversion. */
327    result = Ntr_TestCharToVect(dd,net1,option);
328    if (result == 0) exit(2);
329
330    /* Test extraction of two-literal clauses. */
331    result = Ntr_TestTwoLiteralClauses(dd,net1,option);
332    if (result == 0) exit(2);
333
334    /* Test BDD minimization functions. */
335    result = Ntr_TestMinimization(dd,net1,net2,option);
336    if (result == 0) exit(2);
337
338    /* Test density-related functions. */
339    result = Ntr_TestDensity(dd,net1,option);
340    if (result == 0) exit(2);
341
342    /* Test decomposition functions. */
343    result = Ntr_TestDecomp(dd,net1,option);
344    if (result == 0) exit(2);
345
346    /* Test cofactor estimation functions. */
347    result = Ntr_TestCofactorEstimate(dd,net1,option);
348    if (result == 0) exit(2);
349
350    /* Test BDD clipping functions. */
351    result = Ntr_TestClipping(dd,net1,net2,option);
352    if (result == 0) exit(2);
353
354    /* Test BDD equivalence and containment under DC functions. */
355    result = Ntr_TestEquivAndContain(dd,net1,net2,option);
356    if (result == 0) exit(2);
357
358    /* Test BDD Cudd_bddClosestCube. */
359    result = Ntr_TestClosestCube(dd,net1,option);
360    if (result == 0) exit(2);
361
362    /* Test ZDDs if requested. */
363    if (option->stateOnly == FALSE && option->zddtest == TRUE) {
364        result = Ntr_testZDD(dd,net1,option);
365        if (result == 0)
366            (void) fprintf(stdout,"ZDD test failed.\n");
367        result = Ntr_testISOP(dd,net1,option);
368        if (result == 0)
369            (void) fprintf(stdout,"ISOP test failed.\n");
370    }
371
372    /* Compute maximum flow if requested and if the circuit is sequential. */
373    if (option->maxflow == TRUE && net1->nlatches > 0) {
374        result = Ntr_maxflow(dd,net1,option);
375        if (result == 0)
376            (void) fprintf(stdout,"Maxflow computation failed.\n");
377    }
378
379    /* Compute shortest paths if requested and if the circuit is sequential. */
380    if (option->shortPath != NTR_SHORT_NONE && net1->nlatches > 0) {
381        result = Ntr_ShortestPaths(dd,net1,option);
382        if (result == 0)
383            (void) fprintf(stdout,"Shortest paths computation failed.\n");
384    }
385
386    /* Compute output signatures if so requested. */
387    if (option->signatures) {
388        (void) printf("Positive cofactor measures\n");
389        for (i = 0; i < net1->noutputs; i++) {
390            if (!st_lookup(net1->hash,net1->outputs[i],&node)) {
391                exit(2);
392            }
393            signatures = Cudd_CofMinterm(dd, node->dd);
394            if (signatures) {
395                (void) printf("%s:\n", node->name);
396                for (j = 0; j < Cudd_ReadSize(dd); j++) {
397                    if((j%5 == 0)&&i) (void) printf("\n");
398                    (void) printf("%5d: %-#8.4g ", j, signatures[j]);
399                }
400                (void) printf("\n");
401                FREE(signatures);
402            } else {
403                (void) printf("Signature computation failed.\n");
404            }
405        }
406    }
407
408    /* Dump BDDs if so requested. */
409    if (option->bdddump && option->second == FALSE &&
410        option->density == FALSE && option->decomp == FALSE &&
411        option->cofest == FALSE && option->clip < 0.0 &&
412        option->scc == FALSE) {
413        (void) printf("Dumping BDDs to %s\n", option->dumpfile);
414        if (option->node != NULL) {
415            if (!st_lookup(net1->hash,option->node,&node)) {
416                exit(2);
417            }
418            result = Bnet_bddArrayDump(dd,net1,option->dumpfile,&(node->dd),
419                                       &(node->name),1,option->dumpFmt);
420        } else {
421            result = Bnet_bddDump(dd, net1, option->dumpfile,
422                                  option->dumpFmt, reencoded);
423        }
424        if (result != 1) {
425            (void) printf("BDD dump failed.\n");
426        }
427    }
428
429    /* Print stats and clean up. */
430    if (pr >= 0) {
431        result = Cudd_PrintInfo(dd,stdout);
432        if (result != 1) {
433            (void) printf("Cudd_PrintInfo failed.\n");
434        }
435    }
436
437#if defined(DD_DEBUG) && !defined(DD_NO_DEATH_ROW)
438    (void) fprintf(dd->err,"%d empty slots in death row\n",
439    cuddTimesInDeathRow(dd,NULL));
440#endif
441    (void) printf("Final size: %ld\n", Cudd_ReadNodeCount(dd));
442
443    /* Dispose of node BDDs. */
444    node = net1->nodes;
445    while (node != NULL) {
446        if (node->dd != NULL &&
447        node->type != BNET_INPUT_NODE &&
448        node->type != BNET_PRESENT_STATE_NODE) {
449            Cudd_IterDerefBdd(dd,node->dd);
450        }
451        node = node->next;
452    }
453    /* Dispose of network. */
454    Bnet_FreeNetwork(net1);
455    /* Do the same cleanup for the second network if it was created. */
456    if (option->verify == TRUE || option->second == TRUE ||
457        option->clip > 0.0 || option->dontcares == TRUE) {
458        node = net2->nodes;
459        while (node != NULL) {
460            if (node->dd != NULL &&
461                node->type != BNET_INPUT_NODE &&
462                node->type != BNET_PRESENT_STATE_NODE) {
463                Cudd_IterDerefBdd(dd,node->dd);
464            }
465            node = node->next;
466        }
467        Bnet_FreeNetwork(net2);
468    }
469
470    /* Check reference counts: At this point we should have dereferenced
471    ** everything we had, except in the case of re-encoding.
472    */
473    exitval = Cudd_CheckZeroRef(dd);
474    ok = exitval != 0;  /* ok == 0 means O.K. */
475    if (exitval != 0) {
476        (void) fflush(stdout);
477        (void) fprintf(stderr,
478            "%d non-zero DD reference counts after dereferencing\n", exitval);
479    }
480
481#ifdef DD_DEBUG
482    Cudd_CheckKeys(dd);
483#endif
484
485    Cudd_Quit(dd);
486
487    if (pr >= 0) (void) printf("total time = %s\n",
488            util_print_time(util_cpu_time() - option->initialTime));
489    freeOption(option);
490    if (pr >= 0) util_print_cpu_stats(stdout);
491
492#ifdef MNEMOSYNE
493    mnem_writestats();
494#endif
495
496    exit(ok);
497    /* NOTREACHED */
498
499} /* end of main */
500
501
502/*---------------------------------------------------------------------------*/
503/* Definition of internal functions                                          */
504/*---------------------------------------------------------------------------*/
505
506/*---------------------------------------------------------------------------*/
507/* Definition of static functions                                            */
508/*---------------------------------------------------------------------------*/
509
510
511/**Function********************************************************************
512
513  Synopsis    [Allocates the option structure and initializes it.]
514
515  Description []
516
517  SideEffects [none]
518
519  SeeAlso     [ntrReadOptions]
520
521******************************************************************************/
522static NtrOptions *
523mainInit(
524   )
525{
526    NtrOptions  *option;
527
528    /* Initialize option structure. */
529    option = ALLOC(NtrOptions,1);
530    option->initialTime    = util_cpu_time();
531    option->verify         = FALSE;
532    option->second         = FALSE;
533    option->file1          = NULL;
534    option->file2          = NULL;
535    option->traverse       = FALSE;
536    option->depend         = FALSE;
537    option->image          = NTR_IMAGE_MONO;
538    option->imageClip      = 1.0;
539    option->approx         = NTR_UNDER_APPROX;
540    option->threshold      = -1;
541    option->from           = NTR_FROM_NEW;
542    option->groupnsps      = NTR_GROUP_NONE;
543    option->closure        = FALSE;
544    option->closureClip    = 1.0;
545    option->envelope       = FALSE;
546    option->scc            = FALSE;
547    option->maxflow        = FALSE;
548    option->shortPath      = NTR_SHORT_NONE;
549    option->selectiveTrace = FALSE;
550    option->zddtest        = FALSE;
551    option->printcover     = FALSE;
552    option->sinkfile       = NULL;
553    option->partition      = FALSE;
554    option->char2vect      = FALSE;
555    option->density        = FALSE;
556    option->quality        = 1.0;
557    option->decomp         = FALSE;
558    option->cofest         = FALSE;
559    option->clip           = -1.0;
560    option->dontcares      = FALSE;
561    option->closestCube    = FALSE;
562    option->clauses        = FALSE;
563    option->noBuild        = FALSE;
564    option->stateOnly      = FALSE;
565    option->node           = NULL;
566    option->locGlob        = BNET_GLOBAL_DD;
567    option->progress       = FALSE;
568    option->cacheSize      = 32768;
569    option->maxMemory      = 0; /* set automatically */
570    option->maxMemHard     = 0; /* don't set */
571    option->maxLive        = ~0; /* very large number */
572    option->slots          = CUDD_UNIQUE_SLOTS;
573    option->ordering       = PI_PS_FROM_FILE;
574    option->orderPiPs      = NULL;
575    option->reordering     = CUDD_REORDER_NONE;
576    option->autoMethod     = CUDD_REORDER_SIFT;
577    option->autoDyn        = 0;
578    option->treefile       = NULL;
579    option->firstReorder   = DD_FIRST_REORDER;
580    option->countDead      = FALSE;
581    option->maxGrowth      = 20;
582    option->groupcheck     = CUDD_GROUP_CHECK7;
583    option->arcviolation   = 10;
584    option->symmviolation  = 10;
585    option->recomb         = DD_DEFAULT_RECOMB;
586    option->nodrop         = TRUE;
587    option->signatures     = FALSE;
588    option->verb           = 0;
589    option->gaOnOff        = 0;
590    option->populationSize = 0; /* use default */
591    option->numberXovers   = 0; /* use default */
592    option->bdddump        = FALSE;
593    option->dumpFmt        = 0; /* dot */
594    option->dumpfile       = NULL;
595    option->store          = -1; /* do not store */
596    option->storefile      = NULL;
597    option->load           = FALSE;
598    option->loadfile       = NULL;
599
600    return(option);
601
602} /* end of mainInit */
603
604
605/**Function********************************************************************
606
607  Synopsis    [Reads the command line options.]
608
609  Description [Reads the command line options. Scans the command line
610  one argument at a time and performs a switch on each arguement it
611  hits.  Some arguemnts also read in the following arg from the list
612  (i.e., -f also gets the filename which should folow.)
613  Gives a usage message and exits if any unrecognized args are found.]
614
615  SideEffects [May initialize the random number generator.]
616
617  SeeAlso     [mainInit ntrReadOptionsFile]
618
619******************************************************************************/
620static void
621ntrReadOptions(
622  int  argc,
623  char ** argv,
624  NtrOptions * option)
625{
626    int i = 0;
627
628    if (argc < 2) goto usage;
629
630    if (STRING_EQUAL(argv[1],"-f")) {
631        ntrReadOptionsFile(argv[2],&argv,&argc);
632    }
633
634    for (i = 1; i < argc; i++) {
635        if (argv[i][0] != '-' ) {
636            if (option->file1 == NULL) {
637                option->file1 = util_strsav(argv[i]);
638            } else {
639                goto usage;
640            }
641        } else if (STRING_EQUAL(argv[i],"-second")) {
642            i++;
643            option->file2 = util_strsav(argv[i]);
644            option->second = TRUE;
645        } else if (STRING_EQUAL(argv[i],"-verify")) {
646            i++;
647            option->file2 = util_strsav(argv[i]);
648            option->verify = TRUE;
649        } else if (STRING_EQUAL(argv[i],"-trav")) {
650            option->traverse = TRUE;
651        } else if (STRING_EQUAL(argv[i],"-depend")) {
652            option->traverse = TRUE;
653            option->depend = TRUE;
654        } else if (STRING_EQUAL(argv[i],"-image")) {
655            i++;
656            if (STRING_EQUAL(argv[i],"part")) {
657                option->image = NTR_IMAGE_PART;
658            } else if (STRING_EQUAL(argv[i],"clip")) {
659                option->image = NTR_IMAGE_CLIP;
660            } else if (STRING_EQUAL(argv[i],"depend")) {
661                option->image = NTR_IMAGE_DEPEND;
662            } else if (STRING_EQUAL(argv[i],"mono")) {
663                option->image = NTR_IMAGE_MONO;
664            } else {
665                goto usage;
666            }
667        } else if (STRING_EQUAL(argv[i],"-depth")) {
668            i++;
669            option->imageClip = (double) atof(argv[i]);
670        } else if (STRING_EQUAL(argv[i],"-cdepth")) {
671            i++;
672            option->closureClip = (double) atof(argv[i]);
673        } else if (STRING_EQUAL(argv[i],"-approx")) {
674            i++;
675            if (STRING_EQUAL(argv[i],"under")) {
676                option->approx = NTR_UNDER_APPROX;
677            } else if (STRING_EQUAL(argv[i],"over")) {
678                option->approx = NTR_OVER_APPROX;
679            } else {
680                goto usage;
681            }
682        } else if (STRING_EQUAL(argv[i],"-threshold")) {
683            i++;
684            option->threshold = (int) atoi(argv[i]);
685        } else if (STRING_EQUAL(argv[i],"-from")) {
686            i++;
687            if (STRING_EQUAL(argv[i],"new")) {
688                option->from = NTR_FROM_NEW;
689            } else if (STRING_EQUAL(argv[i],"reached")) {
690                option->from = NTR_FROM_REACHED;
691            } else if (STRING_EQUAL(argv[i],"restrict")) {
692                option->from = NTR_FROM_RESTRICT;
693            } else if (STRING_EQUAL(argv[i],"compact")) {
694                option->from = NTR_FROM_COMPACT;
695            } else if (STRING_EQUAL(argv[i],"squeeze")) {
696                option->from = NTR_FROM_SQUEEZE;
697            } else if (STRING_EQUAL(argv[i],"subset")) {
698                option->from = NTR_FROM_UNDERAPPROX;
699            } else if (STRING_EQUAL(argv[i],"superset")) {
700                option->from = NTR_FROM_OVERAPPROX;
701            } else {
702                goto usage;
703            }
704        } else if (STRING_EQUAL(argv[i],"-groupnsps")) {
705            i++;
706            if (STRING_EQUAL(argv[i],"none")) {
707                option->groupnsps = NTR_GROUP_NONE;
708            } else if (STRING_EQUAL(argv[i],"default")) {
709                option->groupnsps = NTR_GROUP_DEFAULT;
710            } else if (STRING_EQUAL(argv[i],"fixed")) {
711                option->groupnsps = NTR_GROUP_FIXED;
712            } else {
713                goto usage;
714            }
715        } else if (STRING_EQUAL(argv[i],"-closure")) {
716            option->closure = TRUE;
717        } else if (STRING_EQUAL(argv[i],"-envelope")) {
718            option->envelope = TRUE;
719        } else if (STRING_EQUAL(argv[i],"-scc")) {
720            option->scc = TRUE;
721        } else if (STRING_EQUAL(argv[i],"-maxflow")) {
722            option->maxflow = TRUE;
723        } else if (STRING_EQUAL(argv[i],"-shortpaths")) {
724            i++;
725            if (STRING_EQUAL(argv[i],"none")) {
726                option->shortPath = NTR_SHORT_NONE;
727            } else if (STRING_EQUAL(argv[i],"bellman")) {
728                option->shortPath = NTR_SHORT_BELLMAN;
729            } else if (STRING_EQUAL(argv[i],"floyd")) {
730                option->shortPath = NTR_SHORT_FLOYD;
731            } else if (STRING_EQUAL(argv[i],"square")) {
732                option->shortPath = NTR_SHORT_SQUARE;
733            } else {
734                goto usage;
735            }
736        } else if (STRING_EQUAL(argv[i],"-selective")) {
737            option->selectiveTrace = TRUE;
738        } else if (STRING_EQUAL(argv[i],"-zdd")) {
739            option->zddtest = TRUE;
740        } else if (STRING_EQUAL(argv[i],"-cover")) {
741            option->zddtest = TRUE;
742            option->printcover = TRUE;
743        } else if (STRING_EQUAL(argv[i],"-sink")) {
744            i++;
745            option->maxflow = TRUE;
746            option->sinkfile = util_strsav(argv[i]);
747        } else if (STRING_EQUAL(argv[i],"-part")) {
748            option->partition = TRUE;
749        } else if (STRING_EQUAL(argv[i],"-char2vect")) {
750            option->char2vect = TRUE;
751        } else if (STRING_EQUAL(argv[i],"-density")) {
752            option->density = TRUE;
753        } else if (STRING_EQUAL(argv[i],"-quality")) {
754            i++;
755            option->quality = (double) atof(argv[i]);
756        } else if (STRING_EQUAL(argv[i],"-decomp")) {
757            option->decomp = TRUE;
758        } else if (STRING_EQUAL(argv[i],"-cofest")) {
759            option->cofest = TRUE;
760        } else if (STRING_EQUAL(argv[i],"-clip")) {
761            i++;
762            option->clip = (double) atof(argv[i]);
763            i++;
764            option->file2 = util_strsav(argv[i]);
765        } else if (STRING_EQUAL(argv[i],"-dctest")) {
766            option->dontcares = TRUE;
767            i++;
768            option->file2 = util_strsav(argv[i]);
769        } else if (STRING_EQUAL(argv[i],"-closest")) {
770            option->closestCube = TRUE;
771        } else if (STRING_EQUAL(argv[i],"-clauses")) {
772            option->clauses = TRUE;
773        } else if (STRING_EQUAL(argv[i],"-nobuild")) {
774            option->noBuild = TRUE;
775            option->reordering = CUDD_REORDER_NONE;
776        } else if (STRING_EQUAL(argv[i],"-delta")) {
777            option->stateOnly = TRUE;
778        } else if (STRING_EQUAL(argv[i],"-node")) {
779            i++;
780            option->node = util_strsav(argv[i]);
781        } else if (STRING_EQUAL(argv[i],"-local")) {
782            option->locGlob = BNET_LOCAL_DD;
783        } else if (STRING_EQUAL(argv[i],"-progress")) {
784            option->progress = TRUE;
785        } else if (STRING_EQUAL(argv[i],"-cache")) {
786            i++;
787            option->cacheSize = (int) atoi(argv[i]);
788        } else if (STRING_EQUAL(argv[i],"-maxmem")) {
789            i++;
790            option->maxMemory = 1048576 * (int) atoi(argv[i]);
791        } else if (STRING_EQUAL(argv[i],"-memhard")) {
792            i++;
793            option->maxMemHard = 1048576 * (int) atoi(argv[i]);
794        } else if (STRING_EQUAL(argv[i],"-maxlive")) {
795            i++;
796            option->maxLive = (unsigned int) atoi(argv[i]);
797        } else if (STRING_EQUAL(argv[i],"-slots")) {
798            i++;
799            option->slots = (int) atoi(argv[i]);
800        } else if (STRING_EQUAL(argv[i],"-ordering")) {
801            i++;
802            if (STRING_EQUAL(argv[i],"dfs")) {
803                option->ordering = PI_PS_DFS;
804            } else if (STRING_EQUAL(argv[i],"hw")) {
805                option->ordering = PI_PS_FROM_FILE;
806            } else {
807                goto usage;
808            }
809        } else if (STRING_EQUAL(argv[i],"-order")) {
810            i++;
811            option->ordering = PI_PS_GIVEN;
812            option->orderPiPs = util_strsav(argv[i]);
813        } else if (STRING_EQUAL(argv[i],"-reordering")) {
814            i++;
815            if (STRING_EQUAL(argv[i],"none")) {
816                option->reordering = CUDD_REORDER_NONE;
817            } else if (STRING_EQUAL(argv[i],"random")) {
818                option->reordering = CUDD_REORDER_RANDOM;
819            } else if (STRING_EQUAL(argv[i],"bernard") ||
820                STRING_EQUAL(argv[i],"pivot")) {
821                option->reordering = CUDD_REORDER_RANDOM_PIVOT;
822            } else if (STRING_EQUAL(argv[i],"sifting")) {
823                option->reordering = CUDD_REORDER_SIFT;
824            } else if (STRING_EQUAL(argv[i],"converge")) {
825                option->reordering = CUDD_REORDER_SIFT_CONVERGE;
826            } else if (STRING_EQUAL(argv[i],"symm")) {
827                option->reordering = CUDD_REORDER_SYMM_SIFT;
828            } else if (STRING_EQUAL(argv[i],"cosymm")) {
829                option->reordering = CUDD_REORDER_SYMM_SIFT_CONV;
830            } else if (STRING_EQUAL(argv[i],"tree") ||
831                STRING_EQUAL(argv[i],"group")) {
832                option->reordering = CUDD_REORDER_GROUP_SIFT;
833            } else if (STRING_EQUAL(argv[i],"cotree") ||
834                STRING_EQUAL(argv[i],"cogroup")) {
835                option->reordering = CUDD_REORDER_GROUP_SIFT_CONV;
836            } else if (STRING_EQUAL(argv[i],"win2")) {
837                option->reordering = CUDD_REORDER_WINDOW2;
838            } else if (STRING_EQUAL(argv[i],"win3")) {
839                option->reordering = CUDD_REORDER_WINDOW3;
840            } else if (STRING_EQUAL(argv[i],"win4")) {
841                option->reordering = CUDD_REORDER_WINDOW4;
842            } else if (STRING_EQUAL(argv[i],"win2conv")) {
843                option->reordering = CUDD_REORDER_WINDOW2_CONV;
844            } else if (STRING_EQUAL(argv[i],"win3conv")) {
845                option->reordering = CUDD_REORDER_WINDOW3_CONV;
846            } else if (STRING_EQUAL(argv[i],"win4conv")) {
847                option->reordering = CUDD_REORDER_WINDOW4_CONV;
848            } else if (STRING_EQUAL(argv[i],"annealing")) {
849                option->reordering = CUDD_REORDER_ANNEALING;
850            } else if (STRING_EQUAL(argv[i],"genetic")) {
851                option->reordering = CUDD_REORDER_GENETIC;
852            } else if (STRING_EQUAL(argv[i],"linear")) {
853                option->reordering = CUDD_REORDER_LINEAR;
854            } else if (STRING_EQUAL(argv[i],"linconv")) {
855                option->reordering = CUDD_REORDER_LINEAR_CONVERGE;
856            } else if (STRING_EQUAL(argv[i],"exact")) {
857                option->reordering = CUDD_REORDER_EXACT;
858            } else {
859                goto usage;
860            }
861        } else if (STRING_EQUAL(argv[i],"-autodyn")) {
862            option->autoDyn = 3;
863        } else if (STRING_EQUAL(argv[i],"-autodynB")) {
864            option->autoDyn |= 1;
865        } else if (STRING_EQUAL(argv[i],"-autodynZ")) {
866            option->autoDyn |= 2;
867        } else if (STRING_EQUAL(argv[i],"-automethod")) {
868            i++;
869            if (STRING_EQUAL(argv[i],"none")) {
870                option->autoMethod = CUDD_REORDER_NONE;
871            } else if (STRING_EQUAL(argv[i],"random")) {
872                option->autoMethod = CUDD_REORDER_RANDOM;
873            } else if (STRING_EQUAL(argv[i],"bernard") ||
874                STRING_EQUAL(argv[i],"pivot")) {
875                option->autoMethod = CUDD_REORDER_RANDOM_PIVOT;
876            } else if (STRING_EQUAL(argv[i],"sifting")) {
877                option->autoMethod = CUDD_REORDER_SIFT;
878            } else if (STRING_EQUAL(argv[i],"converge")) {
879                option->autoMethod = CUDD_REORDER_SIFT_CONVERGE;
880            } else if (STRING_EQUAL(argv[i],"symm")) {
881                option->autoMethod = CUDD_REORDER_SYMM_SIFT;
882            } else if (STRING_EQUAL(argv[i],"cosymm")) {
883                option->autoMethod = CUDD_REORDER_SYMM_SIFT_CONV;
884            } else if (STRING_EQUAL(argv[i],"tree") ||
885                STRING_EQUAL(argv[i],"group")) {
886                option->autoMethod = CUDD_REORDER_GROUP_SIFT;
887            } else if (STRING_EQUAL(argv[i],"cotree") ||
888                STRING_EQUAL(argv[i],"cogroup")) {
889                option->autoMethod = CUDD_REORDER_GROUP_SIFT_CONV;
890            } else if (STRING_EQUAL(argv[i],"win2")) {
891                option->autoMethod = CUDD_REORDER_WINDOW2;
892            } else if (STRING_EQUAL(argv[i],"win3")) {
893                option->autoMethod = CUDD_REORDER_WINDOW3;
894            } else if (STRING_EQUAL(argv[i],"win4")) {
895                option->autoMethod = CUDD_REORDER_WINDOW4;
896            } else if (STRING_EQUAL(argv[i],"win2conv")) {
897                option->autoMethod = CUDD_REORDER_WINDOW2_CONV;
898            } else if (STRING_EQUAL(argv[i],"win3conv")) {
899                option->autoMethod = CUDD_REORDER_WINDOW3_CONV;
900            } else if (STRING_EQUAL(argv[i],"win4conv")) {
901                option->autoMethod = CUDD_REORDER_WINDOW4_CONV;
902            } else if (STRING_EQUAL(argv[i],"annealing")) {
903                option->autoMethod = CUDD_REORDER_ANNEALING;
904            } else if (STRING_EQUAL(argv[i],"genetic")) {
905                option->autoMethod = CUDD_REORDER_GENETIC;
906            } else if (STRING_EQUAL(argv[i],"linear")) {
907                option->autoMethod = CUDD_REORDER_LINEAR;
908            } else if (STRING_EQUAL(argv[i],"linconv")) {
909                option->autoMethod = CUDD_REORDER_LINEAR_CONVERGE;
910            } else if (STRING_EQUAL(argv[i],"exact")) {
911                option->autoMethod = CUDD_REORDER_EXACT;
912            } else {
913                goto usage;
914            }
915        } else if (STRING_EQUAL(argv[i],"-tree")) {
916            i++;
917            option->treefile = util_strsav(argv[i]);
918        } else if (STRING_EQUAL(argv[i],"-first")) {
919            i++;
920            option->firstReorder = (int)atoi(argv[i]);
921        } else if (STRING_EQUAL(argv[i],"-countdead")) {
922            option->countDead = TRUE;
923        } else if (STRING_EQUAL(argv[i],"-growth")) {
924            i++;
925            option->maxGrowth = (int)atoi(argv[i]);
926        } else if (STRING_EQUAL(argv[i],"-groupcheck")) {
927            i++;
928            if (STRING_EQUAL(argv[i],"check")) {
929                option->groupcheck = CUDD_GROUP_CHECK;
930            } else if (STRING_EQUAL(argv[i],"nocheck")) {
931                option->groupcheck = CUDD_NO_CHECK;
932            } else if (STRING_EQUAL(argv[i],"check2")) {
933                option->groupcheck = CUDD_GROUP_CHECK2;
934            } else if (STRING_EQUAL(argv[i],"check3")) {
935                option->groupcheck = CUDD_GROUP_CHECK3;
936            } else if (STRING_EQUAL(argv[i],"check4")) {
937                option->groupcheck = CUDD_GROUP_CHECK4;
938            } else if (STRING_EQUAL(argv[i],"check5")) {
939                option->groupcheck = CUDD_GROUP_CHECK5;
940            } else if (STRING_EQUAL(argv[i],"check6")) {
941                option->groupcheck = CUDD_GROUP_CHECK6;
942            } else if (STRING_EQUAL(argv[i],"check7")) {
943                option->groupcheck = CUDD_GROUP_CHECK7;
944            } else if (STRING_EQUAL(argv[i],"check8")) {
945                option->groupcheck = CUDD_GROUP_CHECK8;
946            } else if (STRING_EQUAL(argv[i],"check9")) {
947                option->groupcheck = CUDD_GROUP_CHECK9;
948            } else {
949                goto usage;
950            }
951        } else if (STRING_EQUAL(argv[i],"-arcviolation")) {
952            i++;
953            option->arcviolation = (int)atoi(argv[i]);
954        } else if (STRING_EQUAL(argv[i],"-symmviolation")) {
955            i++;
956            option->symmviolation = (int)atoi(argv[i]);
957        } else if (STRING_EQUAL(argv[i],"-recomb")) {
958            i++;
959            option->recomb = (int)atoi(argv[i]);
960        } else if (STRING_EQUAL(argv[i],"-drop")) {
961            option->nodrop = FALSE;
962        } else if (STRING_EQUAL(argv[i],"-sign")) {
963            option->signatures = TRUE;
964        } else if (STRING_EQUAL(argv[i],"-genetic")) {
965            option->gaOnOff = 1;
966        } else if (STRING_EQUAL(argv[i],"-genepop")) {
967            option->gaOnOff = 1;
968            i++;
969            option->populationSize = (int)atoi(argv[i]);
970        } else if (STRING_EQUAL(argv[i],"-genexover")) {
971            option->gaOnOff = 1;
972            i++;
973            option->numberXovers = (int) atoi(argv[i]);
974        } else if (STRING_EQUAL(argv[i],"-seed")) {
975            i++;
976            Cudd_Srandom((long)atoi(argv[i]));
977        } else if (STRING_EQUAL(argv[i],"-dumpfile")) {
978            i++;
979            option->bdddump = TRUE;
980            option->dumpfile = util_strsav(argv[i]);
981        } else if (STRING_EQUAL(argv[i],"-dumpblif")) {
982            option->dumpFmt = 1; /* blif */
983        } else if (STRING_EQUAL(argv[i],"-dumpdaVinci")) {
984            option->dumpFmt = 2; /* daVinci */
985        } else if (STRING_EQUAL(argv[i],"-dumpddcal")) {
986            option->dumpFmt = 3; /* DDcal */
987        } else if (STRING_EQUAL(argv[i],"-dumpfact")) {
988            option->dumpFmt = 4; /* factored form */
989        } else if (STRING_EQUAL(argv[i],"-dumpmv")) {
990            option->dumpFmt = 5; /* blif-MV */
991        } else if (STRING_EQUAL(argv[i],"-store")) {
992            i++;
993            option->store = (int) atoi(argv[i]);
994        } else if (STRING_EQUAL(argv[i],"-storefile")) {
995            i++;
996            option->storefile = util_strsav(argv[i]);
997        } else if (STRING_EQUAL(argv[i],"-loadfile")) {
998            i++;
999            option->load = 1;
1000            option->loadfile = util_strsav(argv[i]);
1001        } else if (STRING_EQUAL(argv[i],"-p")) {
1002            i++;
1003            option->verb = (int) atoi(argv[i]);
1004        } else {
1005            goto usage;
1006        }
1007    }
1008
1009    if (option->store >= 0 && option->storefile == NULL) {
1010        (void) fprintf(stdout,"-storefile mandatory with -store\n");
1011        exit(-1);
1012    }
1013
1014    if (option->verb >= 0) {
1015        (void) printf("# %s\n", NTR_VERSION);
1016        /* echo command line and arguments */
1017        (void) printf("#");
1018        for (i = 0; i < argc; i++) {
1019            (void) printf(" %s", argv[i]);
1020        }
1021        (void) printf("\n");
1022        (void) printf("# CUDD Version ");
1023        Cudd_PrintVersion(stdout);
1024        (void) fflush(stdout);
1025    }
1026
1027    return;
1028
1029usage:  /* convenient goto */
1030    printf("Usage: please read man page\n");
1031    if (i == 0) {
1032        (void) fprintf(stdout,"too few arguments\n");
1033    } else {
1034        (void) fprintf(stdout,"option: %s is not defined\n",argv[i]);
1035    }
1036    exit(-1);
1037
1038} /* end of ntrReadOptions */
1039
1040
1041/**Function********************************************************************
1042
1043  Synopsis    [Reads the program options from a file.]
1044
1045  Description [Reads the program options from a file. Opens file. Reads
1046  the command line from the otpions file using the read_line func. Scans
1047  the line looking for spaces, each space is a searator and demarks a
1048  new option.  When a space is found, it is changed to a \0 to terminate
1049  that string; then the next value of slot points to the next non-space
1050  character.  There is a limit of 1024 options.
1051  Should produce an error (presently doesn't) on overrun of options, but
1052  this is very unlikely to happen.]
1053
1054  SideEffects [none]
1055
1056  SeeAlso     []
1057
1058******************************************************************************/
1059static void
1060ntrReadOptionsFile(
1061  char * name,
1062  char *** argv,
1063  int * argc)
1064{
1065    char        **slot;
1066    char        *line;
1067    char        c;
1068    int         index,flag;
1069    FILE        *fp;
1070
1071    if ((fp = fopen(name,"r")) == NULL) {
1072        fprintf(stderr,"Error: can not find cmd file %s\n",name);
1073        exit(-1);
1074    }
1075
1076    slot = ALLOC(char *,1024);
1077    index = 1;
1078    line = readLine(fp);
1079    flag = TRUE;
1080
1081    do {
1082        c = *line;
1083        if ( c == ' ')  {
1084            flag = TRUE;
1085            *line = '\0';
1086        } else if ( c != ' ' && flag == TRUE) {
1087            flag = FALSE;
1088            slot[index] = line;
1089            index++;
1090        }
1091        line++;
1092    } while ( *line != '\0');
1093
1094
1095    *argv = slot;
1096    *argc = index;
1097
1098    fclose(fp);
1099
1100} /* end of ntrReadOptionsFile */
1101
1102
1103/**Function********************************************************************
1104
1105  Synopsis    [Reads a line from the option file.]
1106
1107  Description []
1108
1109  SideEffects [none]
1110
1111  SeeAlso     []
1112
1113******************************************************************************/
1114static char*
1115readLine(
1116  FILE * fp)
1117{
1118    int  c;
1119    char *pbuffer;
1120
1121    pbuffer = buffer;
1122
1123    /* Strip white space from beginning of line. */
1124    for(;;) {
1125        c = getc(fp);
1126        if ( c == EOF) return(NULL);
1127        if ( c == '\n') {
1128            *pbuffer = '\0';
1129            return(buffer); /* got a blank line */
1130        }
1131        if ( c != ' ') break;
1132    }
1133    do {
1134        if ( c == '\\' ) { /* if we have a continuation character.. */
1135            do {        /* scan to end of line */
1136                c = getc(fp);
1137                if ( c == '\n' ) break;
1138            } while ( c != EOF);
1139            if ( c != EOF) {
1140                *pbuffer = ' ';
1141                pbuffer++;
1142            } else return( buffer);
1143            c = getc(fp);
1144            continue;
1145        }
1146        *pbuffer = (char) c;
1147        pbuffer++;
1148        c = getc(fp);
1149    } while( c != '\n' &&  c != EOF);
1150    *pbuffer = '\0';
1151    return(buffer);
1152
1153} /* end of readLine */
1154
1155
1156/**Function********************************************************************
1157
1158  Synopsis    [Opens a file.]
1159
1160  Description [Opens a file, or fails with an error message and exits.
1161  Allows '-' as a synonym for standard input.]
1162
1163  SideEffects [None]
1164
1165  SeeAlso     []
1166
1167******************************************************************************/
1168static FILE *
1169open_file(
1170  char * filename,
1171  const char * mode)
1172{
1173    FILE *fp;
1174
1175    if (strcmp(filename, "-") == 0) {
1176        return mode[0] == 'r' ? stdin : stdout;
1177    } else if ((fp = fopen(filename, mode)) == NULL) {
1178        perror(filename);
1179        exit(1);
1180    }
1181    return(fp);
1182
1183} /* end of open_file */
1184
1185
1186/**Function********************************************************************
1187
1188  Synopsis    [Applies reordering to the DDs.]
1189
1190  Description [Explicitly applies reordering to the DDs. Returns 1 if
1191  successful; 0 otherwise.]
1192
1193  SideEffects [None]
1194
1195  SeeAlso     []
1196
1197*****************************************************************************/
1198static int
1199reorder(
1200  BnetNetwork * net,
1201  DdManager * dd /* DD Manager */,
1202  NtrOptions * option)
1203{
1204#ifdef DD_DEBUG
1205    st_table    *mintermTable;  /* minterm counts for each output */
1206#endif
1207    int result;                 /* return value from functions */
1208
1209    (void) printf("Number of inputs = %d\n",net->ninputs);
1210
1211    /* Perform the final reordering */
1212    if (option->reordering != CUDD_REORDER_NONE) {
1213#ifdef DD_DEBUG
1214        result = Cudd_DebugCheck(dd);
1215        if (result != 0) {
1216            (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
1217            return(0);
1218        }
1219        result = Cudd_CheckKeys(dd);
1220        if (result != 0) {
1221            (void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n");
1222            return(0);
1223        }
1224        mintermTable = checkMinterms(net,dd,NULL);
1225        if (mintermTable == NULL) exit(2);
1226#endif
1227
1228        dd->siftMaxVar = 1000000;
1229        dd->siftMaxSwap = 1000000000;
1230        result = Cudd_ReduceHeap(dd,option->reordering,1);
1231        if (result == 0) return(0);
1232#ifdef DD_DEBUG
1233        result = Cudd_DebugCheck(dd);
1234        if (result != 0) {
1235            (void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
1236            return(0);
1237        }
1238        result = Cudd_CheckKeys(dd);
1239        if (result != 0) {
1240            (void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n");
1241            return(0);
1242        }
1243        mintermTable = checkMinterms(net,dd,mintermTable);
1244#endif
1245
1246        /* Print symmetry stats if pertinent */
1247        if (dd->tree == NULL &&
1248            (option->reordering == CUDD_REORDER_SYMM_SIFT ||
1249            option->reordering == CUDD_REORDER_SYMM_SIFT_CONV))
1250            Cudd_SymmProfile(dd,0,dd->size - 1);
1251    }
1252
1253    if (option->gaOnOff) {
1254        result = Cudd_ReduceHeap(dd,CUDD_REORDER_GENETIC,1);
1255        if (result == 0) {
1256            (void) printf("Something went wrong in cuddGa\n");
1257            return(0);
1258        }
1259    }
1260
1261    return(1);
1262
1263} /* end of reorder */
1264
1265
1266/**Function********************************************************************
1267
1268  Synopsis    [Frees the option structure and its appendages.]
1269
1270  Description []
1271
1272  SideEffects [None]
1273
1274  SeeAlso     []
1275
1276*****************************************************************************/
1277static void
1278freeOption(
1279  NtrOptions * option)
1280{
1281    if (option->file1 != NULL) FREE(option->file1);
1282    if (option->file2 != NULL) FREE(option->file2);
1283    if (option->orderPiPs != NULL) FREE(option->orderPiPs);
1284    if (option->treefile != NULL) FREE(option->treefile);
1285    if (option->sinkfile != NULL) FREE(option->sinkfile);
1286    if (option->dumpfile != NULL) FREE(option->dumpfile);
1287    if (option->loadfile != NULL) FREE(option->loadfile);
1288    if (option->storefile != NULL) FREE(option->storefile);
1289    if (option->node != NULL) FREE(option->node);
1290    FREE(option);
1291
1292} /* end of freeOption */
1293
1294
1295/**Function********************************************************************
1296
1297  Synopsis    [Starts the CUDD manager with the desired options.]
1298
1299  Description [Starts the CUDD manager with the desired options.
1300  We start with 0 variables, because Ntr_buildDDs will create new
1301  variables rather than using whatever already exists.]
1302
1303  SideEffects [None]
1304
1305  SeeAlso     []
1306
1307*****************************************************************************/
1308static DdManager *
1309startCudd(
1310  NtrOptions * option,
1311  int  nvars)
1312{
1313    DdManager *dd;
1314    int result;
1315
1316    dd = Cudd_Init(0, 0, option->slots, option->cacheSize, option->maxMemory);
1317    if (dd == NULL) return(NULL);
1318
1319    if (option->maxMemHard != 0) {
1320        Cudd_SetMaxMemory(dd,option->maxMemHard);
1321    }
1322    Cudd_SetMaxLive(dd,option->maxLive);
1323    Cudd_SetGroupcheck(dd,option->groupcheck);
1324    if (option->autoDyn & 1) {
1325        Cudd_AutodynEnable(dd,option->autoMethod);
1326    }
1327    dd->nextDyn = option->firstReorder;
1328    dd->countDead = (option->countDead == FALSE) ? ~0 : 0;
1329    dd->maxGrowth = 1.0 + ((float) option->maxGrowth / 100.0);
1330    dd->recomb = option->recomb;
1331    dd->arcviolation = option->arcviolation;
1332    dd->symmviolation = option->symmviolation;
1333    dd->populationSize = option->populationSize;
1334    dd->numberXovers = option->numberXovers;
1335    result = ntrReadTree(dd,option->treefile,nvars);
1336    if (result == 0) {
1337        Cudd_Quit(dd);
1338        return(NULL);
1339    }
1340#ifndef DD_STATS
1341    result = Cudd_EnableReorderingReporting(dd);
1342    if (result == 0) {
1343        (void) fprintf(stderr,
1344                       "Error reported by Cudd_EnableReorderingReporting\n");
1345        Cudd_Quit(dd);
1346        return(NULL);
1347    }
1348#endif
1349
1350    return(dd);
1351
1352} /* end of startCudd */
1353
1354
1355/**Function********************************************************************
1356
1357  Synopsis    [Reads the variable group tree from a file.]
1358
1359  Description [Reads the variable group tree from a file.
1360  Returns 1 if successful; 0 otherwise.]
1361
1362  SideEffects [None]
1363
1364  SeeAlso     []
1365
1366*****************************************************************************/
1367static int
1368ntrReadTree(
1369  DdManager * dd,
1370  char * treefile,
1371  int  nvars)
1372{
1373    FILE *fp;
1374    MtrNode *root;
1375
1376    if (treefile == NULL) {
1377        return(1);
1378    }
1379
1380    if ((fp = fopen(treefile,"r")) == NULL) {
1381        (void) fprintf(stderr,"Unable to open %s\n",treefile);
1382        return(0);
1383    }
1384
1385    root = Mtr_ReadGroups(fp,ddMax(Cudd_ReadSize(dd),nvars));
1386    if (root == NULL) {
1387        return(0);
1388    }
1389
1390    Cudd_SetTree(dd,root);
1391
1392    return(1);
1393
1394} /* end of ntrReadTree */
Note: See TracBrowser for help on using the repository browser.