source: vis_dev/glu-2.3/src/cuBdd/cuddInit.c@ 25

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

library glu 2.3
File size: 9.9 KB
RevLine 
[13]1/**CFile***********************************************************************
2
3 FileName [cuddInit.c]
4
5 PackageName [cudd]
6
7 Synopsis [Functions to initialize and shut down the DD manager.]
8
9 Description [External procedures included in this module:
10 <ul>
11 <li> Cudd_Init()
12 <li> Cudd_Quit()
13 </ul>
14 Internal procedures included in this module:
15 <ul>
16 <li> cuddZddInitUniv()
17 <li> cuddZddFreeUniv()
18 </ul>
19 ]
20
21 SeeAlso []
22
23 Author [Fabio Somenzi]
24
25 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
26
27 All rights reserved.
28
29 Redistribution and use in source and binary forms, with or without
30 modification, are permitted provided that the following conditions
31 are met:
32
33 Redistributions of source code must retain the above copyright
34 notice, this list of conditions and the following disclaimer.
35
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.
39
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.
43
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.]
56
57******************************************************************************/
58
59#include "util.h"
60#include "cuddInt.h"
61
62/*---------------------------------------------------------------------------*/
63/* Constant declarations */
64/*---------------------------------------------------------------------------*/
65
66
67/*---------------------------------------------------------------------------*/
68/* Stucture declarations */
69/*---------------------------------------------------------------------------*/
70
71
72/*---------------------------------------------------------------------------*/
73/* Type declarations */
74/*---------------------------------------------------------------------------*/
75
76
77/*---------------------------------------------------------------------------*/
78/* Variable declarations */
79/*---------------------------------------------------------------------------*/
80
81#ifndef lint
82static char rcsid[] DD_UNUSED = "$Id: cuddInit.c,v 1.33 2007/07/01 05:10:50 fabio Exp $";
83#endif
84
85/*---------------------------------------------------------------------------*/
86/* Macro declarations */
87/*---------------------------------------------------------------------------*/
88
89
90/**AutomaticStart*************************************************************/
91
92/*---------------------------------------------------------------------------*/
93/* Static function prototypes */
94/*---------------------------------------------------------------------------*/
95
96
97/**AutomaticEnd***************************************************************/
98
99
100/*---------------------------------------------------------------------------*/
101/* Definition of exported functions */
102/*---------------------------------------------------------------------------*/
103
104/**Function********************************************************************
105
106 Synopsis [Creates a new DD manager.]
107
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
113 otherwise.]
114
115 SideEffects [None]
116
117 SeeAlso [Cudd_Quit]
118
119******************************************************************************/
120DdManager *
121Cudd_Init(
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 */)
127{
128 DdManager *unique;
129 int i,result;
130 DdNode *one, *zero;
131 unsigned int maxCacheSize;
132 unsigned int looseUpTo;
133 extern DD_OOMFP MMoutOfMemory;
134 DD_OOMFP saveHandler;
135
136 if (maxMemory == 0) {
137 maxMemory = getSoftDataLimit();
138 }
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);
148
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");
155 }
156
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);
164#ifdef HAVE_IEEE_754
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");
169 }
170#endif
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;
178
179 /* The logical zero is different from the CUDD_VALUE_TYPE zero! */
180 one = unique->one;
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;
186 return(NULL);
187 }
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]);
192 }
193
194 if (unique->sizeZ)
195 cuddZddInitUniv(unique);
196
197 unique->memused += sizeof(DdNode *) * unique->maxSize;
198
199 return(unique);
200
201} /* end of Cudd_Init */
202
203
204/**Function********************************************************************
205
206 Synopsis [Deletes resources associated with a DD manager.]
207
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.)]
211
212 SideEffects [None]
213
214 SeeAlso [Cudd_Init]
215
216******************************************************************************/
217void
218Cudd_Quit(
219 DdManager * unique)
220{
221 if (unique->stash != NULL) FREE(unique->stash);
222 cuddFreeTable(unique);
223
224} /* end of Cudd_Quit */
225
226
227/*---------------------------------------------------------------------------*/
228/* Definition of internal functions */
229/*---------------------------------------------------------------------------*/
230
231
232/**Function********************************************************************
233
234 Synopsis [Initializes the ZDD universe.]
235
236 Description [Initializes the ZDD universe. Returns 1 if successful; 0
237 otherwise.]
238
239 SideEffects [None]
240
241 SeeAlso [cuddZddFreeUniv]
242
243******************************************************************************/
244int
245cuddZddInitUniv(
246 DdManager * zdd)
247{
248 DdNode *p, *res;
249 int i;
250
251 zdd->univ = ALLOC(DdNodePtr, zdd->sizeZ);
252 if (zdd->univ == NULL) {
253 zdd->errorCode = CUDD_MEMORY_OUT;
254 return(0);
255 }
256
257 res = DD_ONE(zdd);
258 cuddRef(res);
259 for (i = zdd->sizeZ - 1; i >= 0; i--) {
260 unsigned int index = zdd->invpermZ[i];
261 p = res;
262 res = cuddUniqueInterZdd(zdd, index, p, p);
263 if (res == NULL) {
264 Cudd_RecursiveDerefZdd(zdd,p);
265 FREE(zdd->univ);
266 return(0);
267 }
268 cuddRef(res);
269 cuddDeref(p);
270 zdd->univ[i] = res;
271 }
272
273#ifdef DD_VERBOSE
274 cuddZddP(zdd, zdd->univ[0]);
275#endif
276
277 return(1);
278
279} /* end of cuddZddInitUniv */
280
281
282/**Function********************************************************************
283
284 Synopsis [Frees the ZDD universe.]
285
286 Description [Frees the ZDD universe.]
287
288 SideEffects [None]
289
290 SeeAlso [cuddZddInitUniv]
291
292******************************************************************************/
293void
294cuddZddFreeUniv(
295 DdManager * zdd)
296{
297 if (zdd->univ) {
298 Cudd_RecursiveDerefZdd(zdd, zdd->univ[0]);
299 FREE(zdd->univ);
300 }
301
302} /* end of cuddZddFreeUniv */
303
304
305/*---------------------------------------------------------------------------*/
306/* Definition of static functions */
307/*---------------------------------------------------------------------------*/
308
Note: See TracBrowser for help on using the repository browser.