-  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