`cal.h`
  External header file
`calInt.h`
  Internal header file
`cal.c`
  Miscellaneous collection of exported BDD functions
`calApplyReduce.c`
  Generic routines for processing temporary nodes during "apply" and "reduce" phases.
`calAssociation.c`
  Contains the routines related to the variable association.
`calBddCompose.c`
  Routine for composing one BDD into another.
`calBddITE.c`
  Routine for computing ITE of 3 BDD operands.
`calBddManager.c`
  Routines for maintaing the manager and creating variables etc.
`calBddOp.c`
  Routines for performing simple boolean operations on a pair of BDDs or on an array of pair of BDDs or on an array of BDDs.
`calBddReorderTest.c`
  A test routine for checking the functionality of dynamic reordering.
`calBddSatisfy.c`
  Routines for BDD satisfying valuation.
`calBddSize.c`
  BDD size and profile routines
`calBddSubstitute.c`
  Routine for simultaneous substitution of an array of variables with an array of functions.
`calBddSupport.c`
  Routines related to the support of a BDD.
`calBddSwapVars.c`
  Routine for swapping two variables.
`calBddVarSubstitute.c`
  Routine for simultaneous substitution of an array of variables with another array of variables.
`calBlk.c`
  Routines for manipulating blocks of variables.
`calCacheTableTwo.c`
  Functions to manage the Cache tables.
`calDump.c`
  BDD library dump/undump routines
`calGC.c`
  Garbage collection routines
`calHashTable.c`
  Functions to manage the hash tables that are a part of 1. unique table 2. request queue
`calHashTableOne.c`
  Routines for managing hash table with Bdd is a key and int, long, or double as a value
`calHashTableThree.c`
  Functions to manage the hash tables that are a part of ITE operation
`calInteract.c`
  Functions to manipulate the variable interaction matrix.
`calMem.c`
  Routines for memory management.
`calMemoryManagement.c`
  Special memory management routines specific to CAL.
`calPerformanceTest.c`
  This file contains the performance test routines for the CAL package.
`calPipeline.c`
  Routines for creating and managing the pipelined BDD operations.
`calPrint.c`
  Routine for printing a BDD.
`calPrintProfile.c`
  Routines for printing various profiles for a BDD.
`calQuant.c`
  Routines for existential/universal quantification and relational product.
`calReduce.c`
  Routines for optimizing a BDD with respect to a don't care set (cofactor and restrict).
`calReorderBF.c`
  Routines for dynamic reordering of variables.
`calReorderDF.c`
  Routines for dynamic reordering of variables.
`calReorderUtil.c`
  Some utility routines used by both breadth-first and depth-first reordering techniques.
`calTerminal.c`
  Contains the terminal function for various BDD operations.
`calTest.c`
  This file contains the test routines for the CAL package.
`calUtil.c`
  Utility functions for the Cal package.

# cal.h

External header file

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu)

See Also `optional`

# calInt.h

Internal header file

