src/calBdd/calDump.c File Reference

#include "calInt.h"
Include dependency graph for calDump.c:

Go to the source code of this file.

Defines

#define MAGIC_COOKIE   0x5e02f795l
#define CAL_BDD_IOERROR   100
#define TRUE_ENCODING   0xffffff00l
#define FALSE_ENCODING   0xffffff01l
#define POSVAR_ENCODING   0xffffff02l
#define NEGVAR_ENCODING   0xffffff03l
#define POSNODE_ENCODING   0xffffff04l
#define NEGNODE_ENCODING   0xffffff05l
#define NODELABEL_ENCODING   0xffffff06l
#define CONSTANT_ENCODING   0xffffff07l

Functions

static void Write (Cal_BddManager_t *bddManager, unsigned long n, int bytes, FILE *fp)
static void BddDumpBddStep (Cal_BddManager_t *bddManager, Cal_Bdd_t f, FILE *fp, CalHashTable_t *h, Cal_BddIndex_t *normalizedIndexes, int indexSize, int nodeNumberSize)
static unsigned long Read (int *error, int bytes, FILE *fp)
static Cal_Bdd_t BddUndumpBddStep (Cal_BddManager_t *bddManager, Cal_Bdd_t *vars, FILE *fp, Cal_BddIndex_t numberVars, Cal_Bdd_t *shared, long numberShared, long *sharedSoFar, int indexSize, int nodeNumberSize, int *error)
static int BytesNeeded (long n)
Cal_Bdd Cal_BddUndumpBdd (Cal_BddManager bddManager, Cal_Bdd *userVars, FILE *fp, int *error)
int Cal_BddDumpBdd (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd *userVars, FILE *fp)

Variables

static long indexMask [] = {0xffl, 0xffffl, 0xffffffl}

Define Documentation

#define CAL_BDD_IOERROR   100

Definition at line 47 of file calDump.c.

#define CONSTANT_ENCODING   0xffffff07l

Definition at line 56 of file calDump.c.

#define FALSE_ENCODING   0xffffff01l

Definition at line 50 of file calDump.c.

#define MAGIC_COOKIE   0x5e02f795l

CFile***********************************************************************

FileName [calDump.c]

PackageName [cal]

Synopsis [BDD library dump/undump routines]

Description [ ]

SeeAlso [optional]

Author [Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu) Originally written by David Long. ]

Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved.

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

Revision [

Id
calDump.c,v 1.1.1.3 1998/05/04 00:58:56 hsv Exp

]

Definition at line 46 of file calDump.c.

#define NEGNODE_ENCODING   0xffffff05l

Definition at line 54 of file calDump.c.

#define NEGVAR_ENCODING   0xffffff03l

Definition at line 52 of file calDump.c.

#define NODELABEL_ENCODING   0xffffff06l

Definition at line 55 of file calDump.c.

#define POSNODE_ENCODING   0xffffff04l

Definition at line 53 of file calDump.c.

#define POSVAR_ENCODING   0xffffff02l

Definition at line 51 of file calDump.c.

#define TRUE_ENCODING   0xffffff00l

Definition at line 49 of file calDump.c.

Function Documentation

static void BddDumpBddStep ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  f,
FILE *  fp,
CalHashTable_t *  h,
Cal_BddIndex_t *  normalizedIndexes,
int  indexSize,
int  nodeNumberSize 
) [static]

Function********************************************************************

Synopsis []

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 342 of file calDump.c.

