distr/nanotrav/bnet.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [bnet.c]
   4
   5   PackageName [bnet]
   6
   7   Synopsis    [Functions to read in a boolean network.]
   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 "bnet.h"
  50
  51 /*---------------------------------------------------------------------------*/
  52 /* Constant declarations                                                     */
  53 /*---------------------------------------------------------------------------*/
  54
  55 #define MAXLENGTH 131072
  56
  57 /*---------------------------------------------------------------------------*/
  58 /* Stucture declarations                                                     */
  59 /*---------------------------------------------------------------------------*/
  60
  61 /*---------------------------------------------------------------------------*/
  62 /* Type declarations                                                         */
  63 /*---------------------------------------------------------------------------*/
  64
  65 /*---------------------------------------------------------------------------*/
  66 /* Variable declarations                                                     */
  67 /*---------------------------------------------------------------------------*/
  68
  69 #ifndef lint
  70 static char rcsid[] UTIL_UNUSED = "$Id: bnet.c,v 1.25 2009/02/21 06:00:31 fabio Exp fabio $";
  71 #endif
  72
  73 static  char    BuffLine[MAXLENGTH];
  74 static  char    *CurPos;
  75 static  int     newNameNumber = 0;
  76
  77 /*---------------------------------------------------------------------------*/
  78 /* Macro declarations                                                        */
  79 /*---------------------------------------------------------------------------*/
  80
  81 /**AutomaticStart*************************************************************/
  82
  83 /*---------------------------------------------------------------------------*/
  84 /* Static function prototypes                                                */
  85 /*---------------------------------------------------------------------------*/
  86
  87 static char * readString (FILE *fp);
  88 static char ** readList (FILE *fp, int *n);
  89 static void printList (char **list, int n);
  90 static char ** bnetGenerateNewNames (st_table *hash, int n);
  91 static int bnetDumpReencodingLogic (DdManager *dd, char *mname, int noutputs, DdNode **outputs, char **inames, char **altnames, char **onames, FILE *fp);
  92 #if 0
  93 static int bnetBlifXnorTable (FILE *fp, int n);
  94 #endif
  95 static int bnetBlifWriteReencode (DdManager *dd, char *mname, char **inames, char **altnames, int *support, FILE *fp);
  96 static int * bnetFindVectorSupport (DdManager *dd, DdNode **list, int n);
  97 static int buildExorBDD (DdManager *dd, BnetNode *nd, st_table *hash, int params, int nodrop);
  98 static int buildMuxBDD (DdManager * dd, BnetNode * nd, st_table * hash, int  params, int  nodrop);
  99 static int bnetSetLevel (BnetNetwork *net);
 100 static int bnetLevelDFS (BnetNetwork *net, BnetNode *node);
 101 static BnetNode ** bnetOrderRoots (BnetNetwork *net, int *nroots);
 102 static int bnetLevelCompare (BnetNode **x, BnetNode **y);
 103 static int bnetDfsOrder (DdManager *dd, BnetNetwork *net, BnetNode *node);
 104
 105 /**AutomaticEnd***************************************************************/
 106
 107 /*---------------------------------------------------------------------------*/
 108 /* Definition of exported functions                                          */
 109 /*---------------------------------------------------------------------------*/
 110
 111
 112 /**Function********************************************************************
 113
 114   Synopsis    [Reads boolean network from blif file.]
 115
 116   Description [Reads a boolean network from a blif file. A very restricted
 117   subset of blif is supported. Specifically:
 118   <ul>
 119   <li> The only directives recognized are:
 120     <ul>
 121     <li> .model
 122     <li> .inputs
 123     <li> .outputs
 124     <li> .latch
 125     <li> .names
 126     <li> .exdc
 127     <li> .wire_load_slope
 128     <li> .end
 129     </ul>
 130   <li> Latches must have an initial values and no other parameters
 131        specified.
 132   <li> Lines must not exceed MAXLENGTH-1 characters, and individual names must
 133        not exceed 1023 characters.
 134   </ul>
 135   Caveat emptor: There may be other limitations as well. One should
 136   check the syntax of the blif file with some other tool before relying
 137   on this parser. Bnet_ReadNetwork returns a pointer to the network if
 138   successful; NULL otherwise.
 139   ]
 140
 141   SideEffects [None]
 142
 143   SeeAlso     [Bnet_PrintNetwork Bnet_FreeNetwork]
 144
 145 ******************************************************************************/
 146 BnetNetwork *
 147 Bnet_ReadNetwork(
 148   FILE * fp /* pointer to the blif file */,
 149   int  pr /* verbosity level */)
 150 {
 151     char *savestring;
 152     char **list;
 153     int i, j, n;
 154     BnetNetwork *net;
 155     BnetNode *newnode;
 156     BnetNode *lastnode = NULL;
 157     BnetTabline *newline;
 158     BnetTabline *lastline;
 159     char ***latches = NULL;
 160     int maxlatches = 0;
 161     int exdc = 0;
 162     BnetNode    *node;
 163     int count;
 164
 165     /* Allocate network object and initialize symbol table. */
 166     net = ALLOC(BnetNetwork,1);
 167     if (net == NULL) goto failure;
 168     memset((char *) net, 0, sizeof(BnetNetwork));
 169     net->hash = st_init_table(strcmp,st_strhash);
 170     if (net->hash == NULL) goto failure;
 171
 172     savestring = readString(fp);
 173     if (savestring == NULL) goto failure;
 174     net->nlatches = 0;
 175     while (strcmp(savestring, ".model") == 0 ||
 176         strcmp(savestring, ".inputs") == 0 ||
 177         strcmp(savestring, ".outputs") == 0 ||
 178         strcmp(savestring, ".latch") == 0 ||
 179         strcmp(savestring, ".wire_load_slope") == 0 ||
 180         strcmp(savestring, ".exdc") == 0 ||
 181         strcmp(savestring, ".names") == 0 || strcmp(savestring,".end") == 0) {
 182         if (strcmp(savestring, ".model") == 0) {
 183             /* Read .model directive. */
 184             FREE(savestring);
 185             /* Read network name. */
 186             savestring = readString(fp);
 187             if (savestring == NULL) goto failure;
 188             net->name = savestring;
 189         } else if (strcmp(savestring, ".inputs") == 0) {
 190             /* Read .inputs directive. */
 191             FREE(savestring);
 192             /* Read input names. */
 193             list = readList(fp,&n);
 194             if (list == NULL) goto failure;
 195             if (pr > 2) printList(list,n);
 196             /* Expect at least one input. */
 197             if (n < 1) {
 198                 (void) fprintf(stdout,"Empty input list.\n");
 199                 goto failure;
 200             }
 201             if (exdc) {
 202                 for (i = 0; i < n; i++)
 203                     FREE(list[i]);
 204                 FREE(list);
 205                 savestring = readString(fp);
 206                 if (savestring == NULL) goto failure;
 207                 continue;
 208             }
 209             if (net->ninputs) {
 210                 net->inputs = REALLOC(char *, net->inputs,
 211                     (net->ninputs + n) * sizeof(char *));
 212                 for (i = 0; i < n; i++)
 213                     net->inputs[net->ninputs + i] = list[i];
 214             }
 215             else
 216                 net->inputs = list;
 217             /* Create a node for each primary input. */
 218             for (i = 0; i < n; i++) {
 219                 newnode = ALLOC(BnetNode,1);
 220                 memset((char *) newnode, 0, sizeof(BnetNode));
 221                 if (newnode == NULL) goto failure;
 222                 newnode->name = list[i];
 223                 newnode->inputs = NULL;
 224                 newnode->type = BNET_INPUT_NODE;
 225                 newnode->active = FALSE;
 226                 newnode->nfo = 0;
 227                 newnode->ninp = 0;
 228                 newnode->f = NULL;
 229                 newnode->polarity = 0;
 230                 newnode->dd = NULL;
 231                 newnode->next = NULL;
 232                 if (lastnode == NULL) {
 233                     net->nodes = newnode;
 234                 } else {
 235                     lastnode->next = newnode;
 236                 }
 237                 lastnode = newnode;
 238             }
 239             net->npis += n;
 240             net->ninputs += n;
 241         } else if (strcmp(savestring, ".outputs") == 0) {
 242             /* Read .outputs directive. We do not create nodes for the primary
 243             ** outputs, because the nodes will be created when the same names
 244             ** appear as outputs of some gates.
 245             */
 246             FREE(savestring);
 247             /* Read output names. */
 248             list = readList(fp,&n);
 249             if (list == NULL) goto failure;
 250             if (pr > 2) printList(list,n);
 251             if (n < 1) {
 252                 (void) fprintf(stdout,"Empty .outputs list.\n");
 253                 goto failure;
 254             }
 255             if (exdc) {
 256                 for (i = 0; i < n; i++)
 257                     FREE(list[i]);
 258                 FREE(list);
 259                 savestring = readString(fp);
 260                 if (savestring == NULL) goto failure;
 261                 continue;
 262             }
 263             if (net->noutputs) {
 264                 net->outputs = REALLOC(char *, net->outputs,
 265                     (net->noutputs + n) * sizeof(char *));
 266                 for (i = 0; i < n; i++)
 267                     net->outputs[net->noutputs + i] = list[i];
 268             } else {
 269                 net->outputs = list;
 270             }
 271             net->npos += n;
 272             net->noutputs += n;
 273         } else if (strcmp(savestring,".wire_load_slope") == 0) {
 274             FREE(savestring);
 275             savestring = readString(fp);
 276             net->slope = savestring;
 277         } else if (strcmp(savestring,".latch") == 0) {
 278             FREE(savestring);
 279             newnode = ALLOC(BnetNode,1);
 280             if (newnode == NULL) goto failure;
 281             memset((char *) newnode, 0, sizeof(BnetNode));
 282             newnode->type = BNET_PRESENT_STATE_NODE;
 283             list = readList(fp,&n);
 284             if (list == NULL) goto failure;
 285             if (pr > 2) printList(list,n);
 286             /* Expect three names. */
 287             if (n != 3) {
 288                 (void) fprintf(stdout,
 289                                ".latch not followed by three tokens.\n");
 290                 goto failure;
 291             }
 292             newnode->name = list[1];
 293             newnode->inputs = NULL;
 294             newnode->ninp = 0;
 295             newnode->f = NULL;
 296             newnode->active = FALSE;
 297             newnode->nfo = 0;
 298             newnode->polarity = 0;
 299             newnode->dd = NULL;
 300             newnode->next = NULL;
 301             if (lastnode == NULL) {
 302                 net->nodes = newnode;
 303             } else {
 304                 lastnode->next = newnode;
 305             }
 306             lastnode = newnode;
 307             /* Add next state variable to list. */
 308             if (maxlatches == 0) {
 309                 maxlatches = 20;
 310                 latches = ALLOC(char **,maxlatches);
 311             } else if (maxlatches <= net->nlatches) {
 312                 maxlatches += 20;
 313                 latches = REALLOC(char **,latches,maxlatches);
 314             }
 315             latches[net->nlatches] = list;
 316             net->nlatches++;
 317             savestring = readString(fp);
 318             if (savestring == NULL) goto failure;
 319         } else if (strcmp(savestring,".names") == 0) {
 320             FREE(savestring);
 321             newnode = ALLOC(BnetNode,1);
 322             memset((char *) newnode, 0, sizeof(BnetNode));
 323             if (newnode == NULL) goto failure;
 324             list = readList(fp,&n);
 325             if (list == NULL) goto failure;
 326             if (pr > 2) printList(list,n);
 327             /* Expect at least one name (the node output). */
 328             if (n < 1) {
 329                 (void) fprintf(stdout,"Missing output name.\n");
 330                 goto failure;
 331             }
 332             newnode->name = list[n-1];
 333             newnode->inputs = list;
 334             newnode->ninp = n-1;
 335             newnode->active = FALSE;
 336             newnode->nfo = 0;
 337             newnode->polarity = 0;
 338             if (newnode->ninp > 0) {
 339                 newnode->type = BNET_INTERNAL_NODE;
 340                 for (i = 0; i < net->noutputs; i++) {
 341                     if (strcmp(net->outputs[i], newnode->name) == 0) {
 342                         newnode->type = BNET_OUTPUT_NODE;
 343                         break;
 344                     }
 345                 }
 346             } else {
 347                 newnode->type = BNET_CONSTANT_NODE;
 348             }
 349             newnode->dd = NULL;
 350             newnode->next = NULL;
 351             if (lastnode == NULL) {
 352                 net->nodes = newnode;
 353             } else {
 354                 lastnode->next = newnode;
 355             }
 356             lastnode = newnode;
 357             /* Read node function. */
 358             newnode->f = NULL;
 359             if (exdc) {
 360                 newnode->exdc_flag = 1;
 361                 node = net->nodes;
 362                 while (node) {
 363                     if (node->type == BNET_OUTPUT_NODE &&
 364                         strcmp(node->name, newnode->name) == 0) {
 365                         node->exdc = newnode;
 366                         break;
 367                     }
 368                     node = node->next;
 369                 }
 370             }
 371             savestring = readString(fp);
 372             if (savestring == NULL) goto failure;
 373             lastline = NULL;
 374             while (savestring[0] != '.') {
 375                 /* Reading a table line. */
 376                 newline = ALLOC(BnetTabline,1);
 377                 if (newline == NULL) goto failure;
 378                 newline->next = NULL;
 379                 if (lastline == NULL) {
 380                     newnode->f = newline;
 381                 } else {
 382                     lastline->next = newline;
 383                 }
 384                 lastline = newline;
 385                 if (newnode->type == BNET_INTERNAL_NODE ||
 386                     newnode->type == BNET_OUTPUT_NODE) {
 387                     newline->values = savestring;
 388                     /* Read output 1 or 0. */
 389                     savestring = readString(fp);
 390                     if (savestring == NULL) goto failure;
 391                 } else {
 392                     newline->values = NULL;
 393                 }
 394                 if (savestring[0] == '0') newnode->polarity = 1;
 395                 FREE(savestring);
 396                 savestring = readString(fp);
 397                 if (savestring == NULL) goto failure;
 398             }
 399         } else if (strcmp(savestring,".exdc") == 0) {
 400             FREE(savestring);
 401             exdc = 1;
 402         } else if (strcmp(savestring,".end") == 0) {
 403             FREE(savestring);
 404             break;
 405         }
 406         if ((!savestring) || savestring[0] != '.')
 407             savestring = readString(fp);
 408         if (savestring == NULL) goto failure;
 409     }
 410
 411     /* Put nodes in symbol table. */
 412     newnode = net->nodes;
 413     while (newnode != NULL) {
 414         int retval = st_insert(net->hash,newnode->name,(char *) newnode);
 415         if (retval == ST_OUT_OF_MEM) {
 416             goto failure;
 417         } else if (retval == 1) {
 418             printf("Error: Multiple drivers for node %s\n", newnode->name);
 419             goto failure;
 420         } else {
 421             if (pr > 2) printf("Inserted %s\n",newnode->name);
 422         }
 423         newnode = newnode->next;
 424     }
 425
 426     if (latches) {
 427         net->latches = latches;
 428
 429         count = 0;
 430         net->outputs = REALLOC(char *, net->outputs,
 431             (net->noutputs + net->nlatches) * sizeof(char *));
 432         for (i = 0; i < net->nlatches; i++) {
 433             for (j = 0; j < net->noutputs; j++) {
 434                 if (strcmp(latches[i][0], net->outputs[j]) == 0)
 435                     break;
 436             }
 437             if (j < net->noutputs)
 438                 continue;
 439             savestring = ALLOC(char, strlen(latches[i][0]) + 1);
 440             strcpy(savestring, latches[i][0]);
 441             net->outputs[net->noutputs + count] = savestring;
 442             count++;
 443             if (st_lookup(net->hash, savestring, &node)) {
 444                 if (node->type == BNET_INTERNAL_NODE) {
 445                     node->type = BNET_OUTPUT_NODE;
 446                 }
 447             }
 448         }
 449         net->noutputs += count;
 450
 451         net->inputs = REALLOC(char *, net->inputs,
 452             (net->ninputs + net->nlatches) * sizeof(char *));
 453         for (i = 0; i < net->nlatches; i++) {
 454             savestring = ALLOC(char, strlen(latches[i][1]) + 1);
 455             strcpy(savestring, latches[i][1]);
 456             net->inputs[net->ninputs + i] = savestring;
 457         }
 458         net->ninputs += net->nlatches;
 459     }
 460
 461     /* Compute fanout counts. For each node in the linked list, fetch
 462     ** all its fanins using the symbol table, and increment the fanout of
 463     ** each fanin.
 464     */
 465     newnode = net->nodes;
 466     while (newnode != NULL) {
 467         BnetNode *auxnd;
 468         for (i = 0; i < newnode->ninp; i++) {
 469             if (!st_lookup(net->hash,newnode->inputs[i],&auxnd)) {
 470                 (void) fprintf(stdout,"%s not driven\n", newnode->inputs[i]);
 471                 goto failure;
 472             }
 473             auxnd->nfo++;
 474         }
 475         newnode = newnode->next;
 476     }
 477
 478     if (!bnetSetLevel(net)) goto failure;
 479
 480     return(net);
 481
 482 failure:
 483     /* Here we should clean up the mess. */
 484     (void) fprintf(stdout,"Error in reading network from file.\n");
 485     return(NULL);
 486
 487 } /* end of Bnet_ReadNetwork */
 488
 489
 490 /**Function********************************************************************
 491
 492   Synopsis    [Prints a boolean network created by readNetwork.]
 493
 494   Description [Prints to the standard output a boolean network created
 495   by Bnet_ReadNetwork. Uses the blif format; this way, one can verify the
 496   equivalence of the input and the output with, say, sis.]
 497
 498   SideEffects [None]
 499
 500   SeeAlso     [Bnet_ReadNetwork]
 501
 502 ******************************************************************************/
 503 void
 504 Bnet_PrintNetwork(
 505   BnetNetwork * net /* boolean network */)
 506 {
 507     BnetNode *nd;
 508     BnetTabline *tl;
 509     int i;
 510
 511     if (net == NULL) return;
 512
 513     (void) fprintf(stdout,".model %s\n", net->name);
 514     (void) fprintf(stdout,".inputs");
 515     printList(net->inputs,net->npis);
 516     (void) fprintf(stdout,".outputs");
 517     printList(net->outputs,net->npos);
 518     for (i = 0; i < net->nlatches; i++) {
 519         (void) fprintf(stdout,".latch");
 520         printList(net->latches[i],3);
 521     }
 522     nd = net->nodes;
 523     while (nd != NULL) {
 524         if (nd->type != BNET_INPUT_NODE && nd->type != BNET_PRESENT_STATE_NODE) {
 525             (void) fprintf(stdout,".names");
 526             for (i = 0; i < nd->ninp; i++) {
 527                 (void) fprintf(stdout," %s",nd->inputs[i]);
 528             }
 529             (void) fprintf(stdout," %s\n",nd->name);
 530             tl = nd->f;
 531             while (tl != NULL) {
 532                 if (tl->values != NULL) {
 533                     (void) fprintf(stdout,"%s %d\n",tl->values,
 534                     1 - nd->polarity);
 535                 } else {
 536                     (void) fprintf(stdout,"%d\n", 1 - nd->polarity);
 537                 }
 538                 tl = tl->next;
 539             }
 540         }
 541         nd = nd->next;
 542     }
 543     (void) fprintf(stdout,".end\n");
 544
 545 } /* end of Bnet_PrintNetwork */
 546
 547
 548 /**Function********************************************************************
 549
 550   Synopsis    [Frees a boolean network created by Bnet_ReadNetwork.]
 551
 552   Description []
 553
 554   SideEffects [None]
 555
 556   SeeAlso     [Bnet_ReadNetwork]
 557
 558 ******************************************************************************/
 559 void
 560 Bnet_FreeNetwork(
 561   BnetNetwork * net)
 562 {
 563     BnetNode *node, *nextnode;
 564     BnetTabline *line, *nextline;
 565     int i;
 566
 567     FREE(net->name);
 568     /* The input name strings are already pointed by the input nodes.
 569     ** Here we only need to free the latch names and the array that
 570     ** points to them.
 571     */
 572     for (i = 0; i < net->nlatches; i++) {
 573         FREE(net->inputs[net->npis + i]);
 574     }
 575     FREE(net->inputs);
 576     /* Free the output name strings and then the array pointing to them.  */
 577     for (i = 0; i < net->noutputs; i++) {
 578         FREE(net->outputs[i]);
 579     }
 580     FREE(net->outputs);
 581
 582     for (i = 0; i < net->nlatches; i++) {
 583         FREE(net->latches[i][0]);
 584         FREE(net->latches[i][1]);
 585         FREE(net->latches[i][2]);
 586         FREE(net->latches[i]);
 587     }
 588     if (net->nlatches) FREE(net->latches);
 589     node = net->nodes;
 590     while (node != NULL) {
 591         nextnode = node->next;
 592         if (node->type != BNET_PRESENT_STATE_NODE)
 593             FREE(node->name);
 594         for (i = 0; i < node->ninp; i++) {
 595             FREE(node->inputs[i]);
 596         }
 597         if (node->inputs != NULL) {
 598             FREE(node->inputs);
 599         }
 600         /* Free the function table. */
 601         line = node->f;
 602         while (line != NULL) {
 603             nextline = line->next;
 604             FREE(line->values);
 605             FREE(line);
 606             line = nextline;
 607         }
 608         FREE(node);
 609         node = nextnode;
 610     }
 611     st_free_table(net->hash);
 612     if (net->slope != NULL) FREE(net->slope);
 613     FREE(net);
 614
 615 } /* end of Bnet_FreeNetwork */
 616
 617
 618 /**Function********************************************************************
 619
 620   Synopsis    [Builds the BDD for the function of a node.]
 621
 622   Description [Builds the BDD for the function of a node and stores a
 623   pointer to it in the dd field of the node itself. The reference count
 624   of the BDD is incremented. If params is BNET_LOCAL_DD, then the BDD is
 625   built in terms of the local inputs to the node; otherwise, if params
 626   is BNET_GLOBAL_DD, the BDD is built in terms of the network primary
 627   inputs. To build the global BDD of a node, the BDDs for its local
 628   inputs must exist. If that is not the case, Bnet_BuildNodeBDD
 629   recursively builds them. Likewise, to create the local BDD for a node,
 630   the local inputs must have variables assigned to them. If that is not
 631   the case, Bnet_BuildNodeBDD recursively assigns variables to nodes.
 632   Bnet_BuildNodeBDD returns 1 in case of success; 0 otherwise.]
 633
 634   SideEffects [Sets the dd field of the node.]
 635
 636   SeeAlso     []
 637
 638 ******************************************************************************/
 639 int
 640 Bnet_BuildNodeBDD(
 641   DdManager * dd /* DD manager */,
 642   BnetNode * nd /* node of the boolean network */,
 643   st_table * hash /* symbol table of the boolean network */,
 644   int  params /* type of DD to be built */,
 645   int  nodrop /* retain the intermediate node DDs until the end */)
 646 {
 647     DdNode *func;
 648     BnetNode *auxnd;
 649     DdNode *tmp;
 650     DdNode *prod, *var;
 651     BnetTabline *line;
 652     int i;
 653
 654     if (nd->dd != NULL) return(1);
 655
 656     if (nd->type == BNET_CONSTANT_NODE) {
 657         if (nd->f == NULL) { /* constant 0 */
 658             func = Cudd_ReadLogicZero(dd);
 659         } else { /* either constant depending on the polarity */
 660             func = Cudd_ReadOne(dd);
 661         }
 662         Cudd_Ref(func);
 663     } else if (nd->type == BNET_INPUT_NODE ||
 664                nd->type == BNET_PRESENT_STATE_NODE) {
 665         if (nd->active == TRUE) { /* a variable is already associated: use it */
 666             func = Cudd_ReadVars(dd,nd->var);
 667             if (func == NULL) goto failure;
 668         } else { /* no variable associated: get a new one */
 669             func = Cudd_bddNewVar(dd);
 670             if (func == NULL) goto failure;
 671             nd->var = func->index;
 672             nd->active = TRUE;
 673         }
 674         Cudd_Ref(func);
 675     } else if (buildExorBDD(dd,nd,hash,params,nodrop)) {
 676         func = nd->dd;
 677     } else if (buildMuxBDD(dd,nd,hash,params,nodrop)) {
 678         func = nd->dd;
 679     } else { /* type == BNET_INTERNAL_NODE or BNET_OUTPUT_NODE */
 680         /* Initialize the sum to logical 0. */
 681         func = Cudd_ReadLogicZero(dd);
 682         Cudd_Ref(func);
 683
 684         /* Build a term for each line of the table and add it to the
 685         ** accumulator (func).
 686         */
 687         line = nd->f;
 688         while (line != NULL) {
 689 #ifdef BNET_DEBUG
 690             (void) fprintf(stdout,"line = %s\n", line->values);
 691 #endif
 692             /* Initialize the product to logical 1. */
 693             prod = Cudd_ReadOne(dd);
 694             Cudd_Ref(prod);
 695             /* Scan the table line. */
 696             for (i = 0; i < nd->ninp; i++) {
 697                 if (line->values[i] == '-') continue;
 698                 if (!st_lookup(hash,nd->inputs[i],&auxnd)) {
 699                     goto failure;
 700                 }
 701                 if (params == BNET_LOCAL_DD) {
 702                     if (auxnd->active == FALSE) {
 703                         if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
 704                             goto failure;
 705                         }
 706                     }
 707                     var = Cudd_ReadVars(dd,auxnd->var);
 708                     if (var == NULL) goto failure;
 709                     Cudd_Ref(var);
 710                     if (line->values[i] == '0') {
 711                         var = Cudd_Not(var);
 712                     }
 713                 } else { /* params == BNET_GLOBAL_DD */
 714                     if (auxnd->dd == NULL) {
 715                         if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
 716                             goto failure;
 717                         }
 718                     }
 719                     if (line->values[i] == '1') {
 720                         var = auxnd->dd;
 721                     } else { /* line->values[i] == '0' */
 722                         var = Cudd_Not(auxnd->dd);
 723                     }
 724                 }
 725                 tmp = Cudd_bddAnd(dd,prod,var);
 726                 if (tmp == NULL) goto failure;
 727                 Cudd_Ref(tmp);
 728                 Cudd_IterDerefBdd(dd,prod);
 729                 if (params == BNET_LOCAL_DD) {
 730                     Cudd_IterDerefBdd(dd,var);
 731                 }
 732                 prod = tmp;
 733             }
 734             tmp = Cudd_bddOr(dd,func,prod);
 735             if (tmp == NULL) goto failure;
 736             Cudd_Ref(tmp);
 737             Cudd_IterDerefBdd(dd,func);
 738             Cudd_IterDerefBdd(dd,prod);
 739             func = tmp;
 740             line = line->next;
 741         }
 742         /* Associate a variable to this node if local BDDs are being
 743         ** built. This is done at the end, so that the primary inputs tend
 744         ** to get lower indices.
 745         */
 746         if (params == BNET_LOCAL_DD && nd->active == FALSE) {
 747             DdNode *auxfunc = Cudd_bddNewVar(dd);
 748             if (auxfunc == NULL) goto failure;
 749             Cudd_Ref(auxfunc);
 750             nd->var = auxfunc->index;
 751             nd->active = TRUE;
 752             Cudd_IterDerefBdd(dd,auxfunc);
 753         }
 754     }
 755     if (nd->polarity == 1) {
 756         nd->dd = Cudd_Not(func);
 757     } else {
 758         nd->dd = func;
 759     }
 760
 761     if (params == BNET_GLOBAL_DD && nodrop == FALSE) {
 762         /* Decrease counters for all faninis.
 763         ** When count reaches 0, the DD is freed.
 764         */
 765         for (i = 0; i < nd->ninp; i++) {
 766             if (!st_lookup(hash,nd->inputs[i],&auxnd)) {
 767                 goto failure;
 768             }
 769             auxnd->count--;
 770             if (auxnd->count == 0) {
 771                 Cudd_IterDerefBdd(dd,auxnd->dd);
 772                 if (auxnd->type == BNET_INTERNAL_NODE ||
 773                     auxnd->type == BNET_CONSTANT_NODE) auxnd->dd = NULL;
 774             }
 775         }
 776     }
 777     return(1);
 778
 779 failure:
 780     /* Here we should clean up the mess. */
 781     return(0);
 782
 783 } /* end of Bnet_BuildNodeBDD */
 784
 785
 786 /**Function********************************************************************
 787
 788   Synopsis    [Orders the BDD variables by DFS.]
 789
 790   Description [Orders the BDD variables by DFS.  Returns 1 in case of
 791   success; 0 otherwise.]
 792
 793   SideEffects [Uses the visited flags of the nodes.]
 794
 795   SeeAlso     []
 796
 797 ******************************************************************************/
 798 int
 799 Bnet_DfsVariableOrder(
 800   DdManager * dd,
 801   BnetNetwork * net)
 802 {
 803     BnetNode **roots;
 804     BnetNode *node;
 805     int nroots;
 806     int i;
 807
 808     roots = bnetOrderRoots(net,&nroots);
 809     if (roots == NULL) return(0);
 810     for (i = 0; i < nroots; i++) {
 811         if (!bnetDfsOrder(dd,net,roots[i])) {
 812             FREE(roots);
 813             return(0);
 814         }
 815     }
 816     /* Clear visited flags. */
 817     node = net->nodes;
 818     while (node != NULL) {
 819         node->visited = 0;
 820         node = node->next;
 821     }
 822     FREE(roots);
 823     return(1);
 824
 825 } /* end of Bnet_DfsVariableOrder */
 826
 827
 828 /**Function********************************************************************
 829
 830   Synopsis    [Writes the network BDDs to a file in dot, blif, or daVinci
 831   format.]
 832
 833   Description [Writes the network BDDs to a file in dot, blif, or daVinci
 834   format. If "-" is passed as file name, the BDDs are dumped to the
 835   standard output. Returns 1 in case of success; 0 otherwise.]
 836
 837   SideEffects [None]
 838
 839   SeeAlso     []
 840
 841 ******************************************************************************/
 842 int
 843 Bnet_bddDump(
 844   DdManager * dd /* DD manager */,
 845   BnetNetwork * network /* network whose BDDs should be dumped */,
 846   char * dfile /* file name */,
 847   int  dumpFmt /* 0 -> dot */,
 848   int  reencoded /* whether variables have been reencoded */)
 849 {
 850     int noutputs;
 851     FILE *dfp = NULL;
 852     DdNode **outputs = NULL;
 853     char **inames = NULL;
 854     char **onames = NULL;
 855     char **altnames = NULL;
 856     BnetNode *node;
 857     int i;
 858     int retval = 0; /* 0 -> failure; 1 -> success */
 859
 860     /* Open dump file. */
 861     if (strcmp(dfile, "-") == 0) {
 862         dfp = stdout;
 863     } else {
 864         dfp = fopen(dfile,"w");
 865     }
 866     if (dfp == NULL) goto endgame;
 867
 868     /* Initialize data structures. */
 869     noutputs = network->noutputs;
 870     outputs = ALLOC(DdNode *,noutputs);
 871     if (outputs == NULL) goto endgame;
 872     onames = ALLOC(char *,noutputs);
 873     if (onames == NULL) goto endgame;
 874     inames = ALLOC(char *,Cudd_ReadSize(dd));
 875     if (inames == NULL) goto endgame;
 876
 877     /* Find outputs and their names. */
 878     for (i = 0; i < network->nlatches; i++) {
 879         onames[i] = network->latches[i][0];
 880         if (!st_lookup(network->hash,network->latches[i][0],&node)) {
 881             goto endgame;
 882         }
 883         outputs[i] = node->dd;
 884     }
 885     for (i = 0; i < network->npos; i++) {
 886         onames[i + network->nlatches] = network->outputs[i];
 887         if (!st_lookup(network->hash,network->outputs[i],&node)) {
 888             goto endgame;
 889         }
 890         outputs[i + network->nlatches] = node->dd;
 891     }
 892
 893     /* Find the input names. */
 894     for (i = 0; i < network->ninputs; i++) {
 895         if (!st_lookup(network->hash,network->inputs[i],&node)) {
 896             goto endgame;
 897         }
 898         inames[node->var] = network->inputs[i];
 899     }
 900     for (i = 0; i < network->nlatches; i++) {
 901         if (!st_lookup(network->hash,network->latches[i][1],&node)) {
 902             goto endgame;
 903         }
 904         inames[node->var] = network->latches[i][1];
 905     }
 906
 907     if (reencoded == 1 && dumpFmt == 1) {
 908         altnames = bnetGenerateNewNames(network->hash,network->ninputs);
 909         if (altnames == NULL) {
 910             retval = 0;
 911             goto endgame;
 912         }
 913         retval = bnetDumpReencodingLogic(dd,network->name,noutputs,outputs,
 914                  inames,altnames,onames,dfp);
 915         for (i = 0; i < network->ninputs; i++) {
 916             FREE(altnames[i]);
 917         }
 918         FREE(altnames);
 919         if (retval == 0) goto endgame;
 920     }
 921
 922     /* Dump the BDDs. */
 923     if (dumpFmt == 1) {
 924         retval = Cudd_DumpBlif(dd,noutputs,outputs,inames,onames,
 925                  network->name,dfp,0);
 926     } else if (dumpFmt == 2) {
 927         retval = Cudd_DumpDaVinci(dd,noutputs,outputs,inames,onames,dfp);
 928     } else if (dumpFmt == 3) {
 929         retval = Cudd_DumpDDcal(dd,noutputs,outputs,inames,onames,dfp);
 930     } else if (dumpFmt == 4) {
 931         retval = Cudd_DumpFactoredForm(dd,noutputs,outputs,inames,onames,dfp);
 932     } else if (dumpFmt == 5) {
 933         retval = Cudd_DumpBlif(dd,noutputs,outputs,inames,onames,
 934                  network->name,dfp,1);
 935     } else {
 936         retval = Cudd_DumpDot(dd,noutputs,outputs,inames,onames,dfp);
 937     }
 938
 939 endgame:
 940     if (dfp != stdout && dfp != NULL) {
 941         if (fclose(dfp) == EOF) retval = 0;
 942     }
 943     if (outputs != NULL) FREE(outputs);
 944     if (onames  != NULL) FREE(onames);
 945     if (inames  != NULL) FREE(inames);
 946
 947     return(retval);
 948
 949 } /* end of Bnet_bddDump */
 950
 951
 952 /**Function********************************************************************
 953
 954   Synopsis    [Writes an array of BDDs to a file in dot, blif, DDcal,
 955   factored-form, daVinci, or blif-MV format.]
 956
 957   Description [Writes an array of BDDs to a file in dot, blif, DDcal,
 958   factored-form, daVinci, or blif-MV format.  The BDDs and their names
 959   are passed as arguments.  The inputs and their names are taken from
 960   the network. If "-" is passed as file name, the BDDs are dumped to
 961   the standard output. Returns 1 in case of success; 0 otherwise.]
 962
 963   SideEffects [None]
 964
 965   SeeAlso     []
 966
 967 ******************************************************************************/
 968 int
 969 Bnet_bddArrayDump(
 970   DdManager * dd /* DD manager */,
 971   BnetNetwork * network /* network whose BDDs should be dumped */,
 972   char * dfile /* file name */,
 973   DdNode ** outputs /* BDDs to be dumped */,
 974   char ** onames /* names of the BDDs to be dumped */,
 975   int  noutputs /* number of BDDs to be dumped */,
 976   int  dumpFmt /* 0 -> dot */)
 977 {
 978     FILE *dfp = NULL;
 979     char **inames = NULL;
 980     BnetNode *node;
 981     int i;
 982     int retval = 0; /* 0 -> failure; 1 -> success */
 983
 984     /* Open dump file. */
 985     if (strcmp(dfile, "-") == 0) {
 986         dfp = stdout;
 987     } else {
 988         dfp = fopen(dfile,"w");
 989     }
 990     if (dfp == NULL) goto endgame;
 991
 992     /* Initialize data structures. */
 993     inames = ALLOC(char *,Cudd_ReadSize(dd));
 994     if (inames == NULL) goto endgame;
 995     for (i = 0; i < Cudd_ReadSize(dd); i++) {
 996         inames[i] = NULL;
 997     }
 998
 999     /* Find the input names. */
1000     for (i = 0; i < network->ninputs; i++) {
1001         if (!st_lookup(network->hash,network->inputs[i],&node)) {
1002             goto endgame;
1003         }
1004         inames[node->var] = network->inputs[i];
1005     }
1006     for (i = 0; i < network->nlatches; i++) {
1007         if (!st_lookup(network->hash,network->latches[i][1],&node)) {
1008             goto endgame;
1009         }
1010         inames[node->var] = network->latches[i][1];
1011     }
1012
1013     /* Dump the BDDs. */
1014     if (dumpFmt == 1) {
1015         retval = Cudd_DumpBlif(dd,noutputs,outputs,inames,onames,
1016                  network->name,dfp,0);
1017     } else if (dumpFmt == 2) {
1018         retval = Cudd_DumpDaVinci(dd,noutputs,outputs,inames,onames,dfp);
1019     } else if (dumpFmt == 3) {
1020         retval = Cudd_DumpDDcal(dd,noutputs,outputs,inames,onames,dfp);
1021     } else if (dumpFmt == 4) {
1022         retval = Cudd_DumpFactoredForm(dd,noutputs,outputs,inames,onames,dfp);
1023     } else if (dumpFmt == 5) {
1024         retval = Cudd_DumpBlif(dd,noutputs,outputs,inames,onames,
1025                  network->name,dfp,1);
1026     } else {
1027         retval = Cudd_DumpDot(dd,noutputs,outputs,inames,onames,dfp);
1028     }
1029
1030 endgame:
1031     if (dfp != stdout && dfp != NULL) {
1032         if (fclose(dfp) == EOF) retval = 0;
1033     }
1034     if (inames  != NULL) FREE(inames);
1035
1036     return(retval);
1037
1038 } /* end of Bnet_bddArrayDump */
1039
1040
1041 /**Function********************************************************************
1042
1043   Synopsis    [Reads the variable order from a file.]
1044
1045   Description [Reads the variable order from a file.
1046   Returns 1 if successful; 0 otherwise.]
1047
1048   SideEffects [The BDDs for the primary inputs and present state variables
1049   are built.]
1050
1051   SeeAlso     []
1052
1053 *****************************************************************************/
1054 int
1055 Bnet_ReadOrder(
1056   DdManager * dd,
1057   char * ordFile,
1058   BnetNetwork * net,
1059   int  locGlob,
1060   int  nodrop)
1061 {
1062     FILE *fp;
1063     st_table *dict;
1064     int result;
1065     BnetNode *node;
1066     char name[MAXLENGTH];
1067
1068     if (ordFile == NULL) {
1069         return(0);
1070     }
1071
1072     dict = st_init_table(strcmp,st_strhash);
1073     if (dict == NULL) {
1074         return(0);
1075     }
1076
1077     if ((fp = fopen(ordFile,"r")) == NULL) {
1078         (void) fprintf(stderr,"Unable to open %s\n",ordFile);
1079         st_free_table(dict);
1080         return(0);
1081     }
1082
1083     while (!feof(fp)) {
1084         result = fscanf(fp, "%s", name);
1085         if (result == EOF) {
1086             break;
1087         } else if (result != 1) {
1088             st_free_table(dict);
1089             return(0);
1090         } else if (strlen(name) > MAXLENGTH) {
1091             st_free_table(dict);
1092             return(0);
1093         }
1094         /* There should be a node named "name" in the network. */
1095         if (!st_lookup(net->hash,name,&node)) {
1096             (void) fprintf(stderr,"Unknown name in order file (%s)\n", name);
1097             st_free_table(dict);
1098             return(0);
1099         }
1100         /* A name should not appear more than once in the order. */
1101         if (st_is_member(dict,name)) {
1102             (void) fprintf(stderr,"Duplicate name in order file (%s)\n", name);
1103             st_free_table(dict);
1104             return(0);
1105         }
1106         /* The name should correspond to a primary input or present state. */
1107         if (node->type != BNET_INPUT_NODE &&
1108             node->type != BNET_PRESENT_STATE_NODE) {
1109             (void) fprintf(stderr,"%s has the wrong type (%d)\n", name,
1110                            node->type);
1111             st_free_table(dict);
1112             return(0);
1113         }
1114         /* Insert in table. Use node->name rather than name, because the
1115         ** latter gets overwritten.
1116         */
1117         if (st_insert(dict,node->name,NULL) == ST_OUT_OF_MEM) {
1118             (void) fprintf(stderr,"Out of memory in Bnet_ReadOrder\n");
1119             st_free_table(dict);
1120             return(0);
1121         }
1122         result = Bnet_BuildNodeBDD(dd,node,net->hash,locGlob,nodrop);
1123         if (result == 0) {
1124             (void) fprintf(stderr,"Construction of BDD failed\n");
1125             st_free_table(dict);
1126             return(0);
1127         }
1128     } /* while (!feof(fp)) */
1129     result = fclose(fp);
1130     if (result == EOF) {
1131         (void) fprintf(stderr,"Error closing order file %s\n", ordFile);
1132         st_free_table(dict);
1133         return(0);
1134     }
1135
1136     /* The number of names in the order file should match exactly the
1137     ** number of primary inputs and present states.
1138     */
1139     if (st_count(dict) != net->ninputs) {
1140         (void) fprintf(stderr,"Order incomplete: %d names instead of %d\n",
1141                        st_count(dict), net->ninputs);
1142         st_free_table(dict);
1143         return(0);
1144     }
1145
1146     st_free_table(dict);
1147     return(1);
1148
1149 } /* end of Bnet_ReadOrder */
1150
1151
1152 /**Function********************************************************************
1153
1154   Synopsis    [Prints the order of the DD variables of a network.]
1155
1156   Description [Prints the order of the DD variables of a network.
1157   Only primary inputs and present states are printed.
1158   Returns 1 if successful; 0 otherwise.]
1159
1160   SideEffects [None]
1161
1162   SeeAlso     []
1163
1164 *****************************************************************************/
1165 int
1166 Bnet_PrintOrder(
1167   BnetNetwork * net,
1168   DdManager *dd)
1169 {
1170     char **names;               /* array used to print variable orders */
1171     int level;                  /* position of a variable in current order */
1172     BnetNode *node;             /* auxiliary pointer to network node */
1173     int i,j;
1174     int retval;
1175     int nvars;
1176
1177     nvars = Cudd_ReadSize(dd);
1178     names = ALLOC(char *, nvars);
1179     if (names == NULL) return(0);
1180     for (i = 0; i < nvars; i++) {
1181         names[i] = NULL;
1182     }
1183     for (i = 0; i < net->npis; i++) {
1184         if (!st_lookup(net->hash,net->inputs[i],&node)) {
1185             FREE(names);
1186             return(0);
1187         }
1188         if (node->dd == NULL) {
1189             FREE(names);
1190             return(0);
1191         }
1192         level = Cudd_ReadPerm(dd,node->var);
1193         names[level] = node->name;
1194     }
1195     for (i = 0; i < net->nlatches; i++) {
1196         if (!st_lookup(net->hash,net->latches[i][1],&node)) {
1197             FREE(names);
1198             return(0);
1199         }
1200         if (node->dd == NULL) {
1201             FREE(names);
1202             return(0);
1203         }
1204         level = Cudd_ReadPerm(dd,node->var);
1205         names[level] = node->name;
1206     }
1207     for (i = 0, j = 0; i < nvars; i++) {
1208         if (names[i] == NULL) continue;
1209         if ((j%8 == 0)&&j) {
1210             retval = printf("\n");
1211             if (retval == EOF) {
1212                 FREE(names);
1213                 return(0);
1214             }
1215         }
1216         retval = printf("%s ",names[i]);
1217         if (retval == EOF) {
1218             FREE(names);
1219             return(0);
1220         }
1221         j++;
1222     }
1223     FREE(names);
1224     retval = printf("\n");
1225     if (retval == EOF) {
1226         return(0);
1227     }
1228     return(1);
1229
1230 } /* end of Bnet_PrintOrder */
1231
1232
1233 /*---------------------------------------------------------------------------*/
1234 /* Definition of internal functions                                          */
1235 /*---------------------------------------------------------------------------*/
1236
1237 /*---------------------------------------------------------------------------*/
1238 /* Definition of static functions                                            */
1239 /*---------------------------------------------------------------------------*/
1240
1241
1242 /**Function********************************************************************
1243
1244   Synopsis    [Reads a string from a file.]
1245
1246   Description [Reads a string from a file. The string can be MAXLENGTH-1
1247   characters at most. readString allocates memory to hold the string and
1248   returns a pointer to the result if successful. It returns NULL
1249   otherwise.]
1250
1251   SideEffects [None]
1252
1253   SeeAlso     [readList]
1254
1255 ******************************************************************************/
1256 static char *
1257 readString(
1258   FILE * fp /* pointer to the file from which the string is read */)
1259 {
1260     char *savestring;
1261     int length;
1262
1263     while (!CurPos) {
1264         if (!fgets(BuffLine, MAXLENGTH, fp))
1265             return(NULL);
1266         BuffLine[strlen(BuffLine) - 1] = '\0';
1267         CurPos = strtok(BuffLine, " \t");
1268         if (CurPos && CurPos[0] == '#') CurPos = (char *)NULL;
1269     }
1270     length = strlen(CurPos);
1271     savestring = ALLOC(char,length+1);
1272     if (savestring == NULL)
1273         return(NULL);
1274     strcpy(savestring,CurPos);
1275     CurPos = strtok(NULL, " \t");
1276     return(savestring);
1277
1278 } /* end of readString */
1279
1280
1281 /**Function********************************************************************
1282
1283   Synopsis    [Reads a list of strings from a file.]
1284
1285   Description [Reads a list of strings from a line of a file.
1286   The strings are sequences of characters separated by spaces or tabs.
1287   The total length of the list, white space included, must not exceed
1288   MAXLENGTH-1 characters.  readList allocates memory for the strings and
1289   creates an array of pointers to the individual lists. Only two pieces
1290   of memory are allocated by readList: One to hold all the strings,
1291   and one to hold the pointers to them. Therefore, when freeing the
1292   memory allocated by readList, only the pointer to the list of
1293   pointers, and the pointer to the beginning of the first string should
1294   be freed. readList returns the pointer to the list of pointers if
1295   successful; NULL otherwise.]
1296
1297   SideEffects [n is set to the number of strings in the list.]
1298
1299   SeeAlso     [readString printList]
1300
1301 ******************************************************************************/
1302 static char **
1303 readList(
1304   FILE * fp /* pointer to the file from which the list is read */,
1305   int * n /* on return, number of strings in the list */)
1306 {
1307     char        *savestring;
1308     int         length;
1309     char        *stack[8192];
1310     char        **list;
1311     int         i, count = 0;
1312
1313     while (CurPos) {
1314         if (strcmp(CurPos, "\\") == 0) {
1315             CurPos = (char *)NULL;
1316             while (!CurPos) {
1317                 if (!fgets(BuffLine, MAXLENGTH, fp)) return(NULL);
1318                 BuffLine[strlen(BuffLine) - 1] = '\0';
1319                 CurPos = strtok(BuffLine, " \t");
1320             }
1321         }
1322         length = strlen(CurPos);
1323         savestring = ALLOC(char,length+1);
1324         if (savestring == NULL) return(NULL);
1325         strcpy(savestring,CurPos);
1326         stack[count] = savestring;
1327         count++;
1328         CurPos = strtok(NULL, " \t");
1329     }
1330     list = ALLOC(char *, count);
1331     for (i = 0; i < count; i++)
1332         list[i] = stack[i];
1333     *n = count;
1334     return(list);
1335
1336 } /* end of readList */
1337
1338
1339 /**Function********************************************************************
1340
1341   Synopsis    [Prints a list of strings to the standard output.]
1342
1343   Description [Prints a list of strings to the standard output. The list
1344   is in the format created by readList.]
1345
1346   SideEffects [None]
1347
1348   SeeAlso     [readList Bnet_PrintNetwork]
1349
1350 ******************************************************************************/
1351 static void
1352 printList(
1353   char ** list /* list of pointers to strings */,
1354   int  n /* length of the list */)
1355 {
1356     int i;
1357
1358     for (i = 0; i < n; i++) {
1359         (void) fprintf(stdout," %s",list[i]);
1360     }
1361     (void) fprintf(stdout,"\n");
1362
1363 } /* end of printList */
1364
1365
1366 /**Function********************************************************************
1367
1368   Synopsis    [Generates names not currently in a symbol table.]
1369
1370   Description [Generates n names not currently in the symbol table hash.
1371   The pointer to the symbol table may be NULL, in which case no test is
1372   made. The names generated by the procedure are unique. So, if there is
1373   no possibility of conflict with pre-existing names, NULL can be passed
1374   for the hash table.  Returns an array of names if succesful; NULL
1375   otherwise.]
1376
1377   SideEffects [None]
1378
1379   SeeAlso     []
1380
1381 ******************************************************************************/
1382 static char **
1383 bnetGenerateNewNames(
1384   st_table * hash /* table of existing names (or NULL) */,
1385   int  n /* number of names to be generated */)
1386 {
1387     char **list;
1388     char name[256];
1389     int i;
1390
1391     if (n < 1) return(NULL);
1392
1393     list = ALLOC(char *,n);
1394     if (list == NULL) return(NULL);
1395     for (i = 0; i < n; i++) {
1396         do {
1397             sprintf(name, "var%d", newNameNumber);
1398             newNameNumber++;
1399         } while (hash != NULL && st_is_member(hash,name));
1400         list[i] = util_strsav(name);
1401     }
1402
1403     return(list);
1404
1405 } /* bnetGenerateNewNames */
1406
1407
1408 /**Function********************************************************************
1409
1410   Synopsis    [Writes blif for the reencoding logic.]
1411
1412   Description []
1413
1414   SideEffects [None]
1415
1416   SeeAlso     []
1417
1418 ******************************************************************************/
1419 static int
1420 bnetDumpReencodingLogic(
1421   DdManager * dd /* DD manager */,
1422   char * mname /* model name */,
1423   int  noutputs /* number of outputs */,
1424   DdNode ** outputs /* array of network outputs */,
1425   char ** inames /* array of network input names */,
1426   char ** altnames /* array of names of reencoded inputs */,
1427   char ** onames /* array of network output names */,
1428   FILE * fp /* file pointer */)
1429 {
1430     int i;
1431     int retval;
1432     int nvars = Cudd_ReadSize(dd);
1433     int *support = NULL;
1434
1435     support = bnetFindVectorSupport(dd,outputs,noutputs);
1436     if (support == NULL) return(0);
1437
1438     /* Write the header (.model .inputs .outputs). */
1439     retval = fprintf(fp,".model %s.global\n.inputs",mname);
1440     if (retval == EOF) goto failure;
1441
1442     for (i = 0; i < nvars; i++) {
1443         if ((i%8 == 0)&&i) {
1444             retval = fprintf(fp," \\\n");
1445             if (retval == EOF) goto failure;
1446         }
1447         retval = fprintf(fp," %s", inames[i]);
1448         if (retval == EOF) goto failure;
1449     }
1450
1451     /* Write the .output line. */
1452     retval = fprintf(fp,"\n.outputs");
1453     if (retval == EOF) goto failure;
1454     for (i = 0; i < noutputs; i++) {
1455         if ((i%8 == 0)&&i) {
1456             retval = fprintf(fp," \\\n");
1457             if (retval == EOF) goto failure;
1458         }
1459         retval = fprintf(fp," %s", onames[i]);
1460         if (retval == EOF) goto failure;
1461     }
1462     retval = fprintf(fp,"\n");
1463     if (retval == EOF) goto failure;
1464
1465     /* Instantiate main subcircuit. */
1466     retval = fprintf(fp,"\n.subckt %s", mname);
1467     if (retval == EOF) goto failure;
1468     for (i = 0; i < nvars; i++) {
1469         if ((i%8 == 0)&&i) {
1470             retval = fprintf(fp," \\\n");
1471             if (retval == EOF) goto failure;
1472         }
1473         if (support[i] == 1) {
1474             retval = fprintf(fp," %s=%s", inames[i], altnames[i]);
1475             if (retval == EOF) goto failure;
1476         }
1477     }
1478     for (i = 0; i < noutputs; i++) {
1479         if ((i%8 == 0)&&i) {
1480             retval = fprintf(fp," \\\n");
1481             if (retval == EOF) goto failure;
1482         }
1483         retval = fprintf(fp," %s=%s", onames[i], onames[i]);
1484         if (retval == EOF) goto failure;
1485     }
1486     retval = fprintf(fp,"\n");
1487     if (retval == EOF) goto failure;
1488
1489     /* Instantiate reencoding subcircuit. */
1490     retval = fprintf(fp,"\n.subckt %s.reencode",mname);
1491     if (retval == EOF) goto failure;
1492     for (i = 0; i < nvars; i++) {
1493         if ((i%8 == 0)&&i) {
1494             retval = fprintf(fp," \\\n");
1495             if (retval == EOF) goto failure;
1496         }
1497         retval = fprintf(fp," %s=%s", inames[i], inames[i]);
1498         if (retval == EOF) goto failure;
1499     }
1500     retval = fprintf(fp," \\\n");
1501     if (retval == EOF) goto failure;
1502     for (i = 0; i < nvars; i++) {
1503         if ((i%8 == 0)&&i) {
1504             retval = fprintf(fp," \\\n");
1505             if (retval == EOF) goto failure;
1506         }
1507         if (support[i] == 1) {
1508             retval = fprintf(fp," %s=%s", altnames[i],altnames[i]);
1509             if (retval == EOF) goto failure;
1510         }
1511     }
1512     retval = fprintf(fp,"\n");
1513     if (retval == EOF) goto failure;
1514
1515     /* Write trailer. */
1516     retval = fprintf(fp,".end\n\n");
1517     if (retval == EOF) goto failure;
1518
1519     /* Write reencoding subcircuit. */
1520     retval = bnetBlifWriteReencode(dd,mname,inames,altnames,support,fp);
1521     if (retval == EOF) goto failure;
1522
1523     FREE(support);
1524     return(1);
1525
1526 failure:
1527     if (support != NULL) FREE(support);
1528     return(0);
1529
1530 } /* end of bnetDumpReencodingLogic */
1531
1532
1533 /**Function********************************************************************
1534
1535   Synopsis    [Writes blif for the truth table of an n-input xnor.]
1536
1537   Description [Writes blif for the truth table of an n-input
1538   xnor. Returns 1 if successful; 0 otherwise.]
1539
1540   SideEffects [None]
1541
1542   SeeAlso     []
1543
1544 ******************************************************************************/
1545 #if 0
1546 static int
1547 bnetBlifXnorTable(
1548   FILE * fp /* file pointer */,
1549   int  n /* number of inputs */)
1550 {
1551     int power;  /* 2 to the power n */
1552     int i,j,k;
1553     int nzeroes;
1554     int retval;
1555     char *line;
1556
1557     line = ALLOC(char,n+1);
1558     if (line == NULL) return(0);
1559     line[n] = '\0';
1560
1561     for (i = 0, power = 1; i < n; i++) {
1562         power *= 2;
1563     }
1564
1565     for (i = 0; i < power; i++) {
1566         k = i;
1567         nzeroes = 0;
1568         for (j = 0; j < n; j++) {
1569             if (k & 1) {
1570                 line[j] = '1';
1571             } else {
1572                 line[j] = '0';
1573                 nzeroes++;
1574             }
1575             k >>= 1;
1576         }
1577         if ((nzeroes & 1) == 0) {
1578             retval = fprintf(fp,"%s 1\n",line);
1579             if (retval == 0) return(0);
1580         }
1581     }
1582     return(1);
1583
1584 } /* end of bnetBlifXnorTable */
1585 #endif
1586
1587
1588 /**Function********************************************************************
1589
1590   Synopsis    [Writes blif for the reencoding logic.]
1591
1592   Description [Writes blif for the reencoding logic. Exclusive NORs
1593   with more than two inputs are decomposed into cascaded two-input
1594   gates. Returns 1 if successful; 0 otherwise.]
1595
1596   SideEffects [None]
1597
1598   SeeAlso     []
1599
1600 ******************************************************************************/
1601 static int
1602 bnetBlifWriteReencode(
1603   DdManager * dd,
1604   char * mname,
1605   char ** inames,
1606   char ** altnames,
1607   int * support,
1608   FILE * fp)
1609 {
1610     int retval;
1611     int nvars = Cudd_ReadSize(dd);
1612     int i,j;
1613     int ninp;
1614
1615     /* Write the header (.model .inputs .outputs). */
1616     retval = fprintf(fp,".model %s.reencode\n.inputs",mname);
1617     if (retval == EOF) return(0);
1618
1619     for (i = 0; i < nvars; i++) {
1620         if ((i%8 == 0)&&i) {
1621             retval = fprintf(fp," \\\n");
1622             if (retval == EOF) goto failure;
1623         }
1624         retval = fprintf(fp," %s", inames[i]);
1625         if (retval == EOF) goto failure;
1626     }
1627
1628     /* Write the .output line. */
1629     retval = fprintf(fp,"\n.outputs");
1630     if (retval == EOF) goto failure;
1631     for (i = 0; i < nvars; i++) {
1632         if ((i%8 == 0)&&i) {
1633             retval = fprintf(fp," \\\n");
1634             if (retval == EOF) goto failure;
1635         }
1636         if (support[i] == 1) {
1637             retval = fprintf(fp," %s", altnames[i]);
1638             if (retval == EOF) goto failure;
1639         }
1640     }
1641     retval = fprintf(fp,"\n");
1642     if (retval == EOF) goto failure;
1643
1644     /* Instantiate exclusive nors. */
1645     for (i = 0; i < nvars; i++) {
1646         char *in1 = NULL;
1647         char *in2 = NULL;
1648         char **oname;
1649         if (support[i] == 0) continue;
1650         ninp = 0;
1651         for (j = 0; j < nvars; j++) {
1652             if (Cudd_ReadLinear(dd,i,j)) {
1653                 switch (ninp) {
1654                 case 0:
1655                     in1 = inames[j];
1656                     ninp++;
1657                     break;
1658                 case 1:
1659                     in2 = inames[j];
1660                     ninp++;
1661                     break;
1662                 case 2:
1663                     oname = bnetGenerateNewNames(NULL,1);
1664                     retval = fprintf(fp,".names %s %s %s\n11 1\n00 1\n",
1665                              in1, in2, oname[0]);
1666                     if (retval == EOF) goto failure;
1667                     in1 = oname[0];
1668                     in2 = inames[j];
1669                     FREE(oname);
1670                     break;
1671                 default:
1672                     goto failure;
1673                 }
1674             }
1675         }
1676         switch (ninp) {
1677         case 1:
1678             retval = fprintf(fp,".names %s %s\n1 1\n", in1, altnames[i]);
1679             if (retval == EOF) goto failure;
1680             break;
1681         case 2:
1682             retval = fprintf(fp,".names %s %s %s\n11 1\n00 1\n",
1683                      in1, in2, altnames[i]);
1684             if (retval == EOF) goto failure;
1685             break;
1686         default:
1687             goto failure;
1688         }
1689     }
1690
1691     /* Write trailer. */
1692     retval = fprintf(fp,"\n.end\n\n");
1693     if (retval == EOF) goto failure;
1694
1695     return(1);
1696
1697 failure:
1698     return(0);
1699
1700 } /* end of bnetBlifWriteReencode */
1701
1702
1703 /**Function********************************************************************
1704
1705   Synopsis    [Finds the support of a list of DDs.]
1706
1707   Description []
1708
1709   SideEffects [None]
1710
1711   SeeAlso     []
1712
1713 ******************************************************************************/
1714 static int *
1715 bnetFindVectorSupport(
1716   DdManager * dd,
1717   DdNode ** list,
1718   int  n)
1719 {
1720     DdNode      *support = NULL;
1721     DdNode      *scan;
1722     int         *array = NULL;
1723     int         nvars = Cudd_ReadSize(dd);
1724     int         i;
1725
1726     /* Build an array with the support of the functions in list. */
1727     array = ALLOC(int,nvars);
1728     if (array == NULL) return(NULL);
1729     for (i = 0; i < nvars; i++) {
1730         array[i] = 0;
1731     }
1732
1733     /* Take the union of the supports of each output function. */
1734     for (i = 0; i < n; i++) {
1735         support = Cudd_Support(dd,list[i]);
1736         if (support == NULL) {
1737             FREE(array);
1738             return(NULL);
1739         }
1740         Cudd_Ref(support);
1741         scan = support;
1742         while (!Cudd_IsConstant(scan)) {
1743             array[scan->index] = 1;
1744             scan = Cudd_T(scan);
1745         }
1746         Cudd_IterDerefBdd(dd,support);
1747     }
1748
1749     return(array);
1750
1751 } /* end of bnetFindVectorSupport */
1752
1753
1754 /**Function********************************************************************
1755
1756   Synopsis    [Builds BDD for a XOR function.]
1757
1758   Description [Checks whether a function is a XOR with 2 or 3 inputs. If so,
1759   it builds the BDD. Returns 1 if the BDD has been built; 0 otherwise.]
1760
1761   SideEffects [None]
1762
1763   SeeAlso     []
1764
1765 ******************************************************************************/
1766 static int
1767 buildExorBDD(
1768   DdManager * dd,
1769   BnetNode * nd,
1770   st_table * hash,
1771   int  params,
1772   int  nodrop)
1773 {
1774     int check[8];
1775     int i;
1776     int nlines;
1777     BnetTabline *line;
1778     DdNode *func, *var, *tmp;
1779     BnetNode *auxnd;
1780
1781     if (nd->ninp < 2 || nd->ninp > 3) return(0);
1782
1783     nlines = 1 << (nd->ninp - 1);
1784     for (i = 0; i < 8; i++) check[i] = 0;
1785     line = nd->f;
1786     while (line != NULL) {
1787         int num = 0;
1788         int count = 0;
1789         nlines--;
1790         for (i = 0; i < nd->ninp; i++) {
1791             num <<= 1;
1792             if (line->values[i] == '-') {
1793                 return(0);
1794             } else if (line->values[i] == '1') {
1795                 count++;
1796                 num++;
1797             }
1798         }
1799         if ((count & 1) == 0) return(0);
1800         if (check[num]) return(0);
1801         line = line->next;
1802     }
1803     if (nlines != 0) return(0);
1804
1805     /* Initialize the exclusive sum to logical 0. */
1806     func = Cudd_ReadLogicZero(dd);
1807     Cudd_Ref(func);
1808
1809     /* Scan the inputs. */
1810     for (i = 0; i < nd->ninp; i++) {
1811         if (!st_lookup(hash, nd->inputs[i], &auxnd)) {
1812             goto failure;
1813         }
1814         if (params == BNET_LOCAL_DD) {
1815             if (auxnd->active == FALSE) {
1816                 if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
1817                     goto failure;
1818                 }
1819             }
1820             var = Cudd_ReadVars(dd,auxnd->var);
1821             if (var == NULL) goto failure;
1822             Cudd_Ref(var);
1823         } else { /* params == BNET_GLOBAL_DD */
1824             if (auxnd->dd == NULL) {
1825                 if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
1826                     goto failure;
1827                 }
1828             }
1829             var = auxnd->dd;
1830         }
1831         tmp = Cudd_bddXor(dd,func,var);
1832         if (tmp == NULL) goto failure;
1833         Cudd_Ref(tmp);
1834         Cudd_IterDerefBdd(dd,func);
1835         if (params == BNET_LOCAL_DD) {
1836             Cudd_IterDerefBdd(dd,var);
1837         }
1838         func = tmp;
1839     }
1840     nd->dd = func;
1841
1842     /* Associate a variable to this node if local BDDs are being
1843     ** built. This is done at the end, so that the primary inputs tend
1844     ** to get lower indices.
1845     */
1846     if (params == BNET_LOCAL_DD && nd->active == FALSE) {
1847         DdNode *auxfunc = Cudd_bddNewVar(dd);
1848         if (auxfunc == NULL) goto failure;
1849         Cudd_Ref(auxfunc);
1850         nd->var = auxfunc->index;
1851         nd->active = TRUE;
1852         Cudd_IterDerefBdd(dd,auxfunc);
1853     }
1854
1855     return(1);
1856 failure:
1857     return(0);
1858
1859 } /* end of buildExorBDD */
1860
1861
1862 /**Function********************************************************************
1863
1864   Synopsis    [Builds BDD for a multiplexer.]
1865
1866   Description [Checks whether a function is a 2-to-1 multiplexer. If so,
1867   it builds the BDD. Returns 1 if the BDD has been built; 0 otherwise.]
1868
1869   SideEffects [None]
1870
1871   SeeAlso     []
1872
1873 ******************************************************************************/
1874 static int
1875 buildMuxBDD(
1876   DdManager * dd,
1877   BnetNode * nd,
1878   st_table * hash,
1879   int  params,
1880   int  nodrop)
1881 {
1882     BnetTabline *line;
1883     char *values[2];
1884     int mux[2];
1885     int phase[2];
1886     int j;
1887     int nlines = 0;
1888     int controlC = -1;
1889     int controlR = -1;
1890     DdNode *func, *f, *g, *h;
1891     BnetNode *auxnd;
1892
1893     if (nd->ninp != 3) return(0);
1894
1895     for (line = nd->f; line != NULL; line = line->next) {
1896         int dc = 0;
1897         if (nlines > 1) return(0);
1898         values[nlines] = line->values;
1899         for (j = 0; j < 3; j++) {
1900             if (values[nlines][j] == '-') {
1901                 if (dc) return(0);
1902                 dc = 1;
1903             }
1904         }
1905         if (!dc) return(0);
1906         nlines++;
1907     }
1908     /* At this point we know we have:
1909     **   3 inputs
1910     **   2 lines
1911     **   1 dash in each line
1912     ** If the two dashes are not in the same column, then there is
1913     ** exaclty one column without dashes: the control column.
1914     */
1915     for (j = 0; j < 3; j++) {
1916         if (values[0][j] == '-' && values[1][j] == '-') return(0);
1917         if (values[0][j] != '-' && values[1][j] != '-') {
1918             if (values[0][j] == values[1][j]) return(0);
1919             controlC = j;
1920             controlR = values[0][j] == '0';
1921         }
1922     }
1923     assert(controlC != -1 && controlR != -1);
1924     /* At this point we know that there is indeed no column with two
1925     ** dashes. The control column has been identified, and we know that
1926     ** its two elelments are different. */
1927     for (j = 0; j < 3; j++) {
1928         if (j == controlC) continue;
1929         if (values[controlR][j] == '1') {
1930             mux[0] = j;
1931             phase[0] = 0;
1932         } else if (values[controlR][j] == '0') {
1933             mux[0] = j;
1934             phase[0] = 1;
1935         } else if (values[1-controlR][j] == '1') {
1936             mux[1] = j;
1937             phase[1] = 0;
1938         } else if (values[1-controlR][j] == '0') {
1939             mux[1] = j;
1940             phase[1] = 1;
1941         }
1942     }
1943
1944     /* Get the inputs. */
1945     if (!st_lookup(hash, nd->inputs[controlC], &auxnd)) {
1946         goto failure;
1947     }
1948     if (params == BNET_LOCAL_DD) {
1949         if (auxnd->active == FALSE) {
1950             if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
1951                 goto failure;
1952             }
1953         }
1954         f = Cudd_ReadVars(dd,auxnd->var);
1955         if (f == NULL) goto failure;
1956         Cudd_Ref(f);
1957     } else { /* params == BNET_GLOBAL_DD */
1958         if (auxnd->dd == NULL) {
1959             if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
1960                 goto failure;
1961             }
1962         }
1963         f = auxnd->dd;
1964     }
1965     if (!st_lookup(hash, nd->inputs[mux[0]], &auxnd)) {
1966         goto failure;
1967     }
1968     if (params == BNET_LOCAL_DD) {
1969         if (auxnd->active == FALSE) {
1970             if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
1971                 goto failure;
1972             }
1973         }
1974         g = Cudd_ReadVars(dd,auxnd->var);
1975         if (g == NULL) goto failure;
1976         Cudd_Ref(g);
1977     } else { /* params == BNET_GLOBAL_DD */
1978         if (auxnd->dd == NULL) {
1979             if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
1980                 goto failure;
1981             }
1982         }
1983         g = auxnd->dd;
1984     }
1985     g = Cudd_NotCond(g,phase[0]);
1986     if (!st_lookup(hash, nd->inputs[mux[1]], &auxnd)) {
1987         goto failure;
1988     }
1989     if (params == BNET_LOCAL_DD) {
1990         if (auxnd->active == FALSE) {
1991             if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
1992                 goto failure;
1993             }
1994         }
1995         h = Cudd_ReadVars(dd,auxnd->var);
1996         if (h == NULL) goto failure;
1997         Cudd_Ref(h);
1998     } else { /* params == BNET_GLOBAL_DD */
1999         if (auxnd->dd == NULL) {
2000             if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
2001                 goto failure;
2002             }
2003         }
2004         h = auxnd->dd;
2005     }
2006     h = Cudd_NotCond(h,phase[1]);
2007     func = Cudd_bddIte(dd,f,g,h);
2008     if (func == NULL) goto failure;
2009     Cudd_Ref(func);
2010     if (params == BNET_LOCAL_DD) {
2011         Cudd_IterDerefBdd(dd,f);
2012         Cudd_IterDerefBdd(dd,g);
2013         Cudd_IterDerefBdd(dd,h);
2014     }
2015     nd->dd = func;
2016
2017     /* Associate a variable to this node if local BDDs are being
2018     ** built. This is done at the end, so that the primary inputs tend
2019     ** to get lower indices.
2020     */
2021     if (params == BNET_LOCAL_DD && nd->active == FALSE) {
2022         DdNode *auxfunc = Cudd_bddNewVar(dd);
2023         if (auxfunc == NULL) goto failure;
2024         Cudd_Ref(auxfunc);
2025         nd->var = auxfunc->index;
2026         nd->active = TRUE;
2027         Cudd_IterDerefBdd(dd,auxfunc);
2028     }
2029
2030     return(1);
2031 failure:
2032     return(0);
2033
2034 } /* end of buildExorBDD */
2035
2036
2037 /**Function********************************************************************
2038
2039   Synopsis    [Sets the level of each node.]
2040
2041   Description [Sets the level of each node. Returns 1 if successful; 0
2042   otherwise.]
2043
2044   SideEffects [Changes the level and visited fields of the nodes it
2045   visits.]
2046
2047   SeeAlso     [bnetLevelDFS]
2048
2049 ******************************************************************************/
2050 static int
2051 bnetSetLevel(
2052   BnetNetwork * net)
2053 {
2054     BnetNode *node;
2055
2056     /* Recursively visit nodes. This is pretty inefficient, because we
2057     ** visit all nodes in this loop, and most of them in the recursive
2058     ** calls to bnetLevelDFS. However, this approach guarantees that
2059     ** all nodes will be reached ven if there are dangling outputs. */
2060     node = net->nodes;
2061     while (node != NULL) {
2062         if (!bnetLevelDFS(net,node)) return(0);
2063         node = node->next;
2064     }
2065
2066     /* Clear visited flags. */
2067     node = net->nodes;
2068     while (node != NULL) {
2069         node->visited = 0;
2070         node = node->next;
2071     }
2072     return(1);
2073
2074 } /* end of bnetSetLevel */
2075
2076
2077 /**Function********************************************************************
2078
2079   Synopsis    [Does a DFS from a node setting the level field.]
2080
2081   Description [Does a DFS from a node setting the level field. Returns
2082   1 if successful; 0 otherwise.]
2083
2084   SideEffects [Changes the level and visited fields of the nodes it
2085   visits.]
2086
2087   SeeAlso     [bnetSetLevel]
2088
2089 ******************************************************************************/
2090 static int
2091 bnetLevelDFS(
2092   BnetNetwork * net,
2093   BnetNode * node)
2094 {
2095     int i;
2096     BnetNode *auxnd;
2097
2098     if (node->visited == 1) {
2099         return(1);
2100     }
2101
2102     node->visited = 1;
2103
2104     /* Graphical sources have level 0.  This is the final value if the
2105     ** node has no fan-ins. Otherwise the successive loop will
2106     ** increase the level. */
2107     node->level = 0;
2108     for (i = 0; i < node->ninp; i++) {
2109         if (!st_lookup(net->hash, node->inputs[i], &auxnd)) {
2110             return(0);
2111         }
2112         if (!bnetLevelDFS(net,auxnd)) {
2113             return(0);
2114         }
2115         if (auxnd->level >= node->level) node->level = 1 + auxnd->level;
2116     }
2117     return(1);
2118
2119 } /* end of bnetLevelDFS */
2120
2121
2122 /**Function********************************************************************
2123
2124   Synopsis    [Orders network roots for variable ordering.]
2125
2126   Description [Orders network roots for variable ordering. Returns
2127   an array with the ordered outputs and next state variables if
2128   successful; NULL otherwise.]
2129
2130   SideEffects [None]
2131
2132   SeeAlso     []
2133
2134 ******************************************************************************/
2135 static BnetNode **
2136 bnetOrderRoots(
2137   BnetNetwork * net,
2138   int * nroots)
2139 {
2140     int i, noutputs;
2141     BnetNode *node;
2142     BnetNode **nodes = NULL;
2143
2144     /* Initialize data structures. */
2145     noutputs = net->noutputs;
2146     nodes = ALLOC(BnetNode *, noutputs);
2147     if (nodes == NULL) goto endgame;
2148
2149     /* Find output names and levels. */
2150     for (i = 0; i < net->noutputs; i++) {
2151         if (!st_lookup(net->hash,net->outputs[i],&node)) {
2152             goto endgame;
2153         }
2154         nodes[i] = node;
2155     }
2156
2157     qsort((void *)nodes, noutputs, sizeof(BnetNode *),
2158           (DD_QSFP)bnetLevelCompare);
2159     *nroots = noutputs;
2160     return(nodes);
2161
2162 endgame:
2163     if (nodes != NULL) FREE(nodes);
2164     return(NULL);
2165
2166 } /* end of bnetOrderRoots */
2167
2168
2169 /**Function********************************************************************
2170
2171   Synopsis    [Comparison function used by qsort.]
2172
2173   Description [Comparison function used by qsort to order the
2174   variables according to the number of keys in the subtables.
2175   Returns the difference in number of keys between the two
2176   variables being compared.]
2177
2178   SideEffects [None]
2179
2180 ******************************************************************************/
2181 static int
2182 bnetLevelCompare(
2183   BnetNode ** x,
2184   BnetNode ** y)
2185 {
2186     return((*y)->level - (*x)->level);
2187
2188 } /* end of bnetLevelCompare */
2189
2190
2191 /**Function********************************************************************
2192
2193   Synopsis    [Does a DFS from a node ordering the inputs.]
2194
2195   Description [Does a DFS from a node ordering the inputs. Returns
2196   1 if successful; 0 otherwise.]
2197
2198   SideEffects [Changes visited fields of the nodes it visits.]
2199
2200   SeeAlso     [Bnet_DfsVariableOrder]
2201
2202 ******************************************************************************/
2203 static int
2204 bnetDfsOrder(
2205   DdManager * dd,
2206   BnetNetwork * net,
2207   BnetNode * node)
2208 {
2209     int i;
2210     BnetNode *auxnd;
2211     BnetNode **fanins;
2212
2213     if (node->visited == 1) {
2214         return(1);
2215     }
2216
2217     node->visited = 1;
2218     if (node->type == BNET_INPUT_NODE ||
2219         node->type == BNET_PRESENT_STATE_NODE) {
2220         node->dd = Cudd_bddNewVar(dd);
2221         if (node->dd == NULL) return(0);
2222         Cudd_Ref(node->dd);
2223         node->active = TRUE;
2224         node->var = node->dd->index;
2225         return(1);
2226     }
2227
2228     fanins = ALLOC(BnetNode *, node->ninp);
2229     if (fanins == NULL) return(0);
2230
2231     for (i = 0; i < node->ninp; i++) {
2232         if (!st_lookup(net->hash, node->inputs[i], &auxnd)) {
2233             FREE(fanins);
2234             return(0);
2235         }
2236         fanins[i] = auxnd;
2237     }
2238
2239     qsort((void *)fanins, node->ninp, sizeof(BnetNode *),
2240           (DD_QSFP)bnetLevelCompare);
2241     for (i = 0; i < node->ninp; i++) {
2242         /* for (i = node->ninp - 1; i >= 0; i--) { */
2243         int res = bnetDfsOrder(dd,net,fanins[i]);
2244         if (res == 0) {
2245             FREE(fanins);
2246             return(0);
2247         }
2248     }
2249     FREE(fanins);
2250     return(1);
2251
2252 } /* end of bnetLevelDFS */