By: Rajeev K. Ranjan (rajeev@ic.eecs.berkeley.edu Jagesh Sanghavi (sanghavi@ic.eecs.berkeley.edu)

See Also `cal.h`

# cal.c

Miscellaneous collection of exported BDD functions

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu

`Cal_BddIsEqual()`
  Returns 1 if argument BDDs are equal, 0 otherwise.
`Cal_BddIsBddOne()`
  Returns 1 if the argument BDD is constant one, 0 otherwise.
`Cal_BddIsBddZero()`
  Returns 1 if the argument BDD is constant zero, 0 otherwise.
`Cal_BddIsBddNull()`
  Returns 1 if the argument BDD is NULL, 0 otherwise.
`Cal_BddIsBddConst()`
  Returns 1 if the argument BDD is a constant, 0 otherwise.
`Cal_BddIdentity()`
  Returns the duplicate BDD of the argument BDD.
`Cal_BddOne()`
  Returns the BDD for the constant one
`Cal_BddZero()`
  Returns the BDD for the constant zero
`Cal_BddNot()`
  Returns the complement of the argument BDD.
`Cal_BddGetIfIndex()`
  Returns the index of the top variable of the argument BDD.
`Cal_BddGetIfId()`
  Returns the id of the top variable of the argument BDD.
`Cal_BddIf()`
  Returns the BDD corresponding to the top variable of the argument BDD.
`Cal_BddThen()`
  Returns the positive cofactor of the argument BDD with respect to the top variable of the BDD.
`Cal_BddElse()`
  Returns the negative cofactor of the argument BDD with respect to the top variable of the BDD.
`Cal_BddFree()`
  Frees the argument BDD.
`Cal_BddUnFree()`
  Unfrees the argument BDD.
`Cal_BddGetRegular()`
  Returns a BDD with positive from a given BDD with arbitrary phase
`Cal_BddIntersects()`
  Computes a BDD that implies conjunction of f and g.
`Cal_BddImplies()`
  Computes a BDD that implies conjunction of f and Cal_BddNot(g)
`Cal_BddTotalSize()`
  Returns the number of nodes in the Unique table
`Cal_BddStats()`
  Prints miscellaneous BDD statistics
`Cal_BddDynamicReordering()`
  Specify dynamic reordering technique.
`Cal_BddReorder()`
  Invoke the current dynamic reodering method.
`Cal_BddType()`
  Returns type of a BDD ( 0, 1, +var, -var, ovrflow, nonterminal)
`Cal_BddVars()`
  Returns the number of BDD variables
`Cal_BddNodeLimit()`
  Sets the node limit to new_limit and returns the old limit.
`Cal_BddOverflow()`
  Returns 1 if the node limit has been exceeded, 0 otherwise. The overflow flag is cleared.
`Cal_BddIsCube()`
  Returns 1 if the argument BDD is a cube, 0 otherwise
`Cal_BddManagerGetHooks()`
  Returns the hooks field of the manager.
`Cal_BddManagerSetHooks()`
  Sets the hooks field of the manager.
`CalBddIf()`
  Returns the BDD corresponding to the top variable of the argument BDD.
`CalBddIsCubeStep()`
  Returns 1 if the argument BDD is a cube, 0 otherwise
`CalBddTypeAux()`
  Returns the BDD type by recursively traversing the argument BDD
`CalBddIdentity()`
  Returns the duplicate BDD of the argument BDD.
`BddIntersectsStep()`
  Recursive routine to returns a BDD that implies conjunction of argument BDDs

# calApplyReduce.c

Generic routines for processing temporary nodes during "apply" and "reduce" phases.

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

See Also `optional`

`CalHashTableApply()`
  required
`CalHashTableReduce()`
  required

# calAssociation.c

Contains the routines related to the variable association.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)

optional

See Also `optional`

`Cal_AssociationInit()`
  Creates or finds a variable association.
`Cal_AssociationQuit()`
  Deletes the variable association given by id
`Cal_AssociationSetCurrent()`
  Sets the current variable association to the one given by id and returns the ID of the old association.
`Cal_TempAssociationAugment()`
  Adds to the temporary variable association.
`Cal_TempAssociationInit()`
  Sets the temporary variable association.
`Cal_TempAssociationQuit()`
  Cleans up temporary association
`CalAssociationListFree()`
  Frees the variable associations
`CalVarAssociationRepackUpdate()`
  Need to be called after repacking.
`CalCheckAssociationValidity()`
  Checks the validity of association.
`CalReorderAssociationFix()`
  required
`AssociationIsEqual()`
  Checks for equality of two associations
`CheckAssoc()`
  required

# calBddCompose.c

Routine for composing one BDD into another.

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

`Cal_BddCompose()`
  composition - substitute a BDD variable by a function
`CalRequestNodeListCompose()`
  required
`CalHashTableComposeApply()`
  required
`CalComposeRequestCreate()`
  required

# calBddITE.c

Routine for computing ITE of 3 BDD operands.

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

See Also `optional`

`Cal_BddITE()`
  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
`CalRequestNodeListArrayITE()`
  required
`CalBddOpITEBF()`
  required
`CalHashTableITEApply()`
  required
`CalBddITE()`
  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

# calBddManager.c

Routines for maintaing the manager and creating variables etc.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)

See Also `optional`

`Cal_BddManagerInit()`
  Creates and initializes a new BDD manager.
`Cal_BddManagerQuit()`
  Frees the BDD manager and all the associated allocations
`Cal_BddManagerSetParameters()`
  Sets appropriate fields of BDD Manager.
`Cal_BddManagerGetNumNodes()`
  Returns the number of BDD nodes
`Cal_BddManagerCreateNewVarFirst()`
  Creates and returns a new variable at the start of the variable order.
`Cal_BddManagerCreateNewVarLast()`
  Creates and returns a new variable at the end of the variable order.
`Cal_BddManagerCreateNewVarBefore()`
  Creates and returns a new variable before the specified one in the variable order.
`Cal_BddManagerCreateNewVarAfter()`
  Creates and returns a new variable after the specified one in the variable order.