00350 {
00351   int negated;
00352   long *number;
00353   Cal_Bdd_t thenBdd, elseBdd;
00354 
00355   switch(CalBddTypeAux(bddManager, f)){
00356   case CAL_BDD_TYPE_ZERO:
00357     Write(bddManager, FALSE_ENCODING, indexSize+1, fp);
00358     break;
00359   case CAL_BDD_TYPE_ONE:
00360     Write(bddManager, TRUE_ENCODING, indexSize+1, fp);
00361     break;
00362   case CAL_BDD_TYPE_CONSTANT:
00363     Write(bddManager, CONSTANT_ENCODING, indexSize+1, fp);
00364 #ifdef JAGESH
00365     Write(bddManager, (unsigned long)BDD_DATA(f)[0], sizeof(long), fp);
00366     Write(bddManager, (unsigned long)BDD_DATA(f)[1], sizeof(long), fp);
00367 #endif
00368     break;
00369   case CAL_BDD_TYPE_POSVAR:
00370     Write(bddManager, POSVAR_ENCODING, indexSize+1, fp);
00371     Write(bddManager,
00372         (unsigned long)normalizedIndexes[CalBddGetBddIndex(bddManager, f)],
00373         indexSize, fp);
00374     break;
00375   case CAL_BDD_TYPE_NEGVAR:
00376     Write(bddManager, NEGVAR_ENCODING, indexSize+1, fp);
00377     Write(bddManager, 
00378         (unsigned long)normalizedIndexes[CalBddGetBddIndex(bddManager, f)],
00379         indexSize, fp);
00380     break;
00381   case CAL_BDD_TYPE_NONTERMINAL:
00382     CalBddNot(f, f);
00383     if(CalHashTableOneLookup(h, f, (char **)0)){
00384       negated  =  1;
00385     }
00386     else{
00387       CalBddNot(f, f);
00388       negated = 0;
00389     }
00390     CalHashTableOneLookup(h, f, (char **)&number);
00391     if(number && *number < 0){
00392           if(negated)
00393             Write(bddManager, NEGNODE_ENCODING, indexSize+1, fp);
00394           else
00395             Write(bddManager, POSNODE_ENCODING, indexSize+1, fp);
00396           Write(bddManager, (unsigned long)(-*number-1), nodeNumberSize, fp);
00397     }
00398     else{
00399       if(number){
00400               Write(bddManager, NODELABEL_ENCODING, indexSize+1, fp);
00401               *number =  -*number-1;
00402       }
00403       Write(bddManager,
00404           (unsigned long)normalizedIndexes[CalBddGetBddIndex(bddManager, f)],
00405           indexSize, fp);
00406       CalBddGetThenBdd(f, thenBdd);
00407       BddDumpBddStep(bddManager, thenBdd, fp, h, normalizedIndexes,
00408           indexSize, nodeNumberSize);
00409       CalBddGetElseBdd(f, elseBdd);
00410       BddDumpBddStep(bddManager, elseBdd, fp, h, normalizedIndexes,
00411           indexSize, nodeNumberSize);
00412     }
00413     break;
00414   default:
00415     CalBddFatalMessage("BddDumpBddStep: unknown type returned by CalBddType");
00416   }
00417 }

static Cal_Bdd_t BddUndumpBddStep ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t *  vars,
FILE *  fp,
Cal_BddIndex_t  numberVars,
Cal_Bdd_t *  shared,
long  numberShared,
long *  sharedSoFar,
int  indexSize,
int  nodeNumberSize,
int *  error 
) [static]

Function********************************************************************

Synopsis []

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 477 of file calDump.c.

