static void 
AddBlock(
  Cal_Block  b1, 
  Cal_Block  b2 
)
optional

Side Effects required

See Also optional
Defined in calBlk.c 

static void 
AddToFreeList(
  Block  b 
)
AddToFreeList(b) adds b to the appropriate free list.

Side Effects required

See Also optional
Defined in calMem.c 

static int 
AssociationIsEqual(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t * p, 
  Cal_Bdd_t * q 
)
Checks for equality of two associations

Side Effects None

Defined in calAssociation.c 

static void 
BddAddInternalReferences(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calReorderDF.c 

static Cal_Bdd_t * 
BddArrayOpBF(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t* bddArray, 
  int  numFunction, 
  CalOpProc_t  calOpProc 
)
Internal common routine for Cal_BddPairwiseAnd and Cal_BddPairwiseOr

Side Effects None

Defined in calBddOp.c 

static void 
BddArrayToRequestNodeListArray(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t * calBddArray, 
  int  numBdds 
)
Converts an array of BDDs to a list of requests representing BDD

Side Effects None

Defined in calBddOp.c 

static Cal_Bdd_t 
BddCofactorBF(
  Cal_BddManager_t * bddManager, 
  CalOpProc_t  calOpProc, 
  Cal_Bdd_t  f, 
  Cal_Bdd_t  c 
)
optional

Side Effects required

See Also optional
Defined in calReduce.c 

static void 
BddConvertDataStructBack(
  Cal_BddManager_t * bddManager 
)
Data structure conversion: thenBddId -> id elseBddId -> ref count

Side Effects required

See Also optional
Defined in calReorderDF.c 

static void 
BddConvertDataStruct(
  Cal_BddManager_t * bddManager 
)
New data structure: thenBddId -> id elseBddId -> ref count

Side Effects required

See Also optional
Defined in calReorderDF.c 

static int 
BddCountNoNodes(
  Cal_Bdd_t  f 
)
optional

Side Effects required

See Also optional
Defined in calBddSize.c 

static int 
BddCountNodes(
  Cal_Bdd_t  f 
)
optional

Side Effects required

See Also optional
Defined in calBddSize.c 

static Cal_Bdd_t 
BddDFStep(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  Cal_Bdd_t  g, 
  CalOpProc_t  calOpProc, 
  unsigned short  opCode 
)
optional

Side Effects required

See Also optional
Defined in calQuant.c 

static void 
BddDefaultTransformFn(
  Cal_BddManager_t * bddManager, 
  CalAddress_t  value1, 
  CalAddress_t  value2, 
  CalAddress_t * result1, 
  CalAddress_t * result2, 
  Cal_Pointer_t  pointer 
)
optional

Side Effects required

See Also optional
Defined in calBddManager.c 

static void 
BddDominatedStep(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  long * funcCounts, 
  CalHashTable_t * h 
)
optional

Side Effects required

See Also optional
Defined in calBddSize.c 

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

Side Effects required

See Also optional
Defined in calDump.c 

static void 
BddExchangeAux(
  Cal_BddManager_t * bddManager, 
  CalBddNode_t * f, 
  int  id, 
  int  nextId 
)
optional

Side Effects required

See Also optional
Defined in calReorderDF.c 

static void 
BddExchangeVarBlocks(
  Cal_BddManager_t * bddManager, 
  Cal_Block  parent, 
  long  blockIndex 
)
optional

Side Effects required

See Also optional
Defined in calReorderDF.c 

static void 
BddExchange(
  Cal_BddManager_t * bddManager, 
  long  id 
)
optional

Side Effects required

See Also optional
Defined in calReorderDF.c 

static void 
BddExistsApply(
  Cal_BddManager_t * bddManager, 
  int  quantifying, 
  CalHashTable_t * existHashTable, 
  CalHashTable_t ** existHashTableArray, 
  CalOpProc1_t  calOpProc, 
  unsigned short  opCode, 
  CalAssociation_t * assoc 
)
optional

Side Effects required

See Also optional
Defined in calQuant.c 

static void 
BddExistsBFAux(
  Cal_BddManager_t * bddManager, 
  int  minIndex, 
  CalHashTable_t ** existHashTableArray, 
  CalHashTable_t ** orHashTableArray, 
  CalOpProc1_t  calOpProc, 
  unsigned short  opCode, 
  CalAssociation_t * assoc 
)
optional

Side Effects required

See Also optional
Defined in calQuant.c 

static Cal_Bdd_t 
BddExistsBFPlusDF(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  unsigned short  opCode, 
  CalAssociation_t * association 
)
optional

Side Effects required

See Also optional
Defined in calQuant.c 

static void 
BddExistsReduce(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * existHashTable, 
  CalHashTable_t ** existHashTableArray, 
  CalHashTable_t ** orHashTableArray, 
  unsigned short  opCode, 
  CalAssociation_t * association 
)
optional

Side Effects required

See Also optional
Defined in calQuant.c 

static Cal_Bdd_t 
BddExistsStep(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  unsigned short  opCode, 
  CalAssociation_t * association 
)
optional

Side Effects required

See Also optional
Defined in calQuant.c 

static void 
BddHighestRefStep(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  CalHashTable_t * h 
)
optional

Side Effects required

See Also optional
Defined in calBddSize.c 

static Cal_Bdd_t 
BddIntersectsStep(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  Cal_Bdd_t  g 
)
Recursive routine to returns a BDD that implies conjunction of argument BDDs

Side Effects None

Defined in cal.c 

static void 
BddMarkBdd(
  Cal_Bdd_t  f 
)
optional

Side Effects required

See Also optional
Defined in calBddSize.c 

static Cal_Bdd_t 
BddMultiwayOp(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t * calBddArray, 
  int  numBdds, 
  CalOpProc_t  op 
)
Internal routine for multiway operations

Side Effects None

Defined in calBddOp.c 

static void 
BddNukeInternalReferences(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calReorderDF.c 

static void 
BddPrintBddStep(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  Cal_VarNamingFn_t  VarNamingFn, 
  Cal_TerminalIdFn_t  TerminalIdFn, 
  Cal_Pointer_t  env, 
  FILE * fp, 
  CalHashTable_t* hashTable, 
  int  indentation 
)
optional

Side Effects required

See Also optional
Defined in calPrint.c 

static void 
BddPrintTopVar(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  Cal_VarNamingFn_t  VarNamingFn, 
  Cal_Pointer_t  env, 
  FILE * fp 
)
optional

Side Effects required

See Also optional
Defined in calPrint.c 

static void 
BddProfileStep(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  long * levelCounts, 
  CountFn_t  countFn 
)
optional

Side Effects required

See Also optional
Defined in calBddSize.c 

static void 
BddReallocateNodesInPlace(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calReorderDF.c 

static void 
BddReallocateNodes(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calReorderDF.c 

static Cal_Bdd_t 
BddReduceBF(
  Cal_BddManager_t * bddManager, 
  CalOpProc_t  calOpProc, 
  Cal_Bdd_t  f, 
  Cal_Bdd_t  c 
)
optional

Side Effects required

See Also optional
Defined in calReduce.c 

static void 
BddRelProdApply(
  Cal_BddManager_t * bddManager, 
  int  quantifying, 
  CalHashTable_t * relProdHashTable, 
  CalHashTable_t ** relProdHashTableArray, 
  CalHashTable_t ** andHashTableArray, 
  CalOpProc_t  calOpProc, 
  unsigned short  opCode, 
  CalAssociation_t * assoc 
)
optional

Side Effects required

See Also optional
Defined in calQuant.c 

static void 
BddRelProdBFAux(
  Cal_BddManager_t * bddManager, 
  int  minIndex, 
  CalHashTable_t ** relProdHashTableArray, 
  CalHashTable_t ** andHashTableArray, 
  CalHashTable_t ** orHashTableArray, 
  unsigned short  opCode, 
  CalAssociation_t * assoc 
)
optional

Side Effects required

See Also optional
Defined in calQuant.c 

static Cal_Bdd_t 
BddRelProdBFPlusDF(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  Cal_Bdd_t  g, 
  unsigned short  opCode, 
  CalAssociation_t * association 
)
optional

Side Effects required

See Also optional
Defined in calQuant.c 

static void 
BddRelProdReduce(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * relProdHashTable, 
  CalHashTable_t ** relProdHashTableArray, 
  CalHashTable_t ** andHashTableArray, 
  CalHashTable_t ** orHashTableArray, 
  unsigned short  opCode, 
  CalAssociation_t * assoc 
)
optional

Side Effects required

See Also optional
Defined in calQuant.c 

static Cal_Bdd_t 
BddRelProdStep(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  Cal_Bdd_t  g, 
  unsigned short  opCode, 
  CalAssociation_t * assoc 
)
optional

Side Effects required

See Also optional
Defined in calQuant.c 

static void 
BddReorderFixAndFreeForwardingNodes(
  Cal_BddManager  bddManager, 
  Cal_BddId_t  id, 
  int  numLevels 
)
optional

Side Effects required

See Also optional
Defined in calReorderBF.c 

static void 
BddReorderFixForwardingNodes(
  Cal_BddManager  bddManager, 
  Cal_BddId_t  id 
)
As opposed to CalBddReorderFixCofactors, which fixes the cofactors of the non-forwarding nodes, this routine traverses the list of forwarding nodes and removes the intermediate level of forwarding. Number of levels should be 1 or 2.

Side Effects required

See Also optional
Defined in calReorderBF.c 

static void 
BddReorderFreeNodes(
  Cal_BddManager_t * bddManager, 
  int  varId 
)
optional

Side Effects required

See Also optional
Defined in calReorderBF.c 

static void 
BddReorderSiftAux(
  Cal_BddManager_t * bddManager, 
  Cal_Block  block, 
  Cal_Block * toSift, 
  double  maxSizeFactor 
)
Reorder variables using "sift" algorithm.

Side Effects None

Defined in calReorderDF.c 

static int 
BddReorderSiftToBestPos(
  Cal_BddManager_t * bddManager, 
  int  varStartIndex, 
  double  maxSizeFactor 
)
optional

Side Effects required

See Also optional
Defined in calReorderBF.c 

static void 
BddReorderSift(
  Cal_BddManager_t * bddManager, 
  double  maxSizeFactor 
)
optional

Side Effects required

See Also optional
Defined in calReorderDF.c 

static void 
BddReorderStableWindow3Aux(
  Cal_BddManager_t * bddManager, 
  Cal_Block  block, 
  char * levels 
)
optional

Side Effects required

See Also optional
Defined in calReorderDF.c 

static void 
BddReorderStableWindow3(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calReorderDF.c 

static void 
BddReorderSwapVarIndex(
  Cal_BddManager_t * bddManager, 
  int  varIndex, 
  int  forwardCheckFlag 
)
Traversesoptional

Side Effects required

See Also optional
Defined in calReorderBF.c 

static void 
BddReorderVarSift(
  Cal_BddManager  bddManager, 
  double  maxSizeFactor 
)
Reorder variables using "sift" algorithm.

Side Effects None

Defined in calReorderBF.c 

static void 
BddReorderVarWindow(
  Cal_BddManager  bddManager, 
  char * levels 
)
optional

Side Effects required

See Also optional
Defined in calReorderBF.c 

static int 
BddReorderWindow2(
  Cal_BddManager  bddManager, 
  long  index, 
  int  directionFlag 
)
optional

Side Effects required

See Also optional
Defined in calReorderBF.c 

static int 
BddReorderWindow2(
  Cal_BddManager_t * bddManager, 
  Cal_Block  block, 
  long  i 
)
optional

Side Effects required

See Also optional
Defined in calReorderDF.c 

static int 
BddReorderWindow3(
  Cal_BddManager  bddManager, 
  long  index, 
  int  directionFlag 
)
optional

Side Effects required

See Also optional
Defined in calReorderBF.c 

static int 
BddReorderWindow3(
  Cal_BddManager_t * bddManager, 
  Cal_Block  block, 
  long  i 
)
optional

Side Effects required

See Also optional
Defined in calReorderDF.c 

static Cal_Bdd_t 
BddSatisfyStep(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f 
)
optional

Side Effects required

See Also optional
Defined in calBddSatisfy.c 

static Cal_Bdd_t 
BddSatisfySupportStep(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  Cal_BddId_t * support 
)
optional

Side Effects required

See Also optional
Defined in calBddSatisfy.c 

static double 
BddSatisfyingFractionStep(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  CalHashTable_t * hashTable 
)
optional

Side Effects required

See Also optional
Defined in calBddSatisfy.c 

static void 
BddSiftBlock(
  Cal_BddManager_t * bddManager, 
  Cal_Block  block, 
  long  startPosition, 
  double  maxSizeFactor 
)
optional

Side Effects required

See Also optional
Defined in calReorderDF.c 

static void 
BddSiftPerfromPhaseIV(
  Cal_BddManager_t * bddManager, 
  int  varStartIndex, 
  int  bestIndex, 
  int  bottomMostSwapIndex 
)
optional

Side Effects required

See Also optional
Defined in calReorderBF.c 

static long 
BddSizeStep(
  Cal_Bdd_t  f, 
  CountFn_t  countFn 
)
optional

Side Effects required

See Also optional
Defined in calBddSize.c 

static char * 
BddTerminalId(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  Cal_TerminalIdFn_t  TerminalIdFn, 
  Cal_Pointer_t  env 
)
optional

Side Effects required

See Also optional
Defined in calPrint.c 

static void 
BddTerminalValueAux(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  CalAddress_t * value1, 
  CalAddress_t * value2 
)
optional

Side Effects required

See Also optional
Defined in calPrint.c 

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 
)
optional

Side Effects required

See Also optional
Defined in calDump.c 

static int 
BlockSizeIndex(
  Cal_Address_t  size 
)
BlockSizeIndex(size) return the coded size for a block.

Side Effects required

See Also optional
Defined in calMem.c 

static Block 
Buddy(
  Block  b 
)
Buddy(b) returns the Buddy block of b, or null if there is no Buddy.

Side Effects required

See Also optional
Defined in calMem.c 

static int 
BytesNeeded(
  long  n 
)
optional

Side Effects required

See Also optional
Defined in calDump.c 

static void 
CacheTablePrint(
  CalCacheTable_t * cacheTable 
)
optional

Side Effects required

See Also optional
Defined in calCacheTableTwo.c 

static void 
CacheTableTwoRehash(
  CalCacheTable_t * cacheTable, 
  int  grow 
)
optional

Side Effects required

See Also optional
Defined in calCacheTableTwo.c 

void 
CalAlignCollisionChains(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calReorderDF.c 

void 
CalAssociationListFree(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calAssociation.c 

int 
CalBddArrayPreProcessing(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd * userBddArray 
)
optional

Side Effects required

See Also optional
Defined in calUtil.c 

void 
CalBddBlockDelta(
  Cal_Block  b, 
  long  delta 
)
optional

Side Effects required

See Also optional
Defined in calBlk.c 

static int 
CalBddDependsOnStep(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  Cal_BddIndex_t  varIndex, 
  int  mark 
)
optional

Side Effects required

See Also optional
Defined in calBddSupport.c 

void 
CalBddFatalMessage(
  char * string 
)
optional

Side Effects required

See Also optional
Defined in calUtil.c 

long 
CalBddFindBlock(
  Cal_Block  block, 
  long  index 
)
optional

Side Effects required

See Also optional
Defined in calBlk.c 

void 
CalBddFunctionPrint(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  calBdd, 
  char * name 
)
Prints the function implemented by the argument BDD

Side Effects None

Defined in calUtil.c 

Cal_Bdd 
CalBddGetExternalBdd(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  internalBdd 
)
optional

Side Effects required

See Also optional
Defined in calUtil.c 

Cal_Bdd_t 
CalBddGetInternalBdd(
  Cal_BddManager  bddManager, 
  Cal_Bdd  userBdd 
)
optional

Side Effects required

See Also optional
Defined in calUtil.c 

Cal_Bdd_t 
CalBddITE(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  F, 
  Cal_Bdd_t  G, 
  Cal_Bdd_t  H 
)
Returns the BDD for logical If-Then-Else Description [Returns the BDD for the logical operation IF f THEN g ELSE h - f g + f' h

Side Effects None

See Also Cal_BddAnd Cal_BddNand Cal_BddOr Cal_BddNor Cal_BddXor Cal_BddXnor
Defined in calBddITE.c 

Cal_Bdd_t 
CalBddIdentity(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  calBdd 
)
Returns the duplicate BDD of the argument BDD.

Side Effects The reference count of the BDD is increased by 1.

See Also Cal_BddNot
Defined in cal.c 

Cal_Bdd_t 
CalBddIf(
  Cal_BddManager  bddManager, 
  Cal_Bdd_t  F 
)
Returns the BDD corresponding to the top variable of the argument BDD.

Side Effects None.

Defined in cal.c 

int 
CalBddIsCubeStep(
  Cal_BddManager  bddManager, 
  Cal_Bdd_t  f 
)
Returns 1 if the argument BDD is a cube, 0 otherwise

Side Effects None

Defined in cal.c 

Cal_Bdd_t 
CalBddManagerCreateNewVar(
  Cal_BddManager_t * bddManager, 
  Cal_BddIndex_t  index 
)
Right now this function does not handle the case when the package is working in multiprocessor mode. We need to put in the necessary code later.

Side Effects If the number of variables in the manager exceeds that of value of numMaxVars, then we need to reallocate various fields of the manager. Also depending upon the value of "index", idToIndex and indexToId tables would change.

Defined in calBddManager.c 

void 
CalBddManagerGCCheck(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calGC.c 

void 
CalBddManagerGetCacheTableData(
  Cal_BddManager_t * bddManager, 
  unsigned long * cacheSize, 
  unsigned long * cacheEntries, 
  unsigned long * cacheInsertions, 
  unsigned long * cacheLookups, 
  unsigned long * cacheHits, 
  unsigned long * cacheCollisions 
)
optional

Side Effects required

See Also optional
Defined in calCacheTableTwo.c 

static int 
CalBddManagerPrint(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calBddManager.c 

void 
CalBddMarkSharedNodes(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f 
)
optional

Side Effects required

See Also optional
Defined in calPrint.c 

void 
CalBddNodePrint(
  CalBddNode_t * bddNode 
)
optional

Side Effects required

See Also optional
Defined in calUtil.c 

void 
CalBddNumberSharedNodes(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  CalHashTable_t * hashTable, 
  long * next 
)
optional

Side Effects required

See Also optional
Defined in calPrint.c 

Cal_Bdd_t 
CalBddOpBF(
  Cal_BddManager_t * bddManager, 
  CalOpProc_t  calOpProc, 
  Cal_Bdd_t  F, 
  Cal_Bdd_t  G 
)
Internal routine to compute a logical operation on a pair of BDDs

Side Effects None

Defined in calBddOp.c 

Cal_Bdd_t 
CalBddOpITEBF(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  Cal_Bdd_t  g, 
  Cal_Bdd_t  h 
)
optional

Side Effects required

See Also optional
Defined in calBddITE.c 

void 
CalBddPackNodesAfterReorderForSingleId(
  Cal_BddManager_t * bddManager, 
  int  fixForwardedNodesFlag, 
  int  bestIndex, 
  int  bottomIndex 
)
fixForwardedNodesFlag: Whether we need to fix the forwarded nodes of variables corresponding to bestIndex through bottomIndex. If this flag is set, then the forwarded nodes of these variables are traversed and updated after the nodes of the bestIndex have been copied. At the end the forwarded nodes are freed. If this flag is not set, it is assumed that the cleanup pass has already been performed.

Side Effects required

See Also optional
Defined in calHashTable.c 

void 
CalBddPackNodesForMultipleIds(
  Cal_BddManager_t * bddManager, 
  Cal_BddId_t  beginId, 
  int  numLevels 
)
optional

Side Effects required

See Also optional
Defined in calHashTable.c 

void 
CalBddPackNodesForSingleId(
  Cal_BddManager_t * bddManager, 
  Cal_BddId_t  id 
)
optional

Side Effects required

See Also optional
Defined in calHashTable.c 

int 
CalBddPostProcessing(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calUtil.c 

int 
CalBddPreProcessing(
  Cal_BddManager_t * bddManager, 
  int  count, 
    
)
optional

Side Effects required

See Also optional
Defined in calUtil.c 

static void 
CalBddPrintProfileAux(
  Cal_BddManager_t * bddManager, 
  long * levelCounts, 
  Cal_VarNamingFn_t  varNamingProc, 
  char * env, 
  int  lineLength, 
  FILE * fp 
)
optional

Side Effects required

See Also optional
Defined in calPrintProfile.c 

void 
CalBddPrint(
  Cal_Bdd_t  calBdd 
)
optional

Side Effects required

See Also optional
Defined in calUtil.c 

void 
CalBddReorderAuxBF(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calReorderBF.c 

void 
CalBddReorderAuxDF(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calReorderDF.c 

void 
CalBddReorderFixCofactors(
  Cal_BddManager  bddManager, 
  Cal_BddId_t  id 
)
This routine traverses the unique table and for each node, looks at the then and else cofactors. If needed fixes the cofactors.

Side Effects required

See Also optional
Defined in calReorderUtil.c 

void 
CalBddReorderFixProvisionalNodes(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calPipeline.c 

void 
CalBddReorderFixUserBddPtrs(
  Cal_BddManager  bddManager 
)
optional

Side Effects required

See Also optional
Defined in calReorderUtil.c 

void 
CalBddReorderReclaimForwardedNodes(
  Cal_BddManager  bddManager, 
  int  startIndex, 
  int  endIndex 
)
optional

Side Effects required

See Also optional
Defined in calReorderUtil.c 

Cal_Block 
CalBddShiftBlock(
  Cal_BddManager_t * bddManager, 
  Cal_Block  b, 
  long  index 
)
optional

Side Effects required

See Also optional
Defined in calBlk.c 

static Cal_Bdd_t * 
CalBddSupportStep(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  Cal_Bdd_t * support 
)
optional

Side Effects required

See Also optional
Defined in calBddSupport.c 

int 
CalBddTypeAux(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f 
)
Returns the BDD type by recursively traversing the argument BDD

Side Effects None

Defined in cal.c 

unsigned long 
CalBddUniqueTableNumLockedNodes(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * uniqueTableForId 
)
optional

Side Effects required

See Also optional
Defined in calHashTable.c 

static void 
CalBddUnmarkNodes(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f 
)
optional

Side Effects required

See Also optional
Defined in calBddSupport.c 

char * 
CalBddVarName(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  v, 
  Cal_VarNamingFn_t  VarNamingFn, 
  Cal_Pointer_t  env 
)
optional

Side Effects required

See Also optional
Defined in calPrint.c 

Cal_Bdd_t 
CalBddVarSubstitute(
  Cal_BddManager  bddManager, 
  Cal_Bdd_t  f, 
  unsigned short  opCode, 
  CalAssociation_t * assoc 
)
Returns a BDD for f using the substitution defined by current variable association. Each variable is replaced by its associated BDDs. The substitution is effective simultaneously

Side Effects None

See Also Cal_BddCompose
Defined in calBddVarSubstitute.c 

void 
CalBddWarningMessage(
  char * string 
)
optional

Side Effects required

See Also optional
Defined in calUtil.c 

unsigned long 
CalBlockMemoryConsumption(
  Cal_Block  block 
)
optional

Side Effects required

See Also optional
Defined in calBlk.c 

unsigned long 
CalCacheTableMemoryConsumption(
  CalCacheTable_t * cacheTable 
)
optional

Side Effects required

See Also optional
Defined in calCacheTableTwo.c 

void 
CalCacheTablePrint(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calCacheTableTwo.c 

void 
CalCacheTableRehash(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calCacheTableTwo.c 

void 
CalCacheTableTwoFixResultPointers(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calCacheTableTwo.c 

int 
CalCacheTableTwoFlushAll(
  CalCacheTable_t * cacheTable 
)
optional

Side Effects required

See Also optional
Defined in calCacheTableTwo.c 

void 
CalCacheTableTwoFlushAssociationId(
  Cal_BddManager_t * bddManager, 
  int  associationId 
)
Flushes the entries from the cache which correspond to the given associationId.

Side Effects Cache entries are affected.

Defined in calCacheTableTwo.c 

void 
CalCacheTableTwoFlush(
  CalCacheTable_t * cacheTable 
)
optional

Side Effects required

See Also optional
Defined in calCacheTableTwo.c 

void 
CalCacheTableTwoGCFlush(
  CalCacheTable_t * cacheTable 
)
optional

Side Effects required

See Also optional
Defined in calCacheTableTwo.c 

CalCacheTable_t * 
CalCacheTableTwoInit(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calCacheTableTwo.c 

void 
CalCacheTableTwoInsert(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  Cal_Bdd_t  g, 
  Cal_Bdd_t  result, 
  unsigned long  opCode, 
  int  cacheLevel 
)
optional

Side Effects required

See Also optional
Defined in calCacheTableTwo.c 

int 
CalCacheTableTwoLookup(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  Cal_Bdd_t  g, 
  unsigned long  opCode, 
  Cal_Bdd_t * resultBddPtr 
)
optional

Side Effects required

See Also optional
Defined in calCacheTableTwo.c 

int 
CalCacheTableTwoQuit(
  CalCacheTable_t * cacheTable 
)
optional

Side Effects required

See Also optional
Defined in calCacheTableTwo.c 

void 
CalCacheTableTwoRepackUpdate(
  CalCacheTable_t * cacheTable 
)
optional

Side Effects required

See Also optional
Defined in calCacheTableTwo.c 

int 
CalCheckAllValidity(
  Cal_BddManager  bddManager 
)
optional

Side Effects required

See Also optional
Defined in calReorderUtil.c 

void 
CalCheckAssociationValidity(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calAssociation.c 

int 
CalCheckAssoc(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calReorderUtil.c 

void 
CalCheckCacheTableValidity(
  Cal_BddManager  bddManager 
)
optional

Side Effects required

See Also optional
Defined in calCacheTableTwo.c 

void 
CalCheckPipelineValidity(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calPipeline.c 

void 
CalCheckRefCountValidity(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calReorderUtil.c 

int 
CalCheckValidityOfANode(
  Cal_BddManager_t * bddManager, 
  CalBddNode_t * bddNode, 
  int  id 
)
optional

Side Effects required

See Also optional
Defined in calReorderUtil.c 

int 
CalCheckValidityOfNodesForId(
  Cal_BddManager  bddManager, 
  int  id 
)
optional

Side Effects required

See Also optional
Defined in calReorderUtil.c 

int 
CalCheckValidityOfNodesForWindow(
  Cal_BddManager  bddManager, 
  Cal_BddIndex_t  index, 
  int  numLevels 
)
optional

Side Effects required

See Also optional
Defined in calReorderUtil.c 

void 
CalComposeRequestCreate(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  Cal_Bdd_t  h, 
  Cal_BddIndex_t  composeIndex, 
  CalHashTable_t ** reqQueForCompose, 
  CalHashTable_t ** reqQueForITE, 
  Cal_Bdd_t * resultPtr 
)
optional

Side Effects required

See Also optional
Defined in calBddCompose.c 

int 
CalDecreasingOrderCompare(
  const void * a, 
  const void * b 
)
optional

Side Effects required

See Also optional
Defined in calPerformanceTest.c 

void 
CalFixupAssoc(
  Cal_BddManager_t * bddManager, 
  long  id1, 
  long  id2, 
  CalAssociation_t * assoc 
)
optional

Side Effects required

See Also optional
Defined in calReorderUtil.c 

void 
CalFreeBlockRecursively(
  Cal_Block  block 
)
optional

Side Effects required

See Also optional
Defined in calBlk.c 

int 
CalHashTableAddDirectAux(
  CalHashTable_t * hashTable, 
  Cal_Bdd_t  thenBdd, 
  Cal_Bdd_t  elseBdd, 
  Cal_Bdd_t * bddPtr 
)
optional

Side Effects required

See Also optional
Defined in calHashTable.c 

void 
CalHashTableAddDirect(
  CalHashTable_t * hashTable, 
  CalBddNode_t * bddNode 
)
optional

Side Effects required

See Also optional
Defined in calHashTable.c 

void 
CalHashTableApply(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable, 
  CalHashTable_t ** reqQueAtPipeDepth, 
  CalOpProc_t  calOpProc 
)
optional

Side Effects required

See Also optional
Defined in calApplyReduce.c 

void 
CalHashTableCleanUp(
  CalHashTable_t * hashTable 
)
optional

Side Effects required

See Also optional
Defined in calHashTable.c 

void 
CalHashTableComposeApply(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable, 
  Cal_BddIndex_t  gIndex, 
  CalHashTable_t ** reqQueForCompose, 
  CalHashTable_t ** reqQueForITE 
)
optional

Side Effects required

See Also optional
Defined in calBddCompose.c 

void 
CalHashTableDelete(
  CalHashTable_t * hashTable, 
  CalBddNode_t * bddNode 
)
optional

Side Effects required

See Also optional
Defined in calHashTable.c 

int 
CalHashTableFindOrAdd(
  CalHashTable_t * hashTable, 
  Cal_Bdd_t  thenBdd, 
  Cal_Bdd_t  elseBdd, 
  Cal_Bdd_t * bddPtr 
)
optional

Side Effects required

See Also optional
Defined in calHashTable.c 

int 
CalHashTableGC(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable 
)
The input is the hash table containing the nodes belonging to that level. Each bin of the hash table is traversed and the Bdd nodes with 0 reference count are put at the appropriate level in the processing que of the manager.

Side Effects The number of nodes in the hash table can possibly decrease.

See Also optional
Defined in calGC.c 

void 
CalHashTableITEApply(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable, 
  CalHashTable_t ** reqQueAtPipeDepth 
)
optional

Side Effects required

See Also optional
Defined in calBddITE.c 

CalHashTable_t * 
CalHashTableInit(
  Cal_BddManager_t * bddManager, 
  Cal_BddId_t  bddId 
)
optional

Side Effects required

See Also optional
Defined in calHashTable.c 

int 
CalHashTableLookup(
  CalHashTable_t * hashTable, 
  Cal_Bdd_t  thenBdd, 
  Cal_Bdd_t  elseBdd, 
  Cal_Bdd_t * bddPtr 
)
optional

Side Effects required

See Also optional
Defined in calHashTable.c 

CalHashTable_t * 
CalHashTableOneInit(
  Cal_BddManager_t * bddManager, 
  int  itemSize 
)
optional

Side Effects required

See Also optional
Defined in calHashTableOne.c 

void 
CalHashTableOneInsert(
  CalHashTable_t * hashTable, 
  Cal_Bdd_t  keyBdd, 
  char * valuePtr 
)
optional

Side Effects required

See Also optional
Defined in calHashTableOne.c 

int 
CalHashTableOneLookup(
  CalHashTable_t * hashTable, 
  Cal_Bdd_t  keyBdd, 
  char ** valuePtrPtr 
)
optional

Side Effects required

See Also optional
Defined in calHashTableOne.c 

void 
CalHashTableOnePrint(
  CalHashTable_t * hashTable, 
  int  flag 
)
optional

Side Effects required

See Also optional
Defined in calUtil.c 

void 
CalHashTableOneQuit(
  CalHashTable_t * hashTable 
)
optional

Side Effects required

See Also optional
Defined in calHashTableOne.c 

void 
CalHashTablePrint(
  CalHashTable_t * hashTable 
)
optional

Side Effects required

See Also optional
Defined in calUtil.c 

int 
CalHashTableQuit(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable 
)
optional

Side Effects required

See Also optional
Defined in calHashTable.c 

void 
CalHashTableReduce(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable, 
  CalHashTable_t * uniqueTableForId 
)
optional

Side Effects required

See Also optional
Defined in calApplyReduce.c 

void 
CalHashTableRehash(
  CalHashTable_t * hashTable, 
  int  grow 
)
optional

Side Effects required

See Also optional
Defined in calHashTable.c 

static void 
CalHashTableSubstituteApply(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable, 
  int  lastIndex, 
  CalHashTable_t ** reqQueForSubstitute 
)
optional

Side Effects required

See Also optional
Defined in calBddSubstitute.c 

static void 
CalHashTableSubstituteApply(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable, 
  int  lastIndex, 
  CalHashTable_t ** reqQueForSubstitute, 
  unsigned short  opCode 
)
optional

Side Effects required

See Also optional
Defined in calBddVarSubstitute.c 

static void 
CalHashTableSubstituteReduce(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable, 
  CalHashTable_t ** reqQueForITE, 
  CalHashTable_t * uniqueTableForId 
)
optional

Side Effects required

See Also optional
Defined in calBddSubstitute.c 

static void 
CalHashTableSubstituteReduce(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable, 
  CalHashTable_t ** reqQueForITE, 
  CalHashTable_t * uniqueTableForId, 
  unsigned short  opCode 
)
optional

Side Effects required

See Also optional
Defined in calBddVarSubstitute.c 

static void 
CalHashTableSwapVarsApply(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable, 
  Cal_BddIndex_t  gIndex, 
  Cal_BddIndex_t  hIndex, 
  CalHashTable_t ** reqQueForSwapVars, 
  CalHashTable_t ** reqQueForSwapVarsPlus, 
  CalHashTable_t ** reqQueForSwapVarsMinus, 
  CalHashTable_t ** reqQueForCompose, 
  CalHashTable_t ** reqQueForITE 
)
optional

Side Effects required

See Also optional
Defined in calBddSwapVars.c 

static void 
CalHashTableSwapVarsMinusApply(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable, 
  Cal_BddIndex_t  hIndex, 
  CalHashTable_t ** reqQueForSwapVars, 
  CalHashTable_t ** reqQueForSwapVarsPlus, 
  CalHashTable_t ** reqQueForSwapVarsMinus, 
  CalHashTable_t ** reqQueForCompose 
)
optional

Side Effects required

See Also optional
Defined in calBddSwapVars.c 

static void 
CalHashTableSwapVarsPlusApply(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable, 
  Cal_BddIndex_t  hIndex, 
  CalHashTable_t ** reqQueForSwapVars, 
  CalHashTable_t ** reqQueForSwapVarsPlus, 
  CalHashTable_t ** reqQueForSwapVarsMinus, 
  CalHashTable_t ** reqQueForCompose 
)
optional

Side Effects required

See Also optional
Defined in calBddSwapVars.c 

int 
CalHashTableThreeFindOrAdd(
  CalHashTable_t * hashTable, 
  Cal_Bdd_t  f, 
  Cal_Bdd_t  g, 
  Cal_Bdd_t  h, 
  Cal_Bdd_t * bddPtr 
)
optional

Side Effects required

See Also optional
Defined in calHashTableThree.c 

static void 
CalHashTableThreeRehash(
  CalHashTable_t * hashTable, 
  int  grow 
)
optional

Side Effects required

See Also optional
Defined in calHashTableThree.c 

int 
CalIncreasingOrderCompare(
  const void * a, 
  const void * b 
)
optional

Side Effects required

See Also optional
Defined in calPerformanceTest.c 

int 
CalInitInteract(
  Cal_BddManager_t * bddManager 
)
Initializes the interaction matrix. The interaction matrix is implemented as a bit vector storing the upper triangle of the symmetric interaction matrix. The bit vector is kept in an array of long integers. The computation is based on a series of depth-first searches, one for each root of the DAG. A local flag (the mark bits) is used.

Side Effects None

Defined in calInteract.c 

CalNodeManager_t * 
CalNodeManagerInit(
  CalPageManager_t * pageManager 
)
optional

See Also optional
Defined in calMemoryManagement.c 

void 
CalNodeManagerPrint(
  CalNodeManager_t * nodeManager 
)
optional

See Also optional
Defined in calMemoryManagement.c 

int 
CalNodeManagerQuit(
  CalNodeManager_t * nodeManager 
)
optional

Side Effects The associated nodes are lost.

See Also optional
Defined in calMemoryManagement.c 

int 
CalOpAnd(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  F, 
  Cal_Bdd_t  G, 
  Cal_Bdd_t * resultBddPtr 
)
optional

Side Effects required

See Also optional
Defined in calTerminal.c 

int 
CalOpBddVarSubstitute(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  Cal_Bdd_t * resultBddPtr 
)
optional

Side Effects required

See Also optional
Defined in calBddVarSubstitute.c 

int 
CalOpCofactor(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  Cal_Bdd_t  c, 
  Cal_Bdd_t * resultBddPtr 
)
optional

Side Effects required

See Also optional
Defined in calReduce.c 

int 
CalOpExists(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  Cal_Bdd_t * resultBddPtr 
)
optional

Side Effects required

See Also optional
Defined in calQuant.c 

Cal_Bdd_t 
CalOpITE(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  Cal_Bdd_t  g, 
  Cal_Bdd_t  h, 
  CalHashTable_t ** reqQueForITE 
)
optional

Side Effects required

See Also optional
Defined in calTerminal.c 

int 
CalOpNand(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  F, 
  Cal_Bdd_t  G, 
  Cal_Bdd_t * resultBddPtr 
)
optional

Side Effects required

See Also optional
Defined in calTerminal.c 

int 
CalOpOr(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  F, 
  Cal_Bdd_t  G, 
  Cal_Bdd_t * resultBddPtr 
)
optional

Side Effects required

See Also optional
Defined in calTerminal.c 

int 
CalOpRelProd(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  Cal_Bdd_t  g, 
  Cal_Bdd_t * resultBddPtr 
)
optional

Side Effects required

See Also optional
Defined in calQuant.c 

int 
CalOpXor(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  F, 
  Cal_Bdd_t  G, 
  Cal_Bdd_t * resultBddPtr 
)
optional

Side Effects required

See Also optional
Defined in calTerminal.c 

void 
CalPackNodes(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calHashTable.c 

CalAddress_t * 
CalPageManagerAllocPage(
  CalPageManager_t * pageManager 
)
optional

Side Effects required

See Also optional
Defined in calMemoryManagement.c 

void 
CalPageManagerFreePage(
  CalPageManager_t * pageManager, 
  CalAddress_t * page 
)
optional

Side Effects required

See Also optional
Defined in calMemoryManagement.c 

CalPageManager_t * 
CalPageManagerInit(
  int  numPagesPerSegment 
)
optional

Side Effects required

See Also optional
Defined in calMemoryManagement.c 

void 
CalPageManagerPrint(
  CalPageManager_t * pageManager 
)
optional

Side Effects required

See Also optional
Defined in calMemoryManagement.c 

int 
CalPageManagerQuit(
  CalPageManager_t * pageManager 
)
optional

Side Effects required

See Also optional
Defined in calMemoryManagement.c 

static void 
CalPerformaceTestSuperscalar(
  Cal_BddManager  bddManager, 
  Cal_Bdd * outputBddArray, 
  int  numFunctions 
)
optional

Side Effects required

See Also optional
Defined in calPerformanceTest.c 

static void 
CalPerformanceMemoryOverhead(
  Cal_BddManager  bddManager, 
  Cal_Bdd * outputBddArray, 
  int  numFunctions 
)
optional

Side Effects required

See Also optional
Defined in calPerformanceTest.c 

static void 
CalPerformanceTestAnd(
  Cal_BddManager  bddManager, 
  Cal_Bdd * outputBddArray, 
  int  numFunctions 
)
optional

Side Effects required

See Also optional
Defined in calPerformanceTest.c 

static void 
CalPerformanceTestCompose(
  Cal_BddManager  bddManager, 
  Cal_Bdd * outputBddArray, 
  int  numFunctions 
)
optional

Side Effects required

See Also optional
Defined in calPerformanceTest.c 

static void 
CalPerformanceTestMultiway(
  Cal_BddManager  bddManager, 
  Cal_Bdd * outputBddArray, 
  int  numFunctions 
)
optional

Side Effects required

See Also optional
Defined in calPerformanceTest.c 

static void 
CalPerformanceTestNonSuperscalar(
  Cal_BddManager  bddManager, 
  Cal_Bdd * outputBddArray, 
  int  numFunctions 
)
optional

Side Effects required

See Also optional
Defined in calPerformanceTest.c 

static void 
CalPerformanceTestOneway(
  Cal_BddManager  bddManager, 
  Cal_Bdd * outputBddArray, 
  int  numFunctions 
)
optional

Side Effects required

See Also optional
Defined in calPerformanceTest.c 

static void 
CalPerformanceTestQuantifyAllTogether(
  Cal_BddManager  bddManager, 
  Cal_Bdd * outputBddArray, 
  int  numFunctions, 
  int  bfZeroBFPlusDFOne, 
  int  cacheExistsResultsFlag, 
  int  cacheOrResultsFlag 
)
optional

Side Effects required

See Also optional
Defined in calPerformanceTest.c 

static void 
CalPerformanceTestRelProd(
  Cal_BddManager  bddManager, 
  Cal_Bdd * outputBddArray, 
  int  numFunctions, 
  int  bfZeroBFPlusDFOne, 
  int  cacheRelProdResultsFlag, 
  int  cacheAndResultsFlag, 
  int  cacheOrResultsFlag 
)
optional

Side Effects required

See Also optional
Defined in calPerformanceTest.c 

static void 
CalPerformanceTestSubstitute(
  Cal_BddManager  bddManager, 
  Cal_Bdd * outputBddArray, 
  int  numFunctions 
)
optional

Side Effects required

See Also optional
Defined in calPerformanceTest.c 

static void 
CalPerformanceTestSwapVars(
  Cal_BddManager  bddManager, 
  Cal_Bdd * outputBddArray, 
  int  numFunctions 
)
optional

Side Effects required

See Also optional
Defined in calPerformanceTest.c 

static void 
CalQuantifySanityCheck(
  Cal_BddManager  bddManager, 
  Cal_Bdd * outputBddArray, 
  int  numFunctions 
)
optional

Side Effects required

See Also optional
Defined in calPerformanceTest.c 

void 
CalReorderAssociationFix(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calAssociation.c 

static void 
CalRepackNodesAfterGC(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calGC.c 

void 
CalRequestNodeListArrayITE(
  Cal_BddManager_t * bddManager, 
  CalRequestNode_t ** requestNodeListArray 
)
This routine is to be used for pipelined and superscalar ITE operations. Currently there is no user interface provided to this routine.

Side Effects required

See Also optional
Defined in calBddITE.c 

void 
CalRequestNodeListArrayOp(
  Cal_BddManager_t * bddManager, 
  CalRequestNode_t ** requestNodeListArray, 
  CalOpProc_t  calOpProc 
)
Computes result BDDs for an array of lists, each entry of which is pair of pointers, each of which points to a operand BDD or an entry in another list with a smaller array index

Side Effects ThenBDD pointer of an entry is over written by the result BDD and ElseBDD pointer is marked using FORWARD_FLAG

Defined in calBddOp.c 

void 
CalRequestNodeListCompose(
  Cal_BddManager_t * bddManager, 
  CalRequestNode_t * requestNodeList, 
  Cal_BddIndex_t  composeIndex 
)
optional

Side Effects required

See Also optional
Defined in calBddCompose.c 

void 
CalSetInteract(
  Cal_BddManager_t * bddManager, 
  int  x, 
  int  y 
)
Given a pair of variables 0 <= x < y < table->size, sets the corresponding bit of the interaction matrix to 1.

Side Effects None

Defined in calInteract.c 

int 
CalTestInteract(
  Cal_BddManager_t * bddManager, 
  int  x, 
  int  y 
)
Given a pair of variables 0 <= x < y < bddManager->numVars, tests whether the corresponding bit of the interaction matrix is 1. Returns the value of the bit.

Side Effects None

Defined in calInteract.c 

int 
CalUniqueTableForIdFindOrAdd(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable, 
  Cal_Bdd_t  thenBdd, 
  Cal_Bdd_t  elseBdd, 
  Cal_Bdd_t * bddPtr 
)
optional

Side Effects If a new BDD node is created (found == false), then the numNodes field of the manager needs to be incremented.

See Also optional
Defined in calHashTable.c 

int 
CalUniqueTableForIdLookup(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable, 
  Cal_Bdd_t  thenBdd, 
  Cal_Bdd_t  elseBdd, 
  Cal_Bdd_t * bddPtr 
)
optional

Side Effects required

See Also optional
Defined in calHashTable.c 

void 
CalUniqueTableForIdRehashNode(
  CalHashTable_t * hashTable, 
  CalBddNode_t * bddNode, 
  CalBddNode_t * thenBddNode, 
  CalBddNode_t * elseBddNode 
)
optional

Side Effects required

See Also optional
Defined in calHashTable.c 

void 
CalUniqueTablePrint(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calUtil.c 

void 
CalVarAssociationRepackUpdate(
  Cal_BddManager_t * bddManager, 
  Cal_BddId_t  id 
)
optional

Side Effects required

See Also optional
Defined in calAssociation.c 

int 
Cal_AssociationInit(
  Cal_BddManager  bddManager, 
  Cal_Bdd * associationInfoUserBdds, 
  int  pairs 
)
Creates or finds a variable association. The association is specified by associationInfo, which is a an array of BDD with Cal_BddNull(bddManager) as the end marker. If pairs is 0, the array is assumed to be an array of variables. In this case, each variable is paired with constant BDD one. Such an association may viewed as specifying a set of variables for use with routines such as Cal_BddExists. If pair is not 0, then the even numbered array elements should be variables and the odd numbered elements should be the BDDs which they are mapped to. In both cases, the return value is an integer identifier for this association. If the given association is equivalent to one which already exists, the same identifier is used for both, and the reference count of the association is increased by one.

Side Effects None

See Also Cal_AssociationQuit
Defined in calAssociation.c 

void 
Cal_AssociationQuit(
  Cal_BddManager  bddManager, 
  int  associationId 
)
Decrements the reference count of the variable association with identifier id, and frees it if the reference count becomes zero.

Side Effects None

See Also Cal_AssociationInit
Defined in calAssociation.c 

int 
Cal_AssociationSetCurrent(
  Cal_BddManager  bddManager, 
  int  associationId 
)
Sets the current variable association to the one given by id and returns the ID of the old association. An id of -1 indicates the temporary association

Side Effects None

Defined in calAssociation.c 

Cal_Bdd 
Cal_BddAnd(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  Cal_Bdd  gUserBdd 
)
Returns the BDD for logical AND of f and g

Side Effects None

Defined in calBddOp.c 

Cal_Bdd 
Cal_BddBetween(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fMinUserBdd, 
  Cal_Bdd  fMaxUserBdd 
)
Returns a minimal BDD f which is contains fMin and is contained in fMax ( fMin <= f <= fMax). This operation is typically used in state space searches to simplify the representation for the set of states wich will be expanded at each step (Rk Rk-1' <= f <= Rk).

Side Effects None

See Also Cal_BddReduce
Defined in calReduce.c 

Cal_Bdd 
Cal_BddCofactor(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  Cal_Bdd  cUserBdd 
)
Returns the generalized cofactor of BDD f with respect to BDD c. The constrain operator given by Coudert et al (ICCAD90) is used to find the generalized cofactor.

Side Effects None.

See Also Cal_BddReduce
Defined in calReduce.c 

Cal_Bdd 
Cal_BddCompose(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  Cal_Bdd  gUserBdd, 
  Cal_Bdd  hUserBdd 
)
Returns the BDD obtained by substituting a variable by a function

Side Effects None

Defined in calBddCompose.c 

int 
Cal_BddDependsOn(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  Cal_Bdd  varUserBdd 
)
Returns 1 if f depends on var and returns 0 otherwise.

Side Effects None

Defined in calBddSupport.c 

int 
Cal_BddDumpBdd(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  Cal_Bdd * userVars, 
  FILE * fp 
)
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.

Side Effects required

See Also optional
Defined in calDump.c 

void 
Cal_BddDynamicReordering(
  Cal_BddManager  bddManager, 
  int  technique 
)
Selects the method for dynamic reordering.

Side Effects None

See Also Cal_BddReorder
Defined in cal.c 

Cal_Bdd 
Cal_BddElse(
  Cal_BddManager  bddManager, 
  Cal_Bdd  userBdd 
)
Returns the negative cofactor of the argument BDD with respect to the top variable of the BDD.

Side Effects The reference count of the returned BDD is increased by 1.

See Also Cal_BddThen
Defined in cal.c 

Cal_Bdd 
Cal_BddExists(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd 
)
Returns the BDD for f with all the variables that are paired with something in the current variable association existentially quantified out.

Side Effects None.

See Also Cal_BddRelProd
Defined in calQuant.c 

Cal_Bdd 
Cal_BddForAll(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd 
)
Returns the BDD for f with all the variables that are paired with something in the current variable association universally quantified out.

Side Effects None.

Defined in calQuant.c 

void 
Cal_BddFree(
  Cal_BddManager  bddManager, 
  Cal_Bdd  userBdd 
)
Frees the argument BDD. It is an error to free a BDD more than once.

Side Effects The reference count of the argument BDD is decreased by 1.

See Also Cal_BddUnFree
Defined in cal.c 

void 
Cal_BddFunctionPrint(
  Cal_BddManager  bddManager, 
  Cal_Bdd  userBdd, 
  char * name 
)
Prints the function implemented by the argument BDD

Side Effects None

Defined in calUtil.c 

void 
Cal_BddFunctionProfileMultiple(
  Cal_BddManager  bddManager, 
  Cal_Bdd * fUserBddArray, 
  long * funcCounts 
)
optional

Side Effects None

See Also optional
Defined in calBddSize.c 

void 
Cal_BddFunctionProfile(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  long * funcCounts 
)
The nth entry of the function profile array is the number of subfunctions of f which may be obtained by restricting the variables whose index is less than n. An entry of zero indicates that f is independent of the variable with the corresponding index.

See Also optional
Defined in calBddSize.c 

Cal_BddId_t 
Cal_BddGetIfId(
  Cal_BddManager  bddManager, 
  Cal_Bdd  userBdd 
)
Returns the id of the top variable of the argument BDD.

Side Effects None

See Also Cal_BddGetIfIndex
Defined in cal.c 

Cal_BddId_t 
Cal_BddGetIfIndex(
  Cal_BddManager  bddManager, 
  Cal_Bdd  userBdd 
)
Returns the index of the top variable of the argument BDD.

Side Effects None

See Also Cal_BddGetIfId
Defined in cal.c 

Cal_Bdd 
Cal_BddGetRegular(
  Cal_BddManager  bddManager, 
  Cal_Bdd  userBdd 
)
Returns a BDD with positive from a given BDD with arbitrary phase

Side Effects None.

Defined in cal.c 

Cal_Bdd 
Cal_BddITE(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  Cal_Bdd  gUserBdd, 
  Cal_Bdd  hUserBdd 
)
Returns the BDD for logical If-Then-Else Description [Returns the BDD for the logical operation IF f THEN g ELSE h - f g + f' h

Side Effects None

See Also Cal_BddAnd Cal_BddNand Cal_BddOr Cal_BddNor Cal_BddXor Cal_BddXnor
Defined in calBddITE.c 

Cal_Bdd 
Cal_BddIdentity(
  Cal_BddManager  bddManager, 
  Cal_Bdd  userBdd 
)
Returns the duplicate BDD of the argument BDD.

Side Effects The reference count of the BDD is increased by 1.

See Also Cal_BddNot
Defined in cal.c 

Cal_Bdd 
Cal_BddIf(
  Cal_BddManager  bddManager, 
  Cal_Bdd  userBdd 
)
Returns the BDD corresponding to the top variable of the argument BDD.

Side Effects None.

Defined in cal.c 

Cal_Bdd 
Cal_BddImplies(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  Cal_Bdd  gUserBdd 
)
Computes a BDD that implies conjunction of f and Cal_BddNot(g)

Side Effects none

See Also Cal_BddIntersects
Defined in cal.c 

Cal_Bdd 
Cal_BddIntersects(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  Cal_Bdd  gUserBdd 
)
Computes a BDD that implies conjunction of f and g.

Side Effects None

See Also Cal_BddImplies
Defined in cal.c 

int 
Cal_BddIsBddConst(
  Cal_BddManager  bddManager, 
  Cal_Bdd  userBdd 
)
Returns 1 if the argument BDD is either constant one or constant zero, otherwise returns 0.

Side Effects None.

See Also Cal_BddIsBddOne Cal_BddIsBddZero
Defined in cal.c 

int 
Cal_BddIsBddNull(
  Cal_BddManager  bddManager, 
  Cal_Bdd  userBdd 
)
Returns 1 if the argument BDD is NULL, 0 otherwise.

Side Effects None.

Defined in cal.c 

int 
Cal_BddIsBddOne(
  Cal_BddManager  bddManager, 
  Cal_Bdd  userBdd 
)
Returns 1 if the argument BDD is constant one, 0 otherwise.

Side Effects None.

See Also Cal_BddIsBddZero
Defined in cal.c 

int 
Cal_BddIsBddZero(
  Cal_BddManager  bddManager, 
  Cal_Bdd  userBdd 
)
Returns 1 if the argument BDD is constant zero, 0 otherwise.

Side Effects None.

See Also Cal_BddIsBddOne
Defined in cal.c 

int 
Cal_BddIsCube(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd 
)
Returns 1 if the argument BDD is a cube, 0 otherwise

Side Effects None

Defined in cal.c 

int 
Cal_BddIsEqual(
  Cal_BddManager  bddManager, 
  Cal_Bdd  userBdd1, 
  Cal_Bdd  userBdd2 
)
Returns 1 if argument BDDs are equal, 0 otherwise.

Side Effects None.

Defined in cal.c 

int 
Cal_BddIsProvisional(
  Cal_BddManager  bddManager, 
  Cal_Bdd  userBdd 
)
Returns 1, if the given user BDD contains provisional BDD node.

Side Effects None.

Defined in calPipeline.c 

Cal_Bdd 
Cal_BddManagerCreateNewVarAfter(
  Cal_BddManager  bddManager, 
  Cal_Bdd  userBdd 
)
Creates and returns a new variable after the specified one in the variable order.

Side Effects None

Defined in calBddManager.c 

Cal_Bdd 
Cal_BddManagerCreateNewVarBefore(
  Cal_BddManager  bddManager, 
  Cal_Bdd  userBdd 
)
Creates and returns a new variable before the specified one in the variable order.

Side Effects None

Defined in calBddManager.c 

Cal_Bdd 
Cal_BddManagerCreateNewVarFirst(
  Cal_BddManager  bddManager 
)
Creates and returns a new variable at the start of the variable order.

Side Effects None

Defined in calBddManager.c 

Cal_Bdd 
Cal_BddManagerCreateNewVarLast(
  Cal_BddManager  bddManager 
)
Creates and returns a new variable at the end of the variable order.

Side Effects None

Defined in calBddManager.c 

int 
Cal_BddManagerGC(
  Cal_BddManager  bddManager 
)
For each variable in the increasing id free nodes with reference count equal to zero freeing a node results in decrementing reference count of then and else nodes by one.

Side Effects None.

Defined in calGC.c 

void * 
Cal_BddManagerGetHooks(
  Cal_BddManager  bddManager 
)
Returns the hooks field of the manager.

Side Effects None

Defined in cal.c 

unsigned long 
Cal_BddManagerGetNumNodes(
  Cal_BddManager  bddManager 
)
Returns the number of BDD nodes

Side Effects None

See Also Cal_BddTotalSize
Defined in calBddManager.c 

Cal_Bdd 
Cal_BddManagerGetVarWithId(
  Cal_BddManager  bddManager, 
  Cal_BddId_t  id 
)
Returns the variable with the specified id, null if no such variable exists

Side Effects None

See Also optional
Defined in calBddManager.c 

Cal_Bdd 
Cal_BddManagerGetVarWithIndex(
  Cal_BddManager  bddManager, 
  Cal_BddIndex_t  index 
)
Returns the variable with the specified index, null if no such variable exists

Side Effects None

Defined in calBddManager.c 

Cal_BddManager 
Cal_BddManagerInit(
    
)
Initializes and allocates fields of the BDD manager. Some of the fields are initialized for maxNumVars+1 or numVars+1, whereas some of them are initialized for maxNumVars or numVars. The first kind of fields are associated with the id of a variable and the second ones are with the index of the variable.

Side Effects None

See Also Cal_BddManagerQuit
Defined in calBddManager.c 

int 
Cal_BddManagerQuit(
  Cal_BddManager  bddManager 
)
Frees the BDD manager and all the associated allocations

Side Effects None

See Also Cal_BddManagerInit
Defined in calBddManager.c 

void 
Cal_BddManagerSetGCLimit(
  Cal_BddManager  manager 
)
It tries to set the limit at twice the number of nodes in the manager at the current point. However, the limit is not allowed to fall below the MIN_GC_LIMIT or to exceed the value of node limit (if one exists).

Side Effects None.

Defined in calGC.c 

void 
Cal_BddManagerSetHooks(
  Cal_BddManager  bddManager, 
  void * hooks 
)
Sets the hooks field of the manager.

Side Effects Hooks field changes.

Defined in cal.c 

void 
Cal_BddManagerSetParameters(
  Cal_BddManager  bddManager, 
  long  reorderingThreshold, 
  long  maxForwardedNodes, 
  double  repackAfterGCThreshold, 
  double  tableRepackThreshold 
)
This function is used to set the parameters which are used to control the reordering process. "reorderingThreshold" determines the number of nodes below which reordering will NOT be invoked, "maxForwardedNodes" determines the maximum number of forwarded nodes which are allowed (at that point the cleanup must be done), and "repackingThreshold" determines the fraction of the page utilized below which repacking has to be invoked. These parameters have different affect on the computational and memory usage aspects of reordeing. For instance, higher value of "maxForwardedNodes" will result in process consuming more memory, and a lower value on the other hand would invoke the cleanup process repeatedly resulting in increased computation.

Side Effects None

Defined in calBddManager.c 

Cal_Bdd 
Cal_BddMultiwayAnd(
  Cal_BddManager  bddManager, 
  Cal_Bdd * userBddArray 
)
Returns the BDD for logical AND of set of BDDs in the bddArray

Side Effects None

Defined in calBddOp.c 

Cal_Bdd 
Cal_BddMultiwayOr(
  Cal_BddManager  bddManager, 
  Cal_Bdd * userBddArray 
)
Returns the BDD for logical OR of set of BDDs in the bddArray

Side Effects None

Defined in calBddOp.c 

Cal_Bdd 
Cal_BddMultiwayXor(
  Cal_BddManager  bddManager, 
  Cal_Bdd * userBddArray 
)
Returns the BDD for logical XOR of set of BDDs in the bddArray

Side Effects None

Defined in calBddOp.c 

Cal_Bdd 
Cal_BddNand(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  Cal_Bdd  gUserBdd 
)
Returns the BDD for logical NAND of f and g

Side Effects None

Defined in calBddOp.c 

Cal_Block 
Cal_BddNewVarBlock(
  Cal_BddManager  bddManager, 
  Cal_Bdd  variable, 
  long  length 
)
The block is specified by passing the first variable and the length of the block. The "length" number of consecutive variables starting from "variable" are put in the block.

Side Effects A new block is created.

Defined in calBlk.c 

long 
Cal_BddNodeLimit(
  Cal_BddManager  bddManager, 
  long  newLimit 
)
Sets the node limit to new_limit and returns the old limit.

Side Effects Threshold for garbage collection may change

See Also Cal_BddManagerGC
Defined in cal.c 

Cal_Bdd 
Cal_BddNor(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  Cal_Bdd  gUserBdd 
)
Returns the BDD for logical NOR of f and g

Side Effects None

Defined in calBddOp.c 

Cal_Bdd 
Cal_BddNot(
  Cal_BddManager  bddManager, 
  Cal_Bdd  userBdd 
)
Returns the complement of the argument BDD.

Side Effects The reference count of the argument BDD is increased by 1.

See Also Cal_BddIdentity
Defined in cal.c 

Cal_Bdd 
Cal_BddOne(
  Cal_BddManager  bddManager 
)
Returns the BDD for the constant one

Side Effects None

See Also Cal_BddZero
Defined in cal.c 

Cal_Bdd 
Cal_BddOr(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  Cal_Bdd  gUserBdd 
)
Returns the BDD for logical OR of f and g

Side Effects None

Defined in calBddOp.c 

int 
Cal_BddOverflow(
  Cal_BddManager  bddManager 
)
Returns 1 if the node limit has been exceeded, 0 otherwise. The overflow flag is cleared.

Side Effects None

See Also Cal_BddNodeLimit
Defined in cal.c 

Cal_Bdd * 
Cal_BddPairwiseAnd(
  Cal_BddManager  bddManager, 
  Cal_Bdd * userBddArray 
)
Returns an array of BDDs obtained by logical AND of BDD pairs specified by an BDD array in which a BDD at an even location is paired with a BDD at an odd location of the array

Side Effects None

See Also Cal_BddPairwiseOr
Defined in calBddOp.c 

Cal_Bdd * 
Cal_BddPairwiseOr(
  Cal_BddManager  bddManager, 
  Cal_Bdd * userBddArray 
)
Returns an array of BDDs obtained by logical OR of BDD pairs specified by an BDD array in which a BDD at an even location is paired with a BDD at an odd location of the array

Side Effects None

See Also Cal_BddPairwiseAnd
Defined in calBddOp.c 

Cal_Bdd * 
Cal_BddPairwiseXor(
  Cal_BddManager  bddManager, 
  Cal_Bdd * userBddArray 
)
Returns an array of BDDs obtained by logical XOR of BDD pairs specified by an BDD array in which a BDD at an even location is paired with a BDD at an odd location of the array

Side Effects None

See Also Cal_BddPairwiseAnd
Defined in calBddOp.c 

void 
Cal_BddPrintBdd(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  Cal_VarNamingFn_t  VarNamingFn, 
  Cal_TerminalIdFn_t  TerminalIdFn, 
  Cal_Pointer_t  env, 
  FILE * fp 
)
Prints a human-readable representation of the BDD f to the file given by fp. The namingFn should be a pointer to a function taking a bddManager, a BDD and the pointer given by env. This function should return either a null pointer or a srting that is the name of the supplied variable. If it returns a null pointer, a default name is generated based on the index of the variable. It is also legal for naminFN to e null; in this case, default names are generated for all variables. The macro bddNamingFnNone is a null pointer of suitable type. terminalIdFn should be apointer to a function taking a bddManager and two longs. plus the pointer given by the env. It should return either a null pointer. If it returns a null pointer, or if terminalIdFn is null, then default names are generated for the terminals. The macro bddTerminalIdFnNone is a null pointer of suitable type.

Side Effects None.

Defined in calPrint.c 

void 
Cal_BddPrintFunctionProfileMultiple(
  Cal_BddManager  bddManager, 
  Cal_Bdd * userBdds, 
  Cal_VarNamingFn_t  varNamingProc, 
  char * env, 
  int  lineLength, 
  FILE * fp 
)
optional

Side Effects None

See Also optional
Defined in calPrintProfile.c 

void 
Cal_BddPrintFunctionProfile(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f, 
  Cal_VarNamingFn_t  varNamingProc, 
  char * env, 
  int  lineLength, 
  FILE * fp 
)
optional

Side Effects None

See Also optional
Defined in calPrintProfile.c 

void 
Cal_BddPrintProfileMultiple(
  Cal_BddManager  bddManager, 
  Cal_Bdd * userBdds, 
  Cal_VarNamingFn_t  varNamingProc, 
  char * env, 
  int  lineLength, 
  FILE * fp 
)
optional

Side Effects None

See Also optional
Defined in calPrintProfile.c 

void 
Cal_BddPrintProfile(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  Cal_VarNamingFn_t  varNamingProc, 
  char * env, 
  int  lineLength, 
  FILE * fp 
)
optional

Side Effects None

See Also optional
Defined in calPrintProfile.c 

void 
Cal_BddProfileMultiple(
  Cal_BddManager  bddManager, 
  Cal_Bdd * fUserBddArray, 
  long * levelCounts, 
  int  negout 
)
optional

Side Effects None

See Also optional
Defined in calBddSize.c 

void 
Cal_BddProfile(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  long * levelCounts, 
  int  negout 
)
negout is as in Cal_BddSize. levelCounts should be an array of size Cal_BddVars(bddManager)+1 to hold the profile.

Side Effects None

See Also optional
Defined in calBddSize.c 

Cal_Bdd 
Cal_BddReduce(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  Cal_Bdd  cUserBdd 
)
Returns a BDD which agrees with f for all valuations which satisfy c. The result is usually smaller in terms of number of BDD nodes than f. This operation is typically used in state space searches to simplify the representation for the set of states wich will be expanded at each step.

Side Effects None

See Also Cal_BddCofactor
Defined in calReduce.c 

Cal_Bdd 
Cal_BddRelProd(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  Cal_Bdd  gUserBdd 
)
Returns the BDD for the logical AND of f and g with all the variables that are paired with something in the current variable association existentially quantified out.

Side Effects None.

Defined in calQuant.c 

void 
Cal_BddReorder(
  Cal_BddManager  bddManager 
)
Invoke the current dynamic reodering method.

Side Effects Index of a variable may change due to reodering

See Also Cal_BddDynamicReordering
Defined in cal.c 

Cal_Bdd 
Cal_BddSatisfySupport(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd 
)
The returned BDD which implies f, is true for some valuation on which f is true, which has at most one node at each level, and which has exactly one node corresponding to each variable which is associated with something in the current variable association.

Side Effects required

See Also optional
Defined in calBddSatisfy.c 

double 
Cal_BddSatisfyingFraction(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd 
)
optional

Side Effects required

See Also optional
Defined in calBddSatisfy.c 

Cal_Bdd 
Cal_BddSatisfy(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd 
)
optional

Side Effects required

See Also optional
Defined in calBddSatisfy.c 

void 
Cal_BddSetGCMode(
  Cal_BddManager  bddManager, 
  int  gcMode 
)
Sets the garbage collection mode, 0 means the garbage collection should be turned off, 1 means garbage collection should be on.

Side Effects None.

Defined in calGC.c 

long 
Cal_BddSizeMultiple(
  Cal_BddManager  bddManager, 
  Cal_Bdd * fUserBddArray, 
  int  negout 
)
optional

Side Effects None

See Also optional
Defined in calBddSize.c 

long 
Cal_BddSize(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  int  negout 
)
optional

Side Effects None

See Also optional
Defined in calBddSize.c 

void 
Cal_BddStats(
  Cal_BddManager  bddManager, 
  FILE * fp 
)
Prints miscellaneous BDD statistics

Side Effects None

Defined in cal.c 

Cal_Bdd 
Cal_BddSubstitute(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd 
)
Returns a BDD for f using the substitution defined by current variable association. Each variable is replaced by its associated BDDs. The substitution is effective simultaneously

Side Effects None

See Also Cal_BddCompose
Defined in calBddSubstitute.c 

void 
Cal_BddSupport(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  Cal_Bdd * support 
)
optional

Side Effects None

See Also optional
Defined in calBddSupport.c 

Cal_Bdd 
Cal_BddSwapVars(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  Cal_Bdd  gUserBdd, 
  Cal_Bdd  hUserBdd 
)
Returns the BDD obtained by simultaneously substituting variable g by variable h and variable h and variable g in the BDD f

Side Effects None

See Also Cal_BddSubstitute
Defined in calBddSwapVars.c 

Cal_Bdd 
Cal_BddThen(
  Cal_BddManager  bddManager, 
  Cal_Bdd  userBdd 
)
Returns the positive cofactor of the argument BDD with respect to the top variable of the BDD.

Side Effects The reference count of the returned BDD is increased by 1.

See Also Cal_BddElse
Defined in cal.c 

unsigned long 
Cal_BddTotalSize(
  Cal_BddManager  bddManager 
)
Returns the number of nodes in the Unique table

Side Effects None

See Also Cal_BddManagerGetNumNodes
Defined in cal.c 

int 
Cal_BddType(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd 
)
Returns BDD_TYPE_ZERO if f is false, BDD_TYPE_ONE if f is true, BDD_TYPE_POSVAR is f is an unnegated variable, BDD_TYPE_NEGVAR if f is a negated variable, BDD_TYPE_OVERFLOW if f is null, and BDD_TYPE_NONTERMINAL otherwise.

Side Effects None

Defined in cal.c 

void 
Cal_BddUnFree(
  Cal_BddManager  bddManager, 
  Cal_Bdd  userBdd 
)
Unfrees the argument BDD. It is an error to pass a BDD with reference count of zero to be unfreed.

Side Effects The reference count of the argument BDD is increased by 1.

See Also Cal_BddFree
Defined in cal.c 

Cal_Bdd 
Cal_BddUndumpBdd(
  Cal_BddManager  bddManager, 
  Cal_Bdd * userVars, 
  FILE * fp, 
  int * error 
)
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

Side Effects required

See Also optional
Defined in calDump.c 

void 
Cal_BddVarBlockReorderable(
  Cal_BddManager  bddManager, 
  Cal_Block  block, 
  int  reorderable 
)
If a block is reorderable, the child blocks are recursively involved in swapping.

Side Effects None.

Defined in calBlk.c 

Cal_Bdd 
Cal_BddVarSubstitute(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd 
)
Returns a BDD for f using the substitution defined by current variable association. It is assumed that each variable is replaced by another variable. For the substitution of a variable by a function, use Cal_BddSubstitute instead.

Side Effects None

See Also Cal_BddSubstitute
Defined in calBddVarSubstitute.c 

long 
Cal_BddVars(
  Cal_BddManager  bddManager 
)
Returns the number of BDD variables

Side Effects None

Defined in cal.c 

Cal_Bdd 
Cal_BddXnor(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  Cal_Bdd  gUserBdd 
)
Returns the BDD for logical exclusive NOR of f and g

Side Effects None

Defined in calBddOp.c 

Cal_Bdd 
Cal_BddXor(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  Cal_Bdd  gUserBdd 
)
Returns the BDD for logical exclusive OR of f and g

Side Effects None

Defined in calBddOp.c 

Cal_Bdd 
Cal_BddZero(
  Cal_BddManager  bddManager 
)
Returns the BDD for the constant zero

Side Effects None

See Also Cal_BddOne
Defined in cal.c 

Cal_Address_t 
Cal_MemAllocation(
    
)
Returns the memory allocated.

Side Effects required

See Also optional
Defined in calMem.c 

void 
Cal_MemFatal(
  char * message 
)
Prints an error message and exits.

Side Effects required

See Also optional
Defined in calMem.c 

void 
Cal_MemFreeBlock(
  Cal_Pointer_t  p 
)
Frees the block.

Side Effects required

See Also optional
Defined in calMem.c 

void 
Cal_MemFreeRecMgr(
  Cal_RecMgr  mgr 
)
Frees all the storage associated with the specified record manager.

Side Effects required

See Also optional
Defined in calMem.c 

void 
Cal_MemFreeRec(
  Cal_RecMgr  mgr, 
  Cal_Pointer_t  rec 
)
Frees a record managed by the indicated record manager.

Side Effects required

See Also optional
Defined in calMem.c 

Cal_Pointer_t 
Cal_MemGetBlock(
  Cal_Address_t  size 
)
Allocates a new block of the specified size.

Side Effects required

See Also optional
Defined in calMem.c 

Cal_RecMgr 
Cal_MemNewRecMgr(
  int  size 
)
Creates a new record manager with the given record size.

Side Effects required

See Also optional
Defined in calMem.c 

Cal_Pointer_t 
Cal_MemNewRec(
  Cal_RecMgr  mgr 
)
Allocates a record from the specified record manager.

Side Effects required

See Also optional
Defined in calMem.c 

Cal_Pointer_t 
Cal_MemResizeBlock(
  Cal_Pointer_t  p, 
  Cal_Address_t  newSize 
)
Expands or contracts the block to a new size. We try to avoid moving the block if possible.

Side Effects required

See Also optional
Defined in calMem.c 

int 
Cal_PerformanceTest(
  Cal_BddManager  bddManager, 
  Cal_Bdd * outputBddArray, 
  int  numFunctions, 
  int  iteration, 
  int  seed, 
  int  andPerformanceFlag, 
  int  multiwayPerformanceFlag, 
  int  onewayPerformanceFlag, 
  int  quantifyPerformanceFlag, 
  int  composePerformanceFlag, 
  int  relprodPerformanceFlag, 
  int  swapPerformanceFlag, 
  int  substitutePerformanceFlag, 
  int  sanityCheckFlag, 
  int  computeMemoryOverheadFlag, 
  int  superscalarFlag 
)
optional

Side Effects required

See Also optional
Defined in calPerformanceTest.c 

Cal_Bdd 
Cal_PipelineCreateProvisionalBdd(
  Cal_BddManager  bddManager, 
  Cal_Bdd  fUserBdd, 
  Cal_Bdd  gUserBdd 
)
The provisional BDD is automatically freed once the pipeline is quitted.

Defined in calPipeline.c 

int 
Cal_PipelineExecute(
  Cal_BddManager  bddManager 
)
All the results are computed. User should update the BDDs of interest. Eventually this feature would become transparent.

Side Effects required

See Also optional
Defined in calPipeline.c 

int 
Cal_PipelineInit(
  Cal_BddManager  bddManager, 
  Cal_BddOp_t  bddOp 
)
All the operations for this pipeline must be of the same kind.

Side Effects None.

Defined in calPipeline.c 

void 
Cal_PipelineQuit(
  Cal_BddManager  bddManager 
)
The user must make sure to update all provisional BDDs of interest before calling this routine.

Defined in calPipeline.c 

void 
Cal_PipelineSetDepth(
  Cal_BddManager  bddManager, 
  int  depth 
)
The "depth" determines the amount of dependency we would allow in pipelined computation.

Side Effects None.

Defined in calPipeline.c 

Cal_Bdd 
Cal_PipelineUpdateProvisionalBdd(
  Cal_BddManager  bddManager, 
  Cal_Bdd  provisionalBdd 
)
The provisional BDD is automatically freed after quitting pipeline.

Defined in calPipeline.c 

void 
Cal_TempAssociationAugment(
  Cal_BddManager  bddManager, 
  Cal_Bdd * associationInfoUserBdds, 
  int  pairs 
)
Pairs is 0 if the information represents only a list of variables rather than a full association.

Side Effects None

Defined in calAssociation.c 

void 
Cal_TempAssociationInit(
  Cal_BddManager  bddManager, 
  Cal_Bdd * associationInfoUserBdds, 
  int  pairs 
)
Pairs is 0 if the information represents only a list of variables rather than a full association.

Side Effects None

Defined in calAssociation.c 

void 
Cal_TempAssociationQuit(
  Cal_BddManager  bddManager 
)
Cleans up temporary associationoptional

Side Effects None

Defined in calAssociation.c 

static int 
CeilLog2(
  int  number 
)
Returns the smallest integer greater than or equal to log2 of a number (The assumption is that the number is >= 1)

Side Effects None

Defined in calBddOp.c 

static int 
CeilLog2(
  int  number 
)
Returns the smallest integer greater than or equal to log2 of a number (The assumption is that the number is >= 1)

Side Effects None

Defined in calGC.c 

static int 
CeilLog2(
  int  number 
)
Returns the smallest integer greater than or equal to log2 of a number (The assumption is that the number is >= 1)

Side Effects None

Defined in calHashTable.c 

static int 
CeilLog2(
  int  number 
)
Returns the smallest integer greater than or equal to log2 of a number (The assumption is that the number is >= 1)

Side Effects None

Defined in calReorderDF.c 

static int 
CeilingLog2(
  Cal_Address_t  i 
)
optional

Side Effects required

See Also optional
Defined in calMem.c 

static void 
Chars(
  char  c, 
  int  n, 
  FILE * fp 
)
optional

Side Effects required

See Also optional
Defined in calPrint.c 

static int 
CheckAssoc(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd * assocInfo, 
  int  pairs 
)
optional

Side Effects required

See Also optional
Defined in calAssociation.c 

static int 
CheckValidityOfNodes(
  Cal_BddManager_t * bddManager, 
  long  id 
)
optional

Side Effects required

See Also optional
Defined in calReorderDF.c 

static int 
CofactorFixAndReclaimForwardedNodes(
  Cal_BddManager_t * bddManager, 
  int  cofactorCheckStartIndex, 
  int  cofactorCheckEndIndex, 
  int  reclaimStartIndex, 
  int  reclaimEndIndex 
)
optional

Side Effects required

See Also optional
Defined in calReorderBF.c 

static TruthTable_t 
Cofactor(
  TruthTable_t  table, 
  int  var, 
  int  value 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static Cal_Bdd 
Decode(
  int  var, 
  TruthTable_t  table 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
Error(
  char * op, 
  Cal_BddManager  bddManager, 
  Cal_Bdd  result, 
  Cal_Bdd  expected, 
    
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
GetRandomNumbers(
  int  lowerBound, 
  int  upperBound, 
  int  count, 
  int * resultVector 
)
The restriction is that count <= upperBound-lowerBound+1. The size of the resultVector should be >= count.

Side Effects required

See Also optional
Defined in calPerformanceTest.c 

static void 
HashTableAddDirect(
  CalHashTable_t * hashTable, 
  CalBddNode_t * bddNode 
)
optional

Side Effects required

See Also optional
Defined in calReorderDF.c 

static void 
HashTableApply(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable, 
  CalHashTable_t ** reqQueAtPipeDepth, 
  CalOpProc_t  calOpProc, 
  unsigned long  opCode 
)
optional

Side Effects required

See Also optional
Defined in calQuant.c 

static void 
HashTableCofactorApply(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable, 
  CalHashTable_t ** cofactorHashTableArray, 
  CalOpProc_t  calOpProc 
)
optional

Side Effects required

See Also optional
Defined in calReduce.c 

static void 
HashTableCofactorReduce(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable, 
  CalHashTable_t * uniqueTableForId 
)
optional

Side Effects required

See Also optional
Defined in calReduce.c 

static int 
HashTableFindOrAdd(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable, 
  CalBddNode_t * thenBdd, 
  CalBddNode_t * elseBdd, 
  CalBddNode_t ** bddPtr 
)
optional

Side Effects required

See Also optional
Defined in calReorderDF.c 

static void 
HashTableOneRehash(
  CalHashTable_t * hashTable, 
  int  grow 
)
optional

Side Effects required

See Also optional
Defined in calHashTableOne.c 

static void 
HashTableReduceApply(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable, 
  CalHashTable_t ** reduceHashTableArray, 
  CalHashTable_t ** orHashTableArray, 
  CalOpProc_t  calOpProc 
)
optional

Side Effects required

See Also optional
Defined in calReduce.c 

static void 
HashTableReduce(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable, 
  CalHashTable_t * uniqueTableForId 
)
optional

Side Effects required

See Also optional
Defined in calQuant.c 

static int 
IndexCmp(
  const void * p1, 
  const void * p2 
)
optional

Side Effects required

See Also optional
Defined in calBddSatisfy.c 

static void 
MergeAndFree(
  Block  b 
)
MergeAndFree(b) repeatedly merges b its Buddy until b has no Buddy or the Buddy isn't free, then adds the result to the appropriate free list.

Side Effects required

See Also optional
Defined in calMem.c 

static CalAddress_t * 
PageAlign(
  CalAddress_t * p 
)
optional

See Also optional
Defined in calMemoryManagement.c 

static int 
PageManagerExpandStorage(
  CalPageManager_t * pageManager 
)
optional

Side Effects The size of the segment is stored in one of the fields of page manager - numPagesPerSegment. If a memory segment of a specific size cannot be allocated, the routine calls itself recursively by reducing numPagesPerSegment by a factor of 2.

See Also optional
Defined in calMemoryManagement.c 

static void 
PrintBddProfileAfterReorder(
  Cal_BddManager_t * bddManager 
)
optional

Side Effects required

See Also optional
Defined in calReorderBF.c 

static void 
PrintBdd(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
RandomTests(
  int  numVars, 
  int  iterations 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

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

Side Effects required

See Also optional
Defined in calDump.c 

static Block 
RemoveFromFreeList(
  Block  b 
)
RemoveFromFreeList(b) removes b from the free list which it is on.

Side Effects required

See Also optional
Defined in calMem.c 

static int 
SegmentToPageList(
  CalAddress_t * segment, 
  int  numPages, 
  CalAddress_t * lastPointer 
)
optional

See Also optional
Defined in calMemoryManagement.c 

static void 
SweepVarTable(
  Cal_BddManager_t * bddManager, 
  long  id 
)
optional

Side Effects required

See Also optional
Defined in calReorderDF.c 

static void 
TestAnd(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f1, 
  TruthTable_t  table1, 
  Cal_Bdd  f2, 
  TruthTable_t  table2 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestArrayOp(
  Cal_BddManager  bddManager, 
  int  numBdds 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestAssoc(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f, 
  TruthTable_t  table 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestCompose(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f1, 
  TruthTable_t  table1, 
  Cal_Bdd  f2, 
  TruthTable_t  table2 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestDump(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestGenCof(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f1, 
  TruthTable_t  table1, 
  Cal_Bdd  f2, 
  TruthTable_t  table2 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestITE(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f1, 
  TruthTable_t  table1, 
  Cal_Bdd  f2, 
  TruthTable_t  table2, 
  Cal_Bdd  f3, 
  TruthTable_t  table3 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestIdNot(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f, 
  TruthTable_t  table 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestInterImpl(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f1, 
  TruthTable_t  table1, 
  Cal_Bdd  f2, 
  TruthTable_t  table2 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestMultiwayAnd(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f1, 
  TruthTable_t  table1, 
  Cal_Bdd  f2, 
  TruthTable_t  table2, 
  Cal_Bdd  f3, 
  TruthTable_t  table3 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestMultiwayLarge(
  Cal_BddManager  bddManager, 
  int  numBdds 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestMultiwayOr(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f1, 
  TruthTable_t  table1, 
  Cal_Bdd  f2, 
  TruthTable_t  table2, 
  Cal_Bdd  f3, 
  TruthTable_t  table3 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestNand(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f1, 
  TruthTable_t  table1, 
  Cal_Bdd  f2, 
  TruthTable_t  table2 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestOr(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f1, 
  TruthTable_t  table1, 
  Cal_Bdd  f2, 
  TruthTable_t  table2 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestPipeline(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f1, 
  TruthTable_t  table1, 
  Cal_Bdd  f2, 
  TruthTable_t  table2, 
  Cal_Bdd  f3, 
  TruthTable_t  table3 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestQnt(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f, 
  TruthTable_t  table, 
  int  bfZeroBFPlusDFOne, 
  int  cacheExistsResultsFlag, 
  int  cacheOrResultsFlag 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestReduce(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f1, 
  TruthTable_t  table1, 
  Cal_Bdd  f2, 
  TruthTable_t  table2 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestRelProd(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f1, 
  TruthTable_t  table1, 
  Cal_Bdd  f2, 
  TruthTable_t  table2, 
  int  bfZeroBFPlusDFOne, 
  int  cacheRelProdResultsFlag, 
  int  cacheAndResultsFlag, 
  int  cacheOrResultsFlag 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestReorderBlock(
  Cal_BddManager  bddManager, 
  TruthTable_t  table, 
  Cal_Bdd  f 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestReorder(
  Cal_BddManager  bddManager, 
  TruthTable_t  table, 
  Cal_Bdd  f 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestSatisfy(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f, 
  TruthTable_t  table 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestSize(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f1, 
  TruthTable_t  table1, 
  Cal_Bdd  f2, 
  TruthTable_t  table2 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestSubstitute(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f1, 
  TruthTable_t  table1, 
  Cal_Bdd  f2, 
  TruthTable_t  table2, 
  Cal_Bdd  f3, 
  TruthTable_t  table3 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestSwapVars(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f, 
  TruthTable_t  table 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestVarSubstitute(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f1, 
  TruthTable_t  table1, 
  Cal_Bdd  f2, 
  TruthTable_t  table2, 
  Cal_Bdd  f3, 
  TruthTable_t  table3 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TestXor(
  Cal_BddManager  bddManager, 
  Cal_Bdd  f1, 
  TruthTable_t  table1, 
  Cal_Bdd  f2, 
  TruthTable_t  table2 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
TrimToSize(
  Block  b, 
  int  sizeIndex 
)
TrimToSize(b, sizeIndex) repeatedly splits b until it has the indicated size. Blocks which are split off are added to the appropriate free list.

Side Effects required

See Also optional
Defined in calMem.c 

static int 
UniqueTableForIdFindOrAdd(
  Cal_BddManager_t * bddManager, 
  CalHashTable_t * hashTable, 
  CalBddNode_t * thenBdd, 
  CalBddNode_t * elseBdd, 
  CalBddNode_t ** bddPtr 
)
optional

Side Effects If a new BDD node is created (found == false), then the numNodes field of the manager needs to be incremented.

See Also optional
Defined in calReorderDF.c 

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

Side Effects required

See Also optional
Defined in calDump.c 

static void 
asAddress(
  double  n, 
  CalAddress_t * r1, 
  CalAddress_t * r2 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static double 
asDouble(
  CalAddress_t  v1, 
  CalAddress_t  v2 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static void 
chars(
  char  c, 
  int  n, 
  FILE * fp 
)
optional

Side Effects required

See Also optional
Defined in calPrintProfile.c 

static double 
cpuTime(
    
)
optional

Side Effects required

See Also optional
Defined in calPerformanceTest.c 

static double 
cpuTime(
    
)
optional

Side Effects required

See Also optional
Defined in calBddReorderTest.c 

static void 
ddClearLocal(
  Cal_Bdd_t  f 
)
Performs a DFS from f, clearing the LSB of the then pointers.

Side Effects None

Defined in calInteract.c 

static void 
ddSuppInteract(
  Cal_BddManager_t * bddManager, 
  Cal_Bdd_t  f, 
  int * support 
)
Performs a DFS from f. Uses the LSB of the then pointer as visited flag.

Side Effects Accumulates in support the variables on which f depends.

Defined in calInteract.c 

static void 
ddUpdateInteract(
  Cal_BddManager_t * bddManager, 
  int * support 
)
If support[i

Side Effects None

Defined in calInteract.c 

static long 
elapsedTime(
    
)
optional

Side Effects required

See Also optional
Defined in calBddReorderTest.c 

static long 
elapsedTime(
    
)
optional

Side Effects required

See Also optional
Defined in calPerformanceTest.c 

static void 
handler(
    
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

int 
main(
  int  argc, 
  char ** argv 
)
optional

Side Effects required

See Also optional
Defined in calBddReorderTest.c 

int 
main(
  int  argc, 
  char ** argv 
)
optional

Side Effects required

See Also optional
Defined in calTest.c 

static long 
pageFaults(
    
)
optional

Side Effects required

See Also optional
Defined in calPerformanceTest.c 

static char * 
terminalIdFn(
  Cal_BddManager  bddManager, 
  CalAddress_t  v1, 
  CalAddress_t  v2, 
  Cal_Pointer_t  pointer 
)
optional

Side Effects required

See Also optional
Defined in calTest.c
Last updated on 970711 20h11