`Cal_BddManagerGetVarWithIndex()`
  Returns the variable with the specified index, null if no such variable exists
`Cal_BddManagerGetVarWithId()`
  Returns the variable with the specified id, null if no such variable exists
`CalBddManagerCreateNewVar()`
  This function creates and returns a new variable with given index value.
`BddDefaultTransformFn()`
  required
`CalBddManagerPrint()`
  required

# calBddOp.c

Routines for performing simple boolean operations on a pair of BDDs or on an array of pair of BDDs or on an array of BDDs.

By: Rajeev Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)

The "cal" specific routines are "Cal_BddPairwiseAnd/Or", "Cal_BddMultiwayAnd/Or".

See Also `optional`

`Cal_BddAnd()`
  Returns the BDD for logical AND of argument BDDs
`Cal_BddNand()`
  Returns the BDD for logical NAND of argument BDDs
`Cal_BddOr()`
  Returns the BDD for logical OR of argument BDDs
`Cal_BddNor()`
  Returns the BDD for logical NOR of argument BDDs
`Cal_BddXor()`
  Returns the BDD for logical exclusive OR of argument BDDs
`Cal_BddXnor()`
  Returns the BDD for logical exclusive NOR of argument BDDs
`Cal_BddPairwiseAnd()`
  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
`Cal_BddPairwiseOr()`
  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
`Cal_BddPairwiseXor()`
  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
`Cal_BddMultiwayAnd()`
  Returns the BDD for logical AND of argument BDDs
`Cal_BddMultiwayOr()`
  Returns the BDD for logical OR of argument BDDs
`Cal_BddMultiwayXor()`
  Returns the BDD for logical XOR of argument BDDs
`CalRequestNodeListArrayOp()`
  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
`CalBddOpBF()`
  Internal routine to compute a logical operation on a pair of BDDs
`BddArrayOpBF()`
  Internal common routine for Cal_BddPairwiseAnd and Cal_BddPairwiseOr
`BddMultiwayOp()`
  Internal routine for multiway operations
`BddArrayToRequestNodeListArray()`
  Converts an array of BDDs to a list of requests representing BDD pairs
`CeilLog2()`
  Returns the smallest integer greater than or equal to log2 of a number

# calBddReorderTest.c

A test routine for checking the functionality of dynamic reordering.

By: Wilsin Gosti (wilsin@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)

See Also `optional`

`main()`
  required
`cpuTime()`
  required
`elapsedTime()`
  Computes the time.

# calBddSatisfy.c

Routines for BDD satisfying valuation.

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

See Also `optional`

`Cal_BddSatisfy()`
  Returns a BDD which implies f, true for some valuation on which f is true, and which has at most one node at each level
`Cal_BddSatisfySupport()`
  Returns a special cube contained in f.
`Cal_BddSatisfyingFraction()`
  Returns the fraction of valuations which make f true. (Note that this fraction is independent of whatever set of variables f is supposed to be a function of)
`BddSatisfyStep()`
  Returns a BDD which implies f, is true for some valuation on which f is true, and which has at most one node at each level
`BddSatisfySupportStep()`
`IndexCmp()`
`BddSatisfyingFractionStep()`

# calBddSize.c

BDD size and profile routines

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu) Originally written by David Long.

See Also `optional`

`Cal_BddSize()`
  Returns the number of nodes in f when negout is nonzero. If negout is zero, we pretend that the BDDs don't have negative-output pointers.
`Cal_BddSizeMultiple()`
  The routine is like Cal_BddSize, but takes a null-terminated array of BDDs and accounts for sharing of nodes.
`Cal_BddProfile()`
  Returns a "node profile" of f, i.e., the number of nodes at each level in f.
`Cal_BddProfileMultiple()`
`Cal_BddFunctionProfile()`
  Returns a "function profile" for f.
`Cal_BddFunctionProfileMultiple()`
  Returns a "function profile" for fArray.
`BddMarkBdd()`
`BddCountNoNodes()`
`BddCountNodes()`
`BddSizeStep()`
`BddProfileStep()`
`BddHighestRefStep()`
`BddDominatedStep()`

# calBddSubstitute.c

Routine for simultaneous substitution of an array of variables with an array of functions.

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

Routine for simultaneous substitution of an array of variables with an array of functions.

See Also `optional`

`Cal_BddSubstitute()`
  Substitute a set of variables by functions
`CalHashTableSubstituteApply()`
  required
`CalHashTableSubstituteReduce()`
  required