00488 {
00489   long nodeNumber;
00490   long encoding;
00491   Cal_BddIndex_t i;
00492   CalAddress_t value1, value2;
00493   Cal_Bdd_t v;
00494   Cal_Bdd_t temp1, temp2;
00495   Cal_Bdd_t result;
00496 
00497   i = Read(error, indexSize, fp);
00498   if(*error){
00499     return CalBddNull(bddManager);
00500   }
00501   if(i == indexMask[indexSize-1]){
00502     encoding = 0xffffff00l+Read(error, 1, fp);
00503     if(*error){
00504       return CalBddNull(bddManager);
00505     }
00506     switch(encoding){
00507     case TRUE_ENCODING:
00508       return (CalBddOne(bddManager));
00509     case FALSE_ENCODING:
00510       return (CalBddZero(bddManager));
00511     case CONSTANT_ENCODING:
00512       value1 = Read(error, sizeof(long), fp);
00513       value2 = Read(error, sizeof(long), fp);
00514       if(*error){
00515         return CalBddNull(bddManager);
00516       }
00517       *error = CAL_BDD_UNDUMP_OVERFLOW;
00518       return CalBddNull(bddManager);
00519     case POSVAR_ENCODING:
00520     case NEGVAR_ENCODING:
00521       i = Read(error, indexSize, fp);
00522       if(!*error && i >=  numberVars){
00523         *error = CAL_BDD_UNDUMP_FORMAT;
00524       }
00525       if(*error){
00526         return CalBddNull(bddManager);
00527       }
00528       v = vars[i];
00529       if(encoding == POSVAR_ENCODING){
00530         return (v);
00531       }
00532       else{
00533         CalBddNot(v, v);
00534         return (v);
00535       }
00536     case POSNODE_ENCODING:
00537     case NEGNODE_ENCODING:
00538       nodeNumber = Read(error, nodeNumberSize, fp);
00539       if(!*error && (nodeNumber >=  numberShared ||
00540           CalBddIsBddNull(bddManager, shared[nodeNumber]))){
00541         *error = CAL_BDD_UNDUMP_FORMAT;
00542       }
00543       if(*error){
00544         return CalBddNull(bddManager);
00545       }
00546       v = shared[nodeNumber];
00547       v = CalBddIdentity(bddManager, v);
00548       if(encoding == POSNODE_ENCODING){
00549         return (v);
00550       }
00551       else{
00552         CalBddNot(v, v);
00553         return (v);
00554       }
00555     case NODELABEL_ENCODING:
00556       nodeNumber =  *sharedSoFar;
00557       ++*sharedSoFar;
00558       v = BddUndumpBddStep(bddManager, vars, fp, numberVars, shared,
00559           numberShared, sharedSoFar, indexSize, nodeNumberSize, error);
00560       shared[nodeNumber] = v;
00561       v = CalBddIdentity(bddManager, v);
00562       return (v);
00563     default:
00564       *error = CAL_BDD_UNDUMP_FORMAT;
00565       return CalBddNull(bddManager);
00566     }
00567   }
00568   if(i >= numberVars){
00569     *error = CAL_BDD_UNDUMP_FORMAT;
00570     return CalBddNull(bddManager);
00571   }
00572   temp1 = BddUndumpBddStep(bddManager, vars, fp, numberVars, shared,
00573        numberShared, sharedSoFar, indexSize, nodeNumberSize, error);
00574   temp2 = BddUndumpBddStep(bddManager, vars, fp, numberVars, shared,
00575        numberShared, sharedSoFar, indexSize, nodeNumberSize, error);
00576   if(*error){
00577       CalBddFree(temp1);
00578       return CalBddNull(bddManager);
00579   }
00580   result = CalBddITE(bddManager, vars[i], temp1, temp2);
00581   CalBddFree(temp1);
00582   CalBddFree(temp2);
00583   if(CalBddIsBddNull(bddManager, result)){
00584      *error = CAL_BDD_UNDUMP_OVERFLOW;
00585   }
00586   return (result);
00587 }

static int BytesNeeded ( long  n  )  [static]

Function********************************************************************

Synopsis []

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 603 of file calDump.c.

00605 {
00606   if(n <= 0x100l){
00607     return (1);
00608   }
00609   if(n <= 0x10000l){
00610     return (2);
00611   }
00612   if(n <= 0x1000000l){
00613     return (3);
00614   }
00615   return (4);
00616 }

int Cal_BddDumpBdd ( Cal_BddManager  bddManager,
Cal_Bdd  fUserBdd,
Cal_Bdd *  userVars,
FILE *  fp 
)

Function********************************************************************

Synopsis [Write a BDD to a file]

Description [Writes an encoded description of the BDD to the file given by fp. The argument vars should be a null-terminated array of variables that include the support of f . These variables need not be in order of increasing index. The function returns a nonzero value if f was written to the file successfully. ]

SideEffects [required]

SeeAlso [optional]

Definition at line 229 of file calDump.c.

