1 /**CFile***********************************************************************
3 FileName [cuddBddPort.c]
7 Synopsis [SIS interface to the Decision Diagram Package of the
8 University of Colorado.]
10 Description [This file implements an interface between the functions in
11 the Berkeley BDD package and the functions provided by the CUDD (decision
12 diagram) package from the University of Colorado. The CUDD package is a
13 generic implementation of a decision diagram data structure. For the time
14 being, only Boole expansion is implemented and the leaves in the
15 in the nodes can be the constants zero, one or any arbitrary value.]
17 Author [Abelardo Pardo]
19 Copyright [Copyright (c) 1994-1996 The Univ. of Colorado.
22 Permission is hereby granted, without written agreement and without license
23 or royalty fees, to use, copy, modify, and distribute this software and its
24 documentation for any purpose, provided that the above copyright notice and
25 the following two paragraphs appear in all copies of this software.
27 IN NO EVENT SHALL THE UNIVERSITY OF COLORADO BE LIABLE TO ANY PARTY FOR
28 DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
29 OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
30 COLORADO HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
32 THE UNIVERSITY OF COLORADO SPECIFICALLY DISCLAIMS ANY WARRANTIES,
33 INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
34 FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN
35 "AS IS" BASIS, AND THE UNIVERSITY OF COLORADO HAS NO OBLIGATION TO PROVIDE
36 MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
38 ******************************************************************************/
52 /*---------------------------------------------------------------------------*/
53 /* Constant declarations */
54 /*---------------------------------------------------------------------------*/
56 /*---------------------------------------------------------------------------*/
57 /* Stucture declarations */
58 /*---------------------------------------------------------------------------*/
66 /*---------------------------------------------------------------------------*/
67 /* Type declarations */
68 /*---------------------------------------------------------------------------*/
70 /*---------------------------------------------------------------------------*/
71 /* Variable declarations */
72 /*---------------------------------------------------------------------------*/
75 static char rcsid
[] DD_UNUSED
= "$Id: cuddBddPort.c,v 1.11 1996/05/08 06:13:08 fabio Exp $";
78 /*---------------------------------------------------------------------------*/
79 /* Macro declarations */
80 /*---------------------------------------------------------------------------*/
83 /**AutomaticStart*************************************************************/
85 /*---------------------------------------------------------------------------*/
86 /* Static function prototypes */
87 /*---------------------------------------------------------------------------*/
89 static bdd_t
* bdd_construct_bdd_t (DdManager
*mgr
, DdNode
* fn
);
91 /**AutomaticEnd***************************************************************/
94 /*---------------------------------------------------------------------------*/
95 /* Definition of exported functions */
96 /*---------------------------------------------------------------------------*/
99 /**Function********************************************************************
101 Synopsis [Terminates the bdd package.]
105 ******************************************************************************/
110 if (mgr
->hooks
!= NULL
) FREE(mgr
->hooks
);
113 } /* end of bdd_end */
116 /**Function********************************************************************
118 Synopsis [Initialize manager with the options given in mgr_init.]
122 ******************************************************************************/
124 bdd_set_mgr_init_dflts(mgr_init
)
125 bdd_mgr_init
*mgr_init
;
127 fprintf(stderr
,"CU DD Package: bdd_set_mgr_init_dflts translated to no-op\n");
130 } /* end of bdd_set_mgr_init_dflts */
133 /**Function********************************************************************
135 Synopsis [Starts the manager with nvariables variables.]
139 ******************************************************************************/
141 bdd_start(nvariables
)
145 bdd_external_hooks
*hooks
;
147 mgr
= Cudd_Init((unsigned int)nvariables
,0,CUDD_UNIQUE_SLOTS
,
150 hooks
= ALLOC(bdd_external_hooks
,1);
151 hooks
->mdd
= hooks
->network
= hooks
->undef1
= (char *) 0;
152 mgr
->hooks
= (char *) hooks
;
154 return (bdd_manager
*)mgr
;
156 } /* end of bdd_start */
159 /**Function********************************************************************
161 Synopsis [Starts the manager with parameters.]
165 ******************************************************************************/
167 bdd_start_with_params(nvariables
, mgr_init
)
169 bdd_mgr_init
*mgr_init
;
171 fprintf(stderr
,"CU DD Package: bdd_start_with_parameters bypassed\n");
172 return (bdd_manager
*)Cudd_Init((unsigned int)nvariables
,0,
173 CUDD_UNIQUE_SLOTS
,CUDD_CACHE_SLOTS
,0);
175 } /* end of bdd_start_with_params */
178 /**Function********************************************************************
180 Synopsis [Creates a new variable in the manager.]
184 ******************************************************************************/
186 bdd_create_variable(mgr
)
190 DdManager
*dd
= (DdManager
*) mgr
;
191 DdNode
*one
= DD_ONE(dd
);
193 if (dd
->size
>= CUDD_MAXINDEX
-1) return(NULL
);
196 var
= cuddUniqueInter(dd
,dd
->size
,one
,Cudd_Not(one
));
197 } while (dd
->reordered
== 1);
199 if (var
== NULL
) return(NULL
);
201 return(bdd_construct_bdd_t(dd
,var
));
203 } /* end of bdd_create_variable */
206 /**Function********************************************************************
208 Synopsis [Creates a new variable and positions it after the
209 variable with the specified index.]
213 ******************************************************************************/
215 bdd_create_variable_after(mgr
, after_id
)
217 bdd_variableId after_id
;
220 DdManager
*dd
= (DdManager
*) mgr
;
223 if (after_id
>= dd
->size
) return(NULL
);
224 level
= 1 + dd
->perm
[after_id
];
225 var
= Cudd_bddNewVarAtLevel(dd
,level
);
226 if (var
== NULL
) return(NULL
);
228 return(bdd_construct_bdd_t(dd
,var
));
230 } /* end of bdd_create_variable_after */
233 /**Function********************************************************************
235 Synopsis [Returns the BDD representing the variable with given ID.]
239 ******************************************************************************/
241 bdd_get_variable(mgr
, variable_ID
)
243 bdd_variableId variable_ID
; /* unsigned int */
246 DdManager
*dd
= (DdManager
*) mgr
;
247 DdNode
*one
= DD_ONE(dd
);
249 if (variable_ID
>= CUDD_MAXINDEX
-1) return(NULL
);
252 var
= cuddUniqueInter(dd
,(int)variable_ID
,one
,Cudd_Not(one
));
253 } while (dd
->reordered
== 1);
255 if (var
== NULL
) return(NULL
);
257 return(bdd_construct_bdd_t(dd
,var
));
259 } /* end of bdd_get_variable */
262 /**Function********************************************************************
264 Synopsis [Creates a copy of the BDD.]
268 ******************************************************************************/
274 return(bdd_construct_bdd_t((DdManager
*)f
->mgr
,f
->node
));
276 } /* end of bdd_dup */
279 /**Function********************************************************************
281 Synopsis [Deletes the BDD of f.]
285 ******************************************************************************/
291 fail("bdd_free: trying to free a NULL bdd_t");
294 if (f
->free
== TRUE
) {
295 fail("bdd_free: trying to free a freed bdd_t");
298 Cudd_RecursiveDeref((DdManager
*)f
->mgr
,f
->node
);
299 /* This is a bit overconservative. */
306 } /* end of bdd_free */
309 /**Function********************************************************************
311 Synopsis [And of two BDDs.]
315 ******************************************************************************/
317 bdd_and(f
, g
, f_phase
, g_phase
)
324 DdNode
*newf
,*newg
,*fandg
;
327 /* Make sure both BDDs belong to the same manager. */
328 assert(f
->mgr
== g
->mgr
);
330 /* Modify the phases of the operands according to the parameters. */
332 newf
= Cudd_Not(f
->node
);
337 newg
= Cudd_Not(g
->node
);
342 /* Perform the AND operation */
343 dd
= (DdManager
*)f
->mgr
;
344 fandg
= Cudd_bddAnd((DdManager
*)f
->mgr
,newf
,newg
);
345 if (fandg
== NULL
) return(NULL
);
347 result
= bdd_construct_bdd_t(dd
,fandg
);
351 } /* end of bdd_and */
354 /**Function********************************************************************
356 Synopsis [Abstracts variables from the product of two BDDs.]
360 ******************************************************************************/
362 bdd_and_smooth(f
, g
, smoothing_vars
)
365 array_t
*smoothing_vars
; /* of bdd_t *'s */
369 DdNode
*cube
,*tmpDd
,*result
;
372 /* Make sure both operands belong to the same manager. */
373 assert(f
->mgr
== g
->mgr
);
375 /* The Boulder package needs the smothing variables passed as a cube.
376 ** Therefore we must build that cube from the indices of variables
377 ** in the array before calling the procedure.
379 mgr
= (DdManager
*)f
->mgr
;
380 Cudd_Ref(cube
= DD_ONE(mgr
));
381 for (i
= 0; i
< array_n(smoothing_vars
); i
++) {
382 variable
= array_fetch(bdd_t
*,smoothing_vars
,i
);
384 /* Make sure the variable belongs to the same manager. */
385 assert(mgr
== variable
->mgr
);
387 tmpDd
= Cudd_bddAnd(mgr
,cube
,variable
->node
);
389 Cudd_RecursiveDeref(mgr
,cube
);
393 Cudd_RecursiveDeref(mgr
, cube
);
397 /* Perform the smoothing */
398 result
= Cudd_bddAndAbstract(mgr
,f
->node
,g
->node
,cube
);
399 if (result
== NULL
) {
400 Cudd_RecursiveDeref(mgr
, cube
);
404 /* Get rid of temporary results. */
405 Cudd_RecursiveDeref(mgr
, cube
);
407 /* Build the bdd_t structure for the result */
408 return(bdd_construct_bdd_t(mgr
,result
));
410 } /* end of bdd_and_smooth */
413 /**Function********************************************************************
415 Synopsis [Return a minimum size BDD between bounds.]
419 ******************************************************************************/
421 bdd_between(f_min
, f_max
)
427 temp
= bdd_or(f_min
, f_max
, 1, 0);
428 ret
= bdd_minimize(f_min
, temp
);
432 } /* end of bdd_between */
435 /**Function********************************************************************
437 Synopsis [Computes the cofactor of f with respect to g.]
441 ******************************************************************************/
449 /* Make sure both operands belong to the same manager */
450 assert(f
->mgr
== g
->mgr
);
452 /* We use Cudd_bddConstrain instead of Cudd_Cofactor for generality. */
453 result
= Cudd_bddConstrain((DdManager
*)f
->mgr
,f
->node
,g
->node
);
454 if (result
== NULL
) return(NULL
);
456 return(bdd_construct_bdd_t((DdManager
*)f
->mgr
,result
));
458 } /* end of bdd_cofactor */
461 /**Function********************************************************************
463 Synopsis [Functional composition of a function by a variable.]
467 ******************************************************************************/
476 /* Make sure all operands belong to the same manager. */
477 assert(f
->mgr
== g
->mgr
);
478 assert(f
->mgr
== v
->mgr
);
480 result
= Cudd_bddCompose(f
->mgr
,f
->node
,g
->node
,(int)Cudd_Regular(v
->node
)->index
);
481 if (result
== NULL
) return(NULL
);
483 return(bdd_construct_bdd_t(f
->mgr
,result
));
485 } /* end of bdd_compose */
488 /**Function********************************************************************
490 Synopsis [Universal Abstraction of Variables.]
494 ******************************************************************************/
496 bdd_consensus(f
, quantifying_vars
)
498 array_t
*quantifying_vars
; /* of bdd_t *'s */
502 DdNode
*cube
,*tmpDd
,*result
;
505 /* The Boulder package needs the smothing variables passed as a cube.
506 ** Therefore we must build that cube from the indices of the variables
507 ** in the array before calling the procedure.
510 Cudd_Ref(cube
= DD_ONE(mgr
));
511 for (i
= 0; i
< array_n(quantifying_vars
); i
++) {
512 variable
= array_fetch(bdd_t
*,quantifying_vars
,i
);
514 /* Make sure the variable belongs to the same manager */
515 assert(mgr
== variable
->mgr
);
517 tmpDd
= Cudd_bddAnd(mgr
,cube
,variable
->node
);
519 Cudd_RecursiveDeref(mgr
, cube
);
523 Cudd_RecursiveDeref(mgr
, cube
);
527 /* Perform the consensus */
528 result
= Cudd_bddUnivAbstract(mgr
,f
->node
,cube
);
529 if (result
== NULL
) {
530 Cudd_RecursiveDeref(mgr
, cube
);
534 /* Get rid of temporary results */
535 Cudd_RecursiveDeref(mgr
, cube
);
537 /* Build the bdd_t structure for the result */
538 return(bdd_construct_bdd_t(mgr
,result
));
540 } /* end of bdd_consensus */
543 /**Function********************************************************************
545 Synopsis [The compatible projection function.]
547 Description [The compatible projection function. The reference minterm
548 is chosen based on the phases of the quantifying variables. If all
549 variables are in positive phase, the minterm 111...111 is used as
554 ******************************************************************************/
556 bdd_cproject(f
, quantifying_vars
)
558 array_t
*quantifying_vars
; /* of bdd_t* */
567 fail ("bdd_cproject: invalid BDD");
570 nvars
= array_n(quantifying_vars
);
572 fail("bdd_cproject: no projection variables");
578 for (i
= nvars
- 1; i
>= 0; i
--) {
580 fi
= array_fetch(bdd_t
*, quantifying_vars
, i
);
581 tmpp
= Cudd_bddAnd(dd
,fi
->node
,cube
);
583 Cudd_RecursiveDeref(dd
,cube
);
587 Cudd_RecursiveDeref(dd
,cube
);
591 res
= Cudd_CProjection(dd
,f
->node
,cube
);
593 Cudd_RecursiveDeref(dd
,cube
);
597 Cudd_RecursiveDeref(dd
,cube
);
599 return(bdd_construct_bdd_t(dd
,res
));
601 } /* end of bdd_cproject */
604 /**Function********************************************************************
610 ******************************************************************************/
612 bdd_ite(i
, t
, e
, i_phase
, t_phase
, e_phase
)
620 DdNode
*newi
,*newt
,*newe
,*ite
;
622 /* Make sure both bdds belong to the same mngr */
623 assert(i
->mgr
== t
->mgr
);
624 assert(i
->mgr
== e
->mgr
);
626 /* Modify the phases of the operands according to the parameters */
628 newi
= Cudd_Not(i
->node
);
633 newt
= Cudd_Not(t
->node
);
638 newe
= Cudd_Not(e
->node
);
643 /* Perform the ITE operation */
644 ite
= Cudd_bddIte(i
->mgr
,newi
,newt
,newe
);
645 if (ite
== NULL
) return(NULL
);
647 return(bdd_construct_bdd_t(i
->mgr
,ite
));
649 } /* end of bdd_ite */
652 /**Function********************************************************************
654 Synopsis [Restric operator as described in Coudert et al. ICCAD90.]
658 ******************************************************************************/
666 /* Make sure both operands belong to the same manager. */
667 assert(f
->mgr
== c
->mgr
);
669 result
= Cudd_bddRestrict(f
->mgr
,f
->node
,c
->node
);
670 if (result
== NULL
) return(NULL
);
673 return(bdd_construct_bdd_t(f
->mgr
,result
));
675 } /* end of bdd_minimize */
678 /**Function********************************************************************
680 Synopsis [Parametrized version of the Restrict operator.]
682 Description [Parametrized version of the Restrict operator. Currently
683 defaults to bdd_minimize.]
687 ******************************************************************************/
690 bdd_minimize_with_params(f
, c
, match_type
, compl, no_new_vars
, return_min
)
693 bdd_min_match_type_t match_type
;
698 return(bdd_minimize(f
,c
));
700 } /* end of bdd_minimize_with_params */
703 /**Function********************************************************************
709 ******************************************************************************/
716 Cudd_Ref(result
= Cudd_Not(f
->node
));
717 return(bdd_construct_bdd_t((DdManager
*)f
->mgr
,result
));
719 } /* end of bdd_not */
722 /**Function********************************************************************
724 Synopsis [Returns the one BDD.]
728 ******************************************************************************/
735 Cudd_Ref(result
= DD_ONE((DdManager
*)mgr
));
736 return(bdd_construct_bdd_t((DdManager
*)mgr
,result
));
738 } /* end of bdd_one */
741 /**Function********************************************************************
743 Synopsis [Or of two BDDs.]
747 ******************************************************************************/
749 bdd_or(f
, g
, f_phase
, g_phase
)
755 DdNode
*newf
,*newg
,*forg
;
758 /* Make sure both bdds belong to the same mngr */
759 assert(f
->mgr
== g
->mgr
);
761 /* Modify the phases of the operands according to the parameters */
763 newf
= Cudd_Not(f
->node
);
768 newg
= Cudd_Not(g
->node
);
773 /* Perform the OR operation */
774 forg
= Cudd_bddAnd(f
->mgr
,newf
,newg
);
775 if (forg
== NULL
) return(NULL
);
776 forg
= Cudd_Not(forg
);
778 result
= bdd_construct_bdd_t(f
->mgr
,forg
);
782 } /* end of bdd_or */
785 /**Function********************************************************************
787 Synopsis [Existential abstraction of variables.]
791 ******************************************************************************/
793 bdd_smooth(f
, smoothing_vars
)
795 array_t
*smoothing_vars
; /* of bdd_t *'s */
799 DdNode
*cube
,*tmpDd
,*result
;
802 /* The Boulder package needs the smothing variables passed as a cube.
803 ** Therefore we must build that cube from the indices of the variables
804 ** in the array before calling the procedure.
807 Cudd_Ref(cube
= DD_ONE(mgr
));
808 for (i
= 0; i
< array_n(smoothing_vars
); i
++) {
809 variable
= array_fetch(bdd_t
*,smoothing_vars
,i
);
811 /* Make sure the variable belongs to the same manager. */
812 assert(mgr
== variable
->mgr
);
814 tmpDd
= Cudd_bddAnd(mgr
,cube
,variable
->node
);
816 Cudd_RecursiveDeref(mgr
, cube
);
820 Cudd_RecursiveDeref(mgr
, cube
);
824 /* Perform the smoothing */
825 result
= Cudd_bddExistAbstract(mgr
,f
->node
,cube
);
826 if (result
== NULL
) {
827 Cudd_RecursiveDeref(mgr
, cube
);
832 /* Get rid of temporary results */
833 Cudd_RecursiveDeref(mgr
, cube
);
835 /* Build the bdd_t structure for the result */
836 return(bdd_construct_bdd_t(mgr
,result
));
838 } /* end of bdd_smooth */
841 /**Function********************************************************************
843 Synopsis [Permutes the variables.]
847 ******************************************************************************/
849 bdd_substitute(f
, old_array
, new_array
)
851 array_t
*old_array
; /* of bdd_t *'s */
852 array_t
*new_array
; /* of bdd_t *'s */
855 int i
,varIndex
,from
,to
;
860 /* Make sure both arrays have the same number of elements. */
861 assert(array_n(old_array
) == array_n(new_array
));
863 /* Detect what is the highest index of variable to rename. */
865 for (i
= 0; i
< array_n(old_array
); i
++) {
866 variable
= array_fetch(bdd_t
*, old_array
, i
);
867 /* Make sure the variable belongs to this manager. */
868 assert(f
->mgr
== variable
->mgr
);
870 varIndex
= Cudd_Regular(variable
->node
)->index
;
871 if (varIndex
> maxOld
) {
877 /* Allocate and fill the array with the trivial permutation. */
878 permut
= ALLOC(int, maxOld
);
879 for (i
= 0; i
< maxOld
; i
++) permut
[i
] = i
;
881 /* Modify the permutation by looking at both arrays old and new. */
882 for (i
= 0; i
< array_n(old_array
); i
++) {
883 variable
= array_fetch(bdd_t
*, old_array
, i
);
884 from
= Cudd_Regular(variable
->node
)->index
;
885 variable
= array_fetch(bdd_t
*, new_array
, i
);
886 /* Make sure the variable belongs to this manager. */
887 assert(f
->mgr
== variable
->mgr
);
889 to
= Cudd_Regular(variable
->node
)->index
;
893 result
= Cudd_bddPermute(f
->mgr
,f
->node
,permut
);
895 if (result
== NULL
) return(NULL
);
897 return(bdd_construct_bdd_t(f
->mgr
,result
));
899 } /* end of bdd_substitute */
902 /**Function********************************************************************
904 Synopsis [Returns the Then branch of the BDD.]
908 ******************************************************************************/
915 result
= Cudd_T(f
->node
);
916 result
= Cudd_NotCond(result
,Cudd_IsComplement(f
->node
));
918 return(bdd_construct_bdd_t(f
->mgr
,result
));
920 } /* end of bdd_then */
923 /**Function********************************************************************
925 Synopsis [Returns the else branch of a BDD.]
929 ******************************************************************************/
936 result
= Cudd_E(f
->node
);
937 result
= Cudd_NotCond(result
,Cudd_IsComplement(f
->node
));
939 return(bdd_construct_bdd_t(f
->mgr
,result
));
941 } /* end of bdd_else */
944 /**Function********************************************************************
946 Synopsis [Returns the BDD of the top variable.]
948 Description [Returns the BDD of the top variable of the argument. If
949 the argument is constant, it returns the constant function itself.]
953 ******************************************************************************/
960 if (Cudd_IsConstant(f
->node
)) {
963 result
= f
->mgr
->vars
[Cudd_Regular(f
->node
)->index
];
966 return(bdd_construct_bdd_t(f
->mgr
,result
));
968 } /* end of bdd_top_var */
971 /**Function********************************************************************
973 Synopsis [Computes the exclusive nor of two BDDs.]
977 ******************************************************************************/
985 /* Make sure both operands belong to the same manager. */
986 assert(f
->mgr
== g
->mgr
);
988 result
= Cudd_bddIte(f
->mgr
,f
->node
,g
->node
,Cudd_Not(g
->node
));
989 if (result
== NULL
) return(NULL
);
991 return(bdd_construct_bdd_t(f
->mgr
,result
));
993 } /* end of bdd_xnor */
996 /**Function********************************************************************
998 Synopsis [Computes the exclusive or of two BDDs.]
1002 ******************************************************************************/
1010 /* Make sure both operands belong to the same manager. */
1011 assert(f
->mgr
== g
->mgr
);
1013 result
= Cudd_bddIte(f
->mgr
,f
->node
,Cudd_Not(g
->node
),g
->node
);
1014 if (result
== NULL
) return(NULL
);
1016 return(bdd_construct_bdd_t(f
->mgr
,result
));
1018 } /* end of bdd_xor */
1021 /**Function********************************************************************
1023 Synopsis [Returns the constant zero BDD.]
1027 ******************************************************************************/
1034 Cudd_Ref(result
= Cudd_Not(DD_ONE((mgr
))));
1035 return(bdd_construct_bdd_t(mgr
,result
));
1037 } /* end of bdd_zero */
1040 /**Function********************************************************************
1042 Synopsis [Equality check.]
1046 ******************************************************************************/
1052 return(f
->node
== g
->node
);
1054 } /* end of bdd_equal */
1057 /**Function********************************************************************
1059 Synopsis [Returns a BDD included in the intersection of f and g.]
1063 ******************************************************************************/
1065 bdd_intersects(f
, g
)
1071 /* Make sure both operands belong to the same manager. */
1072 assert(f
->mgr
== g
->mgr
);
1074 result
= Cudd_bddIntersect(f
->mgr
,f
->node
,g
->node
);
1075 if (result
== NULL
) return(NULL
);
1077 return(bdd_construct_bdd_t(f
->mgr
,result
));
1079 } /* end of bdd_intersects */
1082 /**Function********************************************************************
1084 Synopsis [Checks a BDD for tautology.]
1088 ******************************************************************************/
1090 bdd_is_tautology(f
, phase
)
1095 return(f
->node
== DD_ONE(f
->mgr
));
1097 return(f
->node
== Cudd_Not(DD_ONE(f
->mgr
)));
1100 } /* end of bdd_is_tautology */
1103 /**Function********************************************************************
1105 Synopsis [Tests for containment of f in g.]
1109 ******************************************************************************/
1111 bdd_leq(f
, g
, f_phase
, g_phase
)
1117 DdNode
*newf
, *newg
;
1119 /* Make sure both operands belong to the same manager. */
1120 assert(f
->mgr
== g
->mgr
);
1125 newf
= Cudd_Not(f
->node
);
1130 newg
= Cudd_Not(g
->node
);
1133 return(Cudd_bddLeq(f
->mgr
,newf
,newg
));
1135 } /* end of bdd_leq */
1138 /**Function********************************************************************
1140 Synopsis [Counts the number of minterms in the on set.]
1144 ******************************************************************************/
1146 bdd_count_onset(f
, var_array
)
1148 array_t
*var_array
; /* of bdd_t *'s */
1150 return(Cudd_CountMinterm(f
->mgr
,f
->node
,array_n(var_array
)));
1152 } /* end of bdd_count_onset */
1155 /**Function********************************************************************
1157 Synopsis [Obtains the manager of the BDD.]
1161 ******************************************************************************/
1168 } /* end of bdd_get_manager */
1171 /**Function********************************************************************
1173 Synopsis [Returns the node of the BDD.]
1175 SideEffects [Sets is_complemented.]
1177 ******************************************************************************/
1179 bdd_get_node(f
, is_complemented
)
1181 boolean
*is_complemented
; /* return */
1183 if (Cudd_IsComplement(f
->node
)) {
1184 *is_complemented
= TRUE
;
1185 return(Cudd_Regular(f
->node
));
1187 *is_complemented
= FALSE
;
1190 } /* end of bdd_get_node */
1193 /**Function********************************************************************
1195 Synopsis [Returns the free field of the BDD.]
1199 ******************************************************************************/
1206 } /* end of bdd_get_free */
1209 /**Function********************************************************************
1211 Synopsis [Obtains some statistics of the BDD package.]
1213 SideEffects [Sets stats.]
1215 ******************************************************************************/
1218 bdd_get_stats(mgr
, stats
)
1220 bdd_stats
*stats
; /* return */
1222 stats
->nodes
.total
= mgr
->keys
;
1223 stats
->nodes
.used
= mgr
->keys
- mgr
->dead
;
1224 stats
->nodes
.unused
= mgr
->dead
;
1225 stats
->cache
.itetable
.hits
= (unsigned int) Cudd_ReadCacheHits(mgr
);
1226 stats
->cache
.itetable
.misses
= (unsigned int)
1227 (Cudd_ReadCacheLookUps(mgr
) - Cudd_ReadCacheHits(mgr
));
1228 stats
->cache
.itetable
.collisions
= mgr
->cachecollisions
;
1229 stats
->cache
.itetable
.inserts
= mgr
->cacheinserts
;
1230 stats
->gc
.times
= Cudd_ReadGarbageCollections(mgr
);
1233 } /* end of bdd_get_stats */
1236 /**Function********************************************************************
1238 Synopsis [Obtains the support of the BDD.]
1242 ******************************************************************************/
1247 DdNode
*support
, *scan
;
1250 support
= Cudd_Support(f
->mgr
,f
->node
);
1251 if (support
== NULL
) return(NULL
);
1254 result
= var_set_new((int) f
->mgr
->size
);
1256 while (!cuddIsConstant(scan
)) {
1257 var_set_set_elt(result
, scan
->index
);
1260 Cudd_RecursiveDeref(f
->mgr
,support
);
1264 } /* end of bdd_get_support */
1267 /**Function********************************************************************
1269 Synopsis [Obtains the array of indices of an array of variables.]
1273 ******************************************************************************/
1275 bdd_get_varids(var_array
)
1281 array_t
*result
= array_alloc(int,array_n(var_array
));
1283 for (i
= 0; i
< array_n(var_array
); i
++) {
1284 var
= array_fetch(bdd_t
*, var_array
, i
);
1285 index
= Cudd_Regular(var
->node
)->index
;
1286 (void) array_insert_last(int, result
, index
);
1290 } /* end of bdd_get_varids */
1293 /**Function********************************************************************
1295 Synopsis [Returns the number of variables in the manager.]
1299 ******************************************************************************/
1306 } /* end of bdd_num_vars */
1309 /**Function********************************************************************
1311 Synopsis [Prints the BDD.]
1315 ******************************************************************************/
1320 (void) cuddP(f
->mgr
,f
->node
);
1322 } /* end of bdd_print */
1325 /**Function********************************************************************
1327 Synopsis [Prints statistics about the package.]
1331 ******************************************************************************/
1333 bdd_print_stats(stats
, file
)
1338 fprintf(stderr
,"CU DD package: bdd_print_stats: Statistics turned off. No output\n");
1340 fprintf(file
,"CU DD Package Statistics\n");
1341 fprintf(file
," Cache hits : %d\n",stats
.cache
.itetable
.hits
);
1342 fprintf(file
," Cache misses : %d\n",stats
.cache
.itetable
.misses
);
1343 fprintf(file
," Cache collisions : %d\n",stats
.cache
.itetable
.collisions
);
1344 fprintf(file
," Cache inserts: %d\n",stats
.cache
.itetable
.inserts
);
1348 } /* end of bdd_print_stats */
1351 /**Function********************************************************************
1353 Synopsis [Computes the number of nodes of a BDD.]
1357 ******************************************************************************/
1362 return(Cudd_DagSize(f
->node
));
1364 } /* end of bdd_size */
1367 /**Function********************************************************************
1369 Synopsis [Accesses the id of the top variable.]
1373 ******************************************************************************/
1378 return(Cudd_Regular(f
->node
)->index
);
1380 } /* end of bdd_top_var_id */
1383 /**Function********************************************************************
1385 Synopsis [Accesses the external_hooks field of the manager.]
1389 ******************************************************************************/
1390 bdd_external_hooks
*
1391 bdd_get_external_hooks(mgr
)
1394 return((bdd_external_hooks
*)(mgr
->hooks
));
1396 } /* end of bdd_get_external_hooks */
1399 /**Function********************************************************************
1401 Synopsis [Registers a new hook with the manager.]
1405 ******************************************************************************/
1408 bdd_register_daemon(mgr
, daemon
)
1412 fprintf(stderr
,"CU DD Package: bdd_register_daemon translated to no-op.\n");
1415 } /* end of bdd_register_daemon */
1418 /**Function********************************************************************
1420 Synopsis [Turns on or off garbage collection.]
1424 ******************************************************************************/
1426 bdd_set_gc_mode(mgr
, no_gc
)
1431 Cudd_DisableGarbageCollection(mgr
);
1433 Cudd_EnableGarbageCollection(mgr
);
1437 } /* end of bdd_set_gc_mode */
1440 /**Function********************************************************************
1442 Synopsis [Reorders the BDD pool.]
1446 ******************************************************************************/
1448 bdd_dynamic_reordering(mgr
, algorithm_type
)
1450 bdd_reorder_type_t algorithm_type
;
1452 switch (algorithm_type
) {
1453 case BDD_REORDER_SIFT
:
1454 mgr
->autoMethod
= CUDD_REORDER_SIFT
;
1457 case BDD_REORDER_WINDOW
:
1458 case BDD_REORDER_WINDOW4
:
1459 mgr
->autoMethod
= CUDD_REORDER_WINDOW4
;
1462 case BDD_REORDER_NONE
:
1465 case BDD_REORDER_SAME
:
1468 case BDD_REORDER_RANDOM
:
1469 mgr
->autoMethod
= CUDD_REORDER_RANDOM
;
1472 case BDD_REORDER_RANDOM_PIVOT
:
1473 mgr
->autoMethod
= CUDD_REORDER_RANDOM_PIVOT
;
1476 case BDD_REORDER_SIFT_CONVERGE
:
1477 mgr
->autoMethod
= CUDD_REORDER_SIFT_CONVERGE
;
1480 case BDD_REORDER_SYMM_SIFT
:
1481 mgr
->autoMethod
= CUDD_REORDER_SYMM_SIFT
;
1484 case BDD_REORDER_SYMM_SIFT_CONV
:
1485 mgr
->autoMethod
= CUDD_REORDER_SYMM_SIFT_CONV
;
1488 case BDD_REORDER_WINDOW2
:
1489 mgr
->autoMethod
= CUDD_REORDER_WINDOW2
;
1492 case BDD_REORDER_WINDOW3
:
1493 mgr
->autoMethod
= CUDD_REORDER_WINDOW3
;
1496 case BDD_REORDER_WINDOW2_CONV
:
1497 mgr
->autoMethod
= CUDD_REORDER_WINDOW2_CONV
;
1500 case BDD_REORDER_WINDOW3_CONV
:
1501 mgr
->autoMethod
= CUDD_REORDER_WINDOW3_CONV
;
1504 case BDD_REORDER_WINDOW4_CONV
:
1505 mgr
->autoMethod
= CUDD_REORDER_WINDOW4_CONV
;
1508 case BDD_REORDER_GROUP_SIFT
:
1509 mgr
->autoMethod
= CUDD_REORDER_GROUP_SIFT
;
1512 case BDD_REORDER_GROUP_SIFT_CONV
:
1513 mgr
->autoMethod
= CUDD_REORDER_GROUP_SIFT_CONV
;
1516 case BDD_REORDER_ANNEALING
:
1517 mgr
->autoMethod
= CUDD_REORDER_ANNEALING
;
1520 case BDD_REORDER_GENETIC
:
1521 mgr
->autoMethod
= CUDD_REORDER_GENETIC
;
1525 fprintf(stderr
,"CU DD Package: Reordering algorithm not considered\n");
1528 } /* end of bdd_dynamic_reordering */
1531 /**Function********************************************************************
1533 Synopsis [Calls reordering explicitly.]
1537 ******************************************************************************/
1542 (void) Cudd_ReduceHeap(mgr
,mgr
->autoMethod
,10); /* 10 = whatever (Verbatim from file ddTable.c) */
1545 } /* end of bdd_reorder */
1548 /**Function********************************************************************
1550 Synopsis [Read the number of reorderings the package has performed
1555 ******************************************************************************/
1557 bdd_read_reorderings(mgr
)
1560 return Cudd_ReadReorderings((DdManager
*)mgr
);
1562 } /* end of bdd_read_reorderings */
1565 /**Function********************************************************************
1567 Synopsis [Gets the id variable for one level in the BDD.]
1571 ******************************************************************************/
1573 bdd_get_id_from_level(mgr
, level
)
1577 return(mgr
->invperm
[level
]);
1579 } /* end of bdd_get_id_from_level */
1582 /**Function********************************************************************
1584 Synopsis [Gets the level of the top variable of the BDD.]
1588 ******************************************************************************/
1590 bdd_top_var_level(mgr
, fn
)
1594 return((long) cuddI(mgr
,Cudd_Regular(fn
->node
)->index
));
1596 } /* end of bdd_top_var_level */
1599 /**Function********************************************************************
1601 Synopsis [Returns TRUE if the argument BDD is a cube; FALSE
1606 ******************************************************************************/
1611 struct DdManager
*manager
;
1614 fail("bdd_is_cube: invalid BDD");
1616 if (f
->free
) fail ("Freed BDD passed to bdd_is_cube");
1617 manager
= (DdManager
*) f
->mgr
;
1618 return((boolean
)cuddCheckCube(manager
,f
->node
));
1620 } /* end of bdd_is_cube */
1623 /**Function********************************************************************
1625 Synopsis [Calls the garbage collector explicitly.]
1629 ******************************************************************************/
1634 cuddGarbageCollect(mgr
,1);
1636 } /* end of bdd_gc */
1639 /**Function********************************************************************
1641 Synopsis [Computes the shared size of an array of BDDs.]
1643 Description [Computes the shared size of an array of BDDs. Returns
1644 CUDD_OUT_OF_MEM in case of failure.]
1648 ******************************************************************************/
1650 bdd_size_multiple(bddArray
)
1658 nodeArray
= ALLOC(DdNode
*, array_n(bddArray
));
1659 if (nodeArray
== NULL
) return(CUDD_OUT_OF_MEM
);
1660 for (i
= 0; i
< array_n(bddArray
); i
++) {
1661 bddUnit
= array_fetch(bdd_t
*, bddArray
, i
);
1662 nodeArray
[i
] = bddUnit
->node
;
1665 result
= Cudd_SharingSize(nodeArray
,array_n(bddArray
));
1672 } /* end of bdd_size_multiple */
1675 /**Function********************************************************************
1677 Synopsis [Returns the first cube of the function.
1678 A generator is also returned, which will iterate over the rest.]
1680 Description [Defines an iterator on the onset of a BDD. Two routines
1681 are provided: bdd_first_cube, which extracts one cube from a BDD and
1682 returns a bdd_gen structure containing the information necessary to
1683 continue the enumeration; and bdd_next_cube, which returns 1 if
1684 another cube was found, and 0 otherwise. A cube is represented as an
1685 array of bdd_literal (which are integers in {0, 1, 2}), where 0
1686 represents negated literal, 1 for literal, and 2 for don't care.
1687 Returns a disjoint cover. A third routine is there to clean up.]
1691 SeeAlso [bdd_next_cube bdd_gen_free]
1693 ******************************************************************************/
1695 bdd_first_cube(fn
, cube
)
1697 array_t
**cube
; /* of bdd_literal */
1699 bdd_manager
*manager
;
1703 CUDD_VALUE_TYPE value
;
1705 /* Make sure we receive a valid bdd_t. (So to speak.) */
1710 /* Initialize the generator. */
1711 gen
= ALLOC(bdd_gen
,1);
1712 if (gen
== NULL
) return(NULL
);
1713 gen
->manager
= manager
;
1715 gen
->cube
= array_alloc(bdd_literal
, manager
->size
);
1716 if (gen
->cube
== NULL
) {
1717 fail("Bdd Package: Out of memory in bdd_first_cube");
1720 gen
->ddGen
= Cudd_FirstCube(manager
,fn
->node
,&icube
,&value
);
1721 if (gen
->ddGen
== NULL
) {
1722 fail("Cudd Package: Out of memory in bdd_first_cube");
1725 if (!Cudd_IsGenEmpty(gen
->ddGen
)) {
1726 /* Copy icube to the array_t cube. */
1727 for (i
= 0; i
< manager
->size
; i
++) {
1728 int myconst
= icube
[i
];
1729 array_insert(bdd_literal
, gen
->cube
, i
, myconst
);
1736 } /* end of bdd_first_cube */
1739 /**Function********************************************************************
1741 Synopsis [Gets the next cube on the generator. Returns {TRUE,
1742 FALSE} when {more, no more}.]
1746 SeeAlso [bdd_first_cube bdd_gen_free]
1748 ******************************************************************************/
1750 bdd_next_cube(gen
, cube
)
1752 array_t
**cube
; /* of bdd_literal */
1756 CUDD_VALUE_TYPE value
;
1759 retval
= Cudd_NextCube(gen
->ddGen
,&icube
,&value
);
1760 if (!Cudd_IsGenEmpty(gen
->ddGen
)) {
1761 /* Copy icube to the array_t cube. */
1762 for (i
= 0; i
< gen
->manager
->size
; i
++) {
1763 int myconst
= icube
[i
];
1764 array_insert(bdd_literal
, gen
->cube
, i
, myconst
);
1771 } /* end of bdd_next_cube */
1774 /**Function********************************************************************
1776 Synopsis [Gets the first node in the BDD and returns a generator.]
1780 SeeAlso [bdd_next_node]
1782 ******************************************************************************/
1784 bdd_first_node(fn
, node
)
1786 bdd_node
**node
; /* return */
1788 bdd_manager
*manager
;
1791 /* Make sure we receive a valid bdd_t. (So to speak.) */
1796 /* Initialize the generator. */
1797 gen
= ALLOC(bdd_gen
,1);
1798 if (gen
== NULL
) return(NULL
);
1799 gen
->manager
= manager
;
1802 gen
->ddGen
= Cudd_FirstNode(manager
,fn
->node
,node
);
1803 if (gen
->ddGen
== NULL
) {
1804 fail("Cudd Package: Out of memory in bdd_first_node");
1809 } /* end of bdd_first_node */
1812 /**Function********************************************************************
1814 Synopsis [Gets the next node in the BDD. Returns {TRUE, FALSE} when
1819 SeeAlso [bdd_first_node]
1821 ******************************************************************************/
1823 bdd_next_node(gen
, node
)
1825 bdd_node
**node
; /* return */
1827 return(Cudd_NextNode(gen
->ddGen
,node
));
1829 } /* end of bdd_next_node */
1832 /**Function********************************************************************
1834 Synopsis [Frees up the space used by the generator. Returns an int
1835 so that it is easier to fit in a foreach macro. Returns 0 (to make it
1836 easy to put in expressions).]
1842 ******************************************************************************/
1847 if (gen
->cube
!= NULL
) array_free(gen
->cube
);
1848 Cudd_GenFree(gen
->ddGen
);
1852 } /* end of bdd_gen_free */
1855 /**Function********************************************************************
1857 Synopsis [Queries the status of a generator.]
1859 Description [Queries the status of a generator. Returns 1 if the
1860 generator is empty or NULL; 0 otherswise.]
1864 SeeAlso [bdd_first_cube bdd_next_cube bdd_first_node bdd_next_node
1867 ******************************************************************************/
1869 bdd_is_gen_empty(gen
)
1872 return(Cudd_IsGenEmpty(gen
->ddGen
));
1874 } /* end of bdd_is_gen_empty */
1877 /**Function********************************************************************
1879 Synopsis [Function that creates a variable of a given index.]
1883 ******************************************************************************/
1885 bdd_var_with_index(manager
, index
)
1886 bdd_manager
*manager
;
1891 var
= Cudd_bddIthVar(manager
, index
);
1893 return(bdd_construct_bdd_t(manager
, var
));
1895 } /* end of bdd_var_with_index */
1898 /**Function********************************************************************
1900 Synopsis [Temporary function that is empty.]
1904 ******************************************************************************/
1907 bdd_new_var_block(f
, n
)
1913 } /* end of bdd_new_var_block */
1916 /*---------------------------------------------------------------------------*/
1917 /* Definition of internal functions */
1918 /*---------------------------------------------------------------------------*/
1921 /*---------------------------------------------------------------------------*/
1922 /* Definition of static functions */
1923 /*---------------------------------------------------------------------------*/
1926 /**Function********************************************************************
1928 Synopsis [Builds the bdd_t structure.]
1930 Description [Builds the bdd_t structure from manager and node.
1931 Assumes that the reference count of the node has already been
1936 ******************************************************************************/
1938 bdd_construct_bdd_t(mgr
,fn
)
1944 result
= ALLOC(bdd_t
, 1);
1945 if (result
== NULL
) {
1946 Cudd_RecursiveDeref(mgr
,fn
);
1951 result
->free
= FALSE
;
1954 } /* end of bdd_construct_bdd_t */