# calBddSupport.c

Routines related to the support of a BDD.

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu) Originally written by David Long.

See Also `optional`

`Cal_BddSupport()`
  returns the support of f as a null-terminated array of variables
`Cal_BddDependsOn()`
  Returns 1 if f depends on var and returns 0 otherwise.
`CalBddSupportStep()`
  returns the support of f as a null-terminated array of variables
`CalBddUnmarkNodes()`
  recursively unmarks the nodes
`CalBddDependsOnStep()`
  required

# calBddSwapVars.c

Routine for swapping two variables.

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

Routine for swapping two variables.

See Also `None`

`Cal_BddSwapVars()`
  Return a function obtained by swapping two variables
`CalHashTableSwapVarsApply()`
  required
`CalHashTableSwapVarsPlusApply()`
  required
`CalHashTableSwapVarsMinusApply()`
  required

# calBddVarSubstitute.c

Routine for simultaneous substitution of an array of variables with another array of variables.

By: Rajeev Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)

See Also `optional`

`Cal_BddVarSubstitute()`
  Substitute a set of variables by set of another variables.
`CalBddVarSubstitute()`
  Substitute a set of variables by functions
`CalOpBddVarSubstitute()`
  required
`CalHashTableSubstituteApply()`
  required
`CalHashTableSubstituteReduce()`
  required

# calBlk.c

Routines for manipulating blocks of variables.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu). Modelled on the BDD package developed by David Long.

Routines for manipulating blocks of variables.

`Cal_BddNewVarBlock()`
  Creates and returns a variable block used for controlling dynamic reordering.
`Cal_BddVarBlockReorderable()`
  Sets the reoderability of a particular block.
`CalBddFindBlock()`
  required
`CalBddBlockDelta()`
  required
`CalBddShiftBlock()`
  required
`CalBlockMemoryConsumption()`
  required
`CalFreeBlockRecursively()`
  required
`AddBlock()`
  required

# calCacheTableTwo.c

Functions to manage the Cache tables.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)

See Also `optional`

`CalCacheTableTwoInit()`
  Initialize a Cache table using default parameters.
`CalCacheTableTwoQuit()`
  Free a Cache table along with the associated storage.
`CalCacheTableTwoInsert()`
  Directly insert a BDD node in the Cache table.
`CalCacheTableTwoLookup()`
  required
`CalCacheTableTwoFlush()`
  Free a Cache table along with the associated storage.
`CalCacheTableTwoFlushAll()`
  Free a Cache table along with the associated storage.
`CalCacheTableTwoGCFlush()`
  required
`CalCacheTableTwoRepackUpdate()`
  required
`CalCheckCacheTableValidity()`
  required
`CalCacheTableTwoFixResultPointers()`
  required
`CalCacheTablePrint()`
  required
`CalBddManagerGetCacheTableData()`
  required
`CalCacheTableRehash()`
  required
`CalCacheTableTwoFlushAssociationId()`
  Flushes the entries from the cache which correspond to the given associationId.
`CalCacheTableMemoryConsumption()`
  required
`CacheTableTwoRehash()`
  required
`CacheTablePrint()`
  required

# calDump.c

BDD library dump/undump routines

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu) Originally written by David Long.

See Also `optional`

`Cal_BddUndumpBdd()`
  Reads a BDD from a file
`Cal_BddDumpBdd()`
  Write a BDD to a file
`Write()`
`BddDumpBddStep()`
`Read()`
`BddUndumpBddStep()`
`BytesNeeded()`

# calGC.c

Garbage collection routines

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

optional

See Also `optional`

`Cal_BddSetGCMode()`
  Sets the garbage collection mode, 0 means the garbage collection should be turned off, 1 means garbage collection should be on.
`Cal_BddManagerGC()`
  Invokes the garbage collection at the manager level.
`Cal_BddManagerSetGCLimit()`
  Sets the limit of the garbage collection.
`CalBddManagerGCCheck()`
  required
`CalHashTableGC()`
  This function performs the garbage collection operation for a particular index.
`CalRepackNodesAfterGC()`
  required
`CeilLog2()`
  Returns the smallest integer greater than or equal to log2 of a number

# calHashTable.c

Functions to manage the hash tables that are a part of 1. unique table 2. request queue

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

`CalHashTableInit()`
  Initialize a hash table using default parameters.
`CalHashTableQuit()`
  Free a hash table along with the associated storage.
`CalHashTableAddDirect()`
  Directly insert a BDD node in the hash table.
