distr/nanotrav/main.c

   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-2004, 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
  74 static char rcsid[] UTIL_UNUSED = "$Id: main.c,v 1.40 2009/02/21 06:00:31 fabio Exp fabio $";
  75 #endif
  76
  77 static  char    buffer[BUFLENGTH];
  78 #ifdef DD_DEBUG
  79 extern  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
  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);
 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 ******************************************************************************/
 121 int
 122 main(
 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 ******************************************************************************/
 522 static NtrOptions *
 523 mainInit(
 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 ******************************************************************************/
 620 static void
 621 ntrReadOptions(
 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
1029 usage:  /* 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 ******************************************************************************/
1059 static void
1060 ntrReadOptionsFile(
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 ******************************************************************************/
1114 static char*
1115 readLine(
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 ******************************************************************************/
1168 static FILE *
1169 open_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 *****************************************************************************/
1198 static int
1199 reorder(
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 *****************************************************************************/
1277 static void
1278 freeOption(
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 *****************************************************************************/
1308 static DdManager *
1309 startCudd(
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 *****************************************************************************/
1367 static int
1368 ntrReadTree(
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 */