distr/cudd/cuddInit.c

   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
  82 static 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 ******************************************************************************/
 120 DdManager *
 121 Cudd_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 ******************************************************************************/
 217 void
 218 Cudd_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 ******************************************************************************/
 244 int
 245 cuddZddInitUniv(
 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 ******************************************************************************/
 293 void
 294 cuddZddFreeUniv(
 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