1 /**CFile***********************************************************************
7 Synopsis [Functions to initialize and shut down the DD manager.]
9 Description [External procedures included in this module:
14 Internal procedures included in this module:
16 <li> cuddZddInitUniv()
17 <li> cuddZddFreeUniv()
23 Author [Fabio Somenzi]
25 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
29 Redistribution and use in source and binary forms, with or without
30 modification, are permitted provided that the following conditions
33 Redistributions of source code must retain the above copyright
34 notice, this list of conditions and the following disclaimer.
36 Redistributions in binary form must reproduce the above copyright
37 notice, this list of conditions and the following disclaimer in the
38 documentation and/or other materials provided with the distribution.
40 Neither the name of the University of Colorado nor the names of its
41 contributors may be used to endorse or promote products derived from
42 this software without specific prior written permission.
44 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
45 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
46 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
47 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
48 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
49 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
50 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
51 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
52 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
53 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
54 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
55 POSSIBILITY OF SUCH DAMAGE.]
57 ******************************************************************************/
62 /*---------------------------------------------------------------------------*/
63 /* Constant declarations */
64 /*---------------------------------------------------------------------------*/
67 /*---------------------------------------------------------------------------*/
68 /* Stucture declarations */
69 /*---------------------------------------------------------------------------*/
72 /*---------------------------------------------------------------------------*/
73 /* Type declarations */
74 /*---------------------------------------------------------------------------*/
77 /*---------------------------------------------------------------------------*/
78 /* Variable declarations */
79 /*---------------------------------------------------------------------------*/
82 static char rcsid
[] DD_UNUSED
= "$Id: cuddInit.c,v 1.33 2007/07/01 05:10:50 fabio Exp $";
85 /*---------------------------------------------------------------------------*/
86 /* Macro declarations */
87 /*---------------------------------------------------------------------------*/
90 /**AutomaticStart*************************************************************/
92 /*---------------------------------------------------------------------------*/
93 /* Static function prototypes */
94 /*---------------------------------------------------------------------------*/
97 /**AutomaticEnd***************************************************************/
100 /*---------------------------------------------------------------------------*/
101 /* Definition of exported functions */
102 /*---------------------------------------------------------------------------*/
104 /**Function********************************************************************
106 Synopsis [Creates a new DD manager.]
108 Description [Creates a new DD manager, initializes the table, the
109 basic constants and the projection functions. If maxMemory is 0,
110 Cudd_Init decides suitable values for the maximum size of the cache
111 and for the limit for fast unique table growth based on the available
112 memory. Returns a pointer to the manager if successful; NULL
119 ******************************************************************************/
122 unsigned int numVars
/* initial number of BDD variables (i.e., subtables) */,
123 unsigned int numVarsZ
/* initial number of ZDD variables (i.e., subtables) */,
124 unsigned int numSlots
/* initial size of the unique tables */,
125 unsigned int cacheSize
/* initial size of the cache */,
126 unsigned long maxMemory
/* target maximum memory occupation */)
131 unsigned int maxCacheSize
;
132 unsigned int looseUpTo
;
133 extern DD_OOMFP MMoutOfMemory
;
134 DD_OOMFP saveHandler
;
136 if (maxMemory
== 0) {
137 maxMemory
= getSoftDataLimit();
139 looseUpTo
= (unsigned int) ((maxMemory
/ sizeof(DdNode
)) /
140 DD_MAX_LOOSE_FRACTION
);
141 unique
= cuddInitTable(numVars
,numVarsZ
,numSlots
,looseUpTo
);
142 if (unique
== NULL
) return(NULL
);
143 unique
->maxmem
= (unsigned long) maxMemory
/ 10 * 9;
144 maxCacheSize
= (unsigned int) ((maxMemory
/ sizeof(DdCache
)) /
145 DD_MAX_CACHE_FRACTION
);
146 result
= cuddInitCache(unique
,cacheSize
,maxCacheSize
);
147 if (result
== 0) return(NULL
);
149 saveHandler
= MMoutOfMemory
;
150 MMoutOfMemory
= Cudd_OutOfMem
;
151 unique
->stash
= ALLOC(char,(maxMemory
/ DD_STASH_FRACTION
) + 4);
152 MMoutOfMemory
= saveHandler
;
153 if (unique
->stash
== NULL
) {
154 (void) fprintf(unique
->err
,"Unable to set aside memory\n");
157 /* Initialize constants. */
158 unique
->one
= cuddUniqueConst(unique
,1.0);
159 if (unique
->one
== NULL
) return(0);
160 cuddRef(unique
->one
);
161 unique
->zero
= cuddUniqueConst(unique
,0.0);
162 if (unique
->zero
== NULL
) return(0);
163 cuddRef(unique
->zero
);
165 if (DD_PLUS_INF_VAL
!= DD_PLUS_INF_VAL
* 3 ||
166 DD_PLUS_INF_VAL
!= DD_PLUS_INF_VAL
/ 3) {
167 (void) fprintf(unique
->err
,"Warning: Crippled infinite values\n");
168 (void) fprintf(unique
->err
,"Recompile without -DHAVE_IEEE_754\n");
171 unique
->plusinfinity
= cuddUniqueConst(unique
,DD_PLUS_INF_VAL
);
172 if (unique
->plusinfinity
== NULL
) return(0);
173 cuddRef(unique
->plusinfinity
);
174 unique
->minusinfinity
= cuddUniqueConst(unique
,DD_MINUS_INF_VAL
);
175 if (unique
->minusinfinity
== NULL
) return(0);
176 cuddRef(unique
->minusinfinity
);
177 unique
->background
= unique
->zero
;
179 /* The logical zero is different from the CUDD_VALUE_TYPE zero! */
181 zero
= Cudd_Not(one
);
182 /* Create the projection functions. */
183 unique
->vars
= ALLOC(DdNodePtr
,unique
->maxSize
);
184 if (unique
->vars
== NULL
) {
185 unique
->errorCode
= CUDD_MEMORY_OUT
;
188 for (i
= 0; i
< unique
->size
; i
++) {
189 unique
->vars
[i
] = cuddUniqueInter(unique
,i
,one
,zero
);
190 if (unique
->vars
[i
] == NULL
) return(0);
191 cuddRef(unique
->vars
[i
]);
195 cuddZddInitUniv(unique
);
197 unique
->memused
+= sizeof(DdNode
*) * unique
->maxSize
;
201 } /* end of Cudd_Init */
204 /**Function********************************************************************
206 Synopsis [Deletes resources associated with a DD manager.]
208 Description [Deletes resources associated with a DD manager and
209 resets the global statistical counters. (Otherwise, another manaqger
210 subsequently created would inherit the stats of this one.)]
216 ******************************************************************************/
221 if (unique
->stash
!= NULL
) FREE(unique
->stash
);
222 cuddFreeTable(unique
);
224 } /* end of Cudd_Quit */
227 /*---------------------------------------------------------------------------*/
228 /* Definition of internal functions */
229 /*---------------------------------------------------------------------------*/
232 /**Function********************************************************************
234 Synopsis [Initializes the ZDD universe.]
236 Description [Initializes the ZDD universe. Returns 1 if successful; 0
241 SeeAlso [cuddZddFreeUniv]
243 ******************************************************************************/
251 zdd
->univ
= ALLOC(DdNodePtr
, zdd
->sizeZ
);
252 if (zdd
->univ
== NULL
) {
253 zdd
->errorCode
= CUDD_MEMORY_OUT
;
259 for (i
= zdd
->sizeZ
- 1; i
>= 0; i
--) {
260 unsigned int index
= zdd
->invpermZ
[i
];
262 res
= cuddUniqueInterZdd(zdd
, index
, p
, p
);
264 Cudd_RecursiveDerefZdd(zdd
,p
);
274 cuddZddP(zdd
, zdd
->univ
[0]);
279 } /* end of cuddZddInitUniv */
282 /**Function********************************************************************
284 Synopsis [Frees the ZDD universe.]
286 Description [Frees the ZDD universe.]
290 SeeAlso [cuddZddInitUniv]
292 ******************************************************************************/
298 Cudd_RecursiveDerefZdd(zdd
, zdd
->univ
[0]);
302 } /* end of cuddZddFreeUniv */
305 /*---------------------------------------------------------------------------*/
306 /* Definition of static functions */
307 /*---------------------------------------------------------------------------*/