source: icGREP/icgrep-devel/cudd-2.5.1/nanotrav/bnet.c @ 5815

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

Upload of the CUDD library.

File size: 61.2 KB
Line 
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-2012, Regents of the University of Colorado
16
17  All rights reserved.
18
19  Redistribution and use in source and binary forms, with or without
20  modification, are permitted provided that the following conditions
21  are met:
22
23  Redistributions of source code must retain the above copyright
24  notice, this list of conditions and the following disclaimer.
25
26  Redistributions in binary form must reproduce the above copyright
27  notice, this list of conditions and the following disclaimer in the
28  documentation and/or other materials provided with the distribution.
29
30  Neither the name of the University of Colorado nor the names of its
31  contributors may be used to endorse or promote products derived from
32  this software without specific prior written permission.
33
34  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
35  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
36  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
37  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
38  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
39  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
40  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
41  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
42  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
43  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
44  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
45  POSSIBILITY OF SUCH DAMAGE.]
46
47******************************************************************************/
48
49#include "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
70static char rcsid[] UTIL_UNUSED = "$Id: bnet.c,v 1.27 2014/02/11 02:41:41 fabio Exp fabio $";
71#endif
72
73static  char    BuffLine[MAXLENGTH];
74static  char    *CurPos;
75static  int     newNameNumber = 0;
76
77/*---------------------------------------------------------------------------*/
78/* Macro declarations                                                        */
79/*---------------------------------------------------------------------------*/
80
81/**AutomaticStart*************************************************************/
82
83/*---------------------------------------------------------------------------*/
84/* Static function prototypes                                                */
85/*---------------------------------------------------------------------------*/
86
87static char * readString (FILE *fp);
88static char ** readList (FILE *fp, int *n);
89static void printList (char **list, int n);
90static char ** bnetGenerateNewNames (st_table *hash, int n);
91static int bnetDumpReencodingLogic (DdManager *dd, char *mname, int noutputs, DdNode **outputs, char **inames, char **altnames, char **onames, FILE *fp);
92#if 0
93static int bnetBlifXnorTable (FILE *fp, int n);
94#endif
95static int bnetBlifWriteReencode (DdManager *dd, char *mname, char **inames, char **altnames, int *support, FILE *fp);
96static int * bnetFindVectorSupport (DdManager *dd, DdNode **list, int n);
97static int buildExorBDD (DdManager *dd, BnetNode *nd, st_table *hash, int params, int nodrop);
98static int buildMuxBDD (DdManager * dd, BnetNode * nd, st_table * hash, int  params, int  nodrop);
99static int bnetSetLevel (BnetNetwork *net);
100static int bnetLevelDFS (BnetNetwork *net, BnetNode *node);
101static BnetNode ** bnetOrderRoots (BnetNetwork *net, int *nroots);
102static int bnetLevelCompare (BnetNode **x, BnetNode **y);
103static 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******************************************************************************/
146BnetNetwork *
147Bnet_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
482failure:
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******************************************************************************/
503void
504Bnet_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******************************************************************************/
559void
560Bnet_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******************************************************************************/
639int
640Bnet_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
779failure:
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******************************************************************************/
798int
799Bnet_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******************************************************************************/
842int
843Bnet_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,
925                               (char const * const *) inames,
926                               (char const * const *) onames,
927                               network->name,dfp,0);
928    } else if (dumpFmt == 2) {
929        retval = Cudd_DumpDaVinci(dd,noutputs,outputs,
930                                  (char const * const *) inames,
931                                  (char const * const *) onames,dfp);
932    } else if (dumpFmt == 3) {
933        retval = Cudd_DumpDDcal(dd,noutputs,outputs,
934                                (char const * const *) inames,
935                                (char const * const *) onames,dfp);
936    } else if (dumpFmt == 4) {
937        retval = Cudd_DumpFactoredForm(dd,noutputs,outputs,
938                                       (char const * const *) inames,
939                                       (char const * const *) onames,dfp);
940    } else if (dumpFmt == 5) {
941        retval = Cudd_DumpBlif(dd,noutputs,outputs,
942                               (char const * const *) inames,
943                               (char const * const *) onames,
944                               network->name,dfp,1);
945    } else {
946        retval = Cudd_DumpDot(dd,noutputs,outputs,
947                              (char const * const *) inames,
948                              (char const * const *) onames,dfp);
949    }
950
951endgame:
952    if (dfp != stdout && dfp != NULL) {
953        if (fclose(dfp) == EOF) retval = 0;
954    }
955    if (outputs != NULL) FREE(outputs);
956    if (onames  != NULL) FREE(onames);
957    if (inames  != NULL) FREE(inames);
958
959    return(retval);
960
961} /* end of Bnet_bddDump */
962
963
964/**Function********************************************************************
965
966  Synopsis    [Writes an array of BDDs to a file in dot, blif, DDcal,
967  factored-form, daVinci, or blif-MV format.]
968
969  Description [Writes an array of BDDs to a file in dot, blif, DDcal,
970  factored-form, daVinci, or blif-MV format.  The BDDs and their names
971  are passed as arguments.  The inputs and their names are taken from
972  the network. If "-" is passed as file name, the BDDs are dumped to
973  the standard output. Returns 1 in case of success; 0 otherwise.]
974
975  SideEffects [None]
976
977  SeeAlso     []
978
979******************************************************************************/
980int
981Bnet_bddArrayDump(
982  DdManager * dd /* DD manager */,
983  BnetNetwork * network /* network whose BDDs should be dumped */,
984  char * dfile /* file name */,
985  DdNode ** outputs /* BDDs to be dumped */,
986  char ** onames /* names of the BDDs to be dumped */,
987  int  noutputs /* number of BDDs to be dumped */,
988  int  dumpFmt /* 0 -> dot */)
989{
990    FILE *dfp = NULL;
991    char **inames = NULL;
992    BnetNode *node;
993    int i;
994    int retval = 0; /* 0 -> failure; 1 -> success */
995
996    /* Open dump file. */
997    if (strcmp(dfile, "-") == 0) {
998        dfp = stdout;
999    } else {
1000        dfp = fopen(dfile,"w");
1001    }
1002    if (dfp == NULL) goto endgame;
1003
1004    /* Initialize data structures. */
1005    inames = ALLOC(char *,Cudd_ReadSize(dd));
1006    if (inames == NULL) goto endgame;
1007    for (i = 0; i < Cudd_ReadSize(dd); i++) {
1008        inames[i] = NULL;
1009    }
1010
1011    /* Find the input names. */
1012    for (i = 0; i < network->ninputs; i++) {
1013        if (!st_lookup(network->hash,network->inputs[i],&node)) {
1014            goto endgame;
1015        }
1016        inames[node->var] = network->inputs[i];
1017    }
1018    for (i = 0; i < network->nlatches; i++) {
1019        if (!st_lookup(network->hash,network->latches[i][1],&node)) {
1020            goto endgame;
1021        }
1022        inames[node->var] = network->latches[i][1];
1023    }
1024
1025    /* Dump the BDDs. */
1026    if (dumpFmt == 1) {
1027        retval = Cudd_DumpBlif(dd,noutputs,outputs,
1028                               (char const * const *) inames,
1029                               (char const * const *) onames,
1030                               network->name,dfp,0);
1031    } else if (dumpFmt == 2) {
1032        retval = Cudd_DumpDaVinci(dd,noutputs,outputs,
1033                                  (char const * const *) inames,
1034                                  (char const * const *) onames,dfp);
1035    } else if (dumpFmt == 3) {
1036        retval = Cudd_DumpDDcal(dd,noutputs,outputs,
1037                                (char const * const *) inames,
1038                                (char const * const *) onames,dfp);
1039    } else if (dumpFmt == 4) {
1040        retval = Cudd_DumpFactoredForm(dd,noutputs,outputs,
1041                                       (char const * const *) inames,
1042                                       (char const * const *) onames,dfp);
1043    } else if (dumpFmt == 5) {
1044        retval = Cudd_DumpBlif(dd,noutputs,outputs,
1045                               (char const * const *) inames,
1046                               (char const * const *) onames,
1047                               network->name,dfp,1);
1048    } else {
1049        retval = Cudd_DumpDot(dd,noutputs,outputs,
1050                              (char const * const *) inames,
1051                              (char const * const *) onames,dfp);
1052    }
1053
1054endgame:
1055    if (dfp != stdout && dfp != NULL) {
1056        if (fclose(dfp) == EOF) retval = 0;
1057    }
1058    if (inames  != NULL) FREE(inames);
1059
1060    return(retval);
1061
1062} /* end of Bnet_bddArrayDump */
1063
1064
1065/**Function********************************************************************
1066
1067  Synopsis    [Reads the variable order from a file.]
1068
1069  Description [Reads the variable order from a file.
1070  Returns 1 if successful; 0 otherwise.]
1071
1072  SideEffects [The BDDs for the primary inputs and present state variables
1073  are built.]
1074
1075  SeeAlso     []
1076
1077*****************************************************************************/
1078int
1079Bnet_ReadOrder(
1080  DdManager * dd,
1081  char * ordFile,
1082  BnetNetwork * net,
1083  int  locGlob,
1084  int  nodrop)
1085{
1086    FILE *fp;
1087    st_table *dict;
1088    int result;
1089    BnetNode *node;
1090    char name[MAXLENGTH];
1091
1092    if (ordFile == NULL) {
1093        return(0);
1094    }
1095
1096    dict = st_init_table(strcmp,st_strhash);
1097    if (dict == NULL) {
1098        return(0);
1099    }
1100
1101    if ((fp = fopen(ordFile,"r")) == NULL) {
1102        (void) fprintf(stderr,"Unable to open %s\n",ordFile);
1103        st_free_table(dict);
1104        return(0);
1105    }
1106
1107    while (!feof(fp)) {
1108        result = fscanf(fp, "%s", name);
1109        if (result == EOF) {
1110            break;
1111        } else if (result != 1) {
1112            st_free_table(dict);
1113            return(0);
1114        } else if (strlen(name) > MAXLENGTH) {
1115            st_free_table(dict);
1116            return(0);
1117        }
1118        /* There should be a node named "name" in the network. */
1119        if (!st_lookup(net->hash,name,&node)) {
1120            (void) fprintf(stderr,"Unknown name in order file (%s)\n", name);
1121            st_free_table(dict);
1122            return(0);
1123        }
1124        /* A name should not appear more than once in the order. */
1125        if (st_is_member(dict,name)) {
1126            (void) fprintf(stderr,"Duplicate name in order file (%s)\n", name);
1127            st_free_table(dict);
1128            return(0);
1129        }
1130        /* The name should correspond to a primary input or present state. */
1131        if (node->type != BNET_INPUT_NODE &&
1132            node->type != BNET_PRESENT_STATE_NODE) {
1133            (void) fprintf(stderr,"%s has the wrong type (%d)\n", name,
1134                           node->type);
1135            st_free_table(dict);
1136            return(0);
1137        }
1138        /* Insert in table. Use node->name rather than name, because the
1139        ** latter gets overwritten.
1140        */
1141        if (st_insert(dict,node->name,NULL) == ST_OUT_OF_MEM) {
1142            (void) fprintf(stderr,"Out of memory in Bnet_ReadOrder\n");
1143            st_free_table(dict);
1144            return(0);
1145        }
1146        result = Bnet_BuildNodeBDD(dd,node,net->hash,locGlob,nodrop);
1147        if (result == 0) {
1148            (void) fprintf(stderr,"Construction of BDD failed\n");
1149            st_free_table(dict);
1150            return(0);
1151        }
1152    } /* while (!feof(fp)) */
1153    result = fclose(fp);
1154    if (result == EOF) {
1155        (void) fprintf(stderr,"Error closing order file %s\n", ordFile);
1156        st_free_table(dict);
1157        return(0);
1158    }
1159
1160    /* The number of names in the order file should match exactly the
1161    ** number of primary inputs and present states.
1162    */
1163    if (st_count(dict) != net->ninputs) {
1164        (void) fprintf(stderr,"Order incomplete: %d names instead of %d\n",
1165                       st_count(dict), net->ninputs);
1166        st_free_table(dict);
1167        return(0);
1168    }
1169
1170    st_free_table(dict);
1171    return(1);
1172
1173} /* end of Bnet_ReadOrder */
1174
1175
1176/**Function********************************************************************
1177
1178  Synopsis    [Prints the order of the DD variables of a network.]
1179
1180  Description [Prints the order of the DD variables of a network.
1181  Only primary inputs and present states are printed.
1182  Returns 1 if successful; 0 otherwise.]
1183
1184  SideEffects [None]
1185
1186  SeeAlso     []
1187
1188*****************************************************************************/
1189int
1190Bnet_PrintOrder(
1191  BnetNetwork * net,
1192  DdManager *dd)
1193{
1194    char **names;               /* array used to print variable orders */
1195    int level;                  /* position of a variable in current order */
1196    BnetNode *node;             /* auxiliary pointer to network node */
1197    int i,j;
1198    int retval;
1199    int nvars;
1200
1201    nvars = Cudd_ReadSize(dd);
1202    names = ALLOC(char *, nvars);
1203    if (names == NULL) return(0);
1204    for (i = 0; i < nvars; i++) {
1205        names[i] = NULL;
1206    }
1207    for (i = 0; i < net->npis; i++) {
1208        if (!st_lookup(net->hash,net->inputs[i],&node)) {
1209            FREE(names);
1210            return(0);
1211        }
1212        if (node->dd == NULL) {
1213            FREE(names);
1214            return(0);
1215        }
1216        level = Cudd_ReadPerm(dd,node->var);
1217        names[level] = node->name;
1218    }
1219    for (i = 0; i < net->nlatches; i++) {
1220        if (!st_lookup(net->hash,net->latches[i][1],&node)) {
1221            FREE(names);
1222            return(0);
1223        }
1224        if (node->dd == NULL) {
1225            FREE(names);
1226            return(0);
1227        }
1228        level = Cudd_ReadPerm(dd,node->var);
1229        names[level] = node->name;
1230    }
1231    for (i = 0, j = 0; i < nvars; i++) {
1232        if (names[i] == NULL) continue;
1233        if ((j%8 == 0)&&j) {
1234            retval = printf("\n");
1235            if (retval == EOF) {
1236                FREE(names);
1237                return(0);
1238            }
1239        }
1240        retval = printf("%s ",names[i]);
1241        if (retval == EOF) {
1242            FREE(names);
1243            return(0);
1244        }
1245        j++;
1246    }
1247    FREE(names);
1248    retval = printf("\n");
1249    if (retval == EOF) {
1250        return(0);
1251    }
1252    return(1);
1253
1254} /* end of Bnet_PrintOrder */
1255
1256
1257/*---------------------------------------------------------------------------*/
1258/* Definition of internal functions                                          */
1259/*---------------------------------------------------------------------------*/
1260
1261/*---------------------------------------------------------------------------*/
1262/* Definition of static functions                                            */
1263/*---------------------------------------------------------------------------*/
1264
1265
1266/**Function********************************************************************
1267
1268  Synopsis    [Reads a string from a file.]
1269
1270  Description [Reads a string from a file. The string can be MAXLENGTH-1
1271  characters at most. readString allocates memory to hold the string and
1272  returns a pointer to the result if successful. It returns NULL
1273  otherwise.]
1274
1275  SideEffects [None]
1276
1277  SeeAlso     [readList]
1278
1279******************************************************************************/
1280static char *
1281readString(
1282  FILE * fp /* pointer to the file from which the string is read */)
1283{
1284    char *savestring;
1285    int length;
1286
1287    while (!CurPos) {
1288        if (!fgets(BuffLine, MAXLENGTH, fp))
1289            return(NULL);
1290        BuffLine[strlen(BuffLine) - 1] = '\0';
1291        CurPos = strtok(BuffLine, " \t");
1292        if (CurPos && CurPos[0] == '#') CurPos = (char *)NULL;
1293    }
1294    length = strlen(CurPos);
1295    savestring = ALLOC(char,length+1);
1296    if (savestring == NULL)
1297        return(NULL);
1298    strcpy(savestring,CurPos);
1299    CurPos = strtok(NULL, " \t");
1300    return(savestring);
1301
1302} /* end of readString */
1303
1304
1305/**Function********************************************************************
1306
1307  Synopsis    [Reads a list of strings from a file.]
1308
1309  Description [Reads a list of strings from a line of a file.
1310  The strings are sequences of characters separated by spaces or tabs.
1311  The total length of the list, white space included, must not exceed
1312  MAXLENGTH-1 characters.  readList allocates memory for the strings and
1313  creates an array of pointers to the individual lists. Only two pieces
1314  of memory are allocated by readList: One to hold all the strings,
1315  and one to hold the pointers to them. Therefore, when freeing the
1316  memory allocated by readList, only the pointer to the list of
1317  pointers, and the pointer to the beginning of the first string should
1318  be freed. readList returns the pointer to the list of pointers if
1319  successful; NULL otherwise.]
1320
1321  SideEffects [n is set to the number of strings in the list.]
1322
1323  SeeAlso     [readString printList]
1324
1325******************************************************************************/
1326static char **
1327readList(
1328  FILE * fp /* pointer to the file from which the list is read */,
1329  int * n /* on return, number of strings in the list */)
1330{
1331    char        *savestring;
1332    int         length;
1333    char        *stack[8192];
1334    char        **list;
1335    int         i, count = 0;
1336
1337    while (CurPos) {
1338        if (strcmp(CurPos, "\\") == 0) {
1339            CurPos = (char *)NULL;
1340            while (!CurPos) {
1341                if (!fgets(BuffLine, MAXLENGTH, fp)) return(NULL);
1342                BuffLine[strlen(BuffLine) - 1] = '\0';
1343                CurPos = strtok(BuffLine, " \t");
1344            }
1345        }
1346        length = strlen(CurPos);
1347        savestring = ALLOC(char,length+1);
1348        if (savestring == NULL) return(NULL);
1349        strcpy(savestring,CurPos);
1350        stack[count] = savestring;
1351        count++;
1352        CurPos = strtok(NULL, " \t");
1353    }
1354    list = ALLOC(char *, count);
1355    for (i = 0; i < count; i++)
1356        list[i] = stack[i];
1357    *n = count;
1358    return(list);
1359
1360} /* end of readList */
1361
1362
1363/**Function********************************************************************
1364
1365  Synopsis    [Prints a list of strings to the standard output.]
1366
1367  Description [Prints a list of strings to the standard output. The list
1368  is in the format created by readList.]
1369
1370  SideEffects [None]
1371
1372  SeeAlso     [readList Bnet_PrintNetwork]
1373
1374******************************************************************************/
1375static void
1376printList(
1377  char ** list /* list of pointers to strings */,
1378  int  n /* length of the list */)
1379{
1380    int i;
1381
1382    for (i = 0; i < n; i++) {
1383        (void) fprintf(stdout," %s",list[i]);
1384    }
1385    (void) fprintf(stdout,"\n");
1386
1387} /* end of printList */
1388
1389
1390/**Function********************************************************************
1391
1392  Synopsis    [Generates names not currently in a symbol table.]
1393
1394  Description [Generates n names not currently in the symbol table hash.
1395  The pointer to the symbol table may be NULL, in which case no test is
1396  made. The names generated by the procedure are unique. So, if there is
1397  no possibility of conflict with pre-existing names, NULL can be passed
1398  for the hash table.  Returns an array of names if succesful; NULL
1399  otherwise.]
1400
1401  SideEffects [None]
1402
1403  SeeAlso     []
1404
1405******************************************************************************/
1406static char **
1407bnetGenerateNewNames(
1408  st_table * hash /* table of existing names (or NULL) */,
1409  int  n /* number of names to be generated */)
1410{
1411    char **list;
1412    char name[256];
1413    int i;
1414
1415    if (n < 1) return(NULL);
1416
1417    list = ALLOC(char *,n);
1418    if (list == NULL) return(NULL);
1419    for (i = 0; i < n; i++) {
1420        do {
1421            sprintf(name, "var%d", newNameNumber);
1422            newNameNumber++;
1423        } while (hash != NULL && st_is_member(hash,name));
1424        list[i] = util_strsav(name);
1425    }
1426
1427    return(list);
1428
1429} /* bnetGenerateNewNames */
1430
1431
1432/**Function********************************************************************
1433
1434  Synopsis    [Writes blif for the reencoding logic.]
1435
1436  Description []
1437
1438  SideEffects [None]
1439
1440  SeeAlso     []
1441
1442******************************************************************************/
1443static int
1444bnetDumpReencodingLogic(
1445  DdManager * dd /* DD manager */,
1446  char * mname /* model name */,
1447  int  noutputs /* number of outputs */,
1448  DdNode ** outputs /* array of network outputs */,
1449  char ** inames /* array of network input names */,
1450  char ** altnames /* array of names of reencoded inputs */,
1451  char ** onames /* array of network output names */,
1452  FILE * fp /* file pointer */)
1453{
1454    int i;
1455    int retval;
1456    int nvars = Cudd_ReadSize(dd);
1457    int *support = NULL;
1458
1459    support = bnetFindVectorSupport(dd,outputs,noutputs);
1460    if (support == NULL) return(0);
1461
1462    /* Write the header (.model .inputs .outputs). */
1463    retval = fprintf(fp,".model %s.global\n.inputs",mname);
1464    if (retval == EOF) goto failure;
1465
1466    for (i = 0; i < nvars; i++) {
1467        if ((i%8 == 0)&&i) {
1468            retval = fprintf(fp," \\\n");
1469            if (retval == EOF) goto failure;
1470        }
1471        retval = fprintf(fp," %s", inames[i]);
1472        if (retval == EOF) goto failure;
1473    }
1474
1475    /* Write the .output line. */
1476    retval = fprintf(fp,"\n.outputs");
1477    if (retval == EOF) goto failure;
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", onames[i]);
1484        if (retval == EOF) goto failure;
1485    }
1486    retval = fprintf(fp,"\n");
1487    if (retval == EOF) goto failure;
1488
1489    /* Instantiate main subcircuit. */
1490    retval = fprintf(fp,"\n.subckt %s", 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        if (support[i] == 1) {
1498            retval = fprintf(fp," %s=%s", inames[i], altnames[i]);
1499            if (retval == EOF) goto failure;
1500        }
1501    }
1502    for (i = 0; i < noutputs; i++) {
1503        if ((i%8 == 0)&&i) {
1504            retval = fprintf(fp," \\\n");
1505            if (retval == EOF) goto failure;
1506        }
1507        retval = fprintf(fp," %s=%s", onames[i], onames[i]);
1508        if (retval == EOF) goto failure;
1509    }
1510    retval = fprintf(fp,"\n");
1511    if (retval == EOF) goto failure;
1512
1513    /* Instantiate reencoding subcircuit. */
1514    retval = fprintf(fp,"\n.subckt %s.reencode",mname);
1515    if (retval == EOF) goto failure;
1516    for (i = 0; i < nvars; i++) {
1517        if ((i%8 == 0)&&i) {
1518            retval = fprintf(fp," \\\n");
1519            if (retval == EOF) goto failure;
1520        }
1521        retval = fprintf(fp," %s=%s", inames[i], inames[i]);
1522        if (retval == EOF) goto failure;
1523    }
1524    retval = fprintf(fp," \\\n");
1525    if (retval == EOF) goto failure;
1526    for (i = 0; i < nvars; i++) {
1527        if ((i%8 == 0)&&i) {
1528            retval = fprintf(fp," \\\n");
1529            if (retval == EOF) goto failure;
1530        }
1531        if (support[i] == 1) {
1532            retval = fprintf(fp," %s=%s", altnames[i],altnames[i]);
1533            if (retval == EOF) goto failure;
1534        }
1535    }
1536    retval = fprintf(fp,"\n");
1537    if (retval == EOF) goto failure;
1538
1539    /* Write trailer. */
1540    retval = fprintf(fp,".end\n\n");
1541    if (retval == EOF) goto failure;
1542
1543    /* Write reencoding subcircuit. */
1544    retval = bnetBlifWriteReencode(dd,mname,inames,altnames,support,fp);
1545    if (retval == EOF) goto failure;
1546
1547    FREE(support);
1548    return(1);
1549
1550failure:
1551    if (support != NULL) FREE(support);
1552    return(0);
1553
1554} /* end of bnetDumpReencodingLogic */
1555
1556
1557/**Function********************************************************************
1558
1559  Synopsis    [Writes blif for the truth table of an n-input xnor.]
1560
1561  Description [Writes blif for the truth table of an n-input
1562  xnor. Returns 1 if successful; 0 otherwise.]
1563
1564  SideEffects [None]
1565
1566  SeeAlso     []
1567
1568******************************************************************************/
1569#if 0
1570static int
1571bnetBlifXnorTable(
1572  FILE * fp /* file pointer */,
1573  int  n /* number of inputs */)
1574{
1575    int power;  /* 2 to the power n */
1576    int i,j,k;
1577    int nzeroes;
1578    int retval;
1579    char *line;
1580
1581    line = ALLOC(char,n+1);
1582    if (line == NULL) return(0);
1583    line[n] = '\0';
1584
1585    for (i = 0, power = 1; i < n; i++) {
1586        power *= 2;
1587    }
1588
1589    for (i = 0; i < power; i++) {
1590        k = i;
1591        nzeroes = 0;
1592        for (j = 0; j < n; j++) {
1593            if (k & 1) {
1594                line[j] = '1';
1595            } else {
1596                line[j] = '0';
1597                nzeroes++;
1598            }
1599            k >>= 1;
1600        }
1601        if ((nzeroes & 1) == 0) {
1602            retval = fprintf(fp,"%s 1\n",line);
1603            if (retval == 0) return(0);
1604        }
1605    }
1606    return(1);
1607
1608} /* end of bnetBlifXnorTable */
1609#endif
1610
1611
1612/**Function********************************************************************
1613
1614  Synopsis    [Writes blif for the reencoding logic.]
1615
1616  Description [Writes blif for the reencoding logic. Exclusive NORs
1617  with more than two inputs are decomposed into cascaded two-input
1618  gates. Returns 1 if successful; 0 otherwise.]
1619
1620  SideEffects [None]
1621
1622  SeeAlso     []
1623
1624******************************************************************************/
1625static int
1626bnetBlifWriteReencode(
1627  DdManager * dd,
1628  char * mname,
1629  char ** inames,
1630  char ** altnames,
1631  int * support,
1632  FILE * fp)
1633{
1634    int retval;
1635    int nvars = Cudd_ReadSize(dd);
1636    int i,j;
1637    int ninp;
1638
1639    /* Write the header (.model .inputs .outputs). */
1640    retval = fprintf(fp,".model %s.reencode\n.inputs",mname);
1641    if (retval == EOF) return(0);
1642
1643    for (i = 0; i < nvars; i++) {
1644        if ((i%8 == 0)&&i) {
1645            retval = fprintf(fp," \\\n");
1646            if (retval == EOF) goto failure;
1647        }
1648        retval = fprintf(fp," %s", inames[i]);
1649        if (retval == EOF) goto failure;
1650    }
1651
1652    /* Write the .output line. */
1653    retval = fprintf(fp,"\n.outputs");
1654    if (retval == EOF) goto failure;
1655    for (i = 0; i < nvars; i++) {
1656        if ((i%8 == 0)&&i) {
1657            retval = fprintf(fp," \\\n");
1658            if (retval == EOF) goto failure;
1659        }
1660        if (support[i] == 1) {
1661            retval = fprintf(fp," %s", altnames[i]);
1662            if (retval == EOF) goto failure;
1663        }
1664    }
1665    retval = fprintf(fp,"\n");
1666    if (retval == EOF) goto failure;
1667
1668    /* Instantiate exclusive nors. */
1669    for (i = 0; i < nvars; i++) {
1670        char *in1 = NULL;
1671        char *in2 = NULL;
1672        char **oname;
1673        if (support[i] == 0) continue;
1674        ninp = 0;
1675        for (j = 0; j < nvars; j++) {
1676            if (Cudd_ReadLinear(dd,i,j)) {
1677                switch (ninp) {
1678                case 0:
1679                    in1 = inames[j];
1680                    ninp++;
1681                    break;
1682                case 1:
1683                    in2 = inames[j];
1684                    ninp++;
1685                    break;
1686                case 2:
1687                    oname = bnetGenerateNewNames(NULL,1);
1688                    retval = fprintf(fp,".names %s %s %s\n11 1\n00 1\n",
1689                             in1, in2, oname[0]);
1690                    if (retval == EOF) goto failure;
1691                    in1 = oname[0];
1692                    in2 = inames[j];
1693                    FREE(oname);
1694                    break;
1695                default:
1696                    goto failure;
1697                }
1698            }
1699        }
1700        switch (ninp) {
1701        case 1:
1702            retval = fprintf(fp,".names %s %s\n1 1\n", in1, altnames[i]);
1703            if (retval == EOF) goto failure;
1704            break;
1705        case 2:
1706            retval = fprintf(fp,".names %s %s %s\n11 1\n00 1\n",
1707                     in1, in2, altnames[i]);
1708            if (retval == EOF) goto failure;
1709            break;
1710        default:
1711            goto failure;
1712        }
1713    }
1714
1715    /* Write trailer. */
1716    retval = fprintf(fp,"\n.end\n\n");
1717    if (retval == EOF) goto failure;
1718
1719    return(1);
1720
1721failure:
1722    return(0);
1723
1724} /* end of bnetBlifWriteReencode */
1725
1726
1727/**Function********************************************************************
1728
1729  Synopsis    [Finds the support of a list of DDs.]
1730
1731  Description []
1732
1733  SideEffects [None]
1734
1735  SeeAlso     []
1736
1737******************************************************************************/
1738static int *
1739bnetFindVectorSupport(
1740  DdManager * dd,
1741  DdNode ** list,
1742  int  n)
1743{
1744    DdNode      *support = NULL;
1745    DdNode      *scan;
1746    int         *array = NULL;
1747    int         nvars = Cudd_ReadSize(dd);
1748    int         i;
1749
1750    /* Build an array with the support of the functions in list. */
1751    array = ALLOC(int,nvars);
1752    if (array == NULL) return(NULL);
1753    for (i = 0; i < nvars; i++) {
1754        array[i] = 0;
1755    }
1756
1757    /* Take the union of the supports of each output function. */
1758    for (i = 0; i < n; i++) {
1759        support = Cudd_Support(dd,list[i]);
1760        if (support == NULL) {
1761            FREE(array);
1762            return(NULL);
1763        }
1764        Cudd_Ref(support);
1765        scan = support;
1766        while (!Cudd_IsConstant(scan)) {
1767            array[scan->index] = 1;
1768            scan = Cudd_T(scan);
1769        }
1770        Cudd_IterDerefBdd(dd,support);
1771    }
1772
1773    return(array);
1774
1775} /* end of bnetFindVectorSupport */
1776
1777
1778/**Function********************************************************************
1779
1780  Synopsis    [Builds BDD for a XOR function.]
1781
1782  Description [Checks whether a function is a XOR with 2 or 3 inputs. If so,
1783  it builds the BDD. Returns 1 if the BDD has been built; 0 otherwise.]
1784
1785  SideEffects [None]
1786
1787  SeeAlso     []
1788
1789******************************************************************************/
1790static int
1791buildExorBDD(
1792  DdManager * dd,
1793  BnetNode * nd,
1794  st_table * hash,
1795  int  params,
1796  int  nodrop)
1797{
1798    int check[8];
1799    int i;
1800    int nlines;
1801    BnetTabline *line;
1802    DdNode *func, *var, *tmp;
1803    BnetNode *auxnd;
1804
1805    if (nd->ninp < 2 || nd->ninp > 3) return(0);
1806
1807    nlines = 1 << (nd->ninp - 1);
1808    for (i = 0; i < 8; i++) check[i] = 0;
1809    line = nd->f;
1810    while (line != NULL) {
1811        int num = 0;
1812        int count = 0;
1813        nlines--;
1814        for (i = 0; i < nd->ninp; i++) {
1815            num <<= 1;
1816            if (line->values[i] == '-') {
1817                return(0);
1818            } else if (line->values[i] == '1') {
1819                count++;
1820                num++;
1821            }
1822        }
1823        if ((count & 1) == 0) return(0);
1824        if (check[num]) return(0);
1825        line = line->next;
1826    }
1827    if (nlines != 0) return(0);
1828
1829    /* Initialize the exclusive sum to logical 0. */
1830    func = Cudd_ReadLogicZero(dd);
1831    Cudd_Ref(func);
1832
1833    /* Scan the inputs. */
1834    for (i = 0; i < nd->ninp; i++) {
1835        if (!st_lookup(hash, nd->inputs[i], &auxnd)) {
1836            goto failure;
1837        }
1838        if (params == BNET_LOCAL_DD) {
1839            if (auxnd->active == FALSE) {
1840                if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
1841                    goto failure;
1842                }
1843            }
1844            var = Cudd_ReadVars(dd,auxnd->var);
1845            if (var == NULL) goto failure;
1846            Cudd_Ref(var);
1847        } else { /* params == BNET_GLOBAL_DD */
1848            if (auxnd->dd == NULL) {
1849                if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
1850                    goto failure;
1851                }
1852            }
1853            var = auxnd->dd;
1854        }
1855        tmp = Cudd_bddXor(dd,func,var);
1856        if (tmp == NULL) goto failure;
1857        Cudd_Ref(tmp);
1858        Cudd_IterDerefBdd(dd,func);
1859        if (params == BNET_LOCAL_DD) {
1860            Cudd_IterDerefBdd(dd,var);
1861        }
1862        func = tmp;
1863    }
1864    nd->dd = func;
1865
1866    /* Associate a variable to this node if local BDDs are being
1867    ** built. This is done at the end, so that the primary inputs tend
1868    ** to get lower indices.
1869    */
1870    if (params == BNET_LOCAL_DD && nd->active == FALSE) {
1871        DdNode *auxfunc = Cudd_bddNewVar(dd);
1872        if (auxfunc == NULL) goto failure;
1873        Cudd_Ref(auxfunc);
1874        nd->var = auxfunc->index;
1875        nd->active = TRUE;
1876        Cudd_IterDerefBdd(dd,auxfunc);
1877    }
1878
1879    return(1);
1880failure:
1881    return(0);
1882
1883} /* end of buildExorBDD */
1884
1885
1886/**Function********************************************************************
1887
1888  Synopsis    [Builds BDD for a multiplexer.]
1889
1890  Description [Checks whether a function is a 2-to-1 multiplexer. If so,
1891  it builds the BDD. Returns 1 if the BDD has been built; 0 otherwise.]
1892
1893  SideEffects [None]
1894
1895  SeeAlso     []
1896
1897******************************************************************************/
1898static int
1899buildMuxBDD(
1900  DdManager * dd,
1901  BnetNode * nd,
1902  st_table * hash,
1903  int  params,
1904  int  nodrop)
1905{
1906    BnetTabline *line;
1907    char *values[2];
1908    int mux[2];
1909    int phase[2];
1910    int j;
1911    int nlines = 0;
1912    int controlC = -1;
1913    int controlR = -1;
1914    DdNode *func, *f, *g, *h;
1915    BnetNode *auxnd;
1916
1917    if (nd->ninp != 3) return(0);
1918
1919    for (line = nd->f; line != NULL; line = line->next) {
1920        int dc = 0;
1921        if (nlines > 1) return(0);
1922        values[nlines] = line->values;
1923        for (j = 0; j < 3; j++) {
1924            if (values[nlines][j] == '-') {
1925                if (dc) return(0);
1926                dc = 1;
1927            }
1928        }
1929        if (!dc) return(0);
1930        nlines++;
1931    }
1932    /* At this point we know we have:
1933    **   3 inputs
1934    **   2 lines
1935    **   1 dash in each line
1936    ** If the two dashes are not in the same column, then there is
1937    ** exaclty one column without dashes: the control column.
1938    */
1939    for (j = 0; j < 3; j++) {
1940        if (values[0][j] == '-' && values[1][j] == '-') return(0);
1941        if (values[0][j] != '-' && values[1][j] != '-') {
1942            if (values[0][j] == values[1][j]) return(0);
1943            controlC = j;
1944            controlR = values[0][j] == '0';
1945        }
1946    }
1947    assert(controlC != -1 && controlR != -1);
1948    /* At this point we know that there is indeed no column with two
1949    ** dashes. The control column has been identified, and we know that
1950    ** its two elelments are different. */
1951    for (j = 0; j < 3; j++) {
1952        if (j == controlC) continue;
1953        if (values[controlR][j] == '1') {
1954            mux[0] = j;
1955            phase[0] = 0;
1956        } else if (values[controlR][j] == '0') {
1957            mux[0] = j;
1958            phase[0] = 1;
1959        } else if (values[1-controlR][j] == '1') {
1960            mux[1] = j;
1961            phase[1] = 0;
1962        } else if (values[1-controlR][j] == '0') {
1963            mux[1] = j;
1964            phase[1] = 1;
1965        }
1966    }
1967
1968    /* Get the inputs. */
1969    if (!st_lookup(hash, nd->inputs[controlC], &auxnd)) {
1970        goto failure;
1971    }
1972    if (params == BNET_LOCAL_DD) {
1973        if (auxnd->active == FALSE) {
1974            if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
1975                goto failure;
1976            }
1977        }
1978        f = Cudd_ReadVars(dd,auxnd->var);
1979        if (f == NULL) goto failure;
1980        Cudd_Ref(f);
1981    } else { /* params == BNET_GLOBAL_DD */
1982        if (auxnd->dd == NULL) {
1983            if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
1984                goto failure;
1985            }
1986        }
1987        f = auxnd->dd;
1988    }
1989    if (!st_lookup(hash, nd->inputs[mux[0]], &auxnd)) {
1990        goto failure;
1991    }
1992    if (params == BNET_LOCAL_DD) {
1993        if (auxnd->active == FALSE) {
1994            if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
1995                goto failure;
1996            }
1997        }
1998        g = Cudd_ReadVars(dd,auxnd->var);
1999        if (g == NULL) goto failure;
2000        Cudd_Ref(g);
2001    } else { /* params == BNET_GLOBAL_DD */
2002        if (auxnd->dd == NULL) {
2003            if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
2004                goto failure;
2005            }
2006        }
2007        g = auxnd->dd;
2008    }
2009    g = Cudd_NotCond(g,phase[0]);
2010    if (!st_lookup(hash, nd->inputs[mux[1]], &auxnd)) {
2011        goto failure;
2012    }
2013    if (params == BNET_LOCAL_DD) {
2014        if (auxnd->active == FALSE) {
2015            if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
2016                goto failure;
2017            }
2018        }
2019        h = Cudd_ReadVars(dd,auxnd->var);
2020        if (h == NULL) goto failure;
2021        Cudd_Ref(h);
2022    } else { /* params == BNET_GLOBAL_DD */
2023        if (auxnd->dd == NULL) {
2024            if (!Bnet_BuildNodeBDD(dd,auxnd,hash,params,nodrop)) {
2025                goto failure;
2026            }
2027        }
2028        h = auxnd->dd;
2029    }
2030    h = Cudd_NotCond(h,phase[1]);
2031    func = Cudd_bddIte(dd,f,g,h);
2032    if (func == NULL) goto failure;
2033    Cudd_Ref(func);
2034    if (params == BNET_LOCAL_DD) {
2035        Cudd_IterDerefBdd(dd,f);
2036        Cudd_IterDerefBdd(dd,g);
2037        Cudd_IterDerefBdd(dd,h);
2038    }
2039    nd->dd = func;
2040
2041    /* Associate a variable to this node if local BDDs are being
2042    ** built. This is done at the end, so that the primary inputs tend
2043    ** to get lower indices.
2044    */
2045    if (params == BNET_LOCAL_DD && nd->active == FALSE) {
2046        DdNode *auxfunc = Cudd_bddNewVar(dd);
2047        if (auxfunc == NULL) goto failure;
2048        Cudd_Ref(auxfunc);
2049        nd->var = auxfunc->index;
2050        nd->active = TRUE;
2051        Cudd_IterDerefBdd(dd,auxfunc);
2052    }
2053
2054    return(1);
2055failure:
2056    return(0);
2057
2058} /* end of buildExorBDD */
2059
2060
2061/**Function********************************************************************
2062
2063  Synopsis    [Sets the level of each node.]
2064
2065  Description [Sets the level of each node. Returns 1 if successful; 0
2066  otherwise.]
2067
2068  SideEffects [Changes the level and visited fields of the nodes it
2069  visits.]
2070
2071  SeeAlso     [bnetLevelDFS]
2072
2073******************************************************************************/
2074static int
2075bnetSetLevel(
2076  BnetNetwork * net)
2077{
2078    BnetNode *node;
2079
2080    /* Recursively visit nodes. This is pretty inefficient, because we
2081    ** visit all nodes in this loop, and most of them in the recursive
2082    ** calls to bnetLevelDFS. However, this approach guarantees that
2083    ** all nodes will be reached ven if there are dangling outputs. */
2084    node = net->nodes;
2085    while (node != NULL) {
2086        if (!bnetLevelDFS(net,node)) return(0);
2087        node = node->next;
2088    }
2089
2090    /* Clear visited flags. */
2091    node = net->nodes;
2092    while (node != NULL) {
2093        node->visited = 0;
2094        node = node->next;
2095    }
2096    return(1);
2097
2098} /* end of bnetSetLevel */
2099
2100
2101/**Function********************************************************************
2102
2103  Synopsis    [Does a DFS from a node setting the level field.]
2104
2105  Description [Does a DFS from a node setting the level field. Returns
2106  1 if successful; 0 otherwise.]
2107
2108  SideEffects [Changes the level and visited fields of the nodes it
2109  visits.]
2110
2111  SeeAlso     [bnetSetLevel]
2112
2113******************************************************************************/
2114static int
2115bnetLevelDFS(
2116  BnetNetwork * net,
2117  BnetNode * node)
2118{
2119    int i;
2120    BnetNode *auxnd;
2121
2122    if (node->visited == 1) {
2123        return(1);
2124    }
2125
2126    node->visited = 1;
2127
2128    /* Graphical sources have level 0.  This is the final value if the
2129    ** node has no fan-ins. Otherwise the successive loop will
2130    ** increase the level. */
2131    node->level = 0;
2132    for (i = 0; i < node->ninp; i++) {
2133        if (!st_lookup(net->hash, node->inputs[i], &auxnd)) {
2134            return(0);
2135        }
2136        if (!bnetLevelDFS(net,auxnd)) {
2137            return(0);
2138        }
2139        if (auxnd->level >= node->level) node->level = 1 + auxnd->level;
2140    }
2141    return(1);
2142
2143} /* end of bnetLevelDFS */
2144
2145
2146/**Function********************************************************************
2147
2148  Synopsis    [Orders network roots for variable ordering.]
2149
2150  Description [Orders network roots for variable ordering. Returns
2151  an array with the ordered outputs and next state variables if
2152  successful; NULL otherwise.]
2153
2154  SideEffects [None]
2155
2156  SeeAlso     []
2157
2158******************************************************************************/
2159static BnetNode **
2160bnetOrderRoots(
2161  BnetNetwork * net,
2162  int * nroots)
2163{
2164    int i, noutputs;
2165    BnetNode *node;
2166    BnetNode **nodes = NULL;
2167
2168    /* Initialize data structures. */
2169    noutputs = net->noutputs;
2170    nodes = ALLOC(BnetNode *, noutputs);
2171    if (nodes == NULL) goto endgame;
2172
2173    /* Find output names and levels. */
2174    for (i = 0; i < net->noutputs; i++) {
2175        if (!st_lookup(net->hash,net->outputs[i],&node)) {
2176            goto endgame;
2177        }
2178        nodes[i] = node;
2179    }
2180
2181    qsort((void *)nodes, noutputs, sizeof(BnetNode *),
2182          (DD_QSFP)bnetLevelCompare);
2183    *nroots = noutputs;
2184    return(nodes);
2185
2186endgame:
2187    if (nodes != NULL) FREE(nodes);
2188    return(NULL);
2189
2190} /* end of bnetOrderRoots */
2191
2192
2193/**Function********************************************************************
2194
2195  Synopsis    [Comparison function used by qsort.]
2196
2197  Description [Comparison function used by qsort to order the
2198  variables according to the number of keys in the subtables.
2199  Returns the difference in number of keys between the two
2200  variables being compared.]
2201
2202  SideEffects [None]
2203
2204******************************************************************************/
2205static int
2206bnetLevelCompare(
2207  BnetNode ** x,
2208  BnetNode ** y)
2209{
2210    return((*y)->level - (*x)->level);
2211
2212} /* end of bnetLevelCompare */
2213
2214
2215/**Function********************************************************************
2216
2217  Synopsis    [Does a DFS from a node ordering the inputs.]
2218
2219  Description [Does a DFS from a node ordering the inputs. Returns
2220  1 if successful; 0 otherwise.]
2221
2222  SideEffects [Changes visited fields of the nodes it visits.]
2223
2224  SeeAlso     [Bnet_DfsVariableOrder]
2225
2226******************************************************************************/
2227static int
2228bnetDfsOrder(
2229  DdManager * dd,
2230  BnetNetwork * net,
2231  BnetNode * node)
2232{
2233    int i;
2234    BnetNode *auxnd;
2235    BnetNode **fanins;
2236
2237    if (node->visited == 1) {
2238        return(1);
2239    }
2240
2241    node->visited = 1;
2242    if (node->type == BNET_INPUT_NODE ||
2243        node->type == BNET_PRESENT_STATE_NODE) {
2244        node->dd = Cudd_bddNewVar(dd);
2245        if (node->dd == NULL) return(0);
2246        Cudd_Ref(node->dd);
2247        node->active = TRUE;
2248        node->var = node->dd->index;
2249        return(1);
2250    }
2251
2252    fanins = ALLOC(BnetNode *, node->ninp);
2253    if (fanins == NULL) return(0);
2254
2255    for (i = 0; i < node->ninp; i++) {
2256        if (!st_lookup(net->hash, node->inputs[i], &auxnd)) {
2257            FREE(fanins);
2258            return(0);
2259        }
2260        fanins[i] = auxnd;
2261    }
2262
2263    qsort((void *)fanins, node->ninp, sizeof(BnetNode *),
2264          (DD_QSFP)bnetLevelCompare);
2265    for (i = 0; i < node->ninp; i++) {
2266        /* for (i = node->ninp - 1; i >= 0; i--) { */
2267        int res = bnetDfsOrder(dd,net,fanins[i]);
2268        if (res == 0) {
2269            FREE(fanins);
2270            return(0);
2271        }
2272    }
2273    FREE(fanins);
2274    return(1);
2275
2276} /* end of bnetLevelDFS */
Note: See TracBrowser for help on using the repository browser.