1 /**CFile***********************************************************************
3 FileName [cuddCompose.c]
7 Synopsis [Functional composition and variable permutation of DDs.]
9 Description [External procedures included in this module:
11 <li> Cudd_bddCompose()
12 <li> Cudd_addCompose()
13 <li> Cudd_addPermute()
14 <li> Cudd_addSwapVariables()
15 <li> Cudd_bddPermute()
18 <li> Cudd_bddSwapVariables()
19 <li> Cudd_bddAdjPermuteX()
20 <li> Cudd_addVectorCompose()
21 <li> Cudd_addGeneralVectorCompose()
22 <li> Cudd_addNonSimCompose()
23 <li> Cudd_bddVectorCompose()
25 Internal procedures included in this module:
27 <li> cuddBddComposeRecur()
28 <li> cuddAddComposeRecur()
30 Static procedures included in this module:
32 <li> cuddAddPermuteRecur()
33 <li> cuddBddPermuteRecur()
34 <li> cuddBddVarMapRecur()
35 <li> cuddAddVectorComposeRecur()
36 <li> cuddAddGeneralVectorComposeRecur()
37 <li> cuddAddNonSimComposeRecur()
38 <li> cuddBddVectorComposeRecur()
40 <li> ddIsIthAddVarPair()
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.]
49 Author [Fabio Somenzi and Kavita Ravi]
51 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
55 Redistribution and use in source and binary forms, with or without
56 modification, are permitted provided that the following conditions
59 Redistributions of source code must retain the above copyright
60 notice, this list of conditions and the following disclaimer.
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.
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.
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.]
83 ******************************************************************************/
89 /*---------------------------------------------------------------------------*/
90 /* Constant declarations */
91 /*---------------------------------------------------------------------------*/
93 /*---------------------------------------------------------------------------*/
94 /* Stucture declarations */
95 /*---------------------------------------------------------------------------*/
97 /*---------------------------------------------------------------------------*/
98 /* Type declarations */
99 /*---------------------------------------------------------------------------*/
101 /*---------------------------------------------------------------------------*/
102 /* Variable declarations */
103 /*---------------------------------------------------------------------------*/
106 static char rcsid
[] DD_UNUSED
= "$Id: cuddCompose.c,v 1.45 2004/08/13 18:04:47 fabio Exp $";
110 static int addPermuteRecurHits
;
111 static int bddPermuteRecurHits
;
112 static int bddVectorComposeHits
;
113 static int addVectorComposeHits
;
115 static int addGeneralVectorComposeHits
;
118 /*---------------------------------------------------------------------------*/
119 /* Macro declarations */
120 /*---------------------------------------------------------------------------*/
123 /**AutomaticStart*************************************************************/
125 /*---------------------------------------------------------------------------*/
126 /* Static function prototypes */
127 /*---------------------------------------------------------------------------*/
129 static DdNode
* cuddAddPermuteRecur (DdManager
*manager
, DdHashTable
*table
, DdNode
*node
, int *permut
);
130 static DdNode
* cuddBddPermuteRecur (DdManager
*manager
, DdHashTable
*table
, DdNode
*node
, int *permut
);
131 static DdNode
* cuddBddVarMapRecur (DdManager
*manager
, DdNode
*f
);
132 static DdNode
* cuddAddVectorComposeRecur (DdManager
*dd
, DdHashTable
*table
, DdNode
*f
, DdNode
**vector
, int deepest
);
133 static DdNode
* cuddAddNonSimComposeRecur (DdManager
*dd
, DdNode
*f
, DdNode
**vector
, DdNode
*key
, DdNode
*cube
, int lastsub
);
134 static DdNode
* cuddBddVectorComposeRecur (DdManager
*dd
, DdHashTable
*table
, DdNode
*f
, DdNode
**vector
, int deepest
);
135 DD_INLINE
static int ddIsIthAddVar (DdManager
*dd
, DdNode
*f
, unsigned int i
);
137 static DdNode
* cuddAddGeneralVectorComposeRecur (DdManager
*dd
, DdHashTable
*table
, DdNode
*f
, DdNode
**vectorOn
, DdNode
**vectorOff
, int deepest
);
138 DD_INLINE
static int ddIsIthAddVarPair (DdManager
*dd
, DdNode
*f
, DdNode
*g
, unsigned int i
);
140 /**AutomaticEnd***************************************************************/
143 /*---------------------------------------------------------------------------*/
144 /* Definition of exported functions */
145 /*---------------------------------------------------------------------------*/
148 /**Function********************************************************************
150 Synopsis [Substitutes g for x_v in the BDD for f.]
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.]
159 SeeAlso [Cudd_addCompose]
161 ******************************************************************************/
172 if (v
< 0 || v
>= dd
->size
) return(NULL
);
177 res
= cuddBddComposeRecur(dd
,f
,g
,proj
);
178 } while (dd
->reordered
== 1);
181 } /* end of Cudd_bddCompose */
184 /**Function********************************************************************
186 Synopsis [Substitutes g for x_v in the ADD for f.]
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;
196 SeeAlso [Cudd_bddCompose]
198 ******************************************************************************/
209 if (v
< 0 || v
>= dd
->size
) return(NULL
);
214 res
= cuddAddComposeRecur(dd
,f
,g
,proj
);
215 } while (dd
->reordered
== 1);
218 } /* end of Cudd_addCompose */
221 /**Function********************************************************************
223 Synopsis [Permutes the variables of an ADD.]
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
234 SeeAlso [Cudd_bddPermute Cudd_addSwapVariables]
236 ******************************************************************************/
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);
257 if (res
!= NULL
) cuddDeref(res
);
260 } /* end of Cudd_addPermute */
263 /**Function********************************************************************
265 Synopsis [Swaps two sets of variables of the same size (x and y) in
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.]
275 SeeAlso [Cudd_addPermute Cudd_bddSwapVariables]
277 ******************************************************************************/
279 Cudd_addSwapVariables(
290 permut
= ALLOC(int,dd
->size
);
291 if (permut
== NULL
) {
292 dd
->errorCode
= CUDD_MEMORY_OUT
;
295 for (i
= 0; i
< dd
->size
; i
++) permut
[i
] = i
;
296 for (i
= 0; i
< n
; i
++) {
303 swapped
= Cudd_addPermute(dd
,f
,permut
);
308 } /* end of Cudd_addSwapVariables */
311 /**Function********************************************************************
313 Synopsis [Permutes the variables of a BDD.]
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
324 SeeAlso [Cudd_addPermute Cudd_bddSwapVariables]
326 ******************************************************************************/
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
);
345 } while (manager
->reordered
== 1);
347 if (res
!= NULL
) cuddDeref(res
);
350 } /* end of Cudd_bddPermute */
353 /**Function********************************************************************
355 Synopsis [Remaps the variables of a BDD using the default variable map.]
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
365 SeeAlso [Cudd_bddPermute Cudd_bddSwapVariables Cudd_SetVarMap]
367 ******************************************************************************/
370 DdManager
* manager
/* DD manager */,
371 DdNode
* f
/* function in which to remap variables */)
375 if (manager
->map
== NULL
) return(NULL
);
377 manager
->reordered
= 0;
378 res
= cuddBddVarMapRecur(manager
, f
);
379 } while (manager
->reordered
== 1);
383 } /* end of Cudd_bddVarMap */
386 /**Function********************************************************************
388 Synopsis [Registers a variable mapping with the manager.]
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.]
406 SideEffects [Modifies the manager. May clear the cache.]
408 SeeAlso [Cudd_bddVarMap Cudd_bddPermute Cudd_bddSwapVariables]
410 ******************************************************************************/
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 */)
420 if (manager
->map
!= NULL
) {
421 cuddCacheFlush(manager
);
423 manager
->map
= ALLOC(int,manager
->maxSize
);
424 if (manager
->map
== NULL
) {
425 manager
->errorCode
= CUDD_MEMORY_OUT
;
428 manager
->memused
+= sizeof(int) * manager
->maxSize
;
430 /* Initialize the map to the identity. */
431 for (i
= 0; i
< manager
->size
; i
++) {
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
;
441 } /* end of Cudd_SetVarMap */
444 /**Function********************************************************************
446 Synopsis [Swaps two sets of variables of the same size (x and y) in
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.]
456 SeeAlso [Cudd_bddPermute Cudd_addSwapVariables]
458 ******************************************************************************/
460 Cudd_bddSwapVariables(
471 permut
= ALLOC(int,dd
->size
);
472 if (permut
== NULL
) {
473 dd
->errorCode
= CUDD_MEMORY_OUT
;
476 for (i
= 0; i
< dd
->size
; i
++) permut
[i
] = i
;
477 for (i
= 0; i
< n
; i
++) {
484 swapped
= Cudd_bddPermute(dd
,f
,permut
);
489 } /* end of Cudd_bddSwapVariables */
492 /**Function********************************************************************
494 Synopsis [Rearranges a set of variables in the BDD B.]
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.]
503 SeeAlso [Cudd_bddPermute Cudd_bddSwapVariables
504 Cudd_Dxygtdxz Cudd_Dxygtdyz Cudd_PrioritySelect]
506 ******************************************************************************/
518 permut
= ALLOC(int,dd
->size
);
519 if (permut
== NULL
) {
520 dd
->errorCode
= CUDD_MEMORY_OUT
;
523 for (i
= 0; i
< dd
->size
; i
++) permut
[i
] = i
;
524 for (i
= 0; i
< n
-2; i
+= 3) {
531 swapped
= Cudd_bddPermute(dd
,B
,permut
);
536 } /* end of Cudd_bddAdjPermuteX */
539 /**Function********************************************************************
541 Synopsis [Composes an ADD with a vector of 0-1 ADDs.]
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
554 SeeAlso [Cudd_addNonSimCompose Cudd_addPermute Cudd_addCompose
555 Cudd_bddVectorCompose]
557 ******************************************************************************/
559 Cudd_addVectorCompose(
571 /* Initialize local cache. */
572 table
= cuddHashTableInit(dd
,1,2);
573 if (table
== NULL
) return(NULL
);
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
)) {
583 /* Recursively solve the problem. */
584 res
= cuddAddVectorComposeRecur(dd
,table
,f
,vector
,deepest
);
585 if (res
!= NULL
) cuddRef(res
);
587 /* Dispose of local cache. */
588 cuddHashTableQuit(table
);
589 } while (dd
->reordered
== 1);
591 if (res
!= NULL
) cuddDeref(res
);
594 } /* end of Cudd_addVectorCompose */
597 /**Function********************************************************************
599 Synopsis [Composes an ADD with a vector of ADDs.]
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
612 SeeAlso [Cudd_addVectorCompose Cudd_addNonSimCompose Cudd_addPermute
613 Cudd_addCompose Cudd_bddVectorCompose]
615 ******************************************************************************/
617 Cudd_addGeneralVectorCompose(
630 /* Initialize local cache. */
631 table
= cuddHashTableInit(dd
,1,2);
632 if (table
== NULL
) return(NULL
);
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
)) {
642 /* Recursively solve the problem. */
643 res
= cuddAddGeneralVectorComposeRecur(dd
,table
,f
,vectorOn
,
645 if (res
!= NULL
) cuddRef(res
);
647 /* Dispose of local cache. */
648 cuddHashTableQuit(table
);
649 } while (dd
->reordered
== 1);
651 if (res
!= NULL
) cuddDeref(res
);
654 } /* end of Cudd_addGeneralVectorCompose */
657 /**Function********************************************************************
659 Synopsis [Composes an ADD with a vector of 0-1 ADDs.]
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
674 SeeAlso [Cudd_addVectorCompose Cudd_addPermute Cudd_addCompose]
676 ******************************************************************************/
678 Cudd_addNonSimCompose(
683 DdNode
*cube
, *key
, *var
, *tmp
, *piece
;
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
694 ** First we build replacement relation and cube of substituted
695 ** variables from the vector specifying the desired composition.
701 for (i
= (int) dd
->size
- 1; i
>= 0; i
--) {
702 if (ddIsIthAddVar(dd
,vector
[i
],(unsigned int)i
)) {
705 var
= Cudd_addIthVar(dd
,i
);
707 Cudd_RecursiveDeref(dd
,key
);
708 Cudd_RecursiveDeref(dd
,cube
);
713 tmp
= Cudd_addApply(dd
,Cudd_addTimes
,var
,cube
);
715 Cudd_RecursiveDeref(dd
,key
);
716 Cudd_RecursiveDeref(dd
,cube
);
717 Cudd_RecursiveDeref(dd
,var
);
721 Cudd_RecursiveDeref(dd
,cube
);
723 /* Update replacement relation. */
724 piece
= Cudd_addApply(dd
,Cudd_addXnor
,var
,vector
[i
]);
726 Cudd_RecursiveDeref(dd
,key
);
727 Cudd_RecursiveDeref(dd
,var
);
731 Cudd_RecursiveDeref(dd
,var
);
732 tmp
= Cudd_addApply(dd
,Cudd_addTimes
,key
,piece
);
734 Cudd_RecursiveDeref(dd
,key
);
735 Cudd_RecursiveDeref(dd
,piece
);
739 Cudd_RecursiveDeref(dd
,key
);
740 Cudd_RecursiveDeref(dd
,piece
);
744 /* Now try composition, until no reordering occurs. */
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
)) {
753 /* Recursively solve the problem. */
755 res
= cuddAddNonSimComposeRecur(dd
,f
,vector
,key
,cube
,lastsub
+1);
756 if (res
!= NULL
) cuddRef(res
);
758 } while (dd
->reordered
== 1);
760 Cudd_RecursiveDeref(dd
,key
);
761 Cudd_RecursiveDeref(dd
,cube
);
762 if (res
!= NULL
) cuddDeref(res
);
765 } /* end of Cudd_addNonSimCompose */
768 /**Function********************************************************************
770 Synopsis [Composes a BDD with a vector of BDDs.]
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
783 SeeAlso [Cudd_bddPermute Cudd_bddCompose Cudd_addVectorCompose]
785 ******************************************************************************/
787 Cudd_bddVectorCompose(
799 /* Initialize local cache. */
800 table
= cuddHashTableInit(dd
,1,2);
801 if (table
== NULL
) return(NULL
);
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
]) {
811 /* Recursively solve the problem. */
812 res
= cuddBddVectorComposeRecur(dd
,table
,f
,vector
, deepest
);
813 if (res
!= NULL
) cuddRef(res
);
815 /* Dispose of local cache. */
816 cuddHashTableQuit(table
);
817 } while (dd
->reordered
== 1);
819 if (res
!= NULL
) cuddDeref(res
);
822 } /* end of Cudd_bddVectorCompose */
825 /*---------------------------------------------------------------------------*/
826 /* Definition of internal functions */
827 /*---------------------------------------------------------------------------*/
830 /**Function********************************************************************
832 Synopsis [Performs the recursive step of Cudd_bddCompose.]
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
842 SeeAlso [Cudd_bddCompose]
844 ******************************************************************************/
852 DdNode
*F
, *G
, *f1
, *f0
, *g1
, *g0
, *r
, *t
, *e
;
853 unsigned int v
, topf
, topg
, topindex
;
857 v
= dd
->perm
[proj
->index
];
859 topf
= cuddI(dd
,F
->index
);
861 /* Terminal case. Subsumes the test for constant f. */
862 if (topf
> v
) return(f
);
864 /* We solve the problem for a regular pointer, and then complement
865 ** the result if the pointer was originally complemented.
867 comple
= Cudd_IsComplement(f
);
870 r
= cuddCacheLookup(dd
,DD_BDD_COMPOSE_RECUR_TAG
,F
,g
,proj
);
872 return(Cudd_NotCond(r
,comple
));
879 r
= cuddBddIteRecur(dd
, g
, f1
, f0
);
880 if (r
== NULL
) return(NULL
);
882 /* Compute cofactors of f and g. Remember the index of the top
886 topg
= cuddI(dd
,G
->index
);
905 /* Recursive step. */
906 t
= cuddBddComposeRecur(dd
, f1
, g1
, proj
);
907 if (t
== NULL
) return(NULL
);
909 e
= cuddBddComposeRecur(dd
, f0
, g0
, proj
);
911 Cudd_IterDerefBdd(dd
, t
);
916 r
= cuddBddIteRecur(dd
, dd
->vars
[topindex
], t
, e
);
918 Cudd_IterDerefBdd(dd
, t
);
919 Cudd_IterDerefBdd(dd
, e
);
923 Cudd_IterDerefBdd(dd
, t
); /* t & e not necessarily part of r */
924 Cudd_IterDerefBdd(dd
, e
);
928 cuddCacheInsert(dd
,DD_BDD_COMPOSE_RECUR_TAG
,F
,g
,proj
,r
);
930 return(Cudd_NotCond(r
,comple
));
932 } /* end of cuddBddComposeRecur */
935 /**Function********************************************************************
937 Synopsis [Performs the recursive step of Cudd_addCompose.]
939 Description [Performs the recursive step of Cudd_addCompose.
940 Returns the composed BDD if successful; NULL otherwise.]
944 SeeAlso [Cudd_addCompose]
946 ******************************************************************************/
954 DdNode
*f1
, *f0
, *g1
, *g0
, *r
, *t
, *e
;
955 unsigned int v
, topf
, topg
, topindex
;
958 v
= dd
->perm
[proj
->index
];
959 topf
= cuddI(dd
,f
->index
);
961 /* Terminal case. Subsumes the test for constant f. */
962 if (topf
> v
) return(f
);
965 r
= cuddCacheLookup(dd
,DD_ADD_COMPOSE_RECUR_TAG
,f
,g
,proj
);
974 r
= cuddAddIteRecur(dd
, g
, f1
, f0
);
975 if (r
== NULL
) return(NULL
);
977 /* Compute cofactors of f and g. Remember the index of the top
980 topg
= cuddI(dd
,g
->index
);
995 /* Recursive step. */
996 t
= cuddAddComposeRecur(dd
, f1
, g1
, proj
);
997 if (t
== NULL
) return(NULL
);
999 e
= cuddAddComposeRecur(dd
, f0
, g0
, proj
);
1001 Cudd_RecursiveDeref(dd
, t
);
1009 r
= cuddUniqueInter(dd
, (int) topindex
, t
, e
);
1011 Cudd_RecursiveDeref(dd
, t
);
1012 Cudd_RecursiveDeref(dd
, e
);
1020 cuddCacheInsert(dd
,DD_ADD_COMPOSE_RECUR_TAG
,f
,g
,proj
,r
);
1024 } /* end of cuddAddComposeRecur */
1027 /*---------------------------------------------------------------------------*/
1028 /* Definition of static functions */
1029 /*---------------------------------------------------------------------------*/
1032 /**Function********************************************************************
1034 Synopsis [Implements the recursive step of Cudd_addPermute.]
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.]
1049 SeeAlso [Cudd_addPermute cuddBddPermuteRecur]
1051 ******************************************************************************/
1053 cuddAddPermuteRecur(
1054 DdManager
* manager
/* DD manager */,
1055 DdHashTable
* table
/* computed table */,
1056 DdNode
* node
/* ADD to be reordered */,
1057 int * permut
/* permutation array */)
1064 /* Check for terminal case of constant node. */
1065 if (cuddIsConstant(node
)) {
1069 /* If problem already solved, look up answer and return. */
1070 if (node
->ref
!= 1 && (res
= cuddHashTableLookup1(table
,node
)) != NULL
) {
1072 addPermuteRecurHits
++;
1077 /* Split and recur on children of this node. */
1078 T
= cuddAddPermuteRecur(manager
,table
,cuddT(node
),permut
);
1079 if (T
== NULL
) return(NULL
);
1081 E
= cuddAddPermuteRecur(manager
,table
,cuddE(node
),permut
);
1083 Cudd_RecursiveDeref(manager
, T
);
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.
1092 index
= permut
[node
->index
];
1093 var
= cuddUniqueInter(manager
,index
,DD_ONE(manager
),DD_ZERO(manager
));
1094 if (var
== NULL
) return(NULL
);
1096 res
= cuddAddIteRecur(manager
,var
,T
,E
);
1098 Cudd_RecursiveDeref(manager
,var
);
1099 Cudd_RecursiveDeref(manager
, T
);
1100 Cudd_RecursiveDeref(manager
, E
);
1104 Cudd_RecursiveDeref(manager
,var
);
1105 Cudd_RecursiveDeref(manager
, T
);
1106 Cudd_RecursiveDeref(manager
, E
);
1108 /* Do not keep the result if the reference count is only 1, since
1109 ** it will not be visited again.
1111 if (node
->ref
!= 1) {
1112 ptrint fanout
= (ptrint
) node
->ref
;
1114 if (!cuddHashTableInsert1(table
,node
,res
,fanout
)) {
1115 Cudd_RecursiveDeref(manager
, res
);
1122 } /* end of cuddAddPermuteRecur */
1125 /**Function********************************************************************
1127 Synopsis [Implements the recursive step of Cudd_bddPermute.]
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.]
1142 SeeAlso [Cudd_bddPermute cuddAddPermuteRecur]
1144 ******************************************************************************/
1146 cuddBddPermuteRecur(
1147 DdManager
* manager
/* DD manager */,
1148 DdHashTable
* table
/* computed table */,
1149 DdNode
* node
/* BDD to be reordered */,
1150 int * permut
/* permutation array */)
1157 N
= Cudd_Regular(node
);
1159 /* Check for terminal case of constant node. */
1160 if (cuddIsConstant(N
)) {
1164 /* If problem already solved, look up answer and return. */
1165 if (N
->ref
!= 1 && (res
= cuddHashTableLookup1(table
,N
)) != NULL
) {
1167 bddPermuteRecurHits
++;
1169 return(Cudd_NotCond(res
,N
!= node
));
1172 /* Split and recur on children of this node. */
1173 T
= cuddBddPermuteRecur(manager
,table
,cuddT(N
),permut
);
1174 if (T
== NULL
) return(NULL
);
1176 E
= cuddBddPermuteRecur(manager
,table
,cuddE(N
),permut
);
1178 Cudd_IterDerefBdd(manager
, T
);
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.
1187 index
= permut
[N
->index
];
1188 res
= cuddBddIteRecur(manager
,manager
->vars
[index
],T
,E
);
1190 Cudd_IterDerefBdd(manager
, T
);
1191 Cudd_IterDerefBdd(manager
, E
);
1195 Cudd_IterDerefBdd(manager
, T
);
1196 Cudd_IterDerefBdd(manager
, E
);
1198 /* Do not keep the result if the reference count is only 1, since
1199 ** it will not be visited again.
1202 ptrint fanout
= (ptrint
) N
->ref
;
1204 if (!cuddHashTableInsert1(table
,N
,res
,fanout
)) {
1205 Cudd_IterDerefBdd(manager
, res
);
1210 return(Cudd_NotCond(res
,N
!= node
));
1212 } /* end of cuddBddPermuteRecur */
1215 /**Function********************************************************************
1217 Synopsis [Implements the recursive step of Cudd_bddVarMap.]
1219 Description [Implements the recursive step of Cudd_bddVarMap.
1220 Returns a pointer to the result if successful; NULL otherwise.]
1224 SeeAlso [Cudd_bddVarMap]
1226 ******************************************************************************/
1229 DdManager
*manager
/* DD manager */,
1230 DdNode
*f
/* BDD to be remapped */)
1237 F
= Cudd_Regular(f
);
1239 /* Check for terminal case of constant node. */
1240 if (cuddIsConstant(F
)) {
1244 /* If problem already solved, look up answer and return. */
1246 (res
= cuddCacheLookup1(manager
,Cudd_bddVarMap
,F
)) != NULL
) {
1247 return(Cudd_NotCond(res
,F
!= f
));
1250 /* Split and recur on children of this node. */
1251 T
= cuddBddVarMapRecur(manager
,cuddT(F
));
1252 if (T
== NULL
) return(NULL
);
1254 E
= cuddBddVarMapRecur(manager
,cuddE(F
));
1256 Cudd_IterDerefBdd(manager
, T
);
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.
1265 index
= manager
->map
[F
->index
];
1266 res
= cuddBddIteRecur(manager
,manager
->vars
[index
],T
,E
);
1268 Cudd_IterDerefBdd(manager
, T
);
1269 Cudd_IterDerefBdd(manager
, E
);
1273 Cudd_IterDerefBdd(manager
, T
);
1274 Cudd_IterDerefBdd(manager
, E
);
1276 /* Do not keep the result if the reference count is only 1, since
1277 ** it will not be visited again.
1280 cuddCacheInsert1(manager
,Cudd_bddVarMap
,F
,res
);
1283 return(Cudd_NotCond(res
,F
!= f
));
1285 } /* end of cuddBddVarMapRecur */
1288 /**Function********************************************************************
1290 Synopsis [Performs the recursive step of Cudd_addVectorCompose.]
1298 ******************************************************************************/
1300 cuddAddVectorComposeRecur(
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 */)
1311 /* If we are past the deepest substitution, return f. */
1312 if (cuddI(dd
,f
->index
) > deepest
) {
1316 if ((res
= cuddHashTableLookup1(table
,f
)) != NULL
) {
1318 addVectorComposeHits
++;
1323 /* Split and recur on children of this node. */
1324 T
= cuddAddVectorComposeRecur(dd
,table
,cuddT(f
),vector
,deepest
);
1325 if (T
== NULL
) return(NULL
);
1327 E
= cuddAddVectorComposeRecur(dd
,table
,cuddE(f
),vector
,deepest
);
1329 Cudd_RecursiveDeref(dd
, T
);
1334 /* Retrieve the 0-1 ADD for the current top variable and call
1335 ** cuddAddIteRecur with the T and E we just created.
1337 res
= cuddAddIteRecur(dd
,vector
[f
->index
],T
,E
);
1339 Cudd_RecursiveDeref(dd
, T
);
1340 Cudd_RecursiveDeref(dd
, E
);
1344 Cudd_RecursiveDeref(dd
, T
);
1345 Cudd_RecursiveDeref(dd
, E
);
1347 /* Do not keep the result if the reference count is only 1, since
1348 ** it will not be visited again
1351 ptrint fanout
= (ptrint
) f
->ref
;
1353 if (!cuddHashTableInsert1(table
,f
,res
,fanout
)) {
1354 Cudd_RecursiveDeref(dd
, res
);
1361 } /* end of cuddAddVectorComposeRecur */
1364 /**Function********************************************************************
1366 Synopsis [Performs the recursive step of Cudd_addGeneralVectorCompose.]
1374 ******************************************************************************/
1376 cuddAddGeneralVectorComposeRecur(
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 */)
1387 /* If we are past the deepest substitution, return f. */
1388 if (cuddI(dd
,f
->index
) > deepest
) {
1392 if ((res
= cuddHashTableLookup1(table
,f
)) != NULL
) {
1394 addGeneralVectorComposeHits
++;
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
);
1404 E
= cuddAddGeneralVectorComposeRecur(dd
,table
,cuddE(f
),
1405 vectorOn
,vectorOff
,deepest
);
1407 Cudd_RecursiveDeref(dd
, T
);
1412 /* Retrieve the compose ADDs for the current top variable and call
1413 ** cuddAddApplyRecur with the T and E we just created.
1415 t
= cuddAddApplyRecur(dd
,Cudd_addTimes
,vectorOn
[f
->index
],T
);
1417 Cudd_RecursiveDeref(dd
,T
);
1418 Cudd_RecursiveDeref(dd
,E
);
1422 e
= cuddAddApplyRecur(dd
,Cudd_addTimes
,vectorOff
[f
->index
],E
);
1424 Cudd_RecursiveDeref(dd
,T
);
1425 Cudd_RecursiveDeref(dd
,E
);
1426 Cudd_RecursiveDeref(dd
,t
);
1430 res
= cuddAddApplyRecur(dd
,Cudd_addPlus
,t
,e
);
1432 Cudd_RecursiveDeref(dd
,T
);
1433 Cudd_RecursiveDeref(dd
,E
);
1434 Cudd_RecursiveDeref(dd
,t
);
1435 Cudd_RecursiveDeref(dd
,e
);
1439 Cudd_RecursiveDeref(dd
,T
);
1440 Cudd_RecursiveDeref(dd
,E
);
1441 Cudd_RecursiveDeref(dd
,t
);
1442 Cudd_RecursiveDeref(dd
,e
);
1444 /* Do not keep the result if the reference count is only 1, since
1445 ** it will not be visited again
1448 ptrint fanout
= (ptrint
) f
->ref
;
1450 if (!cuddHashTableInsert1(table
,f
,res
,fanout
)) {
1451 Cudd_RecursiveDeref(dd
, res
);
1458 } /* end of cuddAddGeneralVectorComposeRecur */
1461 /**Function********************************************************************
1463 Synopsis [Performs the recursive step of Cudd_addNonSimCompose.]
1471 ******************************************************************************/
1473 cuddAddNonSimComposeRecur(
1481 DdNode
*f1
, *f0
, *key1
, *key0
, *cube1
, *var
;
1484 unsigned int top
, topf
, topk
, topc
;
1491 /* If we are past the deepest substitution, return f. */
1492 if (cube
== DD_ONE(dd
) || cuddIsConstant(f
)) {
1496 /* If problem already solved, look up answer and return. */
1497 r
= cuddCacheLookup(dd
,DD_ADD_NON_SIM_COMPOSE_TAG
,f
,key
,cube
);
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.
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
];
1512 /* Compute the cofactors. */
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.
1525 var
= Cudd_addIthVar(dd
, (int) index
);
1530 key1
= cuddAddExistAbstractRecur(dd
, key
, var
);
1532 Cudd_RecursiveDeref(dd
,var
);
1536 Cudd_RecursiveDeref(dd
,var
);
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
);
1556 vect0
= ALLOC(DdNode
*,lastsub
);
1557 if (vect0
== NULL
) {
1558 dd
->errorCode
= CUDD_MEMORY_OUT
;
1559 Cudd_RecursiveDeref(dd
,key1
);
1564 /* Cofactor the gi. Eliminate vect1[index] and vect0[index], because
1565 ** we do not need them.
1567 for (i
= 0; i
< lastsub
; i
++) {
1568 DdNode
*gi
= vector
[i
];
1570 vect1
[i
] = vect0
[i
] = NULL
;
1571 } else if (gi
->index
== index
) {
1572 vect1
[i
] = cuddT(gi
);
1573 vect0
[i
] = cuddE(gi
);
1575 vect1
[i
] = vect0
[i
] = gi
;
1578 vect1
[index
] = vect0
[index
] = NULL
;
1580 /* Recur on children. */
1581 T
= cuddAddNonSimComposeRecur(dd
,f1
,vect1
,key1
,cube1
,lastsub
);
1584 Cudd_RecursiveDeref(dd
,key1
);
1589 E
= cuddAddNonSimComposeRecur(dd
,f0
,vect0
,key0
,cube1
,lastsub
);
1592 Cudd_RecursiveDeref(dd
,key1
);
1593 Cudd_RecursiveDeref(dd
,T
);
1597 Cudd_RecursiveDeref(dd
,key1
);
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.
1602 r
= cuddAddIteRecur(dd
,vector
[index
],T
,E
);
1604 Cudd_RecursiveDeref(dd
,T
);
1605 Cudd_RecursiveDeref(dd
,E
);
1609 Cudd_RecursiveDeref(dd
,T
);
1610 Cudd_RecursiveDeref(dd
,E
);
1613 /* Store answer to trim recursion. */
1614 cuddCacheInsert(dd
,DD_ADD_NON_SIM_COMPOSE_TAG
,f
,key
,cube
,r
);
1618 } /* end of cuddAddNonSimComposeRecur */
1621 /**Function********************************************************************
1623 Synopsis [Performs the recursive step of Cudd_bddVectorCompose.]
1631 ******************************************************************************/
1633 cuddBddVectorComposeRecur(
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 */)
1644 F
= Cudd_Regular(f
);
1646 /* If we are past the deepest substitution, return f. */
1647 if (cuddI(dd
,F
->index
) > deepest
) {
1651 /* If problem already solved, look up answer and return. */
1652 if ((res
= cuddHashTableLookup1(table
,F
)) != NULL
) {
1654 bddVectorComposeHits
++;
1656 return(Cudd_NotCond(res
,F
!= f
));
1659 /* Split and recur on children of this node. */
1660 T
= cuddBddVectorComposeRecur(dd
,table
,cuddT(F
),vector
, deepest
);
1661 if (T
== NULL
) return(NULL
);
1663 E
= cuddBddVectorComposeRecur(dd
,table
,cuddE(F
),vector
, deepest
);
1665 Cudd_IterDerefBdd(dd
, T
);
1670 /* Call cuddBddIteRecur with the BDD that replaces the current top
1671 ** variable and the T and E we just created.
1673 res
= cuddBddIteRecur(dd
,vector
[F
->index
],T
,E
);
1675 Cudd_IterDerefBdd(dd
, T
);
1676 Cudd_IterDerefBdd(dd
, E
);
1680 Cudd_IterDerefBdd(dd
, T
);
1681 Cudd_IterDerefBdd(dd
, E
);
1683 /* Do not keep the result if the reference count is only 1, since
1684 ** it will not be visited again.
1687 ptrint fanout
= (ptrint
) F
->ref
;
1689 if (!cuddHashTableInsert1(table
,F
,res
,fanout
)) {
1690 Cudd_IterDerefBdd(dd
, res
);
1695 return(Cudd_NotCond(res
,F
!= f
));
1697 } /* end of cuddBddVectorComposeRecur */
1700 /**Function********************************************************************
1702 Synopsis [Comparison of a function to the i-th ADD variable.]
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.]
1711 ******************************************************************************/
1719 return(f
->index
== i
&& cuddT(f
) == DD_ONE(dd
) && cuddE(f
) == DD_ZERO(dd
));
1721 } /* end of ddIsIthAddVar */
1724 /**Function********************************************************************
1726 Synopsis [Comparison of a pair of functions to the i-th ADD variable.]
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.]
1736 ******************************************************************************/
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
));
1749 } /* end of ddIsIthAddVarPair */