    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`

    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`

    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

    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

    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`

    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`

    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

    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

    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`

    void
    Cal_BddDynamicReordering(
      Cal_BddManager  bddManager,
      int  technique
    )

  Selects the method for dynamic reordering.

  Side Effects None

  See Also `Cal_BddReorder`

    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`

    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`

    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.

    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`

    void
    Cal_BddFunctionPrint(
      Cal_BddManager  bddManager,
      Cal_Bdd  userBdd,
      char * name
    )

  Prints the function implemented by the argument BDD

  Side Effects None

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

  optional

  Side Effects None

  See Also `optional`

    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`

    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`

    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`

    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.

    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`

    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`

    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.

    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`

    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`

    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`

    int
    Cal_BddIsBddNull(
      Cal_BddManager  bddManager,
      Cal_Bdd  userBdd
    )

  Returns 1 if the argument BDD is NULL, 0 otherwise.

  Side Effects None.

    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`

    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`

    int
    Cal_BddIsCube(
      Cal_BddManager  bddManager,
      Cal_Bdd  fUserBdd
    )

  Returns 1 if the argument BDD is a cube, 0 otherwise

  Side Effects None

    int
    Cal_BddIsEqual(
      Cal_BddManager  bddManager,
      Cal_Bdd  userBdd1,
      Cal_Bdd  userBdd2
    )

  Returns 1 if argument BDDs are equal, 0 otherwise.

  Side Effects None.

    int
    Cal_BddIsProvisional(
      Cal_BddManager  bddManager,
      Cal_Bdd  userBdd
    )

  Returns 1, if the given user BDD contains provisional BDD node.

  Side Effects None.

    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

    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

    Cal_Bdd
    Cal_BddManagerCreateNewVarFirst(
      Cal_BddManager  bddManager
    )

  Creates and returns a new variable at the start of the variable order.

  Side Effects None

    Cal_Bdd
    Cal_BddManagerCreateNewVarLast(
      Cal_BddManager  bddManager
    )

  Creates and returns a new variable at the end of the variable order.

  Side Effects None

    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.

    void *
    Cal_BddManagerGetHooks(
      Cal_BddManager  bddManager
    )

  Returns the hooks field of the manager.

  Side Effects None

    unsigned long
    Cal_BddManagerGetNumNodes(
      Cal_BddManager  bddManager
    )

  Returns the number of BDD nodes

  Side Effects None

  See Also `Cal_BddTotalSize`

    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`

    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

    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`

    int
    Cal_BddManagerQuit(
      Cal_BddManager  bddManager
    )

  Frees the BDD manager and all the associated allocations

  Side Effects None

  See Also `Cal_BddManagerInit`

    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.

    void
    Cal_BddManagerSetHooks(
      Cal_BddManager  bddManager,
      void * hooks
    )

  Sets the hooks field of the manager.

  Side Effects Hooks field changes.

    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

    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

    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

    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

    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

    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.

    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`

    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

    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`

    Cal_Bdd
    Cal_BddOne(
      Cal_BddManager  bddManager
    )

  Returns the BDD for the constant one

  Side Effects None

  See Also `Cal_BddZero`

    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

    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`

    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`

    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`

    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`

    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.

    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`

    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`

    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`

    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`

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

  optional

  Side Effects None

  See Also `optional`

    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`

    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`

    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.

    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`

    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`

    double
    Cal_BddSatisfyingFraction(
      Cal_BddManager  bddManager,
      Cal_Bdd  fUserBdd
    )

  optional

  Side Effects required

  See Also `optional`

    Cal_Bdd
    Cal_BddSatisfy(
      Cal_BddManager  bddManager,
      Cal_Bdd  fUserBdd
    )

  optional

  Side Effects required

  See Also `optional`

    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.

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

  optional

  Side Effects None

  See Also `optional`

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

  optional

  Side Effects None

  See Also `optional`

    void
    Cal_BddStats(
      Cal_BddManager  bddManager,
      FILE * fp
    )

  Prints miscellaneous BDD statistics

  Side Effects None

    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`

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

  optional

  Side Effects None

  See Also `optional`

    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`

    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`

    unsigned long
    Cal_BddTotalSize(
      Cal_BddManager  bddManager
    )

  Returns the number of nodes in the Unique table

  Side Effects None

  See Also `Cal_BddManagerGetNumNodes`

    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

    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`

    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`

    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.

    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`

    long
    Cal_BddVars(
      Cal_BddManager  bddManager
    )

  Returns the number of BDD variables

  Side Effects None

    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

    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

    Cal_Bdd
    Cal_BddZero(
      Cal_BddManager  bddManager
    )

  Returns the BDD for the constant zero

  Side Effects None

  See Also `Cal_BddOne`

    Cal_Address_t
    Cal_MemAllocation(

    )

  Returns the memory allocated.

  Side Effects required

  See Also `optional`

    void
    Cal_MemFatal(
      char * message
    )

  Prints an error message and exits.

  Side Effects required

  See Also `optional`

    void
    Cal_MemFreeBlock(
      Cal_Pointer_t  p
    )

  Frees the block.

  Side Effects required

  See Also `optional`

    void
    Cal_MemFreeRecMgr(
      Cal_RecMgr  mgr
    )

  Frees all the storage associated with the specified record manager.

  Side Effects required

  See Also `optional`

    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`

    Cal_Pointer_t
    Cal_MemGetBlock(
      Cal_Address_t  size
    )

  Allocates a new block of the specified size.

  Side Effects required

  See Also `optional`

    Cal_RecMgr
    Cal_MemNewRecMgr(
      int  size
    )

  Creates a new record manager with the given record size.

  Side Effects required

  See Also `optional`

    Cal_Pointer_t
    Cal_MemNewRec(
      Cal_RecMgr  mgr
    )

  Allocates a record from the specified record manager.

  Side Effects required

  See Also `optional`

    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`

    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`

    Cal_Bdd
    Cal_PipelineCreateProvisionalBdd(
      Cal_BddManager  bddManager,
      Cal_Bdd  fUserBdd,
      Cal_Bdd  gUserBdd
    )

  The provisional BDD is automatically freed once the pipeline is quitted.

    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`

    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.

    void
    Cal_PipelineQuit(
      Cal_BddManager  bddManager
    )

  The user must make sure to update all provisional BDDs of interest before calling this routine.

    void
    Cal_PipelineSetDepth(
      Cal_BddManager  bddManager,
      int  depth
    )

  The "depth" determines the amount of dependency we would allow in pipelined computation.

  Side Effects None.

    Cal_Bdd
    Cal_PipelineUpdateProvisionalBdd(
      Cal_BddManager  bddManager,
      Cal_Bdd  provisionalBdd
    )

  The provisional BDD is automatically freed after quitting pipeline.

    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

    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

    void
    Cal_TempAssociationQuit(
      Cal_BddManager  bddManager
    )

  Cleans up temporary associationoptional

  Side Effects None

Last updated on 970711 20h11