`CalHashTableFindOrAdd()`
  required
`CalHashTableAddDirectAux()`
  required
`CalHashTableCleanUp()`
  required
`CalHashTableLookup()`
  required
`CalHashTableDelete()`
  Deletes a BDD node in the hash table.
`CalUniqueTableForIdLookup()`
  Lookup unique table for id.
`CalUniqueTableForIdFindOrAdd()`
  find or add in the unique table for id.
`CalHashTableRehash()`
  required
`CalUniqueTableForIdRehashNode()`
  required
`CalBddUniqueTableNumLockedNodes()`
  required
`CalPackNodes()`
  required
`CalBddPackNodesForSingleId()`
  required
`CalBddPackNodesAfterReorderForSingleId()`
  Packs the nodes if the variables which has just been sifted.
`CalBddPackNodesForMultipleIds()`
  required
`CeilLog2()`
  Returns the smallest integer greater than or equal to log2 of a number

# calHashTableOne.c

Routines for managing hash table with Bdd is a key and int, long, or double as a value

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

See Also `optional`

`CalHashTableOneInit()`
  Initialize a hash table using default parameters.
`CalHashTableOneQuit()`
  Free a hash table along with the associated storage.
`CalHashTableOneInsert()`
  Directly insert a BDD node in the hash table.
`CalHashTableOneLookup()`
  required
`HashTableOneRehash()`
  required

# calHashTableThree.c

Functions to manage the hash tables that are a part of ITE operation

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

CalHashTableThreeFindOrAdd

See Also `optional`

`CalHashTableThreeFindOrAdd()`
  required
`CalHashTableThreeRehash()`
  required

# calInteract.c

Functions to manipulate the variable interaction matrix.

By: Original author:Fabio Somenzi. Modified for CAL package by Rajeev K. Ranjan

The interaction matrix tells whether two variables are both in the support of some function of the DD. The main use of the interaction matrix is in the in-place swapping. Indeed, if two variables do not interact, there is no arc connecting the two layers; therefore, the swap can be performed in constant time, without scanning the subtables. Another use of the interaction matrix is in the computation of the lower bounds for sifting. Finally, the interaction matrix can be used to speed up aggregation checks in symmetric and group sifting.

The computation of the interaction matrix is done with a series of depth-first searches. The searches start from those nodes that have only external references. The matrix is stored as a packed array of bits; since it is symmetric, only the upper triangle is kept in memory. As a final remark, we note that there may be variables that do intercat, but that for a given variable order have no arc connecting their layers when they are adjacent.

`CalSetInteract()`
  Set interaction matrix entries.
`CalTestInteract()`
  Test interaction matrix entries.
`CalInitInteract()`
  Initializes the interaction matrix.
`ddSuppInteract()`
  Find the support of f.
`ddClearLocal()`
  Performs a DFS from f, clearing the LSB of the then pointers.
`ddUpdateInteract()`
  Marks as interacting all pairs of variables that appear in support.

# calMem.c

Routines for memory management.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu). Originally written by David Long.

Contains allocation, free, resize routines. Also has routines for managing records of fixed size.

See Also `optional`

`Cal_MemFatal()`
  Prints an error message and exits.
`Cal_MemAllocation()`
  Returns the memory allocated.
`Cal_MemGetBlock()`
  Allocates a new block of the specified size.
`Cal_MemFreeBlock()`
  Frees the block.
`Cal_MemResizeBlock()`
  Expands or contracts the block to a new size. We try to avoid moving the block if possible.
`Cal_MemNewRec()`
  Allocates a record from the specified record manager.
`Cal_MemFreeRec()`
  Frees a record managed by the indicated record manager.
`Cal_MemNewRecMgr()`
  Creates a new record manager with the given record size.
`Cal_MemFreeRecMgr()`
  Frees all the storage associated with the specified record manager.
`CeilingLog2()`
  required
`BlockSizeIndex()`
  required
`AddToFreeList()`
  required
`RemoveFromFreeList()`
  required
`Buddy()`
  required
`TrimToSize()`
  required
`MergeAndFree()`
  required

# calMemoryManagement.c

Special memory management routines specific to CAL.

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

Functions for managing the system memory using a set of nodeManagers. Each nodeManager manages a set of fixed size nodes obtained from a set of pages. When additional memory is required, nodeManager obtains a new page from the pageManager. The new page is divided into ( PAGE_SIZE/NODE_SIZE ) number of nodes.

`CalPageManagerInit()`
  Initializes a pageManager.