00234 {
00235   long i;
00236   Cal_BddIndex_t *normalizedIndexes;
00237   Cal_BddIndex_t vIndex;
00238   Cal_Bdd_t f;
00239   Cal_BddIndex_t numberVars;
00240   Cal_Bdd *support;
00241   int ok;
00242   CalHashTable_t *h;
00243   int indexSize;
00244   long next;
00245   int nodeNumberSize;
00246 
00247   if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
00248     f = CalBddGetInternalBdd(bddManager, fUserBdd);
00249     for(i = 0; userVars[i]; ++i){
00250       if(Cal_BddType(bddManager, userVars[i]) !=  CAL_BDD_TYPE_POSVAR){
00251         CalBddWarningMessage("Cal_BddDumpBdd: support is not all positive variables");
00252         return (0);
00253       }
00254     }
00255     normalizedIndexes = Cal_MemAlloc(Cal_BddIndex_t, bddManager->numVars);
00256     for(i = 0; i < bddManager->numVars; ++i){
00257       normalizedIndexes[i] = CAL_BDD_CONST_INDEX;
00258     }
00259     for(i = 0; userVars[i]; ++i){
00260       vIndex = Cal_BddGetIfIndex(bddManager, userVars[i]);
00261       if(normalizedIndexes[vIndex] !=  CAL_BDD_CONST_INDEX){
00262         CalBddWarningMessage("Cal_BddDumpBdd: variables duplicated in support");
00263         Cal_MemFree(normalizedIndexes);
00264         return 0;
00265       }
00266       normalizedIndexes[vIndex] = i;
00267     }
00268     numberVars = i;
00269     support = Cal_MemAlloc(Cal_Bdd, bddManager->numVars+1);
00270     Cal_BddSupport(bddManager, fUserBdd, support);
00271     ok = 1;
00272     for(i = 0; ok && support[i]; ++i){
00273       if(normalizedIndexes[Cal_BddGetIfIndex(bddManager, support[i])] == CAL_BDD_CONST_INDEX){
00274         CalBddWarningMessage("Cal_BddDumpBdd: incomplete support specified");
00275         ok = 0;
00276       }
00277     }
00278     if(!ok){
00279       Cal_MemFree(normalizedIndexes);
00280       Cal_MemFree(support);
00281       return 0;
00282     }
00283     Cal_MemFree(support);
00284     /* Everything checked now; barring I/O errors, we should be able to */
00285     /* Write a valid output file. */
00286     f = CalBddGetInternalBdd(bddManager, fUserBdd);
00287     h = CalHashTableOneInit(bddManager, sizeof(long));
00288     indexSize = BytesNeeded(numberVars+1);
00289     CalBddMarkSharedNodes(bddManager, f);
00290     next = 0;
00291     CalBddNumberSharedNodes(bddManager, f, h, &next);
00292     nodeNumberSize = BytesNeeded(next);
00293     Write(bddManager, MAGIC_COOKIE, sizeof(long), fp);
00294     Write(bddManager, (unsigned long)numberVars, sizeof(Cal_BddIndex_t), fp);
00295     Write(bddManager, (unsigned long)next, sizeof(long), fp);
00296     BddDumpBddStep(bddManager, f, fp, h, normalizedIndexes, indexSize, nodeNumberSize);
00297     CalHashTableOneQuit(h);
00298     Cal_MemFree(normalizedIndexes);
00299     return (1);
00300   }
00301   return (0);
00302 }

Cal_Bdd Cal_BddUndumpBdd ( Cal_BddManager  bddManager,
Cal_Bdd *  userVars,
FILE *  fp,
int *  error 
)

AutomaticEnd Function********************************************************************

Synopsis [Reads a BDD from a file]

Description [Loads an encoded description of a BDD from the file given by fp. The argument vars should be a null terminated array of variables that will become the support of the BDD. As in Cal_BddDumpBdd, these need not be in the order of increasing index. If the same array of variables in used in dumping and undumping, the BDD returned will be equal to the one that was dumped. More generally, if array v1 is used when dumping, and the array v2 is used when undumping, the BDD returned will be equal to the original BDD with the ith variable in v2 substituted for the ith variable in v1 for all i. Null BDD is returned in the operation fails for reason (node limit reached, I/O error, invalid file format, etc.). In this case, an error code is stored in error. the code will be one of the following. CAL_BDD_UNDUMP_FORMAT Invalid file format CAL_BDD_UNDUMP_OVERFLOW Node limit exceeded CAL_BDD_UNDUMP_IOERROR File I/O error CAL_BDD_UNDUMP_EOF Unexpected EOF]

SideEffects [required]

SeeAlso [optional]

Definition at line 121 of file calDump.c.

