glu-2.2: src/cuBdd/cuddInit.c Source File

00001 
00059 #include "util.h"
00060 #include "cuddInt.h"
00061 
00062 /*---------------------------------------------------------------------------*/
00063 /* Constant declarations                                                     */
00064 /*---------------------------------------------------------------------------*/
00065 
00066 
00067 /*---------------------------------------------------------------------------*/
00068 /* Stucture declarations                                                     */
00069 /*---------------------------------------------------------------------------*/
00070 
00071 
00072 /*---------------------------------------------------------------------------*/
00073 /* Type declarations                                                         */
00074 /*---------------------------------------------------------------------------*/
00075 
00076 
00077 /*---------------------------------------------------------------------------*/
00078 /* Variable declarations                                                     */
00079 /*---------------------------------------------------------------------------*/
00080 
00081 #ifndef lint
00082 static char rcsid[] DD_UNUSED = "$Id: cuddInit.c,v 1.33 2007/07/01 05:10:50 fabio Exp $";
00083 #endif
00084 
00085 /*---------------------------------------------------------------------------*/
00086 /* Macro declarations                                                        */
00087 /*---------------------------------------------------------------------------*/
00088 
00089 
00092 /*---------------------------------------------------------------------------*/
00093 /* Static function prototypes                                                */
00094 /*---------------------------------------------------------------------------*/
00095 
00096 
00100 /*---------------------------------------------------------------------------*/
00101 /* Definition of exported functions                                          */
00102 /*---------------------------------------------------------------------------*/
00103 
00120 DdManager *
00121 Cudd_Init(
00122   unsigned int numVars /* initial number of BDD variables (i.e., subtables) */,
00123   unsigned int numVarsZ /* initial number of ZDD variables (i.e., subtables) */,
00124   unsigned int numSlots /* initial size of the unique tables */,
00125   unsigned int cacheSize /* initial size of the cache */,
00126   unsigned long maxMemory /* target maximum memory occupation */)
00127 {
00128     DdManager *unique;
00129     int i,result;
00130     DdNode *one, *zero;
00131     unsigned int maxCacheSize;
00132     unsigned int looseUpTo;
00133     extern DD_OOMFP MMoutOfMemory;
00134     DD_OOMFP saveHandler;
00135 
00136     if (maxMemory == 0) {
00137         maxMemory = getSoftDataLimit();
00138     }
00139     looseUpTo = (unsigned int) ((maxMemory / sizeof(DdNode)) /
00140                                 DD_MAX_LOOSE_FRACTION);
00141     unique = cuddInitTable(numVars,numVarsZ,numSlots,looseUpTo);
00142     if (unique == NULL) return(NULL);
00143     unique->maxmem = (unsigned long) maxMemory / 10 * 9;
00144     maxCacheSize = (unsigned int) ((maxMemory / sizeof(DdCache)) /
00145                                    DD_MAX_CACHE_FRACTION);
00146     result = cuddInitCache(unique,cacheSize,maxCacheSize);
00147     if (result == 0) return(NULL);
00148 
00149     saveHandler = MMoutOfMemory;
00150     MMoutOfMemory = Cudd_OutOfMem;
00151     unique->stash = ALLOC(char,(maxMemory / DD_STASH_FRACTION) + 4);
00152     MMoutOfMemory = saveHandler;
00153     if (unique->stash == NULL) {
00154         (void) fprintf(unique->err,"Unable to set aside memory\n");
00155     }
00156 
00157     /* Initialize constants. */
00158     unique->one = cuddUniqueConst(unique,1.0);
00159     if (unique->one == NULL) return(0);
00160     cuddRef(unique->one);
00161     unique->zero = cuddUniqueConst(unique,0.0);
00162     if (unique->zero == NULL) return(0);
00163     cuddRef(unique->zero);
00164 #ifdef HAVE_IEEE_754
00165     if (DD_PLUS_INF_VAL != DD_PLUS_INF_VAL * 3 ||
00166         DD_PLUS_INF_VAL != DD_PLUS_INF_VAL / 3) {
00167         (void) fprintf(unique->err,"Warning: Crippled infinite values\n");
00168         (void) fprintf(unique->err,"Recompile without -DHAVE_IEEE_754\n");
00169     }
00170 #endif
00171     unique->plusinfinity = cuddUniqueConst(unique,DD_PLUS_INF_VAL);
00172     if (unique->plusinfinity == NULL) return(0);
00173     cuddRef(unique->plusinfinity);
00174     unique->minusinfinity = cuddUniqueConst(unique,DD_MINUS_INF_VAL);
00175     if (unique->minusinfinity == NULL) return(0);
00176     cuddRef(unique->minusinfinity);
00177     unique->background = unique->zero;
00178 
00179     /* The logical zero is different from the CUDD_VALUE_TYPE zero! */
00180     one = unique->one;
00181     zero = Cudd_Not(one);
00182     /* Create the projection functions. */
00183     unique->vars = ALLOC(DdNodePtr,unique->maxSize);
00184     if (unique->vars == NULL) {
00185         unique->errorCode = CUDD_MEMORY_OUT;
00186         return(NULL);
00187     }
00188     for (i = 0; i < unique->size; i++) {
00189         unique->vars[i] = cuddUniqueInter(unique,i,one,zero);
00190         if (unique->vars[i] == NULL) return(0);
00191         cuddRef(unique->vars[i]);
00192     }
00193 
00194     if (unique->sizeZ)
00195         cuddZddInitUniv(unique);
00196 
00197     unique->memused += sizeof(DdNode *) * unique->maxSize;
00198 
00199     return(unique);
00200 
00201 } /* end of Cudd_Init */
00202 
00203 
00217 void
00218 Cudd_Quit(
00219   DdManager * unique)
00220 {
00221     if (unique->stash != NULL) FREE(unique->stash);
00222     cuddFreeTable(unique);
00223 
00224 } /* end of Cudd_Quit */
00225 
00226 
00227 /*---------------------------------------------------------------------------*/
00228 /* Definition of internal functions                                          */
00229 /*---------------------------------------------------------------------------*/
00230 
00231 
00244 int
00245 cuddZddInitUniv(
00246   DdManager * zdd)
00247 {
00248     DdNode      *p, *res;
00249     int         i;
00250 
00251     zdd->univ = ALLOC(DdNodePtr, zdd->sizeZ);
00252     if (zdd->univ == NULL) {
00253         zdd->errorCode = CUDD_MEMORY_OUT;
00254         return(0);
00255     }
00256 
00257     res = DD_ONE(zdd);
00258     cuddRef(res);
00259     for (i = zdd->sizeZ - 1; i >= 0; i--) {
00260         unsigned int index = zdd->invpermZ[i];
00261         p = res;
00262         res = cuddUniqueInterZdd(zdd, index, p, p);
00263         if (res == NULL) {
00264             Cudd_RecursiveDerefZdd(zdd,p);
00265             FREE(zdd->univ);
00266             return(0);
00267         }
00268         cuddRef(res);
00269         cuddDeref(p);
00270         zdd->univ[i] = res;
00271     }
00272 
00273 #ifdef DD_VERBOSE
00274     cuddZddP(zdd, zdd->univ[0]);
00275 #endif
00276 
00277     return(1);
00278 
00279 } /* end of cuddZddInitUniv */
00280 
00281 
00293 void
00294 cuddZddFreeUniv(
00295   DdManager * zdd)
00296 {
00297     if (zdd->univ) {
00298         Cudd_RecursiveDerefZdd(zdd, zdd->univ[0]);
00299         FREE(zdd->univ);
00300     }
00301 
00302 } /* end of cuddZddFreeUniv */
00303 
00304 
00305 /*---------------------------------------------------------------------------*/
00306 /* Definition of static functions                                            */
00307 /*---------------------------------------------------------------------------*/
00308