1 /**CFile***********************************************************************
7 Synopsis [Main program for the nanotrav program.]
13 Author [Fabio Somenzi]
15 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
19 Redistribution and use in source and binary forms, with or without
20 modification, are permitted provided that the following conditions
23 Redistributions of source code must retain the above copyright
24 notice, this list of conditions and the following disclaimer.
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.
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.
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.]
47 ******************************************************************************/
52 /*---------------------------------------------------------------------------*/
53 /* Constant declarations */
54 /*---------------------------------------------------------------------------*/
57 "Nanotrav Version #0.12, Release date 2003/12/31"
59 #define BUFLENGTH 8192
61 /*---------------------------------------------------------------------------*/
62 /* Stucture declarations */
63 /*---------------------------------------------------------------------------*/
65 /*---------------------------------------------------------------------------*/
66 /* Type declarations */
67 /*---------------------------------------------------------------------------*/
69 /*---------------------------------------------------------------------------*/
70 /* Variable declarations */
71 /*---------------------------------------------------------------------------*/
74 static char rcsid
[] UTIL_UNUSED
= "$Id: main.c,v 1.40 2009/02/21 06:00:31 fabio Exp fabio $";
77 static char buffer
[BUFLENGTH
];
79 extern st_table
*checkMinterms (BnetNetwork
*net
, DdManager
*dd
, st_table
*previous
);
82 /*---------------------------------------------------------------------------*/
83 /* Macro declarations */
84 /*---------------------------------------------------------------------------*/
86 /**AutomaticStart*************************************************************/
88 /*---------------------------------------------------------------------------*/
89 /* Static function prototypes */
90 /*---------------------------------------------------------------------------*/
92 static NtrOptions
* mainInit ();
93 static void ntrReadOptions (int argc
, char **argv
, NtrOptions
*option
);
94 static void ntrReadOptionsFile (char *name
, char ***argv
, int *argc
);
95 static char* readLine (FILE *fp
);
96 static FILE * open_file (char *filename
, const char *mode
);
97 static int reorder (BnetNetwork
*net
, DdManager
*dd
, NtrOptions
*option
);
98 static void freeOption (NtrOptions
*option
);
99 static DdManager
* startCudd (NtrOptions
*option
, int nvars
);
100 static int ntrReadTree (DdManager
*dd
, char *treefile
, int nvars
);
102 /**AutomaticEnd***************************************************************/
104 /*---------------------------------------------------------------------------*/
105 /* Definition of exported functions */
106 /*---------------------------------------------------------------------------*/
108 /**Function********************************************************************
110 Synopsis [Main program for ntr.]
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.]
120 ******************************************************************************/
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 */
144 ntrReadOptions(argc
,argv
,option
);
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.
153 if (option
->traverse
== TRUE
|| option
->envelope
== TRUE
||
154 option
->scc
== TRUE
) {
155 option
->locGlob
= BNET_GLOBAL_DD
;
158 /* Read the first network... */
159 fp1
= open_file(option
->file1
, "r");
160 net1
= Bnet_ReadNetwork(fp1
,pr
);
163 (void) fprintf(stderr
,"Syntax error in %s.\n",option
->file1
);
166 /* ... and optionally echo it to the standard output. */
168 Bnet_PrintNetwork(net1
);
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
);
178 (void) fprintf(stderr
,"Syntax error in %s.\n",option
->file2
);
181 /* ... and optionally echo it to the standard output. */
183 Bnet_PrintNetwork(net2
);
187 /* Initialize manager. We start with 0 variables, because
188 ** Ntr_buildDDs will create new variables rather than using
189 ** whatever already exists.
191 dd
= startCudd(option
,net1
->ninputs
);
192 if (dd
== NULL
) { exit(2); }
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); }
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
;
203 result
= Ntr_buildDDs(net2
,dd
,option
,net1
);
204 option
->node
= nodesave
;
205 if (result
== 0) { exit(2); }
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
);
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);
224 /* Perform final reordering */
225 if (option
->zddtest
== FALSE
) {
226 result
= reorder(net1
,dd
,option
);
227 if (result
== 0) exit(2);
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);
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
)) {
243 (void) fprintf(stdout
,"%s:",node
->name
);
244 Cudd_PrintDebug(dd
,node
->dd
,Cudd_ReadSize(dd
),pr
);
246 for (i
= 0; i
< net1
->nlatches
; i
++) {
247 if (!st_lookup(net1
->hash
,net1
->latches
[i
][1],&node
)) {
250 (void) fprintf(stdout
,"%s:",node
->name
);
251 Cudd_PrintDebug(dd
,node
->dd
,Cudd_ReadSize(dd
),pr
);
254 result
= Cudd_PrintLinear(dd
);
255 if (result
== 0) exit(2);
260 /* Verify (combinational) equivalence. */
261 if (option
->verify
== TRUE
) {
262 result
= Ntr_VerifyEquivalence(dd
,net1
,net2
,option
);
264 (void) printf("Verification abnormally terminated\n");
266 } else if (result
== -1) {
267 (void) printf("Combinational verification failed\n");
269 (void) printf("Verification succeeded\n");
273 /* Traverse if requested and if the circuit is sequential. */
274 result
= Ntr_Trav(dd
,net1
,option
);
275 if (result
== 0) exit(2);
277 /* Traverse with trasitive closure. */
278 result
= Ntr_ClosureTrav(dd
,net1
,option
);
279 if (result
== 0) exit(2);
281 /* Compute outer envelope if requested and if the circuit is sequential. */
282 if (option
->envelope
== TRUE
&& net1
->nlatches
> 0) {
284 T
= Ntr_buildTR(dd
,net1
,option
,option
->image
);
285 result
= Ntr_Envelope(dd
,T
,NULL
,option
);
289 /* Compute SCCs if requested and if the circuit is sequential. */
290 result
= Ntr_SCC(dd
,net1
,option
);
291 if (result
== 0) exit(2);
293 /* Test Constrain Decomposition. */
294 if (option
->partition
== TRUE
&& net1
->nlatches
> 0) {
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
);
307 for (i
= 0; i
< Cudd_ReadSize(dd
); i
++) {
308 DdNode
*intermediate
= Cudd_bddAnd(dd
, product
, decomp
[i
]);
309 if (intermediate
== NULL
) {
312 Cudd_Ref(intermediate
);
313 Cudd_IterDerefBdd(dd
, product
);
314 product
= intermediate
;
316 if (product
!= T
->part
[0])
318 Cudd_IterDerefBdd(dd
, product
);
319 for (i
= 0; i
< Cudd_ReadSize(dd
); i
++) {
320 Cudd_IterDerefBdd(dd
, decomp
[i
]);
326 /* Test char-to-vect conversion. */
327 result
= Ntr_TestCharToVect(dd
,net1
,option
);
328 if (result
== 0) exit(2);
330 /* Test extraction of two-literal clauses. */
331 result
= Ntr_TestTwoLiteralClauses(dd
,net1
,option
);
332 if (result
== 0) exit(2);
334 /* Test BDD minimization functions. */
335 result
= Ntr_TestMinimization(dd
,net1
,net2
,option
);
336 if (result
== 0) exit(2);
338 /* Test density-related functions. */
339 result
= Ntr_TestDensity(dd
,net1
,option
);
340 if (result
== 0) exit(2);
342 /* Test decomposition functions. */
343 result
= Ntr_TestDecomp(dd
,net1
,option
);
344 if (result
== 0) exit(2);
346 /* Test cofactor estimation functions. */
347 result
= Ntr_TestCofactorEstimate(dd
,net1
,option
);
348 if (result
== 0) exit(2);
350 /* Test BDD clipping functions. */
351 result
= Ntr_TestClipping(dd
,net1
,net2
,option
);
352 if (result
== 0) exit(2);
354 /* Test BDD equivalence and containment under DC functions. */
355 result
= Ntr_TestEquivAndContain(dd
,net1
,net2
,option
);
356 if (result
== 0) exit(2);
358 /* Test BDD Cudd_bddClosestCube. */
359 result
= Ntr_TestClosestCube(dd
,net1
,option
);
360 if (result
== 0) exit(2);
362 /* Test ZDDs if requested. */
363 if (option
->stateOnly
== FALSE
&& option
->zddtest
== TRUE
) {
364 result
= Ntr_testZDD(dd
,net1
,option
);
366 (void) fprintf(stdout
,"ZDD test failed.\n");
367 result
= Ntr_testISOP(dd
,net1
,option
);
369 (void) fprintf(stdout
,"ISOP test failed.\n");
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
);
376 (void) fprintf(stdout
,"Maxflow computation failed.\n");
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
);
383 (void) fprintf(stdout
,"Shortest paths computation failed.\n");
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
)) {
393 signatures
= Cudd_CofMinterm(dd
, node
->dd
);
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
]);
403 (void) printf("Signature computation failed.\n");
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
)) {
418 result
= Bnet_bddArrayDump(dd
,net1
,option
->dumpfile
,&(node
->dd
),
419 &(node
->name
),1,option
->dumpFmt
);
421 result
= Bnet_bddDump(dd
, net1
, option
->dumpfile
,
422 option
->dumpFmt
, reencoded
);
425 (void) printf("BDD dump failed.\n");
429 /* Print stats and clean up. */
431 result
= Cudd_PrintInfo(dd
,stdout
);
433 (void) printf("Cudd_PrintInfo failed.\n");
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
));
441 (void) printf("Final size: %ld\n", Cudd_ReadNodeCount(dd
));
443 /* Dispose of node BDDs. */
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
);
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
) {
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
);
467 Bnet_FreeNetwork(net2
);
470 /* Check reference counts: At this point we should have dereferenced
471 ** everything we had, except in the case of re-encoding.
473 exitval
= Cudd_CheckZeroRef(dd
);
474 ok
= exitval
!= 0; /* ok == 0 means O.K. */
476 (void) fflush(stdout
);
477 (void) fprintf(stderr
,
478 "%d non-zero DD reference counts after dereferencing\n", exitval
);
487 if (pr
>= 0) (void) printf("total time = %s\n",
488 util_print_time(util_cpu_time() - option
->initialTime
));
490 if (pr
>= 0) util_print_cpu_stats(stdout
);
502 /*---------------------------------------------------------------------------*/
503 /* Definition of internal functions */
504 /*---------------------------------------------------------------------------*/
506 /*---------------------------------------------------------------------------*/
507 /* Definition of static functions */
508 /*---------------------------------------------------------------------------*/
511 /**Function********************************************************************
513 Synopsis [Allocates the option structure and initializes it.]
519 SeeAlso [ntrReadOptions]
521 ******************************************************************************/
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
;
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
;
560 option
->dontcares
= FALSE
;
561 option
->closestCube
= FALSE
;
562 option
->clauses
= FALSE
;
563 option
->noBuild
= FALSE
;
564 option
->stateOnly
= FALSE
;
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
;
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
;
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
;
602 } /* end of mainInit */
605 /**Function********************************************************************
607 Synopsis [Reads the command line options.]
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.]
615 SideEffects [May initialize the random number generator.]
617 SeeAlso [mainInit ntrReadOptionsFile]
619 ******************************************************************************/
628 if (argc
< 2) goto usage
;
630 if (STRING_EQUAL(argv
[1],"-f")) {
631 ntrReadOptionsFile(argv
[2],&argv
,&argc
);
634 for (i
= 1; i
< argc
; i
++) {
635 if (argv
[i
][0] != '-' ) {
636 if (option
->file1
== NULL
) {
637 option
->file1
= util_strsav(argv
[i
]);
641 } else if (STRING_EQUAL(argv
[i
],"-second")) {
643 option
->file2
= util_strsav(argv
[i
]);
644 option
->second
= TRUE
;
645 } else if (STRING_EQUAL(argv
[i
],"-verify")) {
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")) {
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
;
667 } else if (STRING_EQUAL(argv
[i
],"-depth")) {
669 option
->imageClip
= (double) atof(argv
[i
]);
670 } else if (STRING_EQUAL(argv
[i
],"-cdepth")) {
672 option
->closureClip
= (double) atof(argv
[i
]);
673 } else if (STRING_EQUAL(argv
[i
],"-approx")) {
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
;
682 } else if (STRING_EQUAL(argv
[i
],"-threshold")) {
684 option
->threshold
= (int) atoi(argv
[i
]);
685 } else if (STRING_EQUAL(argv
[i
],"-from")) {
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
;
704 } else if (STRING_EQUAL(argv
[i
],"-groupnsps")) {
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
;
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")) {
721 } else if (STRING_EQUAL(argv
[i
],"-maxflow")) {
722 option
->maxflow
= TRUE
;
723 } else if (STRING_EQUAL(argv
[i
],"-shortpaths")) {
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
;
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")) {
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")) {
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")) {
762 option
->clip
= (double) atof(argv
[i
]);
764 option
->file2
= util_strsav(argv
[i
]);
765 } else if (STRING_EQUAL(argv
[i
],"-dctest")) {
766 option
->dontcares
= TRUE
;
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")) {
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")) {
787 option
->cacheSize
= (int) atoi(argv
[i
]);
788 } else if (STRING_EQUAL(argv
[i
],"-maxmem")) {
790 option
->maxMemory
= 1048576 * (int) atoi(argv
[i
]);
791 } else if (STRING_EQUAL(argv
[i
],"-memhard")) {
793 option
->maxMemHard
= 1048576 * (int) atoi(argv
[i
]);
794 } else if (STRING_EQUAL(argv
[i
],"-maxlive")) {
796 option
->maxLive
= (unsigned int) atoi(argv
[i
]);
797 } else if (STRING_EQUAL(argv
[i
],"-slots")) {
799 option
->slots
= (int) atoi(argv
[i
]);
800 } else if (STRING_EQUAL(argv
[i
],"-ordering")) {
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
;
809 } else if (STRING_EQUAL(argv
[i
],"-order")) {
811 option
->ordering
= PI_PS_GIVEN
;
812 option
->orderPiPs
= util_strsav(argv
[i
]);
813 } else if (STRING_EQUAL(argv
[i
],"-reordering")) {
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
;
861 } else if (STRING_EQUAL(argv
[i
],"-autodyn")) {
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")) {
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
;
915 } else if (STRING_EQUAL(argv
[i
],"-tree")) {
917 option
->treefile
= util_strsav(argv
[i
]);
918 } else if (STRING_EQUAL(argv
[i
],"-first")) {
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")) {
925 option
->maxGrowth
= (int)atoi(argv
[i
]);
926 } else if (STRING_EQUAL(argv
[i
],"-groupcheck")) {
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
;
951 } else if (STRING_EQUAL(argv
[i
],"-arcviolation")) {
953 option
->arcviolation
= (int)atoi(argv
[i
]);
954 } else if (STRING_EQUAL(argv
[i
],"-symmviolation")) {
956 option
->symmviolation
= (int)atoi(argv
[i
]);
957 } else if (STRING_EQUAL(argv
[i
],"-recomb")) {
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")) {
966 } else if (STRING_EQUAL(argv
[i
],"-genepop")) {
969 option
->populationSize
= (int)atoi(argv
[i
]);
970 } else if (STRING_EQUAL(argv
[i
],"-genexover")) {
973 option
->numberXovers
= (int) atoi(argv
[i
]);
974 } else if (STRING_EQUAL(argv
[i
],"-seed")) {
976 Cudd_Srandom((long)atoi(argv
[i
]));
977 } else if (STRING_EQUAL(argv
[i
],"-dumpfile")) {
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")) {
993 option
->store
= (int) atoi(argv
[i
]);
994 } else if (STRING_EQUAL(argv
[i
],"-storefile")) {
996 option
->storefile
= util_strsav(argv
[i
]);
997 } else if (STRING_EQUAL(argv
[i
],"-loadfile")) {
1000 option
->loadfile
= util_strsav(argv
[i
]);
1001 } else if (STRING_EQUAL(argv
[i
],"-p")) {
1003 option
->verb
= (int) atoi(argv
[i
]);
1009 if (option
->store
>= 0 && option
->storefile
== NULL
) {
1010 (void) fprintf(stdout
,"-storefile mandatory with -store\n");
1014 if (option
->verb
>= 0) {
1015 (void) printf("# %s\n", NTR_VERSION
);
1016 /* echo command line and arguments */
1018 for (i
= 0; i
< argc
; i
++) {
1019 (void) printf(" %s", argv
[i
]);
1021 (void) printf("\n");
1022 (void) printf("# CUDD Version ");
1023 Cudd_PrintVersion(stdout
);
1024 (void) fflush(stdout
);
1029 usage
: /* convenient goto */
1030 printf("Usage: please read man page\n");
1032 (void) fprintf(stdout
,"too few arguments\n");
1034 (void) fprintf(stdout
,"option: %s is not defined\n",argv
[i
]);
1038 } /* end of ntrReadOptions */
1041 /**Function********************************************************************
1043 Synopsis [Reads the program options from a file.]
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.]
1058 ******************************************************************************/
1071 if ((fp
= fopen(name
,"r")) == NULL
) {
1072 fprintf(stderr
,"Error: can not find cmd file %s\n",name
);
1076 slot
= ALLOC(char *,1024);
1078 line
= readLine(fp
);
1086 } else if ( c
!= ' ' && flag
== TRUE
) {
1092 } while ( *line
!= '\0');
1100 } /* end of ntrReadOptionsFile */
1103 /**Function********************************************************************
1105 Synopsis [Reads a line from the option file.]
1113 ******************************************************************************/
1123 /* Strip white space from beginning of line. */
1126 if ( c
== EOF
) return(NULL
);
1129 return(buffer
); /* got a blank line */
1131 if ( c
!= ' ') break;
1134 if ( c
== '\\' ) { /* if we have a continuation character.. */
1135 do { /* scan to end of line */
1137 if ( c
== '\n' ) break;
1138 } while ( c
!= EOF
);
1142 } else return( buffer
);
1146 *pbuffer
= (char) c
;
1149 } while( c
!= '\n' && c
!= EOF
);
1153 } /* end of readLine */
1156 /**Function********************************************************************
1158 Synopsis [Opens a file.]
1160 Description [Opens a file, or fails with an error message and exits.
1161 Allows '-' as a synonym for standard input.]
1167 ******************************************************************************/
1175 if (strcmp(filename
, "-") == 0) {
1176 return mode
[0] == 'r' ? stdin
: stdout
;
1177 } else if ((fp
= fopen(filename
, mode
)) == NULL
) {
1183 } /* end of open_file */
1186 /**Function********************************************************************
1188 Synopsis [Applies reordering to the DDs.]
1190 Description [Explicitly applies reordering to the DDs. Returns 1 if
1191 successful; 0 otherwise.]
1197 *****************************************************************************/
1201 DdManager
* dd
/* DD Manager */,
1202 NtrOptions
* option
)
1205 st_table
*mintermTable
; /* minterm counts for each output */
1207 int result
; /* return value from functions */
1209 (void) printf("Number of inputs = %d\n",net
->ninputs
);
1211 /* Perform the final reordering */
1212 if (option
->reordering
!= CUDD_REORDER_NONE
) {
1214 result
= Cudd_DebugCheck(dd
);
1216 (void) fprintf(stderr
,"Error reported by Cudd_DebugCheck\n");
1219 result
= Cudd_CheckKeys(dd
);
1221 (void) fprintf(stderr
,"Error reported by Cudd_CheckKeys\n");
1224 mintermTable
= checkMinterms(net
,dd
,NULL
);
1225 if (mintermTable
== NULL
) exit(2);
1228 dd
->siftMaxVar
= 1000000;
1229 dd
->siftMaxSwap
= 1000000000;
1230 result
= Cudd_ReduceHeap(dd
,option
->reordering
,1);
1231 if (result
== 0) return(0);
1233 result
= Cudd_DebugCheck(dd
);
1235 (void) fprintf(stderr
,"Error reported by Cudd_DebugCheck\n");
1238 result
= Cudd_CheckKeys(dd
);
1240 (void) fprintf(stderr
,"Error reported by Cudd_CheckKeys\n");
1243 mintermTable
= checkMinterms(net
,dd
,mintermTable
);
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);
1253 if (option
->gaOnOff
) {
1254 result
= Cudd_ReduceHeap(dd
,CUDD_REORDER_GENETIC
,1);
1256 (void) printf("Something went wrong in cuddGa\n");
1263 } /* end of reorder */
1266 /**Function********************************************************************
1268 Synopsis [Frees the option structure and its appendages.]
1276 *****************************************************************************/
1279 NtrOptions
* option
)
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
);
1292 } /* end of freeOption */
1295 /**Function********************************************************************
1297 Synopsis [Starts the CUDD manager with the desired options.]
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.]
1307 *****************************************************************************/
1310 NtrOptions
* option
,
1316 dd
= Cudd_Init(0, 0, option
->slots
, option
->cacheSize
, option
->maxMemory
);
1317 if (dd
== NULL
) return(NULL
);
1319 if (option
->maxMemHard
!= 0) {
1320 Cudd_SetMaxMemory(dd
,option
->maxMemHard
);
1322 Cudd_SetMaxLive(dd
,option
->maxLive
);
1323 Cudd_SetGroupcheck(dd
,option
->groupcheck
);
1324 if (option
->autoDyn
& 1) {
1325 Cudd_AutodynEnable(dd
,option
->autoMethod
);
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
);
1341 result
= Cudd_EnableReorderingReporting(dd
);
1343 (void) fprintf(stderr
,
1344 "Error reported by Cudd_EnableReorderingReporting\n");
1352 } /* end of startCudd */
1355 /**Function********************************************************************
1357 Synopsis [Reads the variable group tree from a file.]
1359 Description [Reads the variable group tree from a file.
1360 Returns 1 if successful; 0 otherwise.]
1366 *****************************************************************************/
1376 if (treefile
== NULL
) {
1380 if ((fp
= fopen(treefile
,"r")) == NULL
) {
1381 (void) fprintf(stderr
,"Unable to open %s\n",treefile
);
1385 root
= Mtr_ReadGroups(fp
,ddMax(Cudd_ReadSize(dd
),nvars
));
1390 Cudd_SetTree(dd
,root
);
1394 } /* end of ntrReadTree */