00126 {
00127   long i,j;
00128   Cal_BddIndex_t numberVars;
00129   long numberShared;
00130   int indexSize;
00131   int nodeNumberSize;
00132   Cal_Bdd_t *shared;
00133   long sharedSoFar;
00134   Cal_Bdd_t v;
00135   Cal_Bdd_t result;
00136   Cal_Bdd_t *vars;
00137 
00138   *error = 0;
00139   for(i = 0; userVars[i]; ++i){
00140     if(Cal_BddType(bddManager, userVars[i]) !=  CAL_BDD_TYPE_POSVAR){
00141       CalBddWarningMessage("Cal_BddUndumpBdd: support is not all positive variables"); 
00142       return (Cal_Bdd) 0;
00143     }
00144   }
00145   vars = Cal_MemAlloc(Cal_Bdd_t, i);
00146   for (j=0; j < i; j++){
00147     vars[j] = CalBddGetInternalBdd(bddManager,userVars[j]);
00148   }
00149 
00150   if(Read(error, sizeof(long), fp) !=  MAGIC_COOKIE){
00151     if(!*error){
00152       *error = CAL_BDD_UNDUMP_FORMAT;
00153     }
00154     Cal_MemFree(vars);
00155     return (Cal_Bdd) 0;
00156   }
00157   numberVars = Read(error, sizeof(Cal_BddIndex_t), fp);
00158   if(*error){
00159     Cal_MemFree(vars);
00160     return (Cal_Bdd) 0;
00161   }
00162   if(numberVars !=  i){
00163     *error = CAL_BDD_UNDUMP_FORMAT;
00164     Cal_MemFree(vars);
00165     return (Cal_Bdd) 0;
00166   }
00167   numberShared = Read(error, sizeof(long), fp);
00168   if(*error){
00169     Cal_MemFree(vars);
00170     return (Cal_Bdd) 0;
00171   }
00172   indexSize = BytesNeeded(numberVars+1);
00173   nodeNumberSize = BytesNeeded(numberShared);
00174   if(numberShared < 0){
00175     *error = CAL_BDD_UNDUMP_FORMAT;
00176     Cal_MemFree(vars);
00177     return (Cal_Bdd) 0;
00178   }
00179   shared = Cal_MemAlloc(Cal_Bdd_t, numberShared);
00180   for(i = 0; i < numberShared; ++i){
00181     shared[i] = CalBddNull(bddManager);
00182   }
00183   sharedSoFar = 0;
00184   result = BddUndumpBddStep(bddManager, vars, fp, numberVars, shared,
00185       numberShared, &sharedSoFar, indexSize, nodeNumberSize, error);
00186   Cal_MemFree(vars);
00187   
00188   for(i = 0; i < numberShared; ++i){
00189     v = shared[i];
00190     if(!CalBddIsBddNull(bddManager, v)){
00191       CalBddFree(v);
00192     }
00193   }
00194   if(!*error && sharedSoFar !=  numberShared){
00195     *error = CAL_BDD_UNDUMP_FORMAT;
00196   }
00197   Cal_MemFree(shared);
00198   if(*error){
00199     if(!CalBddIsBddNull(bddManager, result)){
00200       CalBddFree(result);
00201     }
00202     return (Cal_Bdd) 0;
00203   }
00204   /*
00205    * Decrement the reference count of result by 1. Since it has
00206    * already been incremented in BddUndumpBddStep.
00207    */
00208   CalBddDcrRefCount(result);
00209   return CalBddGetExternalBdd(bddManager, result);
00210 }

static unsigned long Read ( int *  error,
int  bytes,
FILE *  fp 
) [static]

Function********************************************************************

Synopsis []

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 433 of file calDump.c.

00437 {
00438   int c;
00439   long result;
00440 
00441   result = 0;
00442   if(*error){
00443     return (result);
00444   }
00445   while(bytes){
00446     c = fgetc(fp);
00447     if(c == EOF){
00448       if(ferror(fp)){
00449         *error = CAL_BDD_UNDUMP_IOERROR;
00450       }
00451       else{
00452         *error = CAL_BDD_UNDUMP_EOF;
00453       }
00454       return (0l);
00455     }
00456     result = (result << 8)+c;
00457     --bytes;
00458   } 
00459   return (result);
00460 }

static void Write ( Cal_BddManager_t *  bddManager,
unsigned long  n,
int  bytes,
FILE *  fp 
) [static]

AutomaticStart

Function********************************************************************

Synopsis []

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 316 of file calDump.c.

00321 {
00322   while(bytes){
00323     if(fputc((char)(n >> (8*(bytes-1)) & 0xff), fp) == EOF){
00324     }
00325     --bytes;
00326   }
00327 }

Variable Documentation

long indexMask[] = {0xffl, 0xffffl, 0xffffffl} [static]

Definition at line 71 of file calDump.c.

Generated on Tue Jan 12 13:57:11 2010 for glu-2.2 by  doxygen 1.6.1