`CalPageManagerQuit()`
  Frees pageManager and associated pages.
`CalPageManagerPrint()`
  Prints address of each memory segment and address of each page.
`CalNodeManagerInit()`
  Initializes a node manager.
`CalNodeManagerQuit()`
  Frees a node manager.
`CalNodeManagerPrint()`
  Prints address of each free node.
`CalPageManagerAllocPage()`
  Allocs a new page.
`CalPageManagerFreePage()`
  Free a page.
`PageManagerExpandStorage()`
  Allocates a segment of memory to expand the storage managed by pageManager. The allocated segment is divided into free pages which are linked as a freePageList.
`PageAlign()`
  Return page aligned address greater than or equal to the pointer.
`SegmentToPageList()`
  Converts a memory segment into a linked list of pages. if p is a pointer to a page, *p contains address of the next page if p is a pointer to the last page, *p contains lastPointer.

# calPerformanceTest.c

This file contains the performance test routines for the CAL package.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)

optional

See Also `optional`

`Cal_PerformanceTest()`
  Main routine for testing performances of various routines.
`CalIncreasingOrderCompare()`
  required
`CalDecreasingOrderCompare()`
  required
`CalPerformanceTestAnd()`
  Performance test routine for quantify (all variables at the same time).
`CalPerformanceMemoryOverhead()`
  Performance test routine for quantify (all variables at the same time).
`CalPerformaceTestSuperscalar()`
  Performance test routine for quantify (all variables at the same time).
`CalPerformanceTestNonSuperscalar()`
  Performance test routine for quantify (all variables at the same time).
`CalPerformanceTestMultiway()`
  Performance test routine for quantify (all variables at the same time).
`CalPerformanceTestOneway()`
  Performance test routine for quantify (all variables at the same time).
`CalPerformanceTestCompose()`
  Performance test routine for quantify (all variables at the same time).
`CalPerformanceTestQuantifyAllTogether()`
  Performance test routine for quantify (all variables at the same time).
`CalQuantifySanityCheck()`
  Performance test routine for quantify (all variables at the same time).
`CalPerformanceTestRelProd()`
  Performance test routine for quantify (all variables at the same time).
`CalPerformanceTestSubstitute()`
  Performance test routine for quantify (all variables at the same time).
`CalPerformanceTestSwapVars()`
  Performance test routine for quantify (all variables at the same time).
`elapsedTime()`
  Computes the time.
`cpuTime()`
  Computes the number of page faults.
`pageFaults()`
  Computes the number of page faults.
`GetRandomNumbers()`
  Generates "count" many random numbers ranging between "lowerBound" and "upperBound".

# calPipeline.c

Routines for creating and managing the pipelined BDD operations.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)

Eventually we would like to have this feature transparent to the user.

See Also `optional`

`Cal_PipelineSetDepth()`
  Set depth of a BDD pipeline.
`Cal_PipelineInit()`
  Initialize a BDD pipeline.
`Cal_PipelineCreateProvisionalBdd()`
  Create a provisional BDD in the pipeline.
`Cal_PipelineExecute()`
  Executes a pipeline.
`Cal_PipelineUpdateProvisionalBdd()`
  Update a provisional Bdd obtained during pipelining.
`Cal_BddIsProvisional()`
  Returns 1, if the given user BDD contains provisional BDD node.
`Cal_PipelineQuit()`
  Resets the pipeline freeing all resources.
`CalBddReorderFixProvisionalNodes()`
  required
`CalCheckPipelineValidity()`
  required

# calPrint.c

Routine for printing a BDD.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu) Originally written by David Long.

See Also `None`

`Cal_BddPrintBdd()`
  Prints a BDD in the human readable form.
`CalBddVarName()`
  required
`CalBddNumberSharedNodes()`
  required
`CalBddMarkSharedNodes()`
  required
`Chars()`
  required
`BddPrintTopVar()`
  required
`BddPrintBddStep()`
  required
`BddTerminalId()`
  required
`BddTerminalValueAux()`
  required

# calPrintProfile.c

Routines for printing various profiles for a BDD.

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu) Originally written by David Long.

See Also `optional`

`Cal_BddPrintProfile()`
  Displays the node profile for f on fp. lineLength specifies the maximum line length. varNamingFn is as in Cal_BddPrintBdd.
`Cal_BddPrintProfileMultiple()`
  Cal_BddPrintProfileMultiple is like Cal_BddPrintProfile except it displays the profile for a set of BDDs
