source: icGREP/icgrep-devel/cudd-2.5.1/nanotrav/ntr.c @ 4597

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

Upload of the CUDD library.

File size: 83.5 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [ntr.c]
4
5  PackageName [ntr]
6
7  Synopsis    [A very simple reachability analysis program.]
8
9  Description []
10
11  SeeAlso     []
12
13  Author      [Fabio Somenzi]
14
15  Copyright   [Copyright (c) 1995-2012, Regents of the University of Colorado
16
17  All rights reserved.
18
19  Redistribution and use in source and binary forms, with or without
20  modification, are permitted provided that the following conditions
21  are met:
22
23  Redistributions of source code must retain the above copyright
24  notice, this list of conditions and the following disclaimer.
25
26  Redistributions in binary form must reproduce the above copyright
27  notice, this list of conditions and the following disclaimer in the
28  documentation and/or other materials provided with the distribution.
29
30  Neither the name of the University of Colorado nor the names of its
31  contributors may be used to endorse or promote products derived from
32  this software without specific prior written permission.
33
34  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
35  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
36  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
37  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
38  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
39  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
40  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
41  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
42  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
43  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
44  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
45  POSSIBILITY OF SUCH DAMAGE.]
46
47******************************************************************************/
48
49#include "ntr.h"
50
51/*---------------------------------------------------------------------------*/
52/* Constant declarations                                                     */
53/*---------------------------------------------------------------------------*/
54
55#define NTR_MAX_DEP_SIZE 20
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: ntr.c,v 1.29 2015/01/03 19:41:42 fabio Exp fabio $";
71#endif
72
73static const char *onames[] = { "T", "R" };     /* names of functions to be dumped */
74static double *signatures;              /* signatures for all variables */
75static BnetNetwork *staticNet;  /* pointer to network used by qsort
76                                ** comparison function */
77static DdNode **staticPart;     /* pointer to parts used by qsort
78                                ** comparison function */
79
80/*---------------------------------------------------------------------------*/
81/* Macro declarations                                                        */
82/*---------------------------------------------------------------------------*/
83
84/**AutomaticStart*************************************************************/
85
86/*---------------------------------------------------------------------------*/
87/* Static function prototypes                                                */
88/*---------------------------------------------------------------------------*/
89
90static DdNode * makecube (DdManager *dd, DdNode **x, int n);
91static void ntrInitializeCount (BnetNetwork *net, NtrOptions *option);
92static void ntrCountDFS (BnetNetwork *net, BnetNode *node);
93static DdNode * ntrImage (DdManager *dd, NtrPartTR *TR, DdNode *from, NtrOptions *option);
94static DdNode * ntrPreimage (DdManager *dd, NtrPartTR *T, DdNode *from);
95static DdNode * ntrChooseFrom (DdManager *dd, DdNode *neW, DdNode *reached, NtrOptions *option);
96static DdNode * ntrUpdateReached (DdManager *dd, DdNode *oldreached, DdNode *to);
97static int ntrLatchDependencies (DdManager *dd, DdNode *reached, BnetNetwork *net, NtrOptions *option);
98static NtrPartTR * ntrEliminateDependencies (DdManager *dd, NtrPartTR *TR, DdNode **states, NtrOptions *option);
99static int ntrUpdateQuantificationSchedule (DdManager *dd, NtrPartTR *T);
100static int ntrSignatureCompare (int * ptrX, int * ptrY);
101static int ntrSignatureCompare2 (int * ptrX, int * ptrY);
102static int ntrPartCompare (int * ptrX, int * ptrY);
103static char ** ntrAllocMatrix (int nrows, int ncols);
104static void ntrFreeMatrix (char **matrix);
105static void ntrPermuteParts (DdNode **a, DdNode **b, int *comesFrom, int *goesTo, int size);
106
107/**AutomaticEnd***************************************************************/
108
109/*---------------------------------------------------------------------------*/
110/* Definition of exported functions                                          */
111/*---------------------------------------------------------------------------*/
112
113
114/**Function********************************************************************
115
116  Synopsis    [Builds DDs for a network outputs and next state
117  functions.]
118
119  Description [Builds DDs for a network outputs and next state
120  functions. The method is really brain-dead, but it is very simple.
121  Returns 1 in case of success; 0 otherwise. Some inputs to the network
122  may be shared with another network whose DDs have already been built.
123  In this case we want to share the DDs as well.]
124
125  SideEffects [the dd fields of the network nodes are modified. Uses the
126  count fields of the nodes.]
127
128  SeeAlso     []
129
130******************************************************************************/
131int
132Ntr_buildDDs(
133  BnetNetwork * net /* network for which DDs are to be built */,
134  DdManager * dd /* DD manager */,
135  NtrOptions * option /* option structure */,
136  BnetNetwork * net2 /* companion network with which inputs may be shared */)
137{
138    int pr = option->verb;
139    int result;
140    int i;
141    BnetNode *node, *node2;
142
143    /* If some inputs or present state variables are shared with
144    ** another network, we initialize their BDDs from that network.
145    */
146    if (net2 != NULL) {
147        for (i = 0; i < net->npis; i++) {
148            if (!st_lookup(net->hash,net->inputs[i],&node)) {
149                return(0);
150            }
151            if (!st_lookup(net2->hash,net->inputs[i],&node2)) {
152                /* This input is not shared. */
153                result = Bnet_BuildNodeBDD(dd,node,net->hash,
154                                           option->locGlob,option->nodrop);
155                if (result == 0) return(0);
156            } else {
157                if (node2->dd == NULL) return(0);
158                node->dd = node2->dd;
159                Cudd_Ref(node->dd);
160                node->var = node2->var;
161                node->active = node2->active;
162            }
163        }
164        for (i = 0; i < net->nlatches; i++) {
165            if (!st_lookup(net->hash,net->latches[i][1],&node)) {
166                return(0);
167            }
168            if (!st_lookup(net2->hash,net->latches[i][1],&node2)) {
169                /* This present state variable is not shared. */
170                result = Bnet_BuildNodeBDD(dd,node,net->hash,
171                                           option->locGlob,option->nodrop);
172                if (result == 0) return(0);
173            } else {
174                if (node2->dd == NULL) return(0);
175                node->dd = node2->dd;
176                Cudd_Ref(node->dd);
177                node->var = node2->var;
178                node->active = node2->active;
179            }
180        }
181    } else {
182        /* First assign variables to inputs if the order is provided.
183        ** (Either in the .blif file or in an order file.)
184        */
185        if (option->ordering == PI_PS_FROM_FILE) {
186            /* Follow order given in input file. First primary inputs
187            ** and then present state variables.
188            */
189            for (i = 0; i < net->npis; i++) {
190                if (!st_lookup(net->hash,net->inputs[i],&node)) {
191                    return(0);
192                }
193                result = Bnet_BuildNodeBDD(dd,node,net->hash,
194                                           option->locGlob,option->nodrop);
195                if (result == 0) return(0);
196            }
197            for (i = 0; i < net->nlatches; i++) {
198                if (!st_lookup(net->hash,net->latches[i][1],&node)) {
199                    return(0);
200                }
201                result = Bnet_BuildNodeBDD(dd,node,net->hash,
202                                           option->locGlob,option->nodrop);
203                if (result == 0) return(0);
204            }
205        } else if (option->ordering == PI_PS_GIVEN) {
206            result = Bnet_ReadOrder(dd,option->orderPiPs,net,option->locGlob,
207                                    option->nodrop);
208            if (result == 0) return(0);
209        } else {
210            result = Bnet_DfsVariableOrder(dd,net);
211            if (result == 0) return(0);
212        }
213    }
214    /* At this point the BDDs of all primary inputs and present state
215    ** variables have been built. */
216
217    /* Currently noBuild doesn't do much. */
218    if (option->noBuild == TRUE)
219        return(1);
220
221    if (option->locGlob == BNET_LOCAL_DD) {
222        node = net->nodes;
223        while (node != NULL) {
224            result = Bnet_BuildNodeBDD(dd,node,net->hash,BNET_LOCAL_DD,TRUE);
225            if (result == 0) {
226                return(0);
227            }
228            if (pr > 2) {
229                (void) fprintf(stdout,"%s",node->name);
230                Cudd_PrintDebug(dd,node->dd,Cudd_ReadSize(dd),pr);
231            }
232            node = node->next;
233        }
234    } else { /* option->locGlob == BNET_GLOBAL_DD */
235        /* Create BDDs with DFS from the primary outputs and the next
236        ** state functions. If the inputs had not been ordered yet,
237        ** this would result in a DFS order for the variables.
238        */
239
240        ntrInitializeCount(net,option);
241
242        if (option->node != NULL &&
243            option->closestCube == FALSE && option->dontcares == FALSE) {
244            if (!st_lookup(net->hash,option->node,&node)) {
245                return(0);
246            }
247            result = Bnet_BuildNodeBDD(dd,node,net->hash,BNET_GLOBAL_DD,
248                                       option->nodrop);
249            if (result == 0) return(0);
250        } else {
251            if (option->stateOnly == FALSE) {
252                for (i = 0; i < net->npos; i++) {
253                    if (!st_lookup(net->hash,net->outputs[i],&node)) {
254                        continue;
255                    }
256                    result = Bnet_BuildNodeBDD(dd,node,net->hash,
257                                               BNET_GLOBAL_DD,option->nodrop);
258                    if (result == 0) return(0);
259                    if (option->progress)  {
260                        (void) fprintf(stdout,"%s\n",node->name);
261                    }
262#if 0
263                    Cudd_PrintDebug(dd,node->dd,net->ninputs,option->verb);
264#endif
265                }
266            }
267            for (i = 0; i < net->nlatches; i++) {
268                if (!st_lookup(net->hash,net->latches[i][0],&node)) {
269                    continue;
270                }
271                result = Bnet_BuildNodeBDD(dd,node,net->hash,BNET_GLOBAL_DD,
272                                           option->nodrop);
273                if (result == 0) return(0);
274                if (option->progress)  {
275                    (void) fprintf(stdout,"%s\n",node->name);
276                }
277#if 0
278                Cudd_PrintDebug(dd,node->dd,net->ninputs,option->verb);
279#endif
280            }
281        }
282        /* Make sure all inputs have a DD and dereference the DDs of
283        ** the nodes that are not reachable from the outputs.
284        */
285        for (i = 0; i < net->npis; i++) {
286            if (!st_lookup(net->hash,net->inputs[i],&node)) {
287                return(0);
288            }
289            result = Bnet_BuildNodeBDD(dd,node,net->hash,BNET_GLOBAL_DD,
290                                       option->nodrop);
291            if (result == 0) return(0);
292            if (node->count == -1) Cudd_RecursiveDeref(dd,node->dd);
293        }
294        for (i = 0; i < net->nlatches; i++) {
295            if (!st_lookup(net->hash,net->latches[i][1],&node)) {
296                return(0);
297            }
298            result = Bnet_BuildNodeBDD(dd,node,net->hash,BNET_GLOBAL_DD,
299                                       option->nodrop);
300            if (result == 0) return(0);
301            if (node->count == -1) Cudd_RecursiveDeref(dd,node->dd);
302        }
303
304        /* Dispose of the BDDs of the internal nodes if they have not
305        ** been dropped already.
306        */
307        if (option->nodrop == TRUE) {
308            for (node = net->nodes; node != NULL; node = node->next) {
309                if (node->dd != NULL && node->count != -1 &&
310                    (node->type == BNET_INTERNAL_NODE ||
311                    node->type == BNET_INPUT_NODE ||
312                    node->type == BNET_PRESENT_STATE_NODE)) {
313                    Cudd_RecursiveDeref(dd,node->dd);
314                    if (node->type == BNET_INTERNAL_NODE) node->dd = NULL;
315                }
316            }
317        }
318    }
319
320    return(1);
321
322} /* end of buildDD */
323
324
325/**Function********************************************************************
326
327  Synopsis    [Builds the transition relation for a network.]
328
329  Description [Builds the transition relation for a network. Returns a
330  pointer to the transition relation structure if successful; NULL
331  otherwise.]
332
333  SideEffects [None]
334
335  SeeAlso     []
336
337******************************************************************************/
338NtrPartTR *
339Ntr_buildTR(
340  DdManager * dd /* manager */,
341  BnetNetwork * net /* network */,
342  NtrOptions * option /* options */,
343  int  image /* image type: monolithic ... */)
344{
345    NtrPartTR *TR;
346    DdNode *T, *delta, *support, *scan, *tmp, *preiabs, *prepabs;
347    DdNode **part, **absicubes, **abspcubes, **nscube, *mnscube;
348    DdNode **x, **y;
349    DdNode **pi;
350    int i;
351    int xlevel;
352    BnetNode *node;
353    int *schedule;
354    int depth = 0;
355
356    /* Initialize transition relation structure. */
357    TR = ALLOC(NtrPartTR,1);
358    if (TR == NULL) goto endgame;
359    TR->nlatches = net->nlatches;
360    if (image == NTR_IMAGE_MONO) {
361        TR->nparts = 1;
362    } else if (image == NTR_IMAGE_PART || image == NTR_IMAGE_CLIP ||
363               image == NTR_IMAGE_DEPEND) {
364        TR->nparts = net->nlatches;
365    } else {
366        (void) fprintf(stderr,"Unrecognized image method (%d). Using part.\n",
367                       image);
368        TR->nparts = net->nlatches;
369    }
370    TR->factors = Ntr_InitHeap(TR->nlatches);
371    if (TR->factors == NULL) goto endgame;
372    /* Allocate arrays for present state and next state variables. */
373    TR->x = x = ALLOC(DdNode *,TR->nlatches);
374    if (x == NULL) goto endgame;
375    TR->y = y = ALLOC(DdNode *,TR->nlatches);
376    if (y == NULL) goto endgame;
377    /* Allocate array for primary input variables. */
378    pi = ALLOC(DdNode *,net->npis);
379    if (pi == NULL) goto endgame;
380    /* Allocate array for partitioned transition relation. */
381    part = ALLOC(DdNode *,net->nlatches);
382    if (part == NULL) goto endgame;
383    /* Allocate array of next state cubes. */
384    nscube = ALLOC(DdNode *,net->nlatches);
385    if (nscube == NULL) goto endgame;
386    /* Allocate array for quantification schedule and initialize it. */
387    schedule = ALLOC(int,Cudd_ReadSize(dd));
388    if (schedule == NULL) goto endgame;
389    for (i = 0; i < Cudd_ReadSize(dd); i++) {
390        schedule[i] = -1;
391    }
392
393    /* Create partitioned transition relation from network. */
394    TR->xw = Cudd_ReadOne(dd);
395    Cudd_Ref(TR->xw);
396    for (i = 0; i < net->nlatches; i++) {
397        if (!st_lookup(net->hash,net->latches[i][1],&node)) {
398            goto endgame;
399        }
400        x[i] = node->dd;
401        Cudd_Ref(x[i]);
402        /* Add present state variable to cube TR->xw. */
403        tmp = Cudd_bddAnd(dd,TR->xw,x[i]);
404        if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
405        Cudd_RecursiveDeref(dd,TR->xw);
406        TR->xw = tmp;
407        /* Create new y variable immediately above the x variable. */
408        xlevel = Cudd_ReadPerm(dd,x[i]->index);
409        y[i] = Cudd_bddNewVarAtLevel(dd,xlevel);
410        Cudd_Ref(y[i]);
411        /* Initialize cube of next state variables for this part. */
412        nscube[i] = y[i];
413        Cudd_Ref(nscube[i]);
414        /* Group present and next state variable if so requested. */
415        if (option->groupnsps != NTR_GROUP_NONE) {
416            int method = option->groupnsps == NTR_GROUP_DEFAULT ?
417                MTR_DEFAULT : MTR_FIXED;
418            if (Cudd_MakeTreeNode(dd,y[i]->index,2,method) == NULL)
419                goto endgame;
420        }
421        /* Get next state function and create transition relation part. */
422        if (!st_lookup(net->hash,net->latches[i][0],&node)) {
423            goto endgame;
424        }
425        delta = node->dd;
426        if (image != NTR_IMAGE_DEPEND) {
427            part[i] = Cudd_bddXnor(dd,delta,y[i]);
428            if (part[i] == NULL) goto endgame;
429        } else {
430            part[i] = delta;
431        }
432        Cudd_Ref(part[i]);
433        /* Collect scheduling info for this delta. At the end of this loop
434        ** schedule[i] == j means that the variable of index i does not
435        ** appear in any part with index greater than j, unless j == -1,
436        ** in which case the variable appears in no part.
437        */
438        support = Cudd_Support(dd,delta);
439        Cudd_Ref(support);
440        scan = support;
441        while (!Cudd_IsConstant(scan)) {
442            schedule[scan->index] = i;
443            scan = Cudd_T(scan);
444        }
445        Cudd_RecursiveDeref(dd,support);
446    }
447
448    /* Collect primary inputs. */
449    for (i = 0; i < net->npis; i++) {
450        if (!st_lookup(net->hash,net->inputs[i],&node)) {
451            goto endgame;
452        }
453        pi[i] = node->dd;
454        tmp  = Cudd_bddAnd(dd,TR->xw,pi[i]);
455        if (tmp == NULL) goto endgame; Cudd_Ref(tmp);
456        Cudd_RecursiveDeref(dd,TR->xw);
457        TR->xw = tmp;
458    }
459
460    /* Build abstraction cubes. First primary input variables that go
461    ** in the abstraction cubes for both monolithic and partitioned
462    ** transition relations. */
463    absicubes = ALLOC(DdNode *, net->nlatches);
464    if (absicubes == NULL) goto endgame;
465    abspcubes = ALLOC(DdNode *, net->nlatches);
466    if (abspcubes == NULL) goto endgame;
467
468    for (i = 0; i < net->nlatches; i++) {
469        absicubes[i] = Cudd_ReadOne(dd);
470        Cudd_Ref(absicubes[i]);
471    }
472    preiabs = Cudd_ReadOne(dd);
473    Cudd_Ref(preiabs);
474
475    for (i = 0; i < net->npis; i++) {
476        int j = pi[i]->index;
477        int k = schedule[j];
478        if (k >= 0) {
479            tmp = Cudd_bddAnd(dd,absicubes[k],pi[i]);
480            if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
481            Cudd_RecursiveDeref(dd,absicubes[k]);
482            absicubes[k] = tmp;
483        } else {
484            tmp = Cudd_bddAnd(dd,preiabs,pi[i]);
485            if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
486            Cudd_RecursiveDeref(dd,preiabs);
487            preiabs = tmp;
488        }
489    }
490    FREE(pi);
491
492    /* Build preimage abstraction cubes from image abstraction cubes. */
493    for (i = 0; i < net->nlatches; i++) {
494        abspcubes[i] = Cudd_bddAnd(dd,absicubes[i],nscube[i]);
495        if (abspcubes[i] == NULL) return(NULL);
496        Cudd_Ref(abspcubes[i]);
497    }
498    Cudd_Ref(prepabs = preiabs);
499
500    /* For partitioned transition relations we add present state variables
501    ** to the image abstraction cubes. */
502    if (image != NTR_IMAGE_MONO) {
503        for (i = 0; i < net->nlatches; i++) {
504            int j = x[i]->index;
505            int k = schedule[j];
506            if (k >= 0) {
507                tmp = Cudd_bddAnd(dd,absicubes[k],x[i]);
508                if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
509                Cudd_RecursiveDeref(dd,absicubes[k]);
510                absicubes[k] = tmp;
511            } else {
512                tmp = Cudd_bddAnd(dd,preiabs,x[i]);
513                if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
514                Cudd_RecursiveDeref(dd,preiabs);
515                preiabs = tmp;
516            }
517        }
518    }
519    FREE(schedule);
520
521    if (image != NTR_IMAGE_MONO) {
522        TR->part = part;
523        TR->icube = absicubes;
524        TR->pcube = abspcubes;
525        TR->nscube = nscube;
526        TR->preiabs = preiabs;
527        TR->prepabs = prepabs;
528        return(TR);
529    }
530
531    /* Here we are building a monolithic TR. */
532
533    /* Reinitialize the cube of variables to be quantified before
534    ** image computation. */
535    Cudd_RecursiveDeref(dd,preiabs);
536    preiabs = Cudd_ReadOne(dd);
537    Cudd_Ref(preiabs);
538
539    if (option->imageClip != 1.0) {
540        depth = (int) ((double) Cudd_ReadSize(dd) * option->imageClip);
541    }
542
543    /* Collapse transition relation. */
544    T = Cudd_ReadOne(dd);
545    Cudd_Ref(T);
546    mnscube = Cudd_ReadOne(dd);
547    Cudd_Ref(mnscube);
548    for (i = 0; i < net->nlatches; i++) {
549        /* Eliminate the primary inputs that do not appear in other parts. */
550        if (depth != 0) {
551            tmp = Cudd_bddClippingAndAbstract(dd,T,part[i],absicubes[i],
552                                              depth,option->approx);
553        } else {
554            tmp = Cudd_bddAndAbstract(dd,T,part[i],absicubes[i]);
555        }
556        Cudd_Ref(tmp);
557        Cudd_RecursiveDeref(dd,T);
558        Cudd_RecursiveDeref(dd,part[i]);
559        Cudd_RecursiveDeref(dd,absicubes[i]);
560        Cudd_RecursiveDeref(dd,abspcubes[i]);
561        if (option->threshold >= 0) {
562            if (option->approx) {
563                T = Cudd_RemapOverApprox(dd,tmp,2*net->nlatches,
564                                         option->threshold,option->quality);
565            } else {
566                T = Cudd_RemapUnderApprox(dd,tmp,2*net->nlatches,
567                                          option->threshold,option->quality);
568            }
569        } else {
570            T = tmp;
571        }
572        if (T == NULL) return(NULL);
573        Cudd_Ref(T);
574        Cudd_RecursiveDeref(dd,tmp);
575        /* Add the next state variables of this part to the cube of all
576        ** next state variables. */
577        tmp = Cudd_bddAnd(dd,mnscube,nscube[i]);
578        if (tmp == NULL) return(NULL);
579        Cudd_Ref(tmp);
580        Cudd_RecursiveDeref(dd,mnscube);
581        mnscube = tmp;
582        Cudd_RecursiveDeref(dd,nscube[i]);
583        (void) printf("@"); fflush(stdout);
584    }
585    (void) printf("\n");
586#if 0
587    (void) printf("T"); Cudd_PrintDebug(dd,T,2*net->nlatches,2);
588#endif
589
590    /* Clean up. */
591    FREE(absicubes);
592    FREE(abspcubes);
593    FREE(part);
594    FREE(nscube);
595
596    TR->part = part = ALLOC(DdNode *,1);
597    if (part == NULL) goto endgame;
598    part[0] = T;
599
600    /* Build cube of x (present state) variables for abstraction. */
601    TR->icube = absicubes = ALLOC(DdNode *,1);
602    if (absicubes == NULL) goto endgame;
603    absicubes[0] = makecube(dd,x,TR->nlatches);
604    if (absicubes[0] == NULL) return(0);
605    Cudd_Ref(absicubes[0]);
606    /* Build cube of y (next state) variables for abstraction. */
607    TR->pcube = abspcubes = ALLOC(DdNode *,1);
608    if (abspcubes == NULL) goto endgame;
609    abspcubes[0] = makecube(dd,y,TR->nlatches);
610    if (abspcubes[0] == NULL) return(0);
611    Cudd_Ref(abspcubes[0]);
612    TR->preiabs = preiabs;
613    TR->prepabs = prepabs;
614
615    TR->nscube = ALLOC(DdNode *,1);
616    if (TR->nscube == NULL) return(NULL);
617    TR->nscube[0] = mnscube;
618
619    return(TR);
620
621endgame:
622
623    return(NULL);
624
625} /* end of Ntr_buildTR */
626
627
628/**Function********************************************************************
629
630  Synopsis    [Frees the transition relation for a network.]
631
632  Description []
633
634  SideEffects [None]
635
636  SeeAlso     []
637
638******************************************************************************/
639void
640Ntr_freeTR(
641  DdManager * dd,
642  NtrPartTR * TR)
643{
644    int i;
645    for (i = 0; i < TR->nlatches; i++) {
646        Cudd_RecursiveDeref(dd,TR->x[i]);
647        Cudd_RecursiveDeref(dd,TR->y[i]);
648    }
649    FREE(TR->x);
650    FREE(TR->y);
651    for (i = 0; i < TR->nparts; i++) {
652        Cudd_RecursiveDeref(dd,TR->part[i]);
653        Cudd_RecursiveDeref(dd,TR->icube[i]);
654        Cudd_RecursiveDeref(dd,TR->pcube[i]);
655        Cudd_RecursiveDeref(dd,TR->nscube[i]);
656    }
657    FREE(TR->part);
658    FREE(TR->icube);
659    FREE(TR->pcube);
660    FREE(TR->nscube);
661    Cudd_RecursiveDeref(dd,TR->preiabs);
662    Cudd_RecursiveDeref(dd,TR->prepabs);
663    Cudd_RecursiveDeref(dd,TR->xw);
664    for (i = 0; i < TR->factors->nslots; i++) {
665        Cudd_RecursiveDeref(dd, (DdNode *) TR->factors->slots[i].item);
666    }
667    Ntr_FreeHeap(TR->factors);
668    FREE(TR);
669
670    return;
671
672} /* end of Ntr_freeTR */
673
674
675/**Function********************************************************************
676
677  Synopsis    [Makes a copy of a transition relation.]
678
679  Description [Makes a copy of a transition relation. Returns a pointer
680  to the copy if successful; NULL otherwise.]
681
682  SideEffects [None]
683
684  SeeAlso     [Ntr_buildTR Ntr_freeTR]
685
686******************************************************************************/
687NtrPartTR *
688Ntr_cloneTR(
689  NtrPartTR *TR)
690{
691    NtrPartTR *T;
692    int nparts, nlatches, i;
693
694    T = ALLOC(NtrPartTR,1);
695    if (T == NULL) return(NULL);
696    nparts = T->nparts = TR->nparts;
697    nlatches = T->nlatches = TR->nlatches;
698    T->part = ALLOC(DdNode *,nparts);
699    if (T->part == NULL) {
700        FREE(T);
701        return(NULL);
702    }
703    T->icube = ALLOC(DdNode *,nparts);
704    if (T->icube == NULL) {
705        FREE(T->part);
706        FREE(T);
707        return(NULL);
708    }
709    T->pcube = ALLOC(DdNode *,nparts);
710    if (T->pcube == NULL) {
711        FREE(T->icube);
712        FREE(T->part);
713        FREE(T);
714        return(NULL);
715    }
716    T->x = ALLOC(DdNode *,nlatches);
717    if (T->x == NULL) {
718        FREE(T->pcube);
719        FREE(T->icube);
720        FREE(T->part);
721        FREE(T);
722        return(NULL);
723    }
724    T->y = ALLOC(DdNode *,nlatches);
725    if (T->y == NULL) {
726        FREE(T->x);
727        FREE(T->pcube);
728        FREE(T->icube);
729        FREE(T->part);
730        FREE(T);
731        return(NULL);
732    }
733    T->nscube = ALLOC(DdNode *,nparts);
734    if (T->nscube == NULL) {
735        FREE(T->y);
736        FREE(T->x);
737        FREE(T->pcube);
738        FREE(T->icube);
739        FREE(T->part);
740        FREE(T);
741        return(NULL);
742    }
743    T->factors = Ntr_HeapClone(TR->factors);
744    if (T->factors == NULL) {
745        FREE(T->nscube);
746        FREE(T->y);
747        FREE(T->x);
748        FREE(T->pcube);
749        FREE(T->icube);
750        FREE(T->part);
751        FREE(T);
752        return(NULL);
753    }
754    for (i = 0; i < T->factors->nslots; i++) {
755        Cudd_Ref((DdNode *) T->factors->slots[i].item);
756    }
757    for (i = 0; i < nparts; i++) {
758        T->part[i] = TR->part[i];
759        Cudd_Ref(T->part[i]);
760        T->icube[i] = TR->icube[i];
761        Cudd_Ref(T->icube[i]);
762        T->pcube[i] = TR->pcube[i];
763        Cudd_Ref(T->pcube[i]);
764        T->nscube[i] = TR->nscube[i];
765        Cudd_Ref(T->nscube[i]);
766    }
767    T->preiabs = TR->preiabs;
768    Cudd_Ref(T->preiabs);
769    T->prepabs = TR->prepabs;
770    Cudd_Ref(T->prepabs);
771    T->xw = TR->xw;
772    Cudd_Ref(T->xw);
773    for (i = 0; i < nlatches; i++) {
774        T->x[i] = TR->x[i];
775        Cudd_Ref(T->x[i]);
776        T->y[i] = TR->y[i];
777        Cudd_Ref(T->y[i]);
778    }
779
780    return(T);
781
782} /* end of Ntr_cloneTR */
783
784
785/**Function********************************************************************
786
787  Synopsis    [Poor man's traversal procedure.]
788
789  Description [Poor man's traversal procedure. based on the monolithic
790  transition relation.  Returns 1 in case of success; 0 otherwise.]
791
792  SideEffects [None]
793
794  SeeAlso     [Ntr_ClosureTrav]
795
796******************************************************************************/
797int
798Ntr_Trav(
799  DdManager * dd /* DD manager */,
800  BnetNetwork * net /* network */,
801  NtrOptions * option /* options */)
802{
803    NtrPartTR *TR;              /* Transition relation */
804    DdNode *init;               /* initial state(s) */
805    DdNode *from;
806    DdNode *to;
807    DdNode *reached;
808    DdNode *neW;
809    DdNode *one, *zero;
810    int depth;
811    int retval;
812    int pr = option->verb;
813    int initReord = Cudd_ReadReorderings(dd);
814
815    if (option->traverse == FALSE || net->nlatches == 0) return(1);
816    (void) printf("Building transition relation. Time = %s\n",
817                  util_print_time(util_cpu_time() - option->initialTime));
818    one = Cudd_ReadOne(dd);
819    zero = Cudd_Not(one);
820
821    /* Build transition relation and initial states. */
822    TR = Ntr_buildTR(dd,net,option,option->image);
823    if (TR == NULL) return(0);
824    retval = Cudd_SetVarMap(dd,TR->x,TR->y,TR->nlatches);
825    (void) printf("Transition relation: %d parts %d latches %d nodes\n",
826                  TR->nparts, TR->nlatches,
827                  Cudd_SharingSize(TR->part, TR->nparts));
828    (void) printf("Traversing. Time = %s\n",
829                  util_print_time(util_cpu_time() - option->initialTime));
830    init = Ntr_initState(dd,net,option);
831    if (init == NULL) return(0);
832
833    /* Initialize From. */
834    Cudd_Ref(from = init);
835    (void) printf("S0"); Cudd_PrintDebug(dd,from,TR->nlatches,pr);
836
837    /* Initialize Reached. */
838    Cudd_Ref(reached = from);
839
840    /* Start traversal. */
841    for (depth = 0; ; depth++) {
842        /* Image computation. */
843        to = ntrImage(dd,TR,from,option);
844        if (to == NULL) {
845            Cudd_RecursiveDeref(dd,reached);
846            Cudd_RecursiveDeref(dd,from);
847            return(0);
848        }
849        Cudd_RecursiveDeref(dd,from);
850
851        /* Find new states. */
852        neW = Cudd_bddAnd(dd,to,Cudd_Not(reached));
853        if (neW == NULL) {
854            Cudd_RecursiveDeref(dd,reached);
855            Cudd_RecursiveDeref(dd,to);
856            return(0);
857        }
858        Cudd_Ref(neW);
859        Cudd_RecursiveDeref(dd,to);
860
861        /* Check for convergence. */
862        if (neW == zero) break;
863
864        /* Dump current reached states if requested. */
865        if (option->store == depth) {
866            int ok = Dddmp_cuddBddStore(dd, NULL, reached, NULL,
867                                        NULL, DDDMP_MODE_TEXT, DDDMP_VARIDS,
868                                        option->storefile, NULL);
869            if (ok == 0) return(0);
870            (void) printf("Storing reached in %s after %i iterations.\n",
871                          option->storefile, depth);
872            break;
873        }
874
875        /* Update reached. */
876        reached = ntrUpdateReached(dd,reached,neW);
877        if (reached == NULL) {
878            Cudd_RecursiveDeref(dd,neW);
879            return(0);
880        }
881
882        /* Prepare for new iteration. */
883        from = ntrChooseFrom(dd,neW,reached,option);
884        if (from == NULL) {
885            Cudd_RecursiveDeref(dd,reached);
886            Cudd_RecursiveDeref(dd,neW);
887            return(0);
888        }
889        Cudd_RecursiveDeref(dd,neW);
890        (void) printf("From[%d]",depth+1);
891        Cudd_PrintDebug(dd,from,TR->nlatches,pr);
892        (void) printf("Reached[%d]",depth+1);
893        Cudd_PrintDebug(dd,reached,TR->nlatches,pr);
894        if (pr > 0) {
895            if (!Cudd_ApaPrintMinterm(stdout, dd, reached, TR->nlatches))
896                return(0);
897            if (!Cudd_ApaPrintMintermExp(stdout, dd, reached, TR->nlatches, 6))
898                return(0);
899        } else {
900            (void) printf("\n");
901        }
902    }
903
904    /* Print out result. */
905    (void) printf("depth = %d\n", depth);
906    (void) printf("R"); Cudd_PrintDebug(dd,reached,TR->nlatches,pr);
907
908    /* Dump to file if requested. */
909    if (option->bdddump) {
910        DdNode *dfunc[2];       /* addresses of the functions to be dumped */
911        char *onames[2];        /* names of the functions to be dumped */
912        dfunc[0] = TR->part[0];         onames[0] = (char *) "T";
913        dfunc[1] = reached;             onames[1] = (char *) "R";
914        retval = Bnet_bddArrayDump(dd, net, option->dumpfile, dfunc,
915                                   onames, 2, option->dumpFmt);
916        if (retval == 0) return(0);
917    }
918
919    if (option->depend) {
920        retval = ntrLatchDependencies(dd, reached, net, option);
921        if (retval == -1) return(0);
922        (void) printf("%d latches are redundant\n", retval);
923    }
924    /* Clean up. */
925    Cudd_RecursiveDeref(dd,reached);
926    Cudd_RecursiveDeref(dd,neW);
927    Cudd_RecursiveDeref(dd,init);
928    Ntr_freeTR(dd,TR);
929
930    if (Cudd_ReadReorderings(dd) > initReord) {
931        (void) printf("Order at the end of reachability analysis\n");
932        retval = Bnet_PrintOrder(net,dd);
933        if (retval == 0) return(0);
934    }
935    return(1);
936
937} /* end of Ntr_Trav */
938
939
940/**Function********************************************************************
941
942  Synopsis    [Computes the SCCs of the STG.]
943
944  Description [Computes the strongly connected components of the state
945  transition graph.  Only the first 10 SCCs are computed. Returns 1 in
946  case of success; 0 otherwise.]
947
948  SideEffects [None]
949
950  SeeAlso     [Ntr_Trav]
951
952******************************************************************************/
953int
954Ntr_SCC(
955  DdManager * dd /* DD manager */,
956  BnetNetwork * net /* network */,
957  NtrOptions * option /* options */)
958{
959    NtrPartTR *TR;              /* Transition relation */
960    DdNode *init;               /* initial state(s) */
961    DdNode *from;
962    DdNode *to;
963    DdNode *reached, *reaching;
964    DdNode *neW;
965    DdNode *one, *zero;
966    DdNode *states, *scc;
967    DdNode *tmp;
968    DdNode *SCCs[10];
969    int depth;
970    int nscc = 0;
971    int retval;
972    int pr = option->verb;
973    int i;
974
975    if (option->scc == FALSE || net->nlatches == 0) return(1);
976    (void) printf("Building transition relation. Time = %s\n",
977                  util_print_time(util_cpu_time() - option->initialTime));
978    one = Cudd_ReadOne(dd);
979    zero = Cudd_Not(one);
980
981    /* Build transition relation and initial states. */
982    TR = Ntr_buildTR(dd,net,option,option->image);
983    if (TR == NULL) return(0);
984    retval = Cudd_SetVarMap(dd,TR->x,TR->y,TR->nlatches);
985    (void) printf("Transition relation: %d parts %d latches %d nodes\n",
986                  TR->nparts, TR->nlatches,
987                  Cudd_SharingSize(TR->part, TR->nparts));
988    (void) printf("Computing SCCs. Time = %s\n",
989                  util_print_time(util_cpu_time() - option->initialTime));
990
991    /* Consider all SCCs, including those not reachable. */
992    states = one;
993    Cudd_Ref(states);
994
995    while (states != zero) {
996        if (nscc == 0) {
997            tmp = Ntr_initState(dd,net,option);
998            if (tmp == NULL) return(0);
999            init = Cudd_bddPickOneMinterm(dd,tmp,TR->x,TR->nlatches);
1000        } else {
1001            init = Cudd_bddPickOneMinterm(dd,states,TR->x,TR->nlatches);
1002        }
1003        if (init == NULL) return(0);
1004        Cudd_Ref(init);
1005        if (nscc == 0) {
1006            Cudd_RecursiveDeref(dd,tmp);
1007        }
1008        /* Initialize From. */
1009        Cudd_Ref(from = init);
1010        (void) printf("S0"); Cudd_PrintDebug(dd,from,TR->nlatches,pr);
1011
1012        /* Initialize Reached. */
1013        Cudd_Ref(reached = from);
1014
1015        /* Start forward traversal. */
1016        for (depth = 0; ; depth++) {
1017            /* Image computation. */
1018            to = ntrImage(dd,TR,from,option);
1019            if (to == NULL) {
1020                return(0);
1021            }
1022            Cudd_RecursiveDeref(dd,from);
1023
1024            /* Find new states. */
1025            tmp = Cudd_bddAnd(dd,to,states);
1026            if (tmp == NULL) return(0); Cudd_Ref(tmp);
1027            Cudd_RecursiveDeref(dd,to);
1028            neW = Cudd_bddAnd(dd,tmp,Cudd_Not(reached));
1029            if (neW == NULL) return(0); Cudd_Ref(neW);
1030            Cudd_RecursiveDeref(dd,tmp);
1031
1032            /* Check for convergence. */
1033            if (neW == zero) break;
1034
1035            /* Update reached. */
1036            reached = ntrUpdateReached(dd,reached,neW);
1037            if (reached == NULL) {
1038                return(0);
1039            }
1040
1041            /* Prepare for new iteration. */
1042            from = ntrChooseFrom(dd,neW,reached,option);
1043            if (from == NULL) {
1044                return(0);
1045            }
1046            Cudd_RecursiveDeref(dd,neW);
1047            (void) printf("From[%d]",depth+1);
1048            Cudd_PrintDebug(dd,from,TR->nlatches,pr);
1049            (void) printf("Reached[%d]",depth+1);
1050            Cudd_PrintDebug(dd,reached,TR->nlatches,pr);
1051            if (pr <= 0) {
1052                (void) printf("\n");
1053            }
1054        }
1055        Cudd_RecursiveDeref(dd,neW);
1056
1057        /* Express reached in terms of y variables. This allows us to
1058        ** efficiently test for termination during the backward traversal. */
1059        tmp = Cudd_bddVarMap(dd,reached);
1060        if (tmp == NULL) return(0);
1061        Cudd_Ref(tmp);
1062        Cudd_RecursiveDeref(dd,reached);
1063        reached = tmp;
1064
1065        /* Initialize from and reaching. */
1066        from = Cudd_bddVarMap(dd,init);
1067        Cudd_Ref(from);
1068        (void) printf("S0"); Cudd_PrintDebug(dd,from,TR->nlatches,pr);
1069        Cudd_Ref(reaching = from);
1070
1071        /* Start backward traversal. */
1072        for (depth = 0; ; depth++) {
1073            /* Preimage computation. */
1074            to = ntrPreimage(dd,TR,from);
1075            if (to == NULL) {
1076                return(0);
1077            }
1078            Cudd_RecursiveDeref(dd,from);
1079
1080            /* Find new states. */
1081            tmp = Cudd_bddAnd(dd,to,reached);
1082            if (tmp == NULL) return(0); Cudd_Ref(tmp);
1083            Cudd_RecursiveDeref(dd,to);
1084            neW = Cudd_bddAnd(dd,tmp,Cudd_Not(reaching));
1085            if (neW == NULL) return(0); Cudd_Ref(neW);
1086            Cudd_RecursiveDeref(dd,tmp);
1087
1088            /* Check for convergence. */
1089            if (neW == zero) break;
1090
1091            /* Update reaching. */
1092            reaching = ntrUpdateReached(dd,reaching,neW);
1093            if (reaching == NULL) {
1094                return(0);
1095            }
1096
1097            /* Prepare for new iteration. */
1098            from = ntrChooseFrom(dd,neW,reaching,option);
1099            if (from == NULL) {
1100                return(0);
1101            }
1102            Cudd_RecursiveDeref(dd,neW);
1103            (void) printf("From[%d]",depth+1);
1104            Cudd_PrintDebug(dd,from,TR->nlatches,pr);
1105            (void) printf("Reaching[%d]",depth+1);
1106            Cudd_PrintDebug(dd,reaching,TR->nlatches,pr);
1107            if (pr <= 0) {
1108                (void) printf("\n");
1109            }
1110        }
1111
1112        scc = Cudd_bddAnd(dd,reached,reaching);
1113        if (scc == NULL) {
1114            return(0);
1115        }
1116        Cudd_Ref(scc);
1117        SCCs[nscc] = Cudd_bddVarMap(dd,scc);
1118        if (SCCs[nscc] == NULL) return(0);
1119        Cudd_Ref(SCCs[nscc]);
1120        Cudd_RecursiveDeref(dd,scc);
1121        /* Print out result. */
1122        (void) printf("SCC[%d]",nscc);
1123        Cudd_PrintDebug(dd,SCCs[nscc],TR->nlatches,pr);
1124        tmp = Cudd_bddAnd(dd,states,Cudd_Not(SCCs[nscc]));
1125        if (tmp == NULL) {
1126            return(0);
1127        }
1128        Cudd_Ref(tmp);
1129        Cudd_RecursiveDeref(dd,states);
1130        states = tmp;
1131        Cudd_RecursiveDeref(dd,reached);
1132        Cudd_RecursiveDeref(dd,reaching);
1133        Cudd_RecursiveDeref(dd,neW);
1134        Cudd_RecursiveDeref(dd,init);
1135        nscc++;
1136        if (nscc > 9) break;
1137    }
1138
1139    if (states != zero) {
1140        (void) fprintf(stdout,"More than 10 SCCs. Only the first 10 are computed.\n");
1141    }
1142
1143    /* Dump to file if requested. */
1144    if (option->bdddump) {
1145        char *sccnames[10];     /* names of the SCCs */
1146        sccnames[0] = (char *) "SCC0";
1147        sccnames[1] = (char *) "SCC1";
1148        sccnames[2] = (char *) "SCC2";
1149        sccnames[3] = (char *) "SCC3";
1150        sccnames[4] = (char *) "SCC4";
1151        sccnames[5] = (char *) "SCC5";
1152        sccnames[6] = (char *) "SCC6";
1153        sccnames[7] = (char *) "SCC7";
1154        sccnames[8] = (char *) "SCC8";
1155        sccnames[9] = (char *) "SCC9";
1156        retval = Bnet_bddArrayDump(dd, net, option->dumpfile, SCCs,
1157                                   sccnames, nscc, option->dumpFmt);
1158        if (retval == 0) return(0);
1159    }
1160
1161    /* Verify that the SCCs form a partition of the universe. */
1162    scc = zero;
1163    Cudd_Ref(scc);
1164    for (i = 0; i < nscc; i++) {
1165        assert(Cudd_bddLeq(dd,SCCs[i],Cudd_Not(scc)));
1166        tmp = Cudd_bddOr(dd,SCCs[i],scc);
1167        if (tmp == NULL) return(0);
1168        Cudd_Ref(tmp);
1169        Cudd_RecursiveDeref(dd,scc);
1170        scc = tmp;
1171        Cudd_RecursiveDeref(dd,SCCs[i]);
1172    }
1173    assert(scc == Cudd_Not(states));
1174
1175    /* Clean up. */
1176    Cudd_RecursiveDeref(dd,scc);
1177    Cudd_RecursiveDeref(dd,states);
1178    Ntr_freeTR(dd,TR);
1179
1180    return(1);
1181
1182} /* end of Ntr_SCC */
1183
1184
1185/**Function********************************************************************
1186
1187  Synopsis    [Transitive closure traversal procedure.]
1188
1189  Description [Traversal procedure. based on the transitive closure of the
1190  transition relation.  Returns 1 in case of success; 0 otherwise.]
1191
1192  SideEffects [None]
1193
1194  SeeAlso     [Ntr_Trav]
1195
1196******************************************************************************/
1197int
1198Ntr_ClosureTrav(
1199  DdManager * dd /* DD manager */,
1200  BnetNetwork * net /* network */,
1201  NtrOptions * option /* options */)
1202{
1203    DdNode *init;
1204    DdNode *T;
1205    NtrPartTR *TR;
1206    int retval;
1207    int pr = option->verb;      /* verbosity level */
1208    DdNode *dfunc[2];           /* addresses of the functions to be dumped */
1209    char *onames[2];            /* names of the functions to be dumped */
1210    DdNode *reached, *reachedy, *reachedx;
1211
1212    /* Traverse if requested and if the circuit is sequential. */
1213    if (option->closure == FALSE || net->nlatches == 0) return(1);
1214
1215    TR = Ntr_buildTR(dd,net,option,NTR_IMAGE_MONO);
1216    if (TR == NULL) return(0);
1217    (void) printf("TR"); Cudd_PrintDebug(dd,TR->part[0],2*TR->nlatches,pr);
1218    T = Ntr_TransitiveClosure(dd,TR,option);
1219    if (T == NULL) return(0);
1220    Cudd_Ref(T);
1221    (void) printf("TC"); Cudd_PrintDebug(dd,T,2*TR->nlatches,pr);
1222
1223    init = Ntr_initState(dd,net,option);
1224    if (init == NULL) return(0);
1225    (void) printf("S0"); Cudd_PrintDebug(dd,init,TR->nlatches,pr);
1226
1227    /* Image computation. */
1228    if (option->closureClip != 1.0) {
1229        int depth = (int) ((double) Cudd_ReadSize(dd) * option->closureClip);
1230        reachedy = Cudd_bddClippingAndAbstract(dd,T,init,TR->icube[0],
1231                                               depth,option->approx);
1232    } else {
1233        reachedy = Cudd_bddAndAbstract(dd,T,init,TR->icube[0]);
1234    }
1235    if (reachedy == NULL) return(0);
1236    Cudd_Ref(reachedy);
1237
1238    /* Express in terms of present state variables. */
1239    reachedx = Cudd_bddSwapVariables(dd,reachedy,TR->x,TR->y,TR->nlatches);
1240    if (reachedx == NULL) return(0);
1241    Cudd_Ref(reachedx);
1242    Cudd_RecursiveDeref(dd,reachedy);
1243
1244    /* Add initial state. */
1245    reached = Cudd_bddOr(dd,reachedx,init);
1246    if (reached == NULL) return(0);
1247    Cudd_Ref(reached);
1248    Cudd_RecursiveDeref(dd,reachedx);
1249
1250    /* Print out result. */
1251    (void) printf("R"); Cudd_PrintDebug(dd,reached,TR->nlatches,pr);
1252
1253    /* Dump to file if requested. */
1254    if (option->bdddump) {
1255        dfunc[0] = T;           onames[0] = (char *) "TC";
1256        dfunc[1] = reached;     onames[1] = (char *) "R";
1257        retval = Bnet_bddArrayDump(dd, net, option->dumpfile, dfunc,
1258                                   onames, 2, option->dumpFmt);
1259        if (retval == 0) return(0);
1260    }
1261
1262    /* Clean up. */
1263    Cudd_RecursiveDeref(dd,reached);
1264    Cudd_RecursiveDeref(dd,init);
1265    Cudd_RecursiveDeref(dd,T);
1266    Ntr_freeTR(dd,TR);
1267
1268    return(1);
1269
1270} /* end of Ntr_ClosureTrav */
1271
1272
1273/**Function********************************************************************
1274
1275  Synopsis    [Builds the transitive closure of a transition relation.]
1276
1277  Description [Builds the transitive closure of a transition relation.
1278  Returns a BDD if successful; NULL otherwise. Uses a simple squaring
1279  algorithm.]
1280
1281  SideEffects [None]
1282
1283  SeeAlso     []
1284
1285******************************************************************************/
1286DdNode *
1287Ntr_TransitiveClosure(
1288  DdManager * dd,
1289  NtrPartTR * TR,
1290  NtrOptions * option)
1291{
1292    DdNode *T,*oldT,*Txz,*Tzy,*Tred,*square,*zcube;
1293    DdNode **z;
1294    int i;
1295    int depth = 0;
1296    int ylevel;
1297    int done;
1298
1299    if (option->image != NTR_IMAGE_MONO) return(NULL);
1300
1301    /* Create array of auxiliary variables. */
1302    z = ALLOC(DdNode *,TR->nlatches);
1303    if (z == NULL)
1304        return(NULL);
1305    for (i = 0; i < TR->nlatches; i++) {
1306        ylevel = Cudd_ReadIndex(dd,TR->y[i]->index);
1307        z[i] = Cudd_bddNewVarAtLevel(dd,ylevel);
1308        if (z[i] == NULL)
1309            return(NULL);
1310    }
1311    /* Build cube of auxiliary variables. */
1312    zcube = makecube(dd,z,TR->nlatches);
1313    if (zcube == NULL) return(NULL);
1314    Cudd_Ref(zcube);
1315
1316    if (option->closureClip != 1.0) {
1317        depth = (int) ((double) Cudd_ReadSize(dd) * option->imageClip);
1318    }
1319
1320    T = TR->part[0];
1321    Cudd_Ref(T);
1322    for (i = 0; ; i++) {
1323        if (option->threshold >= 0) {
1324            if (option->approx) {
1325                Tred = Cudd_RemapOverApprox(dd,T,TR->nlatches*2,
1326                                            option->threshold,
1327                                            option->quality);
1328            } else {
1329                Tred = Cudd_RemapUnderApprox(dd,T,TR->nlatches*2,
1330                                             option->threshold,
1331                                             option->quality);
1332            }
1333        } else {
1334            Tred = T;
1335        }
1336        if (Tred == NULL) return(NULL);
1337        Cudd_Ref(Tred);
1338        /* Express T in terms of z and y variables. */
1339        Tzy = Cudd_bddSwapVariables(dd,Tred,TR->x,z,TR->nlatches);
1340        if (Tzy == NULL) return(NULL);
1341        Cudd_Ref(Tzy);
1342        /* Express T in terms of x and z variables. */
1343        Txz = Cudd_bddSwapVariables(dd,Tred,TR->y,z,TR->nlatches);
1344        if (Txz == NULL) return(NULL);
1345        Cudd_Ref(Txz);
1346        Cudd_RecursiveDeref(dd,Tred);
1347        /* Square */
1348        if (depth == 0) {
1349            square = Cudd_bddAndAbstract(dd,Txz,Tzy,zcube);
1350        } else {
1351            square = Cudd_bddClippingAndAbstract(dd,Txz,Tzy,zcube,depth,
1352                                                 option->approx);
1353        }
1354        if (square == NULL) return(NULL);
1355        Cudd_Ref(square);
1356        Cudd_RecursiveDeref(dd,Tzy);
1357        Cudd_RecursiveDeref(dd,Txz);
1358        oldT = T;
1359        T = Cudd_bddOr(dd,square,TR->part[0]);
1360        if (T == NULL) return(NULL);
1361        Cudd_Ref(T);
1362        Cudd_RecursiveDeref(dd,square);
1363        done = T == oldT;
1364        Cudd_RecursiveDeref(dd,oldT);
1365        if (done) break;
1366        (void) fprintf(stdout,"@"); fflush(stdout);
1367    }
1368    (void) fprintf(stdout, "\n");
1369
1370    Cudd_RecursiveDeref(dd,zcube);
1371    Cudd_Deref(T);
1372    FREE(z);
1373    return(T);
1374
1375} /* end of Ntr_TransitiveClosure */
1376
1377
1378/**Function********************************************************************
1379
1380  Synopsis    [Builds the BDD of the initial state(s).]
1381
1382  Description [Builds the BDD of the initial state(s).  Returns a BDD
1383  if successful; NULL otherwise.]
1384
1385  SideEffects [None]
1386
1387  SeeAlso     []
1388
1389******************************************************************************/
1390DdNode *
1391Ntr_initState(
1392  DdManager * dd,
1393  BnetNetwork * net,
1394  NtrOptions * option)
1395{
1396    DdNode *res, *x, *w, *one;
1397    BnetNode *node;
1398    int i;
1399
1400    if (option->load) {
1401        res = Dddmp_cuddBddLoad(dd, DDDMP_VAR_MATCHIDS, NULL, NULL, NULL,
1402                                DDDMP_MODE_DEFAULT, option->loadfile, NULL);
1403    } else {
1404        one = Cudd_ReadOne(dd);
1405        Cudd_Ref(res = one);
1406
1407        if (net->nlatches == 0) return(res);
1408
1409        for (i = 0; i < net->nlatches; i++) {
1410            if (!st_lookup(net->hash,net->latches[i][1],&node)) {
1411                goto endgame;
1412            }
1413            x = node->dd;
1414            switch (net->latches[i][2][0]) {
1415            case '0':
1416                w = Cudd_bddAnd(dd,res,Cudd_Not(x));
1417                break;
1418            case '1':
1419                w = Cudd_bddAnd(dd,res,x);
1420                break;
1421            default: /* don't care */
1422                w = res;
1423                break;
1424            }
1425
1426            if (w == NULL) {
1427                Cudd_RecursiveDeref(dd,res);
1428                return(NULL);
1429            }
1430            Cudd_Ref(w);
1431            Cudd_RecursiveDeref(dd,res);
1432            res = w;
1433        }
1434    }
1435    return(res);
1436
1437endgame:
1438
1439    return(NULL);
1440
1441} /* end of Ntr_initState */
1442
1443
1444/**Function********************************************************************
1445
1446  Synopsis    [Reads a state cube from a file or creates a random one.]
1447
1448  Description [Reads a state cube from a file or create a random one.
1449  Returns a pointer to the BDD of the sink nodes if successful; NULL
1450  otherwise.]
1451
1452  SideEffects [None]
1453
1454  SeeAlso     []
1455
1456*****************************************************************************/
1457DdNode *
1458Ntr_getStateCube(
1459  DdManager * dd,
1460  BnetNetwork * net,
1461  char * filename,
1462  int  pr)
1463{
1464    FILE *fp;
1465    DdNode *cube;
1466    DdNode *w;
1467    char *state;
1468    int i;
1469    int err;
1470    BnetNode *node;
1471    DdNode *x;
1472    char c[2];
1473
1474    cube = Cudd_ReadOne(dd);
1475    if (net->nlatches == 0) {
1476        Cudd_Ref(cube);
1477        return(cube);
1478    }
1479
1480    state = ALLOC(char,net->nlatches+1);
1481    if (state == NULL)
1482        return(NULL);
1483    state[net->nlatches] = 0;
1484
1485    if (filename == NULL) {
1486        /* Pick one random minterm. */
1487        for (i = 0; i < net->nlatches; i++) {
1488            state[i] = (char) ((Cudd_Random() & 0x2000) ? '1' : '0');
1489        }
1490    } else {
1491        if ((fp = fopen(filename,"r")) == NULL) {
1492            (void) fprintf(stderr,"Unable to open %s\n",filename);
1493            return(NULL);
1494        }
1495
1496        /* Read string from file. Allow arbitrary amount of white space. */
1497        for (i = 0; !feof(fp); i++) {
1498            err = fscanf(fp, "%1s", c);
1499            state[i] = c[0];
1500            if (err == EOF || i == net->nlatches - 1) {
1501                break;
1502            } else if (err != 1 || strchr("012xX-", c[0]) == NULL ) {
1503                FREE(state);
1504                return(NULL);
1505            }
1506        }
1507        err = fclose(fp);
1508        if (err == EOF) {
1509            FREE(state);
1510            return(NULL);
1511        }
1512    }
1513
1514    /* Echo the chosen state(s). */
1515    if (pr > 0) {(void) fprintf(stdout,"%s\n", state);}
1516
1517    Cudd_Ref(cube);
1518    for (i = 0; i < net->nlatches; i++) {
1519        if (!st_lookup(net->hash,net->latches[i][1],&node)) {
1520            Cudd_RecursiveDeref(dd,cube);
1521            FREE(state);
1522            return(NULL);
1523        }
1524        x = node->dd;
1525        switch (state[i]) {
1526        case '0':
1527            w = Cudd_bddAnd(dd,cube,Cudd_Not(x));
1528            break;
1529        case '1':
1530            w = Cudd_bddAnd(dd,cube,x);
1531            break;
1532        default: /* don't care */
1533            w = cube;
1534            break;
1535        }
1536
1537        if (w == NULL) {
1538            Cudd_RecursiveDeref(dd,cube);
1539            FREE(state);
1540            return(NULL);
1541        }
1542        Cudd_Ref(w);
1543        Cudd_RecursiveDeref(dd,cube);
1544        cube = w;
1545    }
1546
1547    FREE(state);
1548    return(cube);
1549
1550} /* end of Ntr_getStateCube */
1551
1552
1553/**Function********************************************************************
1554
1555  Synopsis    [Poor man's outer envelope computation.]
1556
1557  Description [ Poor man's outer envelope computation based on the
1558  monolithic transition relation. Returns 1 in case of success; 0
1559  otherwise.]
1560
1561  SideEffects [None]
1562
1563  SeeAlso     []
1564
1565******************************************************************************/
1566int
1567Ntr_Envelope(
1568  DdManager * dd /* DD manager */,
1569  NtrPartTR * TR /* transition relation */,
1570  FILE * dfp /* pointer to file for DD dump */,
1571  NtrOptions * option /* program options */)
1572{
1573    DdNode **x; /* array of x variables */
1574    DdNode **y; /* array of y variables */
1575    int ns;     /* number of x and y variables */
1576    DdNode *dfunc[2];   /* addresses of the functions to be dumped */
1577    DdNode *envelope, *oldEnvelope;
1578    DdNode *one;
1579    int depth;
1580    int retval;
1581    int pr = option->verb;
1582    int dumpFmt = option->dumpFmt;
1583
1584    x = TR->x;
1585    y = TR->y;
1586    ns = TR->nlatches;
1587
1588    one = Cudd_ReadOne(dd);
1589    retval = Cudd_SetVarMap(dd,x,y,ns);
1590
1591    /* Initialize From. */
1592    envelope = one;
1593    if (envelope == NULL) return(0);
1594    Cudd_Ref(envelope);
1595    (void) printf("S0"); Cudd_PrintDebug(dd,envelope,ns,pr);
1596
1597    /* Start traversal. */
1598    for (depth = 0; ; depth++) {
1599        oldEnvelope = envelope;
1600        /* Image computation. */
1601        envelope = ntrImage(dd,TR,oldEnvelope,option);
1602        if (envelope == NULL) {
1603            Cudd_RecursiveDeref(dd,oldEnvelope);
1604            return(0);
1605        }
1606
1607        /* Check for convergence. */
1608        if (envelope == oldEnvelope) break;
1609
1610        /* Prepare for new iteration. */
1611        Cudd_RecursiveDeref(dd,oldEnvelope);
1612        (void) fprintf(stdout,"Envelope[%d]%s",depth+1,(pr>0)? "" : "\n");
1613        Cudd_PrintDebug(dd,envelope,ns,pr);
1614
1615    }
1616    /* Clean up. */
1617    Cudd_RecursiveDeref(dd,oldEnvelope);
1618
1619    /* Print out result. */
1620    (void) printf("depth = %d\n", depth);
1621    (void) printf("Envelope"); Cudd_PrintDebug(dd,envelope,ns,pr);
1622
1623    /* Write dump file if requested. */
1624    if (dfp != NULL) {
1625        dfunc[0] = TR->part[0];
1626        dfunc[1] = envelope;
1627        if (dumpFmt == 1) {
1628            retval = Cudd_DumpBlif(dd,2,dfunc,NULL,(char const * const *)onames,NULL,dfp,0);
1629        } else if (dumpFmt == 2) {
1630            retval = Cudd_DumpDaVinci(dd,2,dfunc,NULL,
1631                                      (char const * const *)onames,dfp);
1632        } else if (dumpFmt == 3) {
1633            retval = Cudd_DumpDDcal(dd,2,dfunc,NULL,
1634                                    (char const * const *)onames,dfp);
1635        } else if (dumpFmt == 4) {
1636            retval = Cudd_DumpFactoredForm(dd,2,dfunc,NULL,
1637                                           (char const * const *)onames,dfp);
1638        } else if (dumpFmt == 5) {
1639            retval = Cudd_DumpBlif(dd,2,dfunc,NULL,
1640                                   (char const * const *)onames,NULL,dfp,1);
1641        } else {
1642            retval = Cudd_DumpDot(dd,2,dfunc,NULL,
1643                                  (char const * const *)onames,dfp);
1644        }
1645        if (retval != 1) {
1646            (void) fprintf(stderr,"abnormal termination\n");
1647            return(0);
1648        }
1649        fclose(dfp);
1650    }
1651
1652    /* Clean up. */
1653    Cudd_RecursiveDeref(dd,envelope);
1654
1655    return(1);
1656
1657} /* end of Ntr_Envelope */
1658
1659
1660/**Function********************************************************************
1661
1662  Synopsis    [Maximum 0-1 flow between source and sink states.]
1663
1664  Description [Maximum 0-1 flow between source and sink
1665  states. Returns 1 in case of success; 0 otherwise.]
1666
1667  SideEffects [Creates two new sets of variables.]
1668
1669  SeeAlso     []
1670
1671******************************************************************************/
1672int
1673Ntr_maxflow(
1674  DdManager * dd,
1675  BnetNetwork * net,
1676  NtrOptions * option)
1677{
1678    DdNode **x = NULL;
1679    DdNode **y = NULL;
1680    DdNode **z = NULL;
1681    DdNode *E = NULL;
1682    DdNode *F = NULL;
1683    DdNode *cut = NULL;
1684    DdNode *sx = NULL;
1685    DdNode *ty = NULL;
1686    DdNode *tx = NULL;
1687    int n;
1688    int pr;
1689    int ylevel;
1690    int i;
1691    double flow;
1692    int result = 0;
1693    NtrPartTR *TR;
1694
1695    n = net->nlatches;
1696    pr = option->verb;
1697    TR = Ntr_buildTR(dd,net,option,NTR_IMAGE_MONO);
1698    if (TR == NULL)
1699        goto endgame;
1700    E = TR->part[0];
1701    x = TR->x;
1702    y = TR->y;
1703    /* Create array of auxiliary variables. */
1704    z = ALLOC(DdNode *,n);
1705    if (z == NULL)
1706        goto endgame;
1707    for (i = 0; i < n; i++) {
1708        ylevel = Cudd_ReadIndex(dd,y[i]->index);
1709        z[i] = Cudd_bddNewVarAtLevel(dd,ylevel);
1710        if (z[i] == NULL)
1711            goto endgame;
1712        Cudd_Ref(z[i]);
1713    }
1714    /* Create BDDs for source and sink. */
1715    sx = Ntr_initState(dd,net,option);
1716    if (sx == NULL)
1717        goto endgame;
1718    if (pr > 0) (void) fprintf(stdout, "Sink(s): ");
1719    tx = Ntr_getStateCube(dd,net,option->sinkfile,pr);
1720    if (tx == NULL)
1721        goto endgame;
1722    ty = Cudd_bddSwapVariables(dd,tx,x,y,n);
1723    if (ty == NULL)
1724        goto endgame;
1725    Cudd_Ref(ty);
1726    Cudd_RecursiveDeref(dd,tx);
1727    tx = NULL;
1728
1729    flow = Ntr_maximum01Flow(dd, sx, ty, E, &F, &cut, x, y, z, n, pr);
1730    if (flow >= 0.0)
1731        result = 1;
1732    if (pr >= 0) {
1733        (void) fprintf(stdout,"Maximum flow = %g\n", flow);
1734        (void) fprintf(stdout,"E"); Cudd_PrintDebug(dd,E,2*n,pr);
1735        (void) fprintf(stdout,"F"); Cudd_PrintDebug(dd,F,2*n,pr);
1736        (void) fprintf(stdout,"cut"); Cudd_PrintDebug(dd,cut,2*n,pr);
1737    }
1738endgame:
1739    /* Clean up. */
1740    if (TR != NULL) Ntr_freeTR(dd,TR);
1741    for (i = 0; i < n; i++) {
1742        if (z != NULL && z[i] != NULL) Cudd_RecursiveDeref(dd,z[i]);
1743    }
1744    if (z != NULL) FREE(z);
1745    if (F != NULL) Cudd_RecursiveDeref(dd,F);
1746    if (cut != NULL) Cudd_RecursiveDeref(dd,cut);
1747    if (sx != NULL) Cudd_RecursiveDeref(dd,sx);
1748    if (ty != NULL) Cudd_RecursiveDeref(dd,ty);
1749    return(result);
1750
1751} /* end of Ntr_Maxflow */
1752
1753/*---------------------------------------------------------------------------*/
1754/* Definition of internal functions                                          */
1755/*---------------------------------------------------------------------------*/
1756
1757/*---------------------------------------------------------------------------*/
1758/* Definition of static functions                                            */
1759/*---------------------------------------------------------------------------*/
1760
1761
1762/**Function********************************************************************
1763
1764  Synopsis    [Builds a positive cube of all the variables in x.]
1765
1766  Description [Builds a positive cube of all the variables in x. Returns
1767  a BDD for the cube if successful; NULL otherwise.]
1768
1769  SideEffects [None]
1770
1771  SeeAlso     []
1772
1773******************************************************************************/
1774static DdNode *
1775makecube(
1776  DdManager * dd,
1777  DdNode ** x,
1778  int  n)
1779{
1780    DdNode *res, *w, *one;
1781    int i;
1782
1783    one = Cudd_ReadOne(dd);
1784    Cudd_Ref(res = one);
1785
1786    for (i = n-1; i >= 0; i--) {
1787        w = Cudd_bddAnd(dd,res,x[i]);
1788        if (w == NULL) {
1789            Cudd_RecursiveDeref(dd,res);
1790            return(NULL);
1791        }
1792        Cudd_Ref(w);
1793        Cudd_RecursiveDeref(dd,res);
1794        res = w;
1795    }
1796    Cudd_Deref(res);
1797    return(res);
1798
1799} /* end of makecube */
1800
1801
1802/**Function********************************************************************
1803
1804  Synopsis    [Initializes the count fields used to drop DDs.]
1805
1806  Description [Initializes the count fields used to drop DDs.
1807  Before actually building the BDDs, we perform a DFS from the outputs
1808  to initialize the count fields of the nodes.  The initial value of the
1809  count field will normally coincide with the fanout of the node.
1810  However, if there are nodes with no path to any primary output or next
1811  state variable, then the initial value of count for some nodes will be
1812  less than the fanout. For primary outputs and next state functions we
1813  add 1, so that we will never try to free their DDs. The count fields
1814  of the nodes that are not reachable from the outputs are set to -1.]
1815
1816  SideEffects [Changes the count fields of the network nodes. Uses the
1817  visited fields.]
1818
1819  SeeAlso     []
1820
1821******************************************************************************/
1822static void
1823ntrInitializeCount(
1824  BnetNetwork * net,
1825  NtrOptions * option)
1826{
1827    BnetNode *node;
1828    int i;
1829
1830    if (option->node != NULL &&
1831        option->closestCube == FALSE && option->dontcares == FALSE) {
1832        if (!st_lookup(net->hash,option->node,&node)) {
1833            (void) fprintf(stdout, "Warning: node %s not found!\n",
1834                           option->node);
1835        } else {
1836            ntrCountDFS(net,node);
1837            node->count++;
1838        }
1839    } else {
1840        if (option->stateOnly == FALSE) {
1841            for (i = 0; i < net->npos; i++) {
1842                if (!st_lookup(net->hash,net->outputs[i],&node)) {
1843                    (void) fprintf(stdout,
1844                                   "Warning: output %s is not driven!\n",
1845                                   net->outputs[i]);
1846                    continue;
1847                }
1848                ntrCountDFS(net,node);
1849                node->count++;
1850            }
1851        }
1852        for (i = 0; i < net->nlatches; i++) {
1853            if (!st_lookup(net->hash,net->latches[i][0],&node)) {
1854                (void) fprintf(stdout,
1855                               "Warning: latch input %s is not driven!\n",
1856                               net->outputs[i]);
1857                continue;
1858            }
1859            ntrCountDFS(net,node);
1860            node->count++;
1861        }
1862    }
1863
1864    /* Clear visited flags. */
1865    node = net->nodes;
1866    while (node != NULL) {
1867        if (node->visited == 0) {
1868            node->count = -1;
1869        } else {
1870            node->visited = 0;
1871        }
1872        node = node->next;
1873    }
1874
1875} /* end of ntrInitializeCount */
1876
1877
1878/**Function********************************************************************
1879
1880  Synopsis    [Does a DFS from a node setting the count field.]
1881
1882  Description []
1883
1884  SideEffects [Changes the count and visited fields of the nodes it
1885  visits.]
1886
1887  SeeAlso     [ntrLevelDFS]
1888
1889******************************************************************************/
1890static void
1891ntrCountDFS(
1892  BnetNetwork * net,
1893  BnetNode * node)
1894{
1895    int i;
1896    BnetNode *auxnd;
1897
1898    node->count++;
1899
1900    if (node->visited == 1) {
1901        return;
1902    }
1903
1904    node->visited = 1;
1905
1906    for (i = 0; i < node->ninp; i++) {
1907        if (!st_lookup(net->hash, node->inputs[i], &auxnd)) {
1908            exit(2);
1909        }
1910        ntrCountDFS(net,auxnd);
1911    }
1912
1913} /* end of ntrCountDFS */
1914
1915
1916/**Function********************************************************************
1917
1918  Synopsis    [Computes the image of a set given a transition relation.]
1919
1920  Description [Computes the image of a set given a transition relation.
1921  Returns a pointer to the result if successful; NULL otherwise. The image is
1922  returned in terms of the present state variables; its reference count is
1923  already increased.]
1924
1925  SideEffects [None]
1926
1927  SeeAlso     [Ntr_Trav]
1928
1929******************************************************************************/
1930static DdNode *
1931ntrImage(
1932  DdManager * dd,
1933  NtrPartTR * TR,
1934  DdNode * from,
1935  NtrOptions * option)
1936{
1937    int i;
1938    DdNode *image;
1939    DdNode *to;
1940    NtrPartTR *T;
1941    int depth = 0;
1942
1943    if (option->image == NTR_IMAGE_CLIP) {
1944        depth = (int) ((double) Cudd_ReadSize(dd) * option->imageClip);
1945    }
1946
1947    /* Existentially quantify the present state variables that are not
1948    ** in the support of any next state function. */
1949    image = Cudd_bddExistAbstract(dd,from,TR->preiabs);
1950    if (image == NULL) return(NULL);
1951    Cudd_Ref(image);
1952    if (option->image == NTR_IMAGE_DEPEND) {
1953        /* Simplify the transition relation based on dependencies
1954        ** and build the conjuncts from the deltas. */
1955        T = ntrEliminateDependencies(dd,TR,&image,option);
1956    } else {
1957        T = TR;
1958    }
1959    if (T == NULL) return(NULL);
1960    for (i = 0; i < T->nparts; i++) {
1961#if 0
1962        (void) printf("  Intermediate product[%d]: %d nodes\n",
1963                      i,Cudd_DagSize(image));
1964#endif
1965        if (option->image == NTR_IMAGE_CLIP) {
1966            to = Cudd_bddClippingAndAbstract(dd,T->part[i],image,T->icube[i],
1967                                             depth,option->approx);
1968        } else {
1969            to = Cudd_bddAndAbstract(dd,T->part[i],image,T->icube[i]);
1970        }
1971        if (to == NULL) return(NULL);
1972        Cudd_Ref(to);
1973        if (option->image == NTR_IMAGE_DEPEND) {
1974            /* Extract dependencies from intermediate product. */
1975            DdNode *abs, *positive, *absabs, *phi, *exnor, *tmp;
1976            abs = Cudd_bddExistAbstract(dd,to,T->xw);
1977            if (abs == NULL) return(NULL); Cudd_Ref(abs);
1978            if (Cudd_bddVarIsDependent(dd,abs,T->nscube[i]) &&
1979                Cudd_EstimateCofactor(dd,abs,T->nscube[i]->index,1) <=
1980                T->nlatches) {
1981                int retval, sizex;
1982                positive = Cudd_Cofactor(dd,abs,T->nscube[i]);
1983                if (positive == NULL) return(NULL); Cudd_Ref(positive);
1984                absabs = Cudd_bddExistAbstract(dd,abs,T->nscube[i]);
1985                if (absabs == NULL) return(NULL); Cudd_Ref(absabs);
1986                Cudd_RecursiveDeref(dd,abs);
1987                phi = Cudd_bddLICompaction(dd,positive,absabs);
1988                if (phi == NULL) return(NULL); Cudd_Ref(phi);
1989                Cudd_RecursiveDeref(dd,positive);
1990                Cudd_RecursiveDeref(dd,absabs);
1991                exnor = Cudd_bddXnor(dd,T->nscube[i],phi);
1992                if (exnor == NULL) return(NULL); Cudd_Ref(exnor);
1993                Cudd_RecursiveDeref(dd,phi);
1994                sizex = Cudd_DagSize(exnor);
1995                (void) printf("new factor of %d nodes\n", sizex);
1996                retval = Ntr_HeapInsert(T->factors,exnor,sizex);
1997                if (retval == 0) return(NULL);
1998                tmp = Cudd_bddExistAbstract(dd,to,T->nscube[i]);
1999                if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
2000                Cudd_RecursiveDeref(dd,to);
2001                to = tmp;
2002            } else {
2003                Cudd_RecursiveDeref(dd,abs);
2004            }
2005        }
2006        Cudd_RecursiveDeref(dd,image);
2007        image = to;
2008    }
2009    if (option->image == NTR_IMAGE_DEPEND) {
2010        int size1, size2;
2011        DdNode *factor1, *factor2, *tmp;
2012        int retval;
2013        size1 = Cudd_DagSize(image);
2014        retval = Ntr_HeapInsert(T->factors,image,size1);
2015        if (retval == 0) return(NULL);
2016        (void) printf("Merging %d factors. Independent image: %d nodes\n",
2017                      Ntr_HeapCount(T->factors), size1);
2018        while (Ntr_HeapCount(T->factors) > 1) {
2019            retval = Ntr_HeapExtractMin(T->factors,&factor1,&size1);
2020            if (retval == 0) return(NULL);
2021            retval = Ntr_HeapExtractMin(T->factors,&factor2,&size2);
2022            if (retval == 0) return(NULL);
2023            tmp = Cudd_bddAnd(dd,factor1,factor2);
2024            if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
2025            size1 = Cudd_DagSize(tmp);
2026            (void) printf("new factor %d nodes\n", size1);
2027            Cudd_RecursiveDeref(dd,factor1);
2028            Cudd_RecursiveDeref(dd,factor2);
2029            retval = Ntr_HeapInsert(T->factors,tmp,size1);
2030            if (retval == 0) return(NULL);
2031        }
2032        retval = Ntr_HeapExtractMin(T->factors,&image,&size1);
2033        if (retval == 0) return(NULL);
2034        Ntr_freeTR(dd,T);
2035    }
2036
2037    /* Express image in terms of x variables. */
2038    to = Cudd_bddVarMap(dd,image);
2039    if (to == NULL) {
2040        Cudd_RecursiveDeref(dd,image);
2041        return(NULL);
2042    }
2043    Cudd_Ref(to);
2044    Cudd_RecursiveDeref(dd,image);
2045    return(to);
2046
2047} /* end of ntrImage */
2048
2049
2050/**Function********************************************************************
2051
2052  Synopsis    [Computes the preimage of a set given a transition relation.]
2053
2054  Description [Computes the preimage of a set given a transition relation.
2055  Returns a pointer to the result if successful; NULL otherwise. The preimage
2056  is returned in terms of the next state variables; its reference count is
2057  already increased.]
2058
2059  SideEffects [None]
2060
2061  SeeAlso     [ntrImage Ntr_SCC]
2062
2063******************************************************************************/
2064static DdNode *
2065ntrPreimage(
2066  DdManager * dd,
2067  NtrPartTR * T,
2068  DdNode * from)
2069{
2070    int i;
2071    DdNode *preimage;
2072    DdNode *to;
2073
2074    /* Existentially quantify the present state variables that are not
2075    ** in the support of any next state function. */
2076    preimage = Cudd_bddExistAbstract(dd,from,T->prepabs);
2077    if (preimage == NULL) return(NULL);
2078    Cudd_Ref(preimage);
2079    for (i = 0; i < T->nparts; i++) {
2080#if 0
2081        (void) printf("  Intermediate product[%d]: %d nodes\n",
2082                      i,Cudd_DagSize(preimage));
2083#endif
2084        to = Cudd_bddAndAbstract(dd,T->part[i],preimage,T->pcube[i]);
2085        if (to == NULL) return(NULL);
2086        Cudd_Ref(to);
2087        Cudd_RecursiveDeref(dd,preimage);
2088        preimage = to;
2089    }
2090
2091    /* Express preimage in terms of x variables. */
2092    to = Cudd_bddVarMap(dd,preimage);
2093    if (to == NULL) {
2094        Cudd_RecursiveDeref(dd,preimage);
2095        return(NULL);
2096    }
2097    Cudd_Ref(to);
2098    Cudd_RecursiveDeref(dd,preimage);
2099    return(to);
2100
2101} /* end of ntrPreimage */
2102
2103
2104/**Function********************************************************************
2105
2106  Synopsis    [Chooses the initial states for a BFS step.]
2107
2108  Description [Chooses the initial states for a BFS step. Returns a
2109  pointer to the chose set if successful; NULL otherwise. The
2110  reference count of the result is already incremented.]
2111
2112  SideEffects [none]
2113
2114  SeeAlso     [Ntr_Trav]
2115
2116******************************************************************************/
2117static DdNode *
2118ntrChooseFrom(
2119  DdManager * dd,
2120  DdNode * neW,
2121  DdNode * reached,
2122  NtrOptions * option)
2123{
2124    DdNode *min, *c;
2125    int threshold;
2126
2127    switch (option->from) {
2128    case NTR_FROM_NEW:
2129        Cudd_Ref(neW);
2130        return(neW);
2131    case NTR_FROM_REACHED:
2132        Cudd_Ref(reached);
2133        return(reached);
2134    case NTR_FROM_RESTRICT:
2135        c = Cudd_bddOr(dd, neW, Cudd_Not(reached));
2136        if (c == NULL) return(NULL);
2137        Cudd_Ref(c);
2138        min = Cudd_bddRestrict(dd,neW,c);
2139        if (min == NULL) {
2140            Cudd_RecursiveDeref(dd, c);
2141            return(NULL);
2142        }
2143        Cudd_Ref(min);
2144        Cudd_RecursiveDeref(dd, c);
2145        return(min);
2146    case NTR_FROM_COMPACT:
2147        c = Cudd_bddOr(dd, neW, Cudd_Not(reached));
2148        if (c == NULL) return(NULL);
2149        Cudd_Ref(c);
2150        min = Cudd_bddLICompaction(dd,neW,c);
2151        if (min == NULL) {
2152            Cudd_RecursiveDeref(dd, c);
2153            return(NULL);
2154        }
2155        Cudd_Ref(min);
2156        Cudd_RecursiveDeref(dd, c);
2157        return(min);
2158    case NTR_FROM_SQUEEZE:
2159        min = Cudd_bddSqueeze(dd,neW,reached);
2160        if (min == NULL) return(NULL);
2161        Cudd_Ref(min);
2162        return(min);
2163    case NTR_FROM_UNDERAPPROX:
2164        threshold = (option->threshold < 0) ? 0 : option->threshold;
2165        min = Cudd_RemapUnderApprox(dd,neW,Cudd_SupportSize(dd,neW),
2166                threshold,option->quality);
2167        if (min == NULL) return(NULL);
2168        Cudd_Ref(min);
2169        return(min);
2170    case NTR_FROM_OVERAPPROX:
2171        threshold = (option->threshold < 0) ? 0 : option->threshold;
2172        min = Cudd_RemapOverApprox(dd,neW,Cudd_SupportSize(dd,neW),
2173                threshold,option->quality);
2174        if (min == NULL) return(NULL);
2175        Cudd_Ref(min);
2176        return(min);
2177    default:
2178        return(NULL);
2179    }
2180
2181} /* end of ntrChooseFrom */
2182
2183
2184/**Function********************************************************************
2185
2186  Synopsis    [Updates the reached states after a traversal step.]
2187
2188  Description [Updates the reached states after a traversal
2189  step. Returns a pointer to the new reached set if successful; NULL
2190  otherwise. The reference count of the result is already incremented.]
2191
2192  SideEffects [The old reached set is dereferenced.]
2193
2194  SeeAlso     [Ntr_Trav]
2195
2196******************************************************************************/
2197static DdNode *
2198ntrUpdateReached(
2199  DdManager * dd /* manager */,
2200  DdNode * oldreached /* old reached state set */,
2201  DdNode * to /* result of last image computation */)
2202{
2203    DdNode *reached;
2204
2205    reached = Cudd_bddOr(dd,oldreached,to);
2206    if (reached == NULL) {
2207        Cudd_RecursiveDeref(dd,oldreached);
2208        return(NULL);
2209    }
2210    Cudd_Ref(reached);
2211    Cudd_RecursiveDeref(dd,oldreached);
2212    return(reached);
2213
2214} /* end of ntrUpdateReached */
2215
2216
2217/**Function********************************************************************
2218
2219  Synopsis    [Analyzes the reached states after traversal to find
2220  dependent latches.]
2221
2222  Description [Analyzes the reached states after traversal to find
2223  dependent latches.  Returns the number of latches that can be
2224  eliminated because they are stuck at a constant value or are
2225  dependent on others if successful; -1 otherwise. The algorithm is
2226  greedy and determines a local optimum, not a global one.]
2227
2228  SideEffects []
2229
2230  SeeAlso     [Ntr_Trav]
2231
2232******************************************************************************/
2233static int
2234ntrLatchDependencies(
2235  DdManager *dd,
2236  DdNode *reached,
2237  BnetNetwork *net,
2238  NtrOptions *option)
2239{
2240    int i;
2241    int howMany;                /* number of latches that can be eliminated */
2242    DdNode *var, *newreached, *abs, *positive, *phi;
2243    char *name;
2244    BnetNode *node;
2245    int initVars, finalVars;
2246    double initStates, finalStates;
2247    DdNode **roots;
2248    char **onames;
2249    int howManySmall = 0;
2250    int *candidates;
2251    double minStates;
2252    int totalVars;
2253
2254    (void) printf("Analyzing latch dependencies\n");
2255    roots = ALLOC(DdNode *, net->nlatches);
2256    if (roots == NULL) return(-1);
2257    onames = ALLOC(char *, net->nlatches);
2258    if (onames == NULL) return(-1);
2259
2260    candidates = ALLOC(int,net->nlatches);
2261    if (candidates == NULL) return(-1);
2262    for (i = 0; i < net->nlatches; i++) {
2263        candidates[i] = i;
2264    }
2265    /* The signatures of the variables in a function are the number
2266    ** of minterms of the positive cofactors with respect to the
2267    ** variables themselves. */
2268    newreached = reached;
2269    Cudd_Ref(newreached);
2270    signatures = Cudd_CofMinterm(dd,newreached);
2271    if (signatures == NULL) return(-1);
2272    /* We now extract a positive quantity which is higher for those
2273    ** variables that are closer to being essential. */
2274    totalVars = Cudd_ReadSize(dd);
2275    minStates = signatures[totalVars];
2276#if 0
2277    (void) printf("Raw signatures (minStates = %g)\n", minStates);
2278    for (i = 0; i < net->nlatches; i++) {
2279        int j = candidates[i];
2280        if (!st_lookup(net->hash,net->latches[j][1],(char **) &node)) {
2281            return(-1);
2282        }
2283        (void) printf("%s -> %g\n", node->name, signatures[node->dd->index]);
2284    }
2285#endif
2286    for (i = 0; i < totalVars; i++) {
2287        double z = signatures[i] / minStates - 1.0;
2288        signatures[i] = (z >= 0.0) ? z : -z;    /* make positive */
2289    }
2290    staticNet = net;
2291    qsort((void *)candidates,net->nlatches,sizeof(int),
2292          (DD_QSFP)ntrSignatureCompare2);
2293#if 0
2294    (void) printf("Cooked signatures\n");
2295    for (i = 0; i < net->nlatches; i++) {
2296        int j = candidates[i];
2297        if (!st_lookup(net->hash,net->latches[j][1],(char **) &node)) {
2298            return(-1);
2299        }
2300        (void) printf("%s -> %g\n", node->name, signatures[node->dd->index]);
2301    }
2302#endif
2303    FREE(signatures);
2304
2305    /* Extract simple dependencies. */
2306    for (i = 0; i < net->nlatches; i++) {
2307        int j = candidates[i];
2308        if (!st_lookup(net->hash,net->latches[j][1],&node)) {
2309            return(-1);
2310        }
2311        var = node->dd;
2312        name = node->name;
2313        if (Cudd_bddVarIsDependent(dd,newreached,var)) {
2314            positive = Cudd_Cofactor(dd,newreached,var);
2315            if (positive == NULL) return(-1); Cudd_Ref(positive);
2316            abs = Cudd_bddExistAbstract(dd,newreached,var);
2317            if (abs == NULL) return(-1); Cudd_Ref(abs);
2318            phi = Cudd_bddLICompaction(dd,positive,abs);
2319            if (phi == NULL) return(-1); Cudd_Ref(phi);
2320            Cudd_RecursiveDeref(dd,positive);
2321            if (Cudd_DagSize(phi) < NTR_MAX_DEP_SIZE) {
2322                if (Cudd_bddLeq(dd,newreached,var)) {
2323                    (void) printf("%s is stuck at 1\n",name);
2324                } else if (Cudd_bddLeq(dd,newreached,Cudd_Not(var))) {
2325                    (void) printf("%s is stuck at 0\n",name);
2326                } else {
2327                    (void) printf("%s depends on the other variables\n",name);
2328                }
2329                roots[howManySmall] = phi;
2330                onames[howManySmall] = util_strsav(name);
2331                Cudd_RecursiveDeref(dd,newreached);
2332                newreached = abs;
2333                howManySmall++;
2334                candidates[i] = -1; /* do not reconsider */
2335            } else {
2336                Cudd_RecursiveDeref(dd,abs);
2337                Cudd_RecursiveDeref(dd,phi);
2338            }
2339        } else {
2340            candidates[i] = -1; /* do not reconsider */
2341        }
2342    }
2343    /* Now remove remaining dependent variables. */
2344    howMany = howManySmall;
2345    for (i = 0; i < net->nlatches; i++) {
2346        int j = candidates[i];
2347        if (j == -1) continue;
2348        if (!st_lookup(net->hash,net->latches[j][1],&node)) {
2349            return(-1);
2350        }
2351        var = node->dd;
2352        name = node->name;
2353        if (Cudd_bddVarIsDependent(dd,newreached,var)) {
2354            if (Cudd_bddLeq(dd,newreached,var)) {
2355                (void) printf("%s is stuck at 1\n",name);
2356            } else if (Cudd_bddLeq(dd,newreached,Cudd_Not(var))) {
2357                (void) printf("%s is stuck at 0\n",name);
2358            } else {
2359                (void) printf("%s depends on the other variables\n",name);
2360            }
2361            abs = Cudd_bddExistAbstract(dd,newreached,var);
2362            if (abs == NULL) return(-1); Cudd_Ref(abs);
2363            Cudd_RecursiveDeref(dd,newreached);
2364            newreached = abs;
2365            howMany++;
2366        }
2367    }
2368    FREE(candidates);
2369    if (howManySmall > 0) {
2370        if (!Bnet_bddArrayDump(dd,net,(char *)"-",roots,onames,howManySmall,1))
2371            return(-1);
2372    }
2373    for (i = 0; i < howManySmall; i++) {
2374        Cudd_RecursiveDeref(dd,roots[i]);
2375        FREE(onames[i]);
2376    }
2377    FREE(roots);
2378    FREE(onames);
2379
2380    initVars = net->nlatches;
2381    initStates = Cudd_CountMinterm(dd,reached,initVars);
2382    finalVars = initVars - howMany;
2383    finalStates = Cudd_CountMinterm(dd,newreached,finalVars);
2384    if (initStates != finalStates) {
2385        (void) printf("Error: the number of states changed from %g to %g\n",
2386                      initStates, finalStates);
2387        return(-1);
2388    }
2389    (void) printf("new reached");
2390    Cudd_PrintDebug(dd,newreached,finalVars,option->verb);
2391    Cudd_RecursiveDeref(dd,newreached);
2392    return(howMany);
2393
2394} /* end of ntrLatchDependencies */
2395
2396
2397/**Function********************************************************************
2398
2399  Synopsis    [Eliminates dependent variables from a transition relation.]
2400
2401  Description [Eliminates dependent variables from a transition
2402  relation.  Returns a simplified copy of the given transition
2403  relation if successful; NULL otherwise.]
2404
2405  SideEffects [The modified set of states is returned as a side effect.]
2406
2407  SeeAlso     [ntrImage]
2408
2409******************************************************************************/
2410static NtrPartTR *
2411ntrEliminateDependencies(
2412  DdManager *dd,
2413  NtrPartTR *TR,
2414  DdNode **states,
2415  NtrOptions *option)
2416{
2417    NtrPartTR *T;               /* new TR without dependent vars */
2418    int pr = option->verb;
2419    int i, j;
2420    int howMany = 0;            /* number of latches that can be eliminated */
2421    DdNode *var, *newstates, *abs, *positive, *phi;
2422    DdNode *support, *scan, *tmp;
2423    int finalSize;              /* size of the TR after substitutions */
2424    int nvars;                  /* vars in the support of the state set */
2425    int *candidates;            /* vars to be considered for elimination */
2426    int totalVars;
2427    double minStates;
2428
2429    /* Initialize the new transition relation by copying the old one. */
2430    T = Ntr_cloneTR(TR);
2431    if (T == NULL) return(NULL);
2432    newstates = *states;
2433    Cudd_Ref(newstates);
2434
2435    /* Find and rank the candidate variables. */
2436    support = Cudd_Support(dd,newstates);
2437    if (support == NULL) {
2438        Ntr_freeTR(dd,T);
2439        return(NULL);
2440    }
2441    Cudd_Ref(support);
2442    nvars = Cudd_DagSize(support) - 1;
2443    candidates = ALLOC(int,nvars);
2444    if (candidates == NULL) {
2445        Cudd_RecursiveDeref(dd,support);
2446        Ntr_freeTR(dd,T);
2447        return(NULL);
2448    }
2449    scan  = support;
2450    for (i = 0; i < nvars; i++) {
2451        candidates[i] = scan->index;
2452        scan = Cudd_T(scan);
2453    }
2454    Cudd_RecursiveDeref(dd,support);
2455    /* The signatures of the variables in a function are the number
2456    ** of minterms of the positive cofactors with respect to the
2457    ** variables themselves. */
2458    signatures = Cudd_CofMinterm(dd,newstates);
2459    if (signatures == NULL) {
2460        FREE(candidates);
2461        Ntr_freeTR(dd,T);
2462        return(NULL);
2463    }
2464    /* We now extract a positive quantity which is higher for those
2465    ** variables that are closer to being essential. */
2466    totalVars = Cudd_ReadSize(dd);
2467    minStates = signatures[totalVars];
2468    for (i = 0; i < totalVars; i++) {
2469        double z = signatures[i] / minStates - 1.0;
2470        signatures[i] = (z < 0.0) ? -z : z;     /* make positive */
2471    }
2472    /* Sort candidates in decreasing order of signature. */
2473    qsort((void *)candidates,nvars,sizeof(int),
2474          (DD_QSFP)ntrSignatureCompare);
2475    FREE(signatures);
2476
2477    /* Now process the candidates in the given order. */
2478    for (i = 0; i < nvars; i++) {
2479        var = Cudd_bddIthVar(dd,candidates[i]);
2480        if (Cudd_bddVarIsDependent(dd,newstates,var)) {
2481            abs = Cudd_bddExistAbstract(dd,newstates,var);
2482            if (abs == NULL) return(NULL); Cudd_Ref(abs);
2483            positive = Cudd_Cofactor(dd,newstates,var);
2484            if (positive == NULL) return(NULL); Cudd_Ref(positive);
2485            phi = Cudd_bddLICompaction(dd,positive,abs);
2486            if (phi == NULL) return(NULL); Cudd_Ref(phi);
2487            Cudd_RecursiveDeref(dd,positive);
2488#if 0
2489            if (pr > 0) {
2490                (void) printf("Phi");
2491                Cudd_PrintDebug(dd,phi,T->nlatches,pr);
2492            }
2493#endif
2494            if (Cudd_DagSize(phi) < NTR_MAX_DEP_SIZE) {
2495                howMany++;
2496                for (j = 0; j < T->nparts; j++) {
2497                    tmp = Cudd_bddCompose(dd,T->part[j],phi,candidates[i]);
2498                    if (tmp == NULL) return(NULL); Cudd_Ref(tmp);
2499                    Cudd_RecursiveDeref(dd,T->part[j]);
2500                    T->part[j] = tmp;
2501                }
2502                Cudd_RecursiveDeref(dd,newstates);
2503                newstates = abs;
2504            } else {
2505                Cudd_RecursiveDeref(dd,abs);
2506            }
2507            Cudd_RecursiveDeref(dd,phi);
2508        }
2509    }
2510    FREE(candidates);
2511
2512    if (pr > 0) {
2513        finalSize = Cudd_SharingSize(T->part,T->nparts);
2514        (void) printf("Eliminated %d vars. Transition function %d nodes.\n",
2515                      howMany,finalSize);
2516    }
2517
2518    if (!ntrUpdateQuantificationSchedule(dd,T)) return(NULL);
2519
2520    /* Quantify out of states variables that no longer appear in any part. */
2521    Cudd_RecursiveDeref(dd,*states);
2522    *states = Cudd_bddExistAbstract(dd,newstates,T->preiabs);
2523    if (*states == NULL) return(NULL); Cudd_Ref(*states);
2524    Cudd_RecursiveDeref(dd,newstates);
2525    return(T);
2526
2527} /* end of ntrEliminateDependencies */
2528
2529
2530/**Function********************************************************************
2531
2532  Synopsis    [Updates the quantification schedule of a transition relation.]
2533
2534  Description [Updates the quantification schedule of a transition relation.
2535  Returns 1 if successful; 0 otherwise.]
2536
2537  SideEffects [None]
2538
2539  SeeAlso     [ntrEliminateDependencies]
2540
2541******************************************************************************/
2542static int
2543ntrUpdateQuantificationSchedule(
2544  DdManager *dd,
2545  NtrPartTR *T)
2546{
2547    int i, j, k;
2548    int *schedule;
2549    DdNode *one, *support, *scan, *var, *tmp;
2550    char **matrix;
2551    int *position, *row;
2552    char *flags;
2553    int nparts, nvars;
2554    int extracted;
2555#if 0
2556    int schedcost;
2557#endif
2558
2559    nparts = T->nparts;
2560    nvars = Cudd_ReadSize(dd);
2561    one = Cudd_ReadOne(dd);
2562
2563    /* Reinitialize the abstraction cubes. */
2564    Cudd_RecursiveDeref(dd,T->preiabs);
2565    T->preiabs = one;
2566    Cudd_Ref(one);
2567    for (i = 0; i < nparts; i++) {
2568        Cudd_RecursiveDeref(dd,T->icube[i]);
2569        T->icube[i] = one;
2570        Cudd_Ref(one);
2571    }
2572
2573    /* Initialize row permutations to the identity. */
2574    position = ALLOC(int,nparts);
2575    if (position == NULL) return(0);
2576    for (i = 0; i < nparts; i++) {
2577        position[i] = i;
2578    }
2579    /* Sort parts so that parts that differ only
2580    ** in the index of the next state variable are contiguous. */
2581    staticPart = T->part;
2582    qsort((void *)position,nparts,sizeof(int), (DD_QSFP)ntrPartCompare);
2583    /* Extract repeated parts. */
2584    extracted = 0;
2585    for (i = 0; i < nparts - 1; i += j) {
2586        int pi, pij;
2587        DdNode *eq;
2588        j = 1;
2589        pi = position[i];
2590        eq = one;
2591        Cudd_Ref(eq);
2592        pij = position[i+j];
2593        while (Cudd_Regular(staticPart[pij]) == Cudd_Regular(staticPart[pi])) {
2594            int comple = staticPart[pij] != staticPart[pi];
2595            DdNode *xnor = Cudd_bddXnor(dd,T->nscube[pi],
2596                                        Cudd_NotCond(T->nscube[pij],comple));
2597            if (xnor == NULL) return(0); Cudd_Ref(xnor);
2598            tmp = Cudd_bddAnd(dd,xnor,eq);
2599            if (tmp == NULL) return(0); Cudd_Ref(tmp);
2600            Cudd_RecursiveDeref(dd,xnor);
2601            Cudd_RecursiveDeref(dd,eq);
2602            eq = tmp;
2603            Cudd_RecursiveDeref(dd,T->part[pij]);
2604            Cudd_RecursiveDeref(dd,T->icube[pij]);
2605            Cudd_RecursiveDeref(dd,T->nscube[pij]);
2606            T->part[pij] = NULL;
2607            j++;
2608            if (i+j == nparts) break;
2609            pij = position[i+j];
2610        }
2611        if (eq != one) {
2612            int retval = Ntr_HeapInsert(T->factors,eq,Cudd_DagSize(eq));
2613            if (retval == 0) return(0);
2614            extracted += j - 1;
2615        } else {
2616            Cudd_RecursiveDeref(dd,eq);
2617        }
2618    }
2619    /* Compact the part array by removing extracted parts. */
2620    for (i = 0, j = 0; i < nparts; i++) {
2621        if (T->part[i] != NULL) {
2622            T->part[j] = T->part[i];
2623            T->icube[j] = T->icube[i];
2624            T->nscube[j] = T->nscube[i];
2625            j++;
2626        }
2627    }
2628    nparts = T->nparts -= extracted;
2629    (void) printf("Extracted %d repeated parts in %d factors.\n",
2630                  extracted, Ntr_HeapCount(T->factors));
2631
2632    /* Build the support matrix. Each row corresponds to a part of the
2633    ** transition relation; each column corresponds to a variable in
2634    ** the manager. A 1 in position (i,j) means that Part i depends
2635    ** on Variable j. */
2636    matrix = ntrAllocMatrix(nparts,nvars);
2637    if (matrix == NULL) return(0);
2638
2639    /* Allocate array for quantification schedule and initialize it. */
2640    schedule = ALLOC(int,nvars);
2641    if (schedule == NULL) return(0);
2642    for (i = 0; i < nvars; i++) {
2643        schedule[i] = -1;
2644    }
2645    /* Collect scheduling info for this part. At the end of this loop
2646    ** schedule[i] == j means that the variable of index i does not
2647    ** appear in any part with index greater than j, unless j == -1,
2648    ** in which case the variable appears in no part.
2649    */
2650    for (i = 0; i < nparts; i++) {
2651        support = Cudd_Support(dd,T->part[i]);
2652        if (support == NULL) return(0); Cudd_Ref(support);
2653        scan = support;
2654        while (!Cudd_IsConstant(scan)) {
2655            int index = scan->index;
2656            schedule[index] = i;
2657            matrix[i][index] = 1;
2658            scan = Cudd_T(scan);
2659        }
2660        Cudd_RecursiveDeref(dd,support);
2661    }
2662#if 0
2663    (void) printf("Initial schedule:");
2664    schedcost = 0;
2665    for (i = 0; i < nvars; i++) {
2666        (void) printf(" %d", schedule[i]);
2667        if (schedule[i] != -1) schedcost += schedule[i];
2668    }
2669    (void) printf("\nCost = %d\n", schedcost);
2670#endif
2671
2672    /* Initialize direct and inverse row permutations to the identity
2673    ** permutation. */
2674    row = ALLOC(int,nparts);
2675    if (row == NULL) return(0);
2676    for (i = 0; i < nparts; i++) {
2677        position[i] = row[i] = i;
2678    }
2679
2680    /* Sift the matrix. */
2681    flags = ALLOC(char,nvars);
2682    if (flags == NULL) return(0);
2683    for (i = 0; i < nparts; i++) {
2684        int cost = 0;           /* cost of moving the row */
2685        int bestcost = 0;
2686        int posn = position[i];
2687        int bestposn = posn;
2688        /* Sift up. */
2689        /* Initialize the flags to one is for the variables that are
2690        ** currently scheduled to be quantified after this part gets
2691        ** multiplied. When we cross a row of a part that depends on
2692        ** a variable whose flag is 1, we know that the row being sifted
2693        ** is no longer responsible for that variable. */
2694        for (k = 0; k < nvars; k++) {
2695            flags[k] = (char) (schedule[k] == i);
2696        }
2697        for (j = posn - 1; j >= 0; j--) {
2698            for (k = 0; k < nvars; k++) {
2699                if (schedule[k] == row[j]) {
2700                    cost++;
2701                } else {
2702                    flags[k] &= matrix[row[j]][k] == 0;
2703                    cost -= flags[k];
2704                }
2705            }
2706            if (cost < bestcost) {
2707                bestposn = j;
2708                bestcost = cost;
2709            }
2710        }
2711        /* Sift down. */
2712        /* Reinitialize the flags. (We are implicitly undoing the sift
2713        ** down step.) */
2714        for (k = 0; k < nvars; k++) {
2715            flags[k] = (char) (schedule[k] == i);
2716        }
2717        for (j = posn + 1; j < nparts; j++) {
2718            for (k = 0; k < nvars; k++) {
2719                if (schedule[k] == row[j]) {
2720                    flags[k] |= matrix[i][k] == 1;
2721                    cost -= flags[k] == 0;
2722                } else {
2723                    cost += flags[k];
2724                }
2725            }
2726            if (cost < bestcost) {
2727                bestposn = j;
2728                bestcost = cost;
2729            }
2730        }
2731        /* Move to best position. */
2732        if (bestposn < posn) {
2733            for (j = posn; j >= bestposn; j--) {
2734                k = row[j];
2735                if (j > 0) row[j] = row[j-1];
2736                position[k]++;
2737            }
2738        } else {
2739            for (j = posn; j <= bestposn; j++) {
2740                k = row[j];
2741                if (j < nparts - 1) row[j] = row[j+1];
2742                position[k]--;
2743            }
2744        }
2745        position[i] = bestposn;
2746        row[bestposn] = i;
2747        /* Fix the schedule. */
2748        for (k = 0; k < nvars; k++) {
2749            if (matrix[i][k] == 1) {
2750                if (position[schedule[k]] < bestposn) {
2751                    schedule[k] = i;
2752                } else {
2753                    for (j = nparts - 1; j >= position[i]; j--) {
2754                        if (matrix[row[j]][k] == 1) break;
2755                    }
2756                    schedule[k] = row[j];
2757                }
2758            }
2759        }
2760    }
2761    ntrFreeMatrix(matrix);
2762    FREE(flags);
2763
2764    /* Update schedule to account for the permutation. */
2765    for (i = 0; i < nvars; i++) {
2766        if (schedule[i] >= 0) {
2767            schedule[i] = position[schedule[i]];
2768        }
2769    }
2770    /* Sort parts. */
2771    ntrPermuteParts(T->part,T->nscube,row,position,nparts);
2772    FREE(position);
2773    FREE(row);
2774#if 0
2775    (void) printf("New schedule:");
2776    schedcost = 0;
2777    for (i = 0; i < nvars; i++) {
2778        (void) printf(" %d", schedule[i]);
2779        if (schedule[i] != -1) schedcost += schedule[i];
2780    }
2781    (void) printf("\nCost = %d\n", schedcost);
2782#endif
2783
2784    /* Mark the next state varibles so that they do not go in the
2785    ** abstraction cubes. */
2786    for (i = 0; i < T->nlatches; i++) {
2787        schedule[T->y[i]->index] = -2;
2788    }
2789
2790    /* Rebuild the cubes from the schedule. */
2791    for (i = 0; i < nvars; i++) {
2792        k = schedule[i];
2793        var = Cudd_bddIthVar(dd,i);
2794        if (k >= 0) {
2795            tmp = Cudd_bddAnd(dd,T->icube[k],var);
2796            if (tmp == NULL) return(0); Cudd_Ref(tmp);
2797            Cudd_RecursiveDeref(dd,T->icube[k]);
2798            T->icube[k] = tmp;
2799        } else if (k != -2) {
2800            tmp = Cudd_bddAnd(dd,T->preiabs,var);
2801            if (tmp == NULL) return(0); Cudd_Ref(tmp);
2802            Cudd_RecursiveDeref(dd,T->preiabs);
2803            T->preiabs = tmp;
2804        }
2805    }
2806    FREE(schedule);
2807
2808    /* Build the conjuncts. */
2809    for (i = 0; i < nparts; i++) {
2810        tmp = Cudd_bddXnor(dd,T->nscube[i],T->part[i]);
2811        if (tmp == NULL) return(0); Cudd_Ref(tmp);
2812        Cudd_RecursiveDeref(dd,T->part[i]);
2813        T->part[i] = tmp;
2814    }
2815
2816    return(1);
2817
2818} /* end of ntrUpdateQuantificationSchedule */
2819
2820
2821/**Function********************************************************************
2822
2823  Synopsis    [Comparison function used by qsort.]
2824
2825  Description [Comparison function used by qsort to order the
2826  variables according to their signatures.]
2827
2828  SideEffects [None]
2829
2830******************************************************************************/
2831static int
2832ntrSignatureCompare(
2833  int * ptrX,
2834  int * ptrY)
2835{
2836    if (signatures[*ptrY] > signatures[*ptrX]) return(1);
2837    if (signatures[*ptrY] < signatures[*ptrX]) return(-1);
2838    return(0);
2839
2840} /* end of ntrSignatureCompare */
2841
2842
2843/**Function********************************************************************
2844
2845  Synopsis    [Comparison function used by qsort.]
2846
2847  Description [Comparison function used by qsort to order the
2848  variables according to their signatures.]
2849
2850  SideEffects [None]
2851
2852******************************************************************************/
2853static int
2854ntrSignatureCompare2(
2855  int * ptrX,
2856  int * ptrY)
2857{
2858    BnetNode *node;
2859    int x,y;
2860    if (!st_lookup(staticNet->hash,staticNet->latches[*ptrX][1],&node)) {
2861        return(0);
2862    }
2863    x = node->dd->index;
2864    if (!st_lookup(staticNet->hash,staticNet->latches[*ptrY][1],&node)) {
2865        return(0);
2866    }
2867    y = node->dd->index;
2868    if (signatures[x] < signatures[y]) return(1);
2869    if (signatures[x] > signatures[y]) return(-1);
2870    return(0);
2871
2872} /* end of ntrSignatureCompare2 */
2873
2874
2875/**Function********************************************************************
2876
2877  Synopsis    [Comparison function used by qsort.]
2878
2879  Description [Comparison function used by qsort to order the
2880  parts according to the BDD addresses.]
2881
2882  SideEffects [None]
2883
2884******************************************************************************/
2885static int
2886ntrPartCompare(
2887  int * ptrX,
2888  int * ptrY)
2889{
2890    if (staticPart[*ptrY] > staticPart[*ptrX]) return(1);
2891    if (staticPart[*ptrY] < staticPart[*ptrX]) return(-1);
2892    return(0);
2893
2894} /* end of ntrPartCompare */
2895
2896
2897/**Function********************************************************************
2898
2899  Synopsis    [Allocates a matrix.]
2900
2901  Description [Allocates a matrix of char's. Returns a pointer to the matrix
2902  if successful; NULL otherwise.]
2903
2904  SideEffects [None]
2905
2906  SeeAlso     []
2907
2908******************************************************************************/
2909static char **
2910ntrAllocMatrix(
2911  int nrows,
2912  int ncols)
2913{
2914    int i;
2915    char **matrix;
2916
2917    matrix = ALLOC(char *,nrows);
2918    if (matrix == NULL) return(NULL);
2919    matrix[0] = ALLOC(char,nrows * ncols);
2920    if (matrix[0] == NULL) {
2921        FREE(matrix);
2922        return(NULL);
2923    }
2924    for (i = 1; i < nrows; i++) {
2925        matrix[i] = matrix[i-1] + ncols;
2926    }
2927    for (i = 0; i < nrows * ncols; i++) {
2928        matrix[0][i] = 0;
2929    }
2930    return(matrix);
2931
2932} /* end of ntrAllocMatrix */
2933
2934
2935/**Function********************************************************************
2936
2937  Synopsis    [Frees a matrix of char's.]
2938
2939  Description []
2940
2941  SideEffects [None]
2942
2943  SeeAlso     []
2944
2945******************************************************************************/
2946static void
2947ntrFreeMatrix(
2948  char **matrix)
2949{
2950    FREE(matrix[0]);
2951    FREE(matrix);
2952    return;
2953
2954} /* end of ntrFreeMatrix */
2955
2956
2957/**Function********************************************************************
2958
2959  Synopsis    [Sorts parts according to given permutation.]
2960
2961  Description []
2962
2963  SideEffects [The permutation arrays are turned into the identity
2964  permutations.]
2965
2966  SeeAlso     []
2967
2968******************************************************************************/
2969static void
2970ntrPermuteParts(
2971  DdNode **a,
2972  DdNode **b,
2973  int *comesFrom,
2974  int *goesTo,
2975  int size)
2976{
2977    int i, j;
2978    DdNode *tmp;
2979
2980    for (i = 0; i < size; i++) {
2981        if (comesFrom[i] == i) continue;
2982        j = comesFrom[i];
2983        tmp = a[i]; a[i] = a[j]; a[j] = tmp;
2984        tmp = b[i]; b[i] = b[j]; b[j] = tmp;
2985        comesFrom[goesTo[i]] = j;
2986        comesFrom[i] = i;
2987        goesTo[j] = goesTo[i];
2988        goesTo[i] = i;
2989    }
2990    return;
2991
2992} /* end of ntrPermuteParts */
Note: See TracBrowser for help on using the repository browser.