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

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

library glu 2.3
File size: 9.9 KB
Line 
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.