`Cal_BddPrintFunctionProfile()`
  Cal_BddPrintFunctionProfile is like Cal_BddPrintProfile except it displays a function profile for f
`Cal_BddPrintFunctionProfileMultiple()`
  Cal_BddPrintFunctionProfileMultiple is like Cal_BddPrintFunctionProfile except for multiple BDDs
`CalBddPrintProfileAux()`
  Prints a profile to the file given by fp. The varNamingProc is as in Cal_BddPrintBdd. lineLength gives the line width to scale the profile to.
`chars()`

# calQuant.c

Routines for existential/universal quantification and relational product.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu)

See Also `None`

`Cal_BddExists()`
  Returns the result of existentially quantifying some variables from the given BDD.
`Cal_BddRelProd()`
  Returns the result of taking the logical AND of the argument BDDs and existentially quantifying some variables from the product.
`Cal_BddForAll()`
  Returns the result of universally quantifying some variables from the given BDD.
`CalOpExists()`
  required
`CalOpRelProd()`
  required
`BddExistsStep()`
  required
`BddRelProdStep()`
  required
`BddDFStep()`
  required
`HashTableApply()`
  required
`HashTableReduce()`
  required
`BddExistsApply()`
  required
`BddExistsBFAux()`
  required
`BddExistsReduce()`
  required
`BddExistsBFPlusDF()`
  required
`BddRelProdApply()`
  required
`BddRelProdReduce()`
  required
`BddRelProdBFAux()`
  required
`BddRelProdBFPlusDF()`
  required

# calReduce.c

Routines for optimizing a BDD with respect to a don't care set (cofactor and restrict).

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu

See Also `None`

`Cal_BddCofactor()`
  Returns the generalized cofactor of BDD f with respect to BDD c.
`Cal_BddReduce()`
  Returns a BDD which agrees with f for all valuations which satisfy c.
`Cal_BddBetween()`
  Returns a minimal BDD whose function contains fMin and is contained in fMax.
`CalOpCofactor()`
  required
`BddReduceBF()`
  required
`BddCofactorBF()`
  required
`HashTableReduceApply()`
  required
`HashTableCofactorApply()`
  required
`HashTableCofactorReduce()`
  required

# calReorderBF.c

Routines for dynamic reordering of variables.

By: Rajeev K. Ranjan (rajeev@ic.eecs.berkeley.edu) Wilsin Gosti (wilsin@ic.eecs.berkeley.edu)

This method dynamically reorders variables while preserving their locality. This entails both memory and computational overheads. Conceptually and experimentally it has been observed that these overheads lead to poorer performance compared to the traditional reordering methods. For details, please refer to the work by Rajeev K. Ranjan et al - "Dynamic variable reordering in a breadth-first manipulation based package: Challenges and Solutions"- Proceedings of ICCD'97.

See Also `calReorderDF.c` `calReorderUtil.c`

`CalBddReorderAuxBF()`
  required
`BddReorderFixForwardingNodes()`
  Fixes the forwarding nodes in a unique table.
`BddReorderFixAndFreeForwardingNodes()`
  Traverses the forwarding node lists of index, index+1 .. up to index+level. Frees the intermediate forwarding nodes.
`BddReorderSwapVarIndex()`
  required
`CofactorFixAndReclaimForwardedNodes()`
  required
`BddReorderFreeNodes()`
  required
`PrintBddProfileAfterReorder()`
  required
`BddReorderVarSift()`
  Reorder variables using "sift" algorithm.
`BddReorderSiftToBestPos()`
  required
`BddSiftPerfromPhaseIV()`
  required
`BddReorderVarWindow()`
  required
`BddReorderWindow2()`
  required
`BddReorderWindow3()`
  required

# calReorderDF.c

Routines for dynamic reordering of variables.

By: Rajeev K. Ranjan (rajeev@@ic. eecs.berkeley.edu)

This method is based on traditional dynamic reordering technique found in depth-first based packages. The data structure is first converted to conform to traditional one and then reordering is performed. At the end the nodes are arranged back on the pages. The computational overheads are in terms of converting the data structure back and forth and the memory overhead due to the extra space needed to arrange the nodes. This overhead can be eliminated by proper implementation. For details, please refer to the work by Rajeev K. Ranjan et al - "Dynamic variable reordering in a breadth-first manipulation based package: Challenges and Solutions"- Proceedings of ICCD'97.

See Also `calReorderBF.c` `calReorderUtil.c`

`CalBddReorderAuxDF()`
  required
`UniqueTableForIdFindOrAdd()`
  find or add in the unique table for id.
