source: vis_dev/glu-2.3/src/cuBdd/cuddCompose.c

Last change on this file was 13, checked in by cecile, 13 years ago

library glu 2.3
File size: 48.8 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddCompose.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Functional composition and variable permutation of DDs.]
8
9  Description [External procedures included in this module:
10                <ul>
11                <li> Cudd_bddCompose()
12                <li> Cudd_addCompose()
13                <li> Cudd_addPermute()
14                <li> Cudd_addSwapVariables()
15                <li> Cudd_bddPermute()
16                <li> Cudd_bddVarMap()
17                <li> Cudd_SetVarMap()
18                <li> Cudd_bddSwapVariables()
19                <li> Cudd_bddAdjPermuteX()
20                <li> Cudd_addVectorCompose()
21                <li> Cudd_addGeneralVectorCompose()
22                <li> Cudd_addNonSimCompose()
23                <li> Cudd_bddVectorCompose()
24                </ul>
25               Internal procedures included in this module:
26                <ul>
27                <li> cuddBddComposeRecur()
28                <li> cuddAddComposeRecur()
29                </ul>
30               Static procedures included in this module:
31                <ul>
32                <li> cuddAddPermuteRecur()
33                <li> cuddBddPermuteRecur()
34                <li> cuddBddVarMapRecur()
35                <li> cuddAddVectorComposeRecur()
36                <li> cuddAddGeneralVectorComposeRecur()
37                <li> cuddAddNonSimComposeRecur()
38                <li> cuddBddVectorComposeRecur()
39                <li> ddIsIthAddVar()
40                <li> ddIsIthAddVarPair()
41               </ul>
42  The permutation functions use a local cache because the results to
43  be remembered depend on the permutation being applied.  Since the
44  permutation is just an array, it cannot be stored in the global
45  cache. There are different procedured for BDDs and ADDs. This is
46  because bddPermuteRecur uses cuddBddIteRecur. If this were changed,
47  the procedures could be merged.]
48
49  Author      [Fabio Somenzi and Kavita Ravi]
50
51  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
52
53  All rights reserved.
54
55  Redistribution and use in source and binary forms, with or without
56  modification, are permitted provided that the following conditions
57  are met:
58
59  Redistributions of source code must retain the above copyright
60  notice, this list of conditions and the following disclaimer.
61
62  Redistributions in binary form must reproduce the above copyright
63  notice, this list of conditions and the following disclaimer in the
64  documentation and/or other materials provided with the distribution.
65
66  Neither the name of the University of Colorado nor the names of its
67  contributors may be used to endorse or promote products derived from
68  this software without specific prior written permission.
69
70  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
71  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
72  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
73  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
74  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
75  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
76  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
77  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
78  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
79  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
80  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
81  POSSIBILITY OF SUCH DAMAGE.]
82
83******************************************************************************/
84
85#include "util.h"
86#include "cuddInt.h"
87
88
89/*---------------------------------------------------------------------------*/
90/* Constant declarations                                                     */
91/*---------------------------------------------------------------------------*/
92
93/*---------------------------------------------------------------------------*/
94/* Stucture declarations                                                     */
95/*---------------------------------------------------------------------------*/
96
97/*---------------------------------------------------------------------------*/
98/* Type declarations                                                         */
99/*---------------------------------------------------------------------------*/
100
101/*---------------------------------------------------------------------------*/
102/* Variable declarations                                                     */
103/*---------------------------------------------------------------------------*/
104
105#ifndef lint
106static char rcsid[] DD_UNUSED = "$Id: cuddCompose.c,v 1.45 2004/08/13 18:04:47 fabio Exp $";
107#endif
108
109#ifdef DD_DEBUG
110static int addPermuteRecurHits;
111static int bddPermuteRecurHits;
112static int bddVectorComposeHits;
113static int addVectorComposeHits;
114
115static int addGeneralVectorComposeHits;
116#endif
117
118/*---------------------------------------------------------------------------*/
119/* Macro declarations                                                        */
120/*---------------------------------------------------------------------------*/
121
122
123/**AutomaticStart*************************************************************/
124
125/*---------------------------------------------------------------------------*/
126/* Static function prototypes                                                */
127/*---------------------------------------------------------------------------*/
128
129static DdNode * cuddAddPermuteRecur (DdManager *manager, DdHashTable *table, DdNode *node, int *permut);
130static DdNode * cuddBddPermuteRecur (DdManager *manager, DdHashTable *table, DdNode *node, int *permut);
131static DdNode * cuddBddVarMapRecur (DdManager *manager, DdNode *f);
132static DdNode * cuddAddVectorComposeRecur (DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vector, int deepest);
133static DdNode * cuddAddNonSimComposeRecur (DdManager *dd, DdNode *f, DdNode **vector, DdNode *key, DdNode *cube, int lastsub);
134static DdNode * cuddBddVectorComposeRecur (DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vector, int deepest);
135DD_INLINE static int ddIsIthAddVar (DdManager *dd, DdNode *f, unsigned int i);
136
137static DdNode * cuddAddGeneralVectorComposeRecur (DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vectorOn, DdNode **vectorOff, int deepest);
138DD_INLINE static int ddIsIthAddVarPair (DdManager *dd, DdNode *f, DdNode *g, unsigned int i);
139
140/**AutomaticEnd***************************************************************/
141
142
143/*---------------------------------------------------------------------------*/
144/* Definition of exported functions                                          */
145/*---------------------------------------------------------------------------*/
146
147
148/**Function********************************************************************
149
150  Synopsis    [Substitutes g for x_v in the BDD for f.]
151
152  Description [Substitutes g for x_v in the BDD for f. v is the index of the
153  variable to be substituted. Cudd_bddCompose passes the corresponding
154  projection function to the recursive procedure, so that the cache may
155  be used.  Returns the composed BDD if successful; NULL otherwise.]
156
157  SideEffects [None]
158
159  SeeAlso     [Cudd_addCompose]
160
161******************************************************************************/
162DdNode *
163Cudd_bddCompose(
164  DdManager * dd,
165  DdNode * f,
166  DdNode * g,
167  int  v)
168{
169    DdNode *proj, *res;
170
171    /* Sanity check. */
172    if (v < 0 || v >= dd->size) return(NULL);
173
174    proj =  dd->vars[v];
175    do {
176        dd->reordered = 0;
177        res = cuddBddComposeRecur(dd,f,g,proj);
178    } while (dd->reordered == 1);
179    return(res);
180
181} /* end of Cudd_bddCompose */
182
183
184/**Function********************************************************************
185
186  Synopsis    [Substitutes g for x_v in the ADD for f.]
187
188  Description [Substitutes g for x_v in the ADD for f. v is the index of the
189  variable to be substituted. g must be a 0-1 ADD. Cudd_bddCompose passes
190  the corresponding projection function to the recursive procedure, so
191  that the cache may be used.  Returns the composed ADD if successful;
192  NULL otherwise.]
193
194  SideEffects [None]
195
196  SeeAlso     [Cudd_bddCompose]
197
198******************************************************************************/
199DdNode *
200Cudd_addCompose(
201  DdManager * dd,
202  DdNode * f,
203  DdNode * g,
204  int  v)
205{
206    DdNode *proj, *res;
207
208    /* Sanity check. */
209    if (v < 0 || v >= dd->size) return(NULL);
210
211    proj =  dd->vars[v];
212    do {
213        dd->reordered = 0;
214        res = cuddAddComposeRecur(dd,f,g,proj);
215    } while (dd->reordered == 1);
216    return(res);
217
218} /* end of Cudd_addCompose */
219
220
221/**Function********************************************************************
222
223  Synopsis    [Permutes the variables of an ADD.]
224
225  Description [Given a permutation in array permut, creates a new ADD
226  with permuted variables. There should be an entry in array permut
227  for each variable in the manager. The i-th entry of permut holds the
228  index of the variable that is to substitute the i-th
229  variable. Returns a pointer to the resulting ADD if successful; NULL
230  otherwise.]
231
232  SideEffects [None]
233
234  SeeAlso     [Cudd_bddPermute Cudd_addSwapVariables]
235
236******************************************************************************/
237DdNode *
238Cudd_addPermute(
239  DdManager * manager,
240  DdNode * node,
241  int * permut)
242{
243    DdHashTable         *table;
244    DdNode              *res;
245
246    do {
247        manager->reordered = 0;
248        table = cuddHashTableInit(manager,1,2);
249        if (table == NULL) return(NULL);
250        /* Recursively solve the problem. */
251        res = cuddAddPermuteRecur(manager,table,node,permut);
252        if (res != NULL) cuddRef(res);
253        /* Dispose of local cache. */
254        cuddHashTableQuit(table);
255    } while (manager->reordered == 1);
256
257    if (res != NULL) cuddDeref(res);
258    return(res);
259
260} /* end of Cudd_addPermute */
261
262
263/**Function********************************************************************
264
265  Synopsis [Swaps two sets of variables of the same size (x and y) in
266  the ADD f.]
267
268  Description [Swaps two sets of variables of the same size (x and y) in
269  the ADD f.  The size is given by n. The two sets of variables are
270  assumed to be disjoint. Returns a pointer to the resulting ADD if
271  successful; NULL otherwise.]
272
273  SideEffects [None]
274
275  SeeAlso     [Cudd_addPermute Cudd_bddSwapVariables]
276
277******************************************************************************/
278DdNode *
279Cudd_addSwapVariables(
280  DdManager * dd,
281  DdNode * f,
282  DdNode ** x,
283  DdNode ** y,
284  int  n)
285{
286    DdNode *swapped;
287    int  i, j, k;
288    int  *permut;
289
290    permut = ALLOC(int,dd->size);
291    if (permut == NULL) {
292        dd->errorCode = CUDD_MEMORY_OUT;
293        return(NULL);
294    }
295    for (i = 0; i < dd->size; i++) permut[i] = i;
296    for (i = 0; i < n; i++) {
297        j = x[i]->index;
298        k = y[i]->index;
299        permut[j] = k;
300        permut[k] = j;
301    }
302
303    swapped = Cudd_addPermute(dd,f,permut);
304    FREE(permut);
305
306    return(swapped);
307
308} /* end of Cudd_addSwapVariables */
309
310
311/**Function********************************************************************
312
313  Synopsis    [Permutes the variables of a BDD.]
314
315  Description [Given a permutation in array permut, creates a new BDD
316  with permuted variables. There should be an entry in array permut
317  for each variable in the manager. The i-th entry of permut holds the
318  index of the variable that is to substitute the i-th variable.
319  Returns a pointer to the resulting BDD if successful; NULL
320  otherwise.]
321
322  SideEffects [None]
323
324  SeeAlso     [Cudd_addPermute Cudd_bddSwapVariables]
325
326******************************************************************************/
327DdNode *
328Cudd_bddPermute(
329  DdManager * manager,
330  DdNode * node,
331  int * permut)
332{
333    DdHashTable         *table;
334    DdNode              *res;
335
336    do {
337        manager->reordered = 0;
338        table = cuddHashTableInit(manager,1,2);
339        if (table == NULL) return(NULL);
340        res = cuddBddPermuteRecur(manager,table,node,permut);
341        if (res != NULL) cuddRef(res);
342        /* Dispose of local cache. */
343        cuddHashTableQuit(table);
344
345    } while (manager->reordered == 1);
346
347    if (res != NULL) cuddDeref(res);
348    return(res);
349
350} /* end of Cudd_bddPermute */
351
352
353/**Function********************************************************************
354
355  Synopsis    [Remaps the variables of a BDD using the default variable map.]
356
357  Description [Remaps the variables of a BDD using the default
358  variable map.  A typical use of this function is to swap two sets of
359  variables.  The variable map must be registered with Cudd_SetVarMap.
360  Returns a pointer to the resulting BDD if successful; NULL
361  otherwise.]
362
363  SideEffects [None]
364
365  SeeAlso     [Cudd_bddPermute Cudd_bddSwapVariables Cudd_SetVarMap]
366
367******************************************************************************/
368DdNode *
369Cudd_bddVarMap(
370  DdManager * manager /* DD manager */,
371  DdNode * f /* function in which to remap variables */)
372{
373    DdNode *res;
374
375    if (manager->map == NULL) return(NULL);
376    do {
377        manager->reordered = 0;
378        res = cuddBddVarMapRecur(manager, f);
379    } while (manager->reordered == 1);
380
381    return(res);
382
383} /* end of Cudd_bddVarMap */
384
385
386/**Function********************************************************************
387
388  Synopsis [Registers a variable mapping with the manager.]
389
390  Description [Registers with the manager a variable mapping described
391  by two sets of variables.  This variable mapping is then used by
392  functions like Cudd_bddVarMap.  This function is convenient for
393  those applications that perform the same mapping several times.
394  However, if several different permutations are used, it may be more
395  efficient not to rely on the registered mapping, because changing
396  mapping causes the cache to be cleared.  (The initial setting,
397  however, does not clear the cache.) The two sets of variables (x and
398  y) must have the same size (x and y).  The size is given by n. The
399  two sets of variables are normally disjoint, but this restriction is
400  not imposeded by the function. When new variables are created, the
401  map is automatically extended (each new variable maps to
402  itself). The typical use, however, is to wait until all variables
403  are created, and then create the map.  Returns 1 if the mapping is
404  successfully registered with the manager; 0 otherwise.]
405
406  SideEffects [Modifies the manager. May clear the cache.]
407
408  SeeAlso     [Cudd_bddVarMap Cudd_bddPermute Cudd_bddSwapVariables]
409
410******************************************************************************/
411int
412Cudd_SetVarMap (
413  DdManager *manager /* DD manager */,
414  DdNode **x /* first array of variables */,
415  DdNode **y /* second array of variables */,
416  int n /* length of both arrays */)
417{
418    int i;
419
420    if (manager->map != NULL) {
421        cuddCacheFlush(manager);
422    } else {
423        manager->map = ALLOC(int,manager->maxSize);
424        if (manager->map == NULL) {
425            manager->errorCode = CUDD_MEMORY_OUT;
426            return(0);
427        }
428        manager->memused += sizeof(int) * manager->maxSize;
429    }
430    /* Initialize the map to the identity. */
431    for (i = 0; i < manager->size; i++) {
432        manager->map[i] = i;
433    }
434    /* Create the map. */
435    for (i = 0; i < n; i++) {
436        manager->map[x[i]->index] = y[i]->index;
437        manager->map[y[i]->index] = x[i]->index;
438    }
439    return(1);
440
441} /* end of Cudd_SetVarMap */
442
443
444/**Function********************************************************************
445
446  Synopsis [Swaps two sets of variables of the same size (x and y) in
447  the BDD f.]
448
449  Description [Swaps two sets of variables of the same size (x and y)
450  in the BDD f. The size is given by n. The two sets of variables are
451  assumed to be disjoint.  Returns a pointer to the resulting BDD if
452  successful; NULL otherwise.]
453
454  SideEffects [None]
455
456  SeeAlso     [Cudd_bddPermute Cudd_addSwapVariables]
457
458******************************************************************************/
459DdNode *
460Cudd_bddSwapVariables(
461  DdManager * dd,
462  DdNode * f,
463  DdNode ** x,
464  DdNode ** y,
465  int  n)
466{
467    DdNode *swapped;
468    int  i, j, k;
469    int  *permut;
470
471    permut = ALLOC(int,dd->size);
472    if (permut == NULL) {
473        dd->errorCode = CUDD_MEMORY_OUT;
474        return(NULL);
475    }
476    for (i = 0; i < dd->size; i++) permut[i] = i;
477    for (i = 0; i < n; i++) {
478        j = x[i]->index;
479        k = y[i]->index;
480        permut[j] = k;
481        permut[k] = j;
482    }
483
484    swapped = Cudd_bddPermute(dd,f,permut);
485    FREE(permut);
486
487    return(swapped);
488
489} /* end of Cudd_bddSwapVariables */
490
491
492/**Function********************************************************************
493
494  Synopsis [Rearranges a set of variables in the BDD B.]
495
496  Description [Rearranges a set of variables in the BDD B. The size of
497  the set is given by n. This procedure is intended for the
498  `randomization' of the priority functions. Returns a pointer to the
499  BDD if successful; NULL otherwise.]
500
501  SideEffects [None]
502
503  SeeAlso     [Cudd_bddPermute Cudd_bddSwapVariables
504  Cudd_Dxygtdxz Cudd_Dxygtdyz Cudd_PrioritySelect]
505
506******************************************************************************/
507DdNode *
508Cudd_bddAdjPermuteX(
509  DdManager * dd,
510  DdNode * B,
511  DdNode ** x,
512  int  n)
513{
514    DdNode *swapped;
515    int  i, j, k;
516    int  *permut;
517
518    permut = ALLOC(int,dd->size);
519    if (permut == NULL) {
520        dd->errorCode = CUDD_MEMORY_OUT;
521        return(NULL);
522    }
523    for (i = 0; i < dd->size; i++) permut[i] = i;
524    for (i = 0; i < n-2; i += 3) {
525        j = x[i]->index;
526        k = x[i+1]->index;
527        permut[j] = k;
528        permut[k] = j;
529    }
530
531    swapped = Cudd_bddPermute(dd,B,permut);
532    FREE(permut);
533
534    return(swapped);
535
536} /* end of Cudd_bddAdjPermuteX */
537
538
539/**Function********************************************************************
540
541  Synopsis    [Composes an ADD with a vector of 0-1 ADDs.]
542
543  Description [Given a vector of 0-1 ADDs, creates a new ADD by
544  substituting the 0-1 ADDs for the variables of the ADD f.  There
545  should be an entry in vector for each variable in the manager.
546  If no substitution is sought for a given variable, the corresponding
547  projection function should be specified in the vector.
548  This function implements simultaneous composition.
549  Returns a pointer to the resulting ADD if successful; NULL
550  otherwise.]
551
552  SideEffects [None]
553
554  SeeAlso     [Cudd_addNonSimCompose Cudd_addPermute Cudd_addCompose
555  Cudd_bddVectorCompose]
556
557******************************************************************************/
558DdNode *
559Cudd_addVectorCompose(
560  DdManager * dd,
561  DdNode * f,
562  DdNode ** vector)
563{
564    DdHashTable         *table;
565    DdNode              *res;
566    int                 deepest;
567    int                 i;
568
569    do {
570        dd->reordered = 0;
571        /* Initialize local cache. */
572        table = cuddHashTableInit(dd,1,2);
573        if (table == NULL) return(NULL);
574
575        /* Find deepest real substitution. */
576        for (deepest = dd->size - 1; deepest >= 0; deepest--) {
577            i = dd->invperm[deepest];
578            if (!ddIsIthAddVar(dd,vector[i],i)) {
579                break;
580            }
581        }
582
583        /* Recursively solve the problem. */
584        res = cuddAddVectorComposeRecur(dd,table,f,vector,deepest);
585        if (res != NULL) cuddRef(res);
586
587        /* Dispose of local cache. */
588        cuddHashTableQuit(table);
589    } while (dd->reordered == 1);
590
591    if (res != NULL) cuddDeref(res);
592    return(res);
593
594} /* end of Cudd_addVectorCompose */
595
596
597/**Function********************************************************************
598
599  Synopsis    [Composes an ADD with a vector of ADDs.]
600
601  Description [Given a vector of ADDs, creates a new ADD by substituting the
602  ADDs for the variables of the ADD f. vectorOn contains ADDs to be substituted
603  for the x_v and vectorOff the ADDs to be substituted for x_v'. There should
604  be an entry in vector for each variable in the manager.  If no substitution
605  is sought for a given variable, the corresponding projection function should
606  be specified in the vector.  This function implements simultaneous
607  composition.  Returns a pointer to the resulting ADD if successful; NULL
608  otherwise.]
609
610  SideEffects [None]
611
612  SeeAlso [Cudd_addVectorCompose Cudd_addNonSimCompose Cudd_addPermute
613  Cudd_addCompose Cudd_bddVectorCompose]
614
615******************************************************************************/
616DdNode *
617Cudd_addGeneralVectorCompose(
618  DdManager * dd,
619  DdNode * f,
620  DdNode ** vectorOn,
621  DdNode ** vectorOff)
622{
623    DdHashTable         *table;
624    DdNode              *res;
625    int                 deepest;
626    int                 i;
627
628    do {
629        dd->reordered = 0;
630        /* Initialize local cache. */
631        table = cuddHashTableInit(dd,1,2);
632        if (table == NULL) return(NULL);
633
634        /* Find deepest real substitution. */
635        for (deepest = dd->size - 1; deepest >= 0; deepest--) {
636            i = dd->invperm[deepest];
637            if (!ddIsIthAddVarPair(dd,vectorOn[i],vectorOff[i],i)) {
638                break;
639            }
640        }
641
642        /* Recursively solve the problem. */
643        res = cuddAddGeneralVectorComposeRecur(dd,table,f,vectorOn,
644                                               vectorOff,deepest);
645        if (res != NULL) cuddRef(res);
646
647        /* Dispose of local cache. */
648        cuddHashTableQuit(table);
649    } while (dd->reordered == 1);
650
651    if (res != NULL) cuddDeref(res);
652    return(res);
653
654} /* end of Cudd_addGeneralVectorCompose */
655
656
657/**Function********************************************************************
658
659  Synopsis    [Composes an ADD with a vector of 0-1 ADDs.]
660
661  Description [Given a vector of 0-1 ADDs, creates a new ADD by
662  substituting the 0-1 ADDs for the variables of the ADD f.  There
663  should be an entry in vector for each variable in the manager.
664  This function implements non-simultaneous composition. If any of the
665  functions being composed depends on any of the variables being
666  substituted, then the result depends on the order of composition,
667  which in turn depends on the variable order: The variables farther from
668  the roots in the order are substituted first.
669  Returns a pointer to the resulting ADD if successful; NULL
670  otherwise.]
671
672  SideEffects [None]
673
674  SeeAlso     [Cudd_addVectorCompose Cudd_addPermute Cudd_addCompose]
675
676******************************************************************************/
677DdNode *
678Cudd_addNonSimCompose(
679  DdManager * dd,
680  DdNode * f,
681  DdNode ** vector)
682{
683    DdNode              *cube, *key, *var, *tmp, *piece;
684    DdNode              *res;
685    int                 i, lastsub;
686
687    /* The cache entry for this function is composed of three parts:
688    ** f itself, the replacement relation, and the cube of the
689    ** variables being substituted.
690    ** The replacement relation is the product of the terms (yi EXNOR gi).
691    ** This apporach allows us to use the global cache for this function,
692    ** with great savings in memory with respect to using arrays for the
693    ** cache entries.
694    ** First we build replacement relation and cube of substituted
695    ** variables from the vector specifying the desired composition.
696    */
697    key = DD_ONE(dd);
698    cuddRef(key);
699    cube = DD_ONE(dd);
700    cuddRef(cube);
701    for (i = (int) dd->size - 1; i >= 0; i--) {
702        if (ddIsIthAddVar(dd,vector[i],(unsigned int)i)) {
703            continue;
704        }
705        var = Cudd_addIthVar(dd,i);
706        if (var == NULL) {
707            Cudd_RecursiveDeref(dd,key);
708            Cudd_RecursiveDeref(dd,cube);
709            return(NULL);
710        }
711        cuddRef(var);
712        /* Update cube. */
713        tmp = Cudd_addApply(dd,Cudd_addTimes,var,cube);
714        if (tmp == NULL) {
715            Cudd_RecursiveDeref(dd,key);
716            Cudd_RecursiveDeref(dd,cube);
717            Cudd_RecursiveDeref(dd,var);
718            return(NULL);
719        }
720        cuddRef(tmp);
721        Cudd_RecursiveDeref(dd,cube);
722        cube = tmp;
723        /* Update replacement relation. */
724        piece = Cudd_addApply(dd,Cudd_addXnor,var,vector[i]);
725        if (piece == NULL) {
726            Cudd_RecursiveDeref(dd,key);
727            Cudd_RecursiveDeref(dd,var);
728            return(NULL);
729        }
730        cuddRef(piece);
731        Cudd_RecursiveDeref(dd,var);
732        tmp = Cudd_addApply(dd,Cudd_addTimes,key,piece);
733        if (tmp == NULL) {
734            Cudd_RecursiveDeref(dd,key);
735            Cudd_RecursiveDeref(dd,piece);
736            return(NULL);
737        }
738        cuddRef(tmp);
739        Cudd_RecursiveDeref(dd,key);
740        Cudd_RecursiveDeref(dd,piece);
741        key = tmp;
742    }
743
744    /* Now try composition, until no reordering occurs. */
745    do {
746        /* Find real substitution with largest index. */
747        for (lastsub = dd->size - 1; lastsub >= 0; lastsub--) {
748            if (!ddIsIthAddVar(dd,vector[lastsub],(unsigned int)lastsub)) {
749                break;
750            }
751        }
752
753        /* Recursively solve the problem. */
754        dd->reordered = 0;
755        res = cuddAddNonSimComposeRecur(dd,f,vector,key,cube,lastsub+1);
756        if (res != NULL) cuddRef(res);
757
758    } while (dd->reordered == 1);
759
760    Cudd_RecursiveDeref(dd,key);
761    Cudd_RecursiveDeref(dd,cube);
762    if (res != NULL) cuddDeref(res);
763    return(res);
764
765} /* end of Cudd_addNonSimCompose */
766
767
768/**Function********************************************************************
769
770  Synopsis    [Composes a BDD with a vector of BDDs.]
771
772  Description [Given a vector of BDDs, creates a new BDD by
773  substituting the BDDs for the variables of the BDD f.  There
774  should be an entry in vector for each variable in the manager.
775  If no substitution is sought for a given variable, the corresponding
776  projection function should be specified in the vector.
777  This function implements simultaneous composition.
778  Returns a pointer to the resulting BDD if successful; NULL
779  otherwise.]
780
781  SideEffects [None]
782
783  SeeAlso     [Cudd_bddPermute Cudd_bddCompose Cudd_addVectorCompose]
784
785******************************************************************************/
786DdNode *
787Cudd_bddVectorCompose(
788  DdManager * dd,
789  DdNode * f,
790  DdNode ** vector)
791{
792    DdHashTable         *table;
793    DdNode              *res;
794    int                 deepest;
795    int                 i;
796
797    do {
798        dd->reordered = 0;
799        /* Initialize local cache. */
800        table = cuddHashTableInit(dd,1,2);
801        if (table == NULL) return(NULL);
802
803        /* Find deepest real substitution. */
804        for (deepest = dd->size - 1; deepest >= 0; deepest--) {
805            i = dd->invperm[deepest];
806            if (vector[i] != dd->vars[i]) {
807                break;
808            }
809        }
810
811        /* Recursively solve the problem. */
812        res = cuddBddVectorComposeRecur(dd,table,f,vector, deepest);
813        if (res != NULL) cuddRef(res);
814
815        /* Dispose of local cache. */
816        cuddHashTableQuit(table);
817    } while (dd->reordered == 1);
818
819    if (res != NULL) cuddDeref(res);
820    return(res);
821
822} /* end of Cudd_bddVectorCompose */
823
824
825/*---------------------------------------------------------------------------*/
826/* Definition of internal functions                                          */
827/*---------------------------------------------------------------------------*/
828
829
830/**Function********************************************************************
831
832  Synopsis    [Performs the recursive step of Cudd_bddCompose.]
833
834  Description [Performs the recursive step of Cudd_bddCompose.
835  Exploits the fact that the composition of f' with g
836  produces the complement of the composition of f with g to better
837  utilize the cache.  Returns the composed BDD if successful; NULL
838  otherwise.]
839
840  SideEffects [None]
841
842  SeeAlso     [Cudd_bddCompose]
843
844******************************************************************************/
845DdNode *
846cuddBddComposeRecur(
847  DdManager * dd,
848  DdNode * f,
849  DdNode * g,
850  DdNode * proj)
851{
852    DdNode      *F, *G, *f1, *f0, *g1, *g0, *r, *t, *e;
853    unsigned int v, topf, topg, topindex;
854    int         comple;
855
856    statLine(dd);
857    v = dd->perm[proj->index];
858    F = Cudd_Regular(f);
859    topf = cuddI(dd,F->index);
860
861    /* Terminal case. Subsumes the test for constant f. */
862    if (topf > v) return(f);
863
864    /* We solve the problem for a regular pointer, and then complement
865    ** the result if the pointer was originally complemented.
866    */
867    comple = Cudd_IsComplement(f);
868
869    /* Check cache. */
870    r = cuddCacheLookup(dd,DD_BDD_COMPOSE_RECUR_TAG,F,g,proj);
871    if (r != NULL) {
872        return(Cudd_NotCond(r,comple));
873    }
874
875    if (topf == v) {
876        /* Compose. */
877        f1 = cuddT(F);
878        f0 = cuddE(F);
879        r = cuddBddIteRecur(dd, g, f1, f0);
880        if (r == NULL) return(NULL);
881    } else {
882        /* Compute cofactors of f and g. Remember the index of the top
883        ** variable.
884        */
885        G = Cudd_Regular(g);
886        topg = cuddI(dd,G->index);
887        if (topf > topg) {
888            topindex = G->index;
889            f1 = f0 = F;
890        } else {
891            topindex = F->index;
892            f1 = cuddT(F);
893            f0 = cuddE(F);
894        }
895        if (topg > topf) {
896            g1 = g0 = g;
897        } else {
898            g1 = cuddT(G);
899            g0 = cuddE(G);
900            if (g != G) {
901                g1 = Cudd_Not(g1);
902                g0 = Cudd_Not(g0);
903            }
904        }
905        /* Recursive step. */
906        t = cuddBddComposeRecur(dd, f1, g1, proj);
907        if (t == NULL) return(NULL);
908        cuddRef(t);
909        e = cuddBddComposeRecur(dd, f0, g0, proj);
910        if (e == NULL) {
911            Cudd_IterDerefBdd(dd, t);
912            return(NULL);
913        }
914        cuddRef(e);
915
916        r = cuddBddIteRecur(dd, dd->vars[topindex], t, e);
917        if (r == NULL) {
918            Cudd_IterDerefBdd(dd, t);
919            Cudd_IterDerefBdd(dd, e);
920            return(NULL);
921        }
922        cuddRef(r);
923        Cudd_IterDerefBdd(dd, t); /* t & e not necessarily part of r */
924        Cudd_IterDerefBdd(dd, e);
925        cuddDeref(r);
926    }
927
928    cuddCacheInsert(dd,DD_BDD_COMPOSE_RECUR_TAG,F,g,proj,r);
929
930    return(Cudd_NotCond(r,comple));
931
932} /* end of cuddBddComposeRecur */
933
934
935/**Function********************************************************************
936
937  Synopsis    [Performs the recursive step of Cudd_addCompose.]
938
939  Description [Performs the recursive step of Cudd_addCompose.
940  Returns the composed BDD if successful; NULL otherwise.]
941
942  SideEffects [None]
943
944  SeeAlso     [Cudd_addCompose]
945
946******************************************************************************/
947DdNode *
948cuddAddComposeRecur(
949  DdManager * dd,
950  DdNode * f,
951  DdNode * g,
952  DdNode * proj)
953{
954    DdNode *f1, *f0, *g1, *g0, *r, *t, *e;
955    unsigned int v, topf, topg, topindex;
956
957    statLine(dd);
958    v = dd->perm[proj->index];
959    topf = cuddI(dd,f->index);
960
961    /* Terminal case. Subsumes the test for constant f. */
962    if (topf > v) return(f);
963
964    /* Check cache. */
965    r = cuddCacheLookup(dd,DD_ADD_COMPOSE_RECUR_TAG,f,g,proj);
966    if (r != NULL) {
967        return(r);
968    }
969
970    if (topf == v) {
971        /* Compose. */
972        f1 = cuddT(f);
973        f0 = cuddE(f);
974        r = cuddAddIteRecur(dd, g, f1, f0);
975        if (r == NULL) return(NULL);
976    } else {
977        /* Compute cofactors of f and g. Remember the index of the top
978        ** variable.
979        */
980        topg = cuddI(dd,g->index);
981        if (topf > topg) {
982            topindex = g->index;
983            f1 = f0 = f;
984        } else {
985            topindex = f->index;
986            f1 = cuddT(f);
987            f0 = cuddE(f);
988        }
989        if (topg > topf) {
990            g1 = g0 = g;
991        } else {
992            g1 = cuddT(g);
993            g0 = cuddE(g);
994        }
995        /* Recursive step. */
996        t = cuddAddComposeRecur(dd, f1, g1, proj);
997        if (t == NULL) return(NULL);
998        cuddRef(t);
999        e = cuddAddComposeRecur(dd, f0, g0, proj);
1000        if (e == NULL) {
1001            Cudd_RecursiveDeref(dd, t);
1002            return(NULL);
1003        }
1004        cuddRef(e);
1005
1006        if (t == e) {
1007            r = t;
1008        } else {
1009            r = cuddUniqueInter(dd, (int) topindex, t, e);
1010            if (r == NULL) {
1011                Cudd_RecursiveDeref(dd, t);
1012                Cudd_RecursiveDeref(dd, e);
1013                return(NULL);
1014            }
1015        }
1016        cuddDeref(t);
1017        cuddDeref(e);
1018    }
1019
1020    cuddCacheInsert(dd,DD_ADD_COMPOSE_RECUR_TAG,f,g,proj,r);
1021
1022    return(r);
1023
1024} /* end of cuddAddComposeRecur */
1025
1026
1027/*---------------------------------------------------------------------------*/
1028/* Definition of static functions                                            */
1029/*---------------------------------------------------------------------------*/
1030
1031
1032/**Function********************************************************************
1033
1034  Synopsis    [Implements the recursive step of Cudd_addPermute.]
1035
1036  Description [ Recursively puts the ADD in the order given in the
1037  array permut. Checks for trivial cases to terminate recursion, then
1038  splits on the children of this node.  Once the solutions for the
1039  children are obtained, it puts into the current position the node
1040  from the rest of the ADD that should be here. Then returns this ADD.
1041  The key here is that the node being visited is NOT put in its proper
1042  place by this instance, but rather is switched when its proper
1043  position is reached in the recursion tree.<p>
1044  The DdNode * that is returned is the same ADD as passed in as node,
1045  but in the new order.]
1046
1047  SideEffects [None]
1048
1049  SeeAlso     [Cudd_addPermute cuddBddPermuteRecur]
1050
1051******************************************************************************/
1052static DdNode *
1053cuddAddPermuteRecur(
1054  DdManager * manager /* DD manager */,
1055  DdHashTable * table /* computed table */,
1056  DdNode * node /* ADD to be reordered */,
1057  int * permut /* permutation array */)
1058{
1059    DdNode      *T,*E;
1060    DdNode      *res,*var;
1061    int         index;
1062   
1063    statLine(manager);
1064    /* Check for terminal case of constant node. */
1065    if (cuddIsConstant(node)) {
1066        return(node);
1067    }
1068
1069    /* If problem already solved, look up answer and return. */
1070    if (node->ref != 1 && (res = cuddHashTableLookup1(table,node)) != NULL) {
1071#ifdef DD_DEBUG
1072        addPermuteRecurHits++;
1073#endif
1074        return(res);
1075    }
1076
1077    /* Split and recur on children of this node. */
1078    T = cuddAddPermuteRecur(manager,table,cuddT(node),permut);
1079    if (T == NULL) return(NULL);
1080    cuddRef(T);
1081    E = cuddAddPermuteRecur(manager,table,cuddE(node),permut);
1082    if (E == NULL) {
1083        Cudd_RecursiveDeref(manager, T);
1084        return(NULL);
1085    }
1086    cuddRef(E);
1087
1088    /* Move variable that should be in this position to this position
1089    ** by creating a single var ADD for that variable, and calling
1090    ** cuddAddIteRecur with the T and E we just created.
1091    */
1092    index = permut[node->index];
1093    var = cuddUniqueInter(manager,index,DD_ONE(manager),DD_ZERO(manager));
1094    if (var == NULL) return(NULL);
1095    cuddRef(var);
1096    res = cuddAddIteRecur(manager,var,T,E);
1097    if (res == NULL) {
1098        Cudd_RecursiveDeref(manager,var);
1099        Cudd_RecursiveDeref(manager, T);
1100        Cudd_RecursiveDeref(manager, E);
1101        return(NULL);
1102    }
1103    cuddRef(res);
1104    Cudd_RecursiveDeref(manager,var);
1105    Cudd_RecursiveDeref(manager, T);
1106    Cudd_RecursiveDeref(manager, E);
1107
1108    /* Do not keep the result if the reference count is only 1, since
1109    ** it will not be visited again.
1110    */
1111    if (node->ref != 1) {
1112        ptrint fanout = (ptrint) node->ref;
1113        cuddSatDec(fanout);
1114        if (!cuddHashTableInsert1(table,node,res,fanout)) {
1115            Cudd_RecursiveDeref(manager, res);
1116            return(NULL);
1117        }
1118    }
1119    cuddDeref(res);
1120    return(res);
1121
1122} /* end of cuddAddPermuteRecur */
1123
1124
1125/**Function********************************************************************
1126
1127  Synopsis    [Implements the recursive step of Cudd_bddPermute.]
1128
1129  Description [ Recursively puts the BDD in the order given in the array permut.
1130  Checks for trivial cases to terminate recursion, then splits on the
1131  children of this node.  Once the solutions for the children are
1132  obtained, it puts into the current position the node from the rest of
1133  the BDD that should be here. Then returns this BDD.
1134  The key here is that the node being visited is NOT put in its proper
1135  place by this instance, but rather is switched when its proper position
1136  is reached in the recursion tree.<p>
1137  The DdNode * that is returned is the same BDD as passed in as node,
1138  but in the new order.]
1139
1140  SideEffects [None]
1141
1142  SeeAlso     [Cudd_bddPermute cuddAddPermuteRecur]
1143
1144******************************************************************************/
1145static DdNode *
1146cuddBddPermuteRecur(
1147  DdManager * manager /* DD manager */,
1148  DdHashTable * table /* computed table */,
1149  DdNode * node /* BDD to be reordered */,
1150  int * permut /* permutation array */)
1151{
1152    DdNode      *N,*T,*E;
1153    DdNode      *res;
1154    int         index;
1155
1156    statLine(manager);
1157    N = Cudd_Regular(node);
1158
1159    /* Check for terminal case of constant node. */
1160    if (cuddIsConstant(N)) {
1161        return(node);
1162    }
1163
1164    /* If problem already solved, look up answer and return. */
1165    if (N->ref != 1 && (res = cuddHashTableLookup1(table,N)) != NULL) {
1166#ifdef DD_DEBUG
1167        bddPermuteRecurHits++;
1168#endif
1169        return(Cudd_NotCond(res,N != node));
1170    }
1171
1172    /* Split and recur on children of this node. */
1173    T = cuddBddPermuteRecur(manager,table,cuddT(N),permut);
1174    if (T == NULL) return(NULL);
1175    cuddRef(T);
1176    E = cuddBddPermuteRecur(manager,table,cuddE(N),permut);
1177    if (E == NULL) {
1178        Cudd_IterDerefBdd(manager, T);
1179        return(NULL);
1180    }
1181    cuddRef(E);
1182
1183    /* Move variable that should be in this position to this position
1184    ** by retrieving the single var BDD for that variable, and calling
1185    ** cuddBddIteRecur with the T and E we just created.
1186    */
1187    index = permut[N->index];
1188    res = cuddBddIteRecur(manager,manager->vars[index],T,E);
1189    if (res == NULL) {
1190        Cudd_IterDerefBdd(manager, T);
1191        Cudd_IterDerefBdd(manager, E);
1192        return(NULL);
1193    }
1194    cuddRef(res);
1195    Cudd_IterDerefBdd(manager, T);
1196    Cudd_IterDerefBdd(manager, E);
1197
1198    /* Do not keep the result if the reference count is only 1, since
1199    ** it will not be visited again.
1200    */
1201    if (N->ref != 1) {
1202        ptrint fanout = (ptrint) N->ref;
1203        cuddSatDec(fanout);
1204        if (!cuddHashTableInsert1(table,N,res,fanout)) {
1205            Cudd_IterDerefBdd(manager, res);
1206            return(NULL);
1207        }
1208    }
1209    cuddDeref(res);
1210    return(Cudd_NotCond(res,N != node));
1211
1212} /* end of cuddBddPermuteRecur */
1213
1214
1215/**Function********************************************************************
1216
1217  Synopsis    [Implements the recursive step of Cudd_bddVarMap.]
1218
1219  Description [Implements the recursive step of Cudd_bddVarMap.
1220  Returns a pointer to the result if successful; NULL otherwise.]
1221
1222  SideEffects [None]
1223
1224  SeeAlso     [Cudd_bddVarMap]
1225
1226******************************************************************************/
1227static DdNode *
1228cuddBddVarMapRecur(
1229  DdManager *manager /* DD manager */,
1230  DdNode *f /* BDD to be remapped */)
1231{
1232    DdNode      *F, *T, *E;
1233    DdNode      *res;
1234    int         index;
1235
1236    statLine(manager);
1237    F = Cudd_Regular(f);
1238
1239    /* Check for terminal case of constant node. */
1240    if (cuddIsConstant(F)) {
1241        return(f);
1242    }
1243
1244    /* If problem already solved, look up answer and return. */
1245    if (F->ref != 1 &&
1246        (res = cuddCacheLookup1(manager,Cudd_bddVarMap,F)) != NULL) {
1247        return(Cudd_NotCond(res,F != f));
1248    }
1249
1250    /* Split and recur on children of this node. */
1251    T = cuddBddVarMapRecur(manager,cuddT(F));
1252    if (T == NULL) return(NULL);
1253    cuddRef(T);
1254    E = cuddBddVarMapRecur(manager,cuddE(F));
1255    if (E == NULL) {
1256        Cudd_IterDerefBdd(manager, T);
1257        return(NULL);
1258    }
1259    cuddRef(E);
1260
1261    /* Move variable that should be in this position to this position
1262    ** by retrieving the single var BDD for that variable, and calling
1263    ** cuddBddIteRecur with the T and E we just created.
1264    */
1265    index = manager->map[F->index];
1266    res = cuddBddIteRecur(manager,manager->vars[index],T,E);
1267    if (res == NULL) {
1268        Cudd_IterDerefBdd(manager, T);
1269        Cudd_IterDerefBdd(manager, E);
1270        return(NULL);
1271    }
1272    cuddRef(res);
1273    Cudd_IterDerefBdd(manager, T);
1274    Cudd_IterDerefBdd(manager, E);
1275
1276    /* Do not keep the result if the reference count is only 1, since
1277    ** it will not be visited again.
1278    */
1279    if (F->ref != 1) {
1280        cuddCacheInsert1(manager,Cudd_bddVarMap,F,res);
1281    }
1282    cuddDeref(res);
1283    return(Cudd_NotCond(res,F != f));
1284
1285} /* end of cuddBddVarMapRecur */
1286
1287
1288/**Function********************************************************************
1289
1290  Synopsis    [Performs the recursive step of Cudd_addVectorCompose.]
1291
1292  Description []
1293
1294  SideEffects [None]
1295
1296  SeeAlso     []
1297
1298******************************************************************************/
1299static DdNode *
1300cuddAddVectorComposeRecur(
1301  DdManager * dd /* DD manager */,
1302  DdHashTable * table /* computed table */,
1303  DdNode * f /* ADD in which to compose */,
1304  DdNode ** vector /* functions to substitute */,
1305  int  deepest /* depth of deepest substitution */)
1306{
1307    DdNode      *T,*E;
1308    DdNode      *res;
1309
1310    statLine(dd);
1311    /* If we are past the deepest substitution, return f. */
1312    if (cuddI(dd,f->index) > deepest) {
1313        return(f);
1314    }
1315
1316    if ((res = cuddHashTableLookup1(table,f)) != NULL) {
1317#ifdef DD_DEBUG
1318        addVectorComposeHits++;
1319#endif
1320        return(res);
1321    }
1322
1323    /* Split and recur on children of this node. */
1324    T = cuddAddVectorComposeRecur(dd,table,cuddT(f),vector,deepest);
1325    if (T == NULL)  return(NULL);
1326    cuddRef(T);
1327    E = cuddAddVectorComposeRecur(dd,table,cuddE(f),vector,deepest);
1328    if (E == NULL) {
1329        Cudd_RecursiveDeref(dd, T);
1330        return(NULL);
1331    }
1332    cuddRef(E);
1333
1334    /* Retrieve the 0-1 ADD for the current top variable and call
1335    ** cuddAddIteRecur with the T and E we just created.
1336    */
1337    res = cuddAddIteRecur(dd,vector[f->index],T,E);
1338    if (res == NULL) {
1339        Cudd_RecursiveDeref(dd, T);
1340        Cudd_RecursiveDeref(dd, E);
1341        return(NULL);
1342    }
1343    cuddRef(res);
1344    Cudd_RecursiveDeref(dd, T);
1345    Cudd_RecursiveDeref(dd, E);
1346
1347    /* Do not keep the result if the reference count is only 1, since
1348    ** it will not be visited again
1349    */
1350    if (f->ref != 1) {
1351        ptrint fanout = (ptrint) f->ref;
1352        cuddSatDec(fanout);
1353        if (!cuddHashTableInsert1(table,f,res,fanout)) {
1354            Cudd_RecursiveDeref(dd, res);
1355            return(NULL);
1356        }
1357    }
1358    cuddDeref(res);
1359    return(res);
1360
1361} /* end of cuddAddVectorComposeRecur */
1362
1363
1364/**Function********************************************************************
1365
1366  Synopsis    [Performs the recursive step of Cudd_addGeneralVectorCompose.]
1367
1368  Description []
1369
1370  SideEffects [None]
1371
1372  SeeAlso     []
1373
1374******************************************************************************/
1375static DdNode *
1376cuddAddGeneralVectorComposeRecur(
1377  DdManager * dd /* DD manager */,
1378  DdHashTable * table /* computed table */,
1379  DdNode * f /* ADD in which to compose */,
1380  DdNode ** vectorOn /* functions to substitute for x_i */,
1381  DdNode ** vectorOff /* functions to substitute for x_i' */,
1382  int  deepest /* depth of deepest substitution */)
1383{
1384    DdNode      *T,*E,*t,*e;
1385    DdNode      *res;
1386
1387    /* If we are past the deepest substitution, return f. */
1388    if (cuddI(dd,f->index) > deepest) {
1389        return(f);
1390    }
1391
1392    if ((res = cuddHashTableLookup1(table,f)) != NULL) {
1393#ifdef DD_DEBUG
1394        addGeneralVectorComposeHits++;
1395#endif
1396        return(res);
1397    }
1398
1399    /* Split and recur on children of this node. */
1400    T = cuddAddGeneralVectorComposeRecur(dd,table,cuddT(f),
1401                                         vectorOn,vectorOff,deepest);
1402    if (T == NULL)  return(NULL);
1403    cuddRef(T);
1404    E = cuddAddGeneralVectorComposeRecur(dd,table,cuddE(f),
1405                                         vectorOn,vectorOff,deepest);
1406    if (E == NULL) {
1407        Cudd_RecursiveDeref(dd, T);
1408        return(NULL);
1409    }
1410    cuddRef(E);
1411
1412    /* Retrieve the compose ADDs for the current top variable and call
1413    ** cuddAddApplyRecur with the T and E we just created.
1414    */
1415    t = cuddAddApplyRecur(dd,Cudd_addTimes,vectorOn[f->index],T);
1416    if (t == NULL) {
1417      Cudd_RecursiveDeref(dd,T);
1418      Cudd_RecursiveDeref(dd,E);
1419      return(NULL);
1420    }
1421    cuddRef(t);
1422    e = cuddAddApplyRecur(dd,Cudd_addTimes,vectorOff[f->index],E);
1423    if (e == NULL) {
1424      Cudd_RecursiveDeref(dd,T);
1425      Cudd_RecursiveDeref(dd,E);
1426      Cudd_RecursiveDeref(dd,t);
1427      return(NULL);
1428    }
1429    cuddRef(e);
1430    res = cuddAddApplyRecur(dd,Cudd_addPlus,t,e);
1431    if (res == NULL) {
1432      Cudd_RecursiveDeref(dd,T);
1433      Cudd_RecursiveDeref(dd,E);
1434      Cudd_RecursiveDeref(dd,t);
1435      Cudd_RecursiveDeref(dd,e);
1436      return(NULL);
1437    }
1438    cuddRef(res);
1439    Cudd_RecursiveDeref(dd,T);
1440    Cudd_RecursiveDeref(dd,E);
1441    Cudd_RecursiveDeref(dd,t);
1442    Cudd_RecursiveDeref(dd,e);
1443
1444    /* Do not keep the result if the reference count is only 1, since
1445    ** it will not be visited again
1446    */
1447    if (f->ref != 1) {
1448        ptrint fanout = (ptrint) f->ref;
1449        cuddSatDec(fanout);
1450        if (!cuddHashTableInsert1(table,f,res,fanout)) {
1451            Cudd_RecursiveDeref(dd, res);
1452            return(NULL);
1453        }
1454    }
1455    cuddDeref(res);
1456    return(res);
1457
1458} /* end of cuddAddGeneralVectorComposeRecur */
1459
1460
1461/**Function********************************************************************
1462
1463  Synopsis    [Performs the recursive step of Cudd_addNonSimCompose.]
1464
1465  Description []
1466
1467  SideEffects [None]
1468
1469  SeeAlso     []
1470
1471******************************************************************************/
1472static DdNode *
1473cuddAddNonSimComposeRecur(
1474  DdManager * dd,
1475  DdNode * f,
1476  DdNode ** vector,
1477  DdNode * key,
1478  DdNode * cube,
1479  int  lastsub)
1480{
1481    DdNode *f1, *f0, *key1, *key0, *cube1, *var;
1482    DdNode *T,*E;
1483    DdNode *r;
1484    unsigned int top, topf, topk, topc;
1485    unsigned int index;
1486    int i;
1487    DdNode **vect1;
1488    DdNode **vect0;
1489
1490    statLine(dd);
1491    /* If we are past the deepest substitution, return f. */
1492    if (cube == DD_ONE(dd) || cuddIsConstant(f)) {
1493        return(f);
1494    }
1495
1496    /* If problem already solved, look up answer and return. */
1497    r = cuddCacheLookup(dd,DD_ADD_NON_SIM_COMPOSE_TAG,f,key,cube);
1498    if (r != NULL) {
1499        return(r);
1500    }
1501
1502    /* Find top variable. we just need to look at f, key, and cube,
1503    ** because all the varibles in the gi are in key.
1504    */
1505    topf = cuddI(dd,f->index);
1506    topk = cuddI(dd,key->index);
1507    top = ddMin(topf,topk);
1508    topc = cuddI(dd,cube->index);
1509    top = ddMin(top,topc);
1510    index = dd->invperm[top];
1511
1512    /* Compute the cofactors. */
1513    if (topf == top) {
1514        f1 = cuddT(f);
1515        f0 = cuddE(f);
1516    } else {
1517        f1 = f0 = f;
1518    }
1519    if (topc == top) {
1520        cube1 = cuddT(cube);
1521        /* We want to eliminate vector[index] from key. Otherwise
1522        ** cache performance is severely affected. Hence we
1523        ** existentially quantify the variable with index "index" from key.
1524        */
1525        var = Cudd_addIthVar(dd, (int) index);
1526        if (var == NULL) {
1527            return(NULL);
1528        }
1529        cuddRef(var);
1530        key1 = cuddAddExistAbstractRecur(dd, key, var);
1531        if (key1 == NULL) {
1532            Cudd_RecursiveDeref(dd,var);
1533            return(NULL);
1534        }
1535        cuddRef(key1);
1536        Cudd_RecursiveDeref(dd,var);
1537        key0 = key1;
1538    } else {
1539        cube1 = cube;
1540        if (topk == top) {
1541            key1 = cuddT(key);
1542            key0 = cuddE(key);
1543        } else {
1544            key1 = key0 = key;
1545        }
1546        cuddRef(key1);
1547    }
1548
1549    /* Allocate two new vectors for the cofactors of vector. */
1550    vect1 = ALLOC(DdNode *,lastsub);
1551    if (vect1 == NULL) {
1552        dd->errorCode = CUDD_MEMORY_OUT;
1553        Cudd_RecursiveDeref(dd,key1);
1554        return(NULL);
1555    }
1556    vect0 = ALLOC(DdNode *,lastsub);
1557    if (vect0 == NULL) {
1558        dd->errorCode = CUDD_MEMORY_OUT;
1559        Cudd_RecursiveDeref(dd,key1);
1560        FREE(vect1);
1561        return(NULL);
1562    }
1563
1564    /* Cofactor the gi. Eliminate vect1[index] and vect0[index], because
1565    ** we do not need them.
1566    */
1567    for (i = 0; i < lastsub; i++) {
1568        DdNode *gi = vector[i];
1569        if (gi == NULL) {
1570            vect1[i] = vect0[i] = NULL;
1571        } else if (gi->index == index) {
1572            vect1[i] = cuddT(gi);
1573            vect0[i] = cuddE(gi);
1574        } else {
1575            vect1[i] = vect0[i] = gi;
1576        }
1577    }
1578    vect1[index] = vect0[index] = NULL;
1579
1580    /* Recur on children. */
1581    T = cuddAddNonSimComposeRecur(dd,f1,vect1,key1,cube1,lastsub);
1582    FREE(vect1);
1583    if (T == NULL) {
1584        Cudd_RecursiveDeref(dd,key1);
1585        FREE(vect0);
1586        return(NULL);
1587    }
1588    cuddRef(T);
1589    E = cuddAddNonSimComposeRecur(dd,f0,vect0,key0,cube1,lastsub);
1590    FREE(vect0);
1591    if (E == NULL) {
1592        Cudd_RecursiveDeref(dd,key1);
1593        Cudd_RecursiveDeref(dd,T);
1594        return(NULL);
1595    }
1596    cuddRef(E);
1597    Cudd_RecursiveDeref(dd,key1);
1598
1599    /* Retrieve the 0-1 ADD for the current top variable from vector,
1600    ** and call cuddAddIteRecur with the T and E we just created.
1601    */
1602    r = cuddAddIteRecur(dd,vector[index],T,E);
1603    if (r == NULL) {
1604        Cudd_RecursiveDeref(dd,T);
1605        Cudd_RecursiveDeref(dd,E);
1606        return(NULL);
1607    }
1608    cuddRef(r);
1609    Cudd_RecursiveDeref(dd,T);
1610    Cudd_RecursiveDeref(dd,E);
1611    cuddDeref(r);
1612
1613    /* Store answer to trim recursion. */
1614    cuddCacheInsert(dd,DD_ADD_NON_SIM_COMPOSE_TAG,f,key,cube,r);
1615
1616    return(r);
1617
1618} /* end of cuddAddNonSimComposeRecur */
1619
1620
1621/**Function********************************************************************
1622
1623  Synopsis    [Performs the recursive step of Cudd_bddVectorCompose.]
1624
1625  Description []
1626
1627  SideEffects [None]
1628
1629  SeeAlso     []
1630
1631******************************************************************************/
1632static DdNode *
1633cuddBddVectorComposeRecur(
1634  DdManager * dd /* DD manager */,
1635  DdHashTable * table /* computed table */,
1636  DdNode * f /* BDD in which to compose */,
1637  DdNode ** vector /* functions to be composed */,
1638  int deepest /* depth of the deepest substitution */)
1639{
1640    DdNode      *F,*T,*E;
1641    DdNode      *res;
1642
1643    statLine(dd);
1644    F = Cudd_Regular(f);
1645
1646    /* If we are past the deepest substitution, return f. */
1647    if (cuddI(dd,F->index) > deepest) {
1648        return(f);
1649    }
1650
1651    /* If problem already solved, look up answer and return. */
1652    if ((res = cuddHashTableLookup1(table,F)) != NULL) {
1653#ifdef DD_DEBUG
1654        bddVectorComposeHits++;
1655#endif
1656        return(Cudd_NotCond(res,F != f));
1657    }
1658
1659    /* Split and recur on children of this node. */
1660    T = cuddBddVectorComposeRecur(dd,table,cuddT(F),vector, deepest);
1661    if (T == NULL) return(NULL);
1662    cuddRef(T);
1663    E = cuddBddVectorComposeRecur(dd,table,cuddE(F),vector, deepest);
1664    if (E == NULL) {
1665        Cudd_IterDerefBdd(dd, T);
1666        return(NULL);
1667    }
1668    cuddRef(E);
1669
1670    /* Call cuddBddIteRecur with the BDD that replaces the current top
1671    ** variable and the T and E we just created.
1672    */
1673    res = cuddBddIteRecur(dd,vector[F->index],T,E);
1674    if (res == NULL) {
1675        Cudd_IterDerefBdd(dd, T);
1676        Cudd_IterDerefBdd(dd, E);
1677        return(NULL);
1678    }
1679    cuddRef(res);
1680    Cudd_IterDerefBdd(dd, T);
1681    Cudd_IterDerefBdd(dd, E);   
1682
1683    /* Do not keep the result if the reference count is only 1, since
1684    ** it will not be visited again.
1685    */
1686    if (F->ref != 1) {
1687        ptrint fanout = (ptrint) F->ref;
1688        cuddSatDec(fanout);
1689        if (!cuddHashTableInsert1(table,F,res,fanout)) {
1690            Cudd_IterDerefBdd(dd, res);
1691            return(NULL);
1692        }
1693    }
1694    cuddDeref(res);
1695    return(Cudd_NotCond(res,F != f));
1696
1697} /* end of cuddBddVectorComposeRecur */
1698
1699
1700/**Function********************************************************************
1701
1702  Synopsis    [Comparison of a function to the i-th ADD variable.]
1703
1704  Description [Comparison of a function to the i-th ADD variable. Returns 1 if
1705  the function is the i-th ADD variable; 0 otherwise.]
1706
1707  SideEffects [None]
1708
1709  SeeAlso     []
1710
1711******************************************************************************/
1712DD_INLINE
1713static int
1714ddIsIthAddVar(
1715  DdManager * dd,
1716  DdNode * f,
1717  unsigned int  i)
1718{
1719    return(f->index == i && cuddT(f) == DD_ONE(dd) && cuddE(f) == DD_ZERO(dd));
1720
1721} /* end of ddIsIthAddVar */
1722
1723
1724/**Function********************************************************************
1725
1726  Synopsis    [Comparison of a pair of functions to the i-th ADD variable.]
1727
1728  Description [Comparison of a pair of functions to the i-th ADD
1729  variable. Returns 1 if the functions are the i-th ADD variable and its
1730  complement; 0 otherwise.]
1731
1732  SideEffects [None]
1733
1734  SeeAlso     []
1735
1736******************************************************************************/
1737DD_INLINE
1738static int
1739ddIsIthAddVarPair(
1740  DdManager * dd,
1741  DdNode * f,
1742  DdNode * g,
1743  unsigned int  i)
1744{
1745    return(f->index == i && g->index == i && 
1746           cuddT(f) == DD_ONE(dd) && cuddE(f) == DD_ZERO(dd) &&
1747           cuddT(g) == DD_ZERO(dd) && cuddE(g) == DD_ONE(dd));
1748
1749} /* end of ddIsIthAddVarPair */
Note: See TracBrowser for help on using the repository browser.