AddBlock()
required
AddToFreeList()
required
AssociationIsEqual()
Checks for equality of two associations
BddAddInternalReferences()
required
BddArrayOpBF()
Internal common routine for Cal_BddPairwiseAnd and Cal_BddPairwiseOr
BddArrayToRequestNodeListArray()
Converts an array of BDDs to a list of requests representing BDD pairs
BddCofactorBF()
required
BddConvertDataStructBack()
Changes the data structure of the bdd nodes to the original one.
BddConvertDataStruct()
Changes the data structure of the bdd nodes.
BddCountNoNodes()
BddCountNodes()
BddDFStep()
required
BddDefaultTransformFn()
required
BddDominatedStep()
BddDumpBddStep()
BddExchangeAux()
required
BddExchangeVarBlocks()
required
BddExchange()
required
BddExistsApply()
required
BddExistsBFAux()
required
BddExistsBFPlusDF()
required
BddExistsReduce()
required
BddExistsStep()
required
BddHighestRefStep()
BddIntersectsStep()
Recursive routine to returns a BDD that implies conjunction of argument BDDs
BddMarkBdd()
BddMultiwayOp()
Internal routine for multiway operations
BddNukeInternalReferences()
required
BddPrintBddStep()
required
BddPrintTopVar()
required
BddProfileStep()
BddReallocateNodesInPlace()
required
BddReallocateNodes()
required
BddReduceBF()
required
BddRelProdApply()
required
BddRelProdBFAux()
required
BddRelProdBFPlusDF()
required
BddRelProdReduce()
required
BddRelProdStep()
required
BddReorderFixAndFreeForwardingNodes()
Traverses the forwarding node lists of index, index+1 .. up to index+level. Frees the intermediate forwarding nodes.
BddReorderFixForwardingNodes()
Fixes the forwarding nodes in a unique table.
BddReorderFreeNodes()
required
BddReorderSiftAux()
Reorder variables using "sift" algorithm.
BddReorderSiftToBestPos()
required
BddReorderSift()
required
BddReorderStableWindow3Aux()
required
BddReorderStableWindow3()
required
BddReorderSwapVarIndex()
required
BddReorderVarSift()
Reorder variables using "sift" algorithm.
BddReorderVarWindow()
required
BddReorderWindow2()
required
BddReorderWindow2()
required
BddReorderWindow3()
required
BddReorderWindow3()
required
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()
BddSatisfyingFractionStep()
BddSiftBlock()
required
BddSiftPerfromPhaseIV()
required
BddSizeStep()
BddTerminalId()
required
BddTerminalValueAux()
required
BddUndumpBddStep()
BlockSizeIndex()
required
Buddy()
required
BytesNeeded()
CacheTablePrint()
required
CacheTableTwoRehash()
required
CalAlignCollisionChains()
required
CalAssociationListFree()
Frees the variable associations
CalBddArrayPreProcessing()
required
CalBddBlockDelta()
required
CalBddDependsOnStep()
required
CalBddFatalMessage()
Prints fatal message and exits.
CalBddFindBlock()
required
CalBddFunctionPrint()
Prints the function implemented by the argument BDD
CalBddGetExternalBdd()
Prints fatal message and exits.
CalBddGetInternalBdd()
Prints fatal message and exits.
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
CalBddIdentity()
Returns the duplicate BDD of the argument BDD.
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
CalBddManagerCreateNewVar()
This function creates and returns a new variable with given index value.
CalBddManagerGCCheck()
required
CalBddManagerGetCacheTableData()
required
CalBddManagerPrint()
required
CalBddMarkSharedNodes()
required
CalBddNodePrint()
required
CalBddNumberSharedNodes()
required
CalBddOpBF()
Internal routine to compute a logical operation on a pair of BDDs
CalBddOpITEBF()
required
CalBddPackNodesAfterReorderForSingleId()
Packs the nodes if the variables which has just been sifted.
CalBddPackNodesForMultipleIds()
required
CalBddPackNodesForSingleId()
required
CalBddPostProcessing()
required
CalBddPreProcessing()
required
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.
CalBddPrint()
required
CalBddReorderAuxBF()
required
CalBddReorderAuxDF()
required
CalBddReorderFixCofactors()
Fixes the cofactors of the nodes belonging to the given index.
CalBddReorderFixProvisionalNodes()
required
CalBddReorderFixUserBddPtrs()
required
CalBddReorderReclaimForwardedNodes()
required
CalBddShiftBlock()
required
CalBddSupportStep()
returns the support of f as a null-terminated array of variables
CalBddTypeAux()
Returns the BDD type by recursively traversing the argument BDD
CalBddUniqueTableNumLockedNodes()
required
CalBddUnmarkNodes()
recursively unmarks the nodes
CalBddVarName()
required
CalBddVarSubstitute()
Substitute a set of variables by functions
CalBddWarningMessage()
Prints warning message.
CalBlockMemoryConsumption()
required
CalCacheTableMemoryConsumption()
required
CalCacheTablePrint()
required
CalCacheTableRehash()
required
CalCacheTableTwoFixResultPointers()
required
CalCacheTableTwoFlushAll()
Free a Cache table along with the associated storage.
CalCacheTableTwoFlushAssociationId()
Flushes the entries from the cache which correspond to the given associationId.
CalCacheTableTwoFlush()
Free a Cache table along with the associated storage.
CalCacheTableTwoGCFlush()
required
CalCacheTableTwoInit()
Initialize a Cache table using default parameters.
CalCacheTableTwoInsert()
Directly insert a BDD node in the Cache table.
CalCacheTableTwoLookup()
required
CalCacheTableTwoQuit()
Free a Cache table along with the associated storage.
CalCacheTableTwoRepackUpdate()
required
CalCheckAllValidity()
required
CalCheckAssociationValidity()
Checks the validity of association.
CalCheckAssoc()
required
CalCheckCacheTableValidity()
required
CalCheckPipelineValidity()
required
CalCheckRefCountValidity()
required
CalCheckValidityOfANode()
required
CalCheckValidityOfNodesForId()
required
CalCheckValidityOfNodesForWindow()
required
CalComposeRequestCreate()
required
CalDecreasingOrderCompare()
required
CalFixupAssoc()
required
CalFreeBlockRecursively()
required
CalHashTableAddDirectAux()
required
CalHashTableAddDirect()
Directly insert a BDD node in the hash table.
CalHashTableApply()
required
CalHashTableCleanUp()
required
CalHashTableComposeApply()
required
CalHashTableDelete()
Deletes a BDD node in the hash table.
CalHashTableFindOrAdd()
required
CalHashTableGC()
This function performs the garbage collection operation for a particular index.
CalHashTableITEApply()
required
CalHashTableInit()
Initialize a hash table using default parameters.
CalHashTableLookup()
required
CalHashTableOneInit()
Initialize a hash table using default parameters.
CalHashTableOneInsert()
Directly insert a BDD node in the hash table.
CalHashTableOneLookup()
required
CalHashTableOnePrint()
required
CalHashTableOneQuit()
Free a hash table along with the associated storage.
CalHashTablePrint()
Prints a hash table.
CalHashTableQuit()
Free a hash table along with the associated storage.
CalHashTableReduce()
required
CalHashTableRehash()
required
CalHashTableSubstituteApply()
required
CalHashTableSubstituteApply()
required
CalHashTableSubstituteReduce()
required
CalHashTableSubstituteReduce()
required
CalHashTableSwapVarsApply()
required
CalHashTableSwapVarsMinusApply()
required
CalHashTableSwapVarsPlusApply()
required
CalHashTableThreeFindOrAdd()
required
CalHashTableThreeRehash()
required
CalIncreasingOrderCompare()
required
CalInitInteract()
Initializes the interaction matrix.
CalNodeManagerInit()
Initializes a node manager.
CalNodeManagerPrint()
Prints address of each free node.
CalNodeManagerQuit()
Frees a node manager.
CalOpAnd()
required
CalOpBddVarSubstitute()
required
CalOpCofactor()
required
CalOpExists()
required
CalOpITE()
required
CalOpNand()
required
CalOpOr()
required
CalOpRelProd()
required
CalOpXor()
required
CalPackNodes()
required
CalPageManagerAllocPage()
Allocs a new page.
CalPageManagerFreePage()
Free a page.
CalPageManagerInit()
Initializes a pageManager.
CalPageManagerPrint()
Prints address of each memory segment and address of each page.
CalPageManagerQuit()
Frees pageManager and associated pages.
CalPerformaceTestSuperscalar()
Performance test routine for quantify (all variables at the same time).
CalPerformanceMemoryOverhead()
Performance test routine for quantify (all variables at the same time).
CalPerformanceTestAnd()
Performance test routine for quantify (all variables at the same time).
CalPerformanceTestCompose()
Performance test routine for quantify (all variables at the same time).
CalPerformanceTestMultiway()
Performance test routine for quantify (all variables at the same time).
CalPerformanceTestNonSuperscalar()
Performance test routine for quantify (all variables at the same time).
CalPerformanceTestOneway()
Performance test routine for quantify (all variables at the same time).
CalPerformanceTestQuantifyAllTogether()
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).
CalQuantifySanityCheck()
Performance test routine for quantify (all variables at the same time).
CalReorderAssociationFix()
required
CalRepackNodesAfterGC()
required
CalRequestNodeListArrayITE()
required
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
CalRequestNodeListCompose()
required
CalSetInteract()
Set interaction matrix entries.
CalTestInteract()
Test interaction matrix entries.
CalUniqueTableForIdFindOrAdd()
find or add in the unique table for id.
CalUniqueTableForIdLookup()
Lookup unique table for id.
CalUniqueTableForIdRehashNode()
required
CalUniqueTablePrint()
required
CalVarAssociationRepackUpdate()
Need to be called after repacking.
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_BddAnd()
Returns the BDD for logical AND of argument BDDs
Cal_BddBetween()
Returns a minimal BDD whose function contains fMin and is contained in fMax.
Cal_BddCofactor()
Returns the generalized cofactor of BDD f with respect to BDD c.
Cal_BddCompose()
composition - substitute a BDD variable by a function
Cal_BddDependsOn()
Returns 1 if f depends on var and returns 0 otherwise.
Cal_BddDumpBdd()
Write a BDD to a file
Cal_BddDynamicReordering()
Specify dynamic reordering technique.
Cal_BddElse()
Returns the negative cofactor of the argument BDD with respect to the top variable of the BDD.
Cal_BddExists()
Returns the result of existentially quantifying some variables from the given BDD.
Cal_BddForAll()
Returns the result of universally quantifying some variables from the given BDD.
Cal_BddFree()
Frees the argument BDD.
Cal_BddFunctionPrint()
Prints the function implemented by the argument BDD
Cal_BddFunctionProfileMultiple()
Returns a "function profile" for fArray.
Cal_BddFunctionProfile()
Returns a "function profile" for f.
Cal_BddGetIfId()
Returns the id of the top variable of the argument BDD.
Cal_BddGetIfIndex()
Returns the index of the top variable of the argument BDD.
Cal_BddGetRegular()
Returns a BDD with positive from a given BDD with arbitrary phase
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
Cal_BddIdentity()
Returns the duplicate BDD of the argument BDD.
Cal_BddIf()
Returns the BDD corresponding to the top variable of the argument BDD.
Cal_BddImplies()
Computes a BDD that implies conjunction of f and Cal_BddNot(g)
Cal_BddIntersects()
Computes a BDD that implies conjunction of f and g.
Cal_BddIsBddConst()
Returns 1 if the argument BDD is a constant, 0 otherwise.
Cal_BddIsBddNull()
Returns 1 if the argument BDD is NULL, 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_BddIsCube()
Returns 1 if the argument BDD is a cube, 0 otherwise
Cal_BddIsEqual()
Returns 1 if argument BDDs are equal, 0 otherwise.
Cal_BddIsProvisional()
Returns 1, if the given user BDD contains provisional BDD node.
Cal_BddManagerCreateNewVarAfter()
Creates and returns a new variable after the specified one in the variable order.
Cal_BddManagerCreateNewVarBefore()
Creates and returns a new variable before the specified one in the variable order.
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_BddManagerGC()
Invokes the garbage collection at the manager level.
Cal_BddManagerGetHooks()
Returns the hooks field of the manager.
Cal_BddManagerGetNumNodes()
Returns the number of BDD nodes
Cal_BddManagerGetVarWithId()
Returns the variable with the specified id, null if no such variable exists
Cal_BddManagerGetVarWithIndex()
Returns the variable with the specified index, null if no such variable exists
Cal_BddManagerInit()
Creates and initializes a new BDD manager.
Cal_BddManagerQuit()
Frees the BDD manager and all the associated allocations
Cal_BddManagerSetGCLimit()
Sets the limit of the garbage collection.
Cal_BddManagerSetHooks()
Sets the hooks field of the manager.
Cal_BddManagerSetParameters()
Sets appropriate fields of BDD Manager.
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
Cal_BddNand()
Returns the BDD for logical NAND of argument BDDs
Cal_BddNewVarBlock()
Creates and returns a variable block used for controlling dynamic reordering.
Cal_BddNodeLimit()
Sets the node limit to new_limit and returns the old limit.
Cal_BddNor()
Returns the BDD for logical NOR of argument BDDs
Cal_BddNot()
Returns the complement of the argument BDD.
Cal_BddOne()
Returns the BDD for the constant one
Cal_BddOr()
Returns the BDD for logical OR of argument BDDs
Cal_BddOverflow()
Returns 1 if the node limit has been exceeded, 0 otherwise. The overflow flag is cleared.
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_BddPrintBdd()
Prints a BDD in the human readable form.
Cal_BddPrintFunctionProfileMultiple()
Cal_BddPrintFunctionProfileMultiple is like Cal_BddPrintFunctionProfile except for multiple BDDs
Cal_BddPrintFunctionProfile()
Cal_BddPrintFunctionProfile is like Cal_BddPrintProfile except it displays a function profile for f
Cal_BddPrintProfileMultiple()
Cal_BddPrintProfileMultiple is like Cal_BddPrintProfile except it displays the profile for a set of BDDs
Cal_BddPrintProfile()
Displays the node profile for f on fp. lineLength specifies the maximum line length. varNamingFn is as in Cal_BddPrintBdd.
Cal_BddProfileMultiple()
Cal_BddProfile()
Returns a "node profile" of f, i.e., the number of nodes at each level in f.
Cal_BddReduce()
Returns a BDD which agrees with f for all valuations which satisfy c.
Cal_BddRelProd()
Returns the result of taking the logical AND of the argument BDDs and existentially quantifying some variables from the product.
Cal_BddReorder()
Invoke the current dynamic reodering method.
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)
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_BddSetGCMode()
Sets the garbage collection mode, 0 means the garbage collection should be turned off, 1 means garbage collection should be on.
Cal_BddSizeMultiple()
The routine is like Cal_BddSize, but takes a null-terminated array of BDDs and accounts for sharing of nodes.
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_BddStats()
Prints miscellaneous BDD statistics
Cal_BddSubstitute()
Substitute a set of variables by functions
Cal_BddSupport()
returns the support of f as a null-terminated array of variables
Cal_BddSwapVars()
Return a function obtained by swapping two variables
Cal_BddThen()
Returns the positive cofactor of the argument BDD with respect to the top variable of the BDD.
Cal_BddTotalSize()
Returns the number of nodes in the Unique table
Cal_BddType()
Returns type of a BDD ( 0, 1, +var, -var, ovrflow, nonterminal)
Cal_BddUnFree()
Unfrees the argument BDD.
Cal_BddUndumpBdd()
Reads a BDD from a file
Cal_BddVarBlockReorderable()
Sets the reoderability of a particular block.
Cal_BddVarSubstitute()
Substitute a set of variables by set of another variables.
Cal_BddVars()
Returns the number of BDD variables
Cal_BddXnor()
Returns the BDD for logical exclusive NOR of argument BDDs
Cal_BddXor()
Returns the BDD for logical exclusive OR of argument BDDs
Cal_BddZero()
Returns the BDD for the constant zero
Cal_MemAllocation()
Returns the memory allocated.
Cal_MemFatal()
Prints an error message and exits.
Cal_MemFreeBlock()
Frees the block.
Cal_MemFreeRecMgr()
Frees all the storage associated with the specified record manager.
Cal_MemFreeRec()
Frees a record managed by the indicated record manager.
Cal_MemGetBlock()
Allocates a new block of the specified size.
Cal_MemNewRecMgr()
Creates a new record manager with the given record size.
Cal_MemNewRec()
Allocates a record from the specified record manager.
Cal_MemResizeBlock()
Expands or contracts the block to a new size. We try to avoid moving the block if possible.
Cal_PerformanceTest()
Main routine for testing performances of various routines.
Cal_PipelineCreateProvisionalBdd()
Create a provisional BDD in the pipeline.
Cal_PipelineExecute()
Executes a pipeline.
Cal_PipelineInit()
Initialize a BDD pipeline.
Cal_PipelineQuit()
Resets the pipeline freeing all resources.
Cal_PipelineSetDepth()
Set depth of a BDD pipeline.
Cal_PipelineUpdateProvisionalBdd()
Update a provisional Bdd obtained during pipelining.
Cal_TempAssociationAugment()
Adds to the temporary variable association.
Cal_TempAssociationInit()
Sets the temporary variable association.
Cal_TempAssociationQuit()
Cleans up temporary association
CeilLog2()
Returns the smallest integer greater than or equal to log2 of a number
CeilLog2()
Returns the smallest integer greater than or equal to log2 of a number
CeilLog2()
Returns the smallest integer greater than or equal to log2 of a number
CeilLog2()
Returns the smallest integer greater than or equal to log2 of a number
CeilingLog2()
required
Chars()
required
CheckAssoc()
required
CheckValidityOfNodes()
required
CofactorFixAndReclaimForwardedNodes()
required
Cofactor()
required
Decode()
required
Error()
required
GetRandomNumbers()
Generates "count" many random numbers ranging between "lowerBound" and "upperBound".
HashTableAddDirect()
Directly insert a BDD node in the hash table.
HashTableApply()
required
HashTableCofactorApply()
required
HashTableCofactorReduce()
required
HashTableFindOrAdd()
required
HashTableOneRehash()
required
HashTableReduceApply()
required
HashTableReduce()
required
IndexCmp()
MergeAndFree()
required
PageAlign()
Return page aligned address greater than or equal to the pointer.
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.
PrintBddProfileAfterReorder()
required
PrintBdd()
required
RandomTests()
required
Read()
RemoveFromFreeList()
required
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.
SweepVarTable()
required
TestAnd()
required
TestArrayOp()
required
TestAssoc()
required
TestCompose()
required
TestDump()
required
TestGenCof()
required
TestITE()
required
TestIdNot()
required
TestInterImpl()
required
TestMultiwayAnd()
required
TestMultiwayLarge()
required
TestMultiwayOr()
required
TestNand()
required
TestOr()
required
TestPipeline()
required
TestQnt()
required
TestReduce()
required
TestRelProd()
required
TestReorderBlock()
required
TestReorder()
required
TestSatisfy()
required
TestSize()
required
TestSubstitute()
required
TestSwapVars()
required
TestVarSubstitute()
required
TestXor()
required
TrimToSize()
required
UniqueTableForIdFindOrAdd()
find or add in the unique table for id.
Write()
asAddress()
required
asDouble()
required
chars()
cpuTime()
Computes the number of page faults.
cpuTime()
required
ddClearLocal()
Performs a DFS from f, clearing the LSB of the then pointers.
ddSuppInteract()
Find the support of f.
ddUpdateInteract()
Marks as interacting all pairs of variables that appear in support.
elapsedTime()
Computes the time.
elapsedTime()
Computes the time.
handler()
required
main()
required
main()
required
pageFaults()
Computes the number of page faults.
terminalIdFn()
required

Last updated on 970711 20h11