`HashTableAddDirect()`
  Directly insert a BDD node in the hash table.
`HashTableFindOrAdd()`
  required
`BddConvertDataStruct()`
  Changes the data structure of the bdd nodes.
`BddConvertDataStructBack()`
  Changes the data structure of the bdd nodes to the original one.
`BddReallocateNodesInPlace()`
  required
`CalAlignCollisionChains()`
  required
`BddReallocateNodes()`
  required
`BddExchangeAux()`
  required
`CheckValidityOfNodes()`
  required
`SweepVarTable()`
  required
`BddExchange()`
  required
`BddExchangeVarBlocks()`
  required
`BddReorderWindow2()`
  required
`BddReorderWindow3()`
  required
`BddReorderStableWindow3Aux()`
  required
`BddReorderStableWindow3()`
  required
`BddSiftBlock()`
  required
`BddReorderSiftAux()`
  Reorder variables using "sift" algorithm.
`BddReorderSift()`
  required
`BddAddInternalReferences()`
  required
`BddNukeInternalReferences()`
  required
`CeilLog2()`
  Returns the smallest integer greater than or equal to log2 of a number

# calReorderUtil.c

Some utility routines used by both breadth-first and depth-first reordering techniques.

By: Rajeev K. Ranjan (rajeev@ic.eecs.berkeley.edu) Wilsin Gosti (wilsin@ic.eecs.berkeley.edu)

See Also `optional`

`CalBddReorderFixUserBddPtrs()`
  required
`CalCheckAllValidity()`
  required
`CalCheckValidityOfNodesForId()`
  required
`CalCheckValidityOfNodesForWindow()`
  required
`CalCheckValidityOfANode()`
  required
`CalCheckRefCountValidity()`
  required
`CalCheckAssoc()`
  required
`CalFixupAssoc()`
  required
`CalBddReorderFixCofactors()`
  Fixes the cofactors of the nodes belonging to the given index.
`CalBddReorderReclaimForwardedNodes()`
  required

# calTerminal.c

Contains the terminal function for various BDD operations.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu

`CalOpAnd()`
  required
`CalOpNand()`
  required
`CalOpOr()`
  required
`CalOpXor()`
  required
`CalOpITE()`
  required

# calTest.c

This file contains the test routines for the CAL package.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Modified and extended from the original version written by David Long.

optional

See Also `optional`

`main()`
  required
`asDouble()`
  required
`asAddress()`
  required
`terminalIdFn()`
  required
`PrintBdd()`
  required
`Error()`
  required
`Cofactor()`
  required
`Decode()`
  required
`TestAnd()`
  required
`TestNand()`
  required
`TestOr()`
  required
`TestITE()`
  required
`TestXor()`
  required
`TestIdNot()`
  required
`TestCompose()`
  required
`TestSubstitute()`
  required
`TestVarSubstitute()`
  required
`TestSwapVars()`
  required
`TestMultiwayAnd()`
  required
`TestMultiwayOr()`
  required
`TestMultiwayLarge()`
  required
`TestArrayOp()`
  required
`TestInterImpl()`
  required
`TestQnt()`
  required
`TestAssoc()`
  required
`TestRelProd()`
  required
`TestReduce()`
  required
`TestGenCof()`
  required
`TestSize()`
  required
`TestSatisfy()`
  required
`TestPipeline()`
  required
`TestDump()`
  required
`TestReorderBlock()`
  required
`TestReorder()`
  required
`handler()`
  required
`RandomTests()`
  required

# calUtil.c

Utility functions for the Cal package.

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev K. Ranjan (rajeev@eecs.berkeley.edu)

Utility functions used in the Cal package.

See Also `optional`

`Cal_BddFunctionPrint()`
  Prints the function implemented by the argument BDD
`CalUniqueTablePrint()`
  required
`CalBddFunctionPrint()`
  Prints the function implemented by the argument BDD
`CalBddPreProcessing()`
  required
`CalBddPostProcessing()`
  required
`CalBddArrayPreProcessing()`
  required
`CalBddGetInternalBdd()`
  Prints fatal message and exits.
`CalBddGetExternalBdd()`
  Prints fatal message and exits.
`CalBddFatalMessage()`
  Prints fatal message and exits.
`CalBddWarningMessage()`
  Prints warning message.
`CalBddNodePrint()`
  required
`CalBddPrint()`
  required
`CalHashTablePrint()`
  Prints a hash table.
`CalHashTableOnePrint()`
  required

Last updated on 970711 20h11