Structure declarations
enum	Cal_BddOpEnum { CAL_AND , CAL_OR , CAL_XOR }

typedef enum Cal_BddOpEnum	Cal_BddOp_t

Type declarations
typedef struct Cal_BddManagerStruct *	Cal_BddManager

typedef struct Cal_BddManagerStruct	Cal_BddManager_t

typedef struct CalBddNodeStruct *	Cal_Bdd

typedef unsigned short int	Cal_BddId_t

typedef unsigned short int	Cal_BddIndex_t

typedef char (	Cal_VarNamingFn_t) (Cal_BddManager, Cal_Bdd, Cal_Pointer_t)

typedef char (	Cal_TerminalIdFn_t) (Cal_BddManager, Cal_Address_t, Cal_Address_t, Cal_Pointer_t)

typedef struct Cal_BlockStruct *	Cal_Block

CAL Manager
EXTERN Cal_BddManager	Cal_BddManagerInit ()
	Creates and initializes a new BDD manager. More...

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

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

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

EXTERN void	Cal_BddManagerSetParameters (Cal_BddManager bddManager, long reorderingThreshold, long maxForwardedNodes, double repackAfterGCThreshold, double tableRepackThreshold)
	Sets appropriate fields of BDD Manager. More...

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

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

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

EXTERN int	Cal_BddOverflow (Cal_BddManager bddManager)
	Returns 1 if the node limit has been exceeded, 0 otherwise. More...

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

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

EXTERN void	Cal_BddSetGCMode (Cal_BddManager bddManager, int gcMode)
	Sets the garbage collection mode. More...

EXTERN void	Cal_BddManagerSetGCLimit (Cal_BddManager manager)
	Sets the limit of the garbage collection. More...

EXTERN int	Cal_BddManagerGC (Cal_BddManager bddManager)
	Invokes the garbage collection at the manager level. More...

EXTERN void	Cal_BddDynamicReordering (Cal_BddManager bddManager, int technique, int method)
	Specify dynamic reordering technique and method. More...

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

EXTERN Cal_Block	Cal_BddNewVarBlock (Cal_BddManager bddManager, Cal_Bdd variable, long length)
	Creates and returns a variable block used for controlling dynamic reordering. More...

EXTERN void	Cal_BddVarBlockReorderable (Cal_BddManager bddManager, Cal_Block block, int reorderable)
	Sets the reoderability of a particular block. More...

EXTERN int	Cal_AssociationInit (Cal_BddManager bddManager, Cal_Bdd *associationInfoUserBdds, int pairs)
	Creates or finds a variable association. More...

EXTERN void	Cal_AssociationQuit (Cal_BddManager bddManager, int associationId)
	Deletes the variable association given by id. More...

EXTERN int	Cal_AssociationSetCurrent (Cal_BddManager bddManager, int associationId)
	Sets the current variable association to the one given. More...

EXTERN void	Cal_TempAssociationInit (Cal_BddManager bddManager, Cal_Bdd *associationInfoUserBdds, int pairs)
	Sets the temporary variable association. More...

EXTERN void	Cal_TempAssociationAugment (Cal_BddManager bddManager, Cal_Bdd *associationInfoUserBdds, int pairs)
	Adds to the temporary variable association. More...

EXTERN void	Cal_TempAssociationQuit (Cal_BddManager bddManager)
	Cleans up temporary association. More...

EXTERN int	Cal_BddDumpBdd (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd userVars, FILE fp)
	Write a BDD to a file. More...

EXTERN Cal_Bdd	Cal_BddUndumpBdd (Cal_BddManager bddManager, Cal_Bdd userVars, FILE fp, int *error)
	Reads a BDD from a file. More...

BDD
EXTERN void	Cal_BddFree (Cal_BddManager bddManager, Cal_Bdd userBdd)
	Frees the argument BDD. More...

EXTERN void	Cal_BddUnFree (Cal_BddManager bddManager, Cal_Bdd userBdd)
	Unfrees the argument BDD. More...

EXTERN Cal_Bdd	Cal_BddNull (Cal_BddManager bddManager)
	Returns the NULL BDD.

EXTERN Cal_Bdd	Cal_BddOne (Cal_BddManager bddManager)
	The BDD for the constant one. More...

EXTERN Cal_Bdd	Cal_BddZero (Cal_BddManager bddManager)
	The BDD for the constant zero. More...

EXTERN Cal_Bdd	Cal_BddManagerCreateNewVarFirst (Cal_BddManager bddManager)
	Create and obtain a new variable at the start of the variable order.

EXTERN Cal_Bdd	Cal_BddManagerCreateNewVarLast (Cal_BddManager bddManager)
	Create and obtain a new variable at the end of the variable order.

EXTERN Cal_Bdd	Cal_BddManagerCreateNewVarBefore (Cal_BddManager bddManager, Cal_Bdd userBdd)
	Create and obtain a new variable before the specified one in the variable order.

EXTERN Cal_Bdd	Cal_BddManagerCreateNewVarAfter (Cal_BddManager bddManager, Cal_Bdd userBdd)
	Create and obtain a new variable after the specified one in the variable order.

EXTERN Cal_Bdd	Cal_BddManagerGetVarWithIndex (Cal_BddManager bddManager, Cal_BddIndex_t index)
	The variable with the specified index, null if no such variable exists. More...

EXTERN Cal_Bdd	Cal_BddManagerGetVarWithId (Cal_BddManager bddManager, Cal_BddId_t id)
	The variable with the specified id, null if no such variable exists. More...

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

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

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

EXTERN 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. More...

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

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

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

EXTERN long	Cal_BddSize (Cal_BddManager bddManager, Cal_Bdd fUserBdd, int negout)
	BDD size of `fUserBdd`. More...

EXTERN long	Cal_BddSizeMultiple (Cal_BddManager bddManager, Cal_Bdd *fUserBddArray, int negout)
	Similar to `Cal_BddSize` for a null-terminated array of BDDs and accounting for sharing of nodes.

EXTERN void	Cal_BddSupport (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd *support)
	Returns the support of f as a null-terminated array of variables.

EXTERN void	Cal_BddProfile (Cal_BddManager bddManager, Cal_Bdd fUserBdd, long *levelCounts, int negout)
	The number of nodes at each level in f. More...

EXTERN void	Cal_BddProfileMultiple (Cal_BddManager bddManager, Cal_Bdd fUserBddArray, long levelCounts, int negout)
	Similar to `Cal_BddProfile` for a null-terminated array of BDDs and accounting for sharing of nodes. More...

EXTERN void	Cal_BddFunctionProfile (Cal_BddManager bddManager, Cal_Bdd fUserBdd, long *funcCounts)
	The number of subfunctions of `f` which may be obtained by restricting variables with an index lower than n. More...

EXTERN void	Cal_BddFunctionProfileMultiple (Cal_BddManager bddManager, Cal_Bdd fUserBddArray, long funcCounts)
	Similar to `Cal_BddFunctionProfile` for a null-terminated array of BDDs and accounting for sharing of nodes. More...

EXTERN 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 BDD in the human readable form. More...

EXTERN void	Cal_BddPrintProfile (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_VarNamingFn_t varNamingProc, char env, int lineLength, FILE fp)
	Displays the node profile for `f` on `fp`. More...

EXTERN void	Cal_BddPrintProfileMultiple (Cal_BddManager bddManager, Cal_Bdd userBdds, Cal_VarNamingFn_t varNamingProc, char env, int lineLength, FILE *fp)
	Similar to `Cal_BddPrintProfile` but displays the profile for a set of BDDs. More...

EXTERN void	Cal_BddPrintFunctionProfile (Cal_BddManager bddManager, Cal_Bdd f, Cal_VarNamingFn_t varNamingProc, char env, int lineLength, FILE fp)
	Similar to `Cal_BddPrintProfile` but displays a function profile for `f`. More...

EXTERN void	Cal_BddPrintFunctionProfileMultiple (Cal_BddManager bddManager, Cal_Bdd userBdds, Cal_VarNamingFn_t varNamingProc, char env, int lineLength, FILE *fp)
	Similar to `Cal_BddPrintFunctionProfile` but displays a function profile for a set of BDDs. More...

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

EXTERN Cal_Bdd	Cal_BddIdentity (Cal_BddManager bddManager, Cal_Bdd userBdd)
	Duplicate of the argument BDD. More...

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

EXTERN Cal_Bdd	Cal_BddNot (Cal_BddManager bddManager, Cal_Bdd userBdd)
	Complement of the argument BDD. More...

EXTERN Cal_Bdd	Cal_BddCompose (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd, Cal_Bdd hUserBdd)
	Substitute a BDD variable by a function.

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

EXTERN 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)`. More...

EXTERN Cal_Bdd	Cal_BddITE (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd, Cal_Bdd hUserBdd)
	Logical If-Then-Else. More...

EXTERN Cal_Bdd	Cal_BddAnd (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
	Logical AND of argument BDDs.

EXTERN Cal_Bdd	Cal_BddMultiwayAnd (Cal_BddManager bddManager, Cal_Bdd *userBddArray)
	Logical AND of BDDs in argument null-terminated array of BDDs. More...

EXTERN Cal_Bdd	Cal_BddNand (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
	Logical NAND of argument BDDs. More...

EXTERN Cal_Bdd	Cal_BddOr (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
	Logical Or of argument BDDs.

EXTERN Cal_Bdd	Cal_BddMultiwayOr (Cal_BddManager bddManager, Cal_Bdd *userBddArray)
	Logical OR of BDDs in argument null-terminated array of BDDs. More...

EXTERN Cal_Bdd	Cal_BddNor (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
	Logical NOR of argument BDDs. More...

EXTERN Cal_Bdd	Cal_BddXor (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
	Logical XOR of argument BDDs.

EXTERN Cal_Bdd	Cal_BddMultiwayXor (Cal_BddManager bddManager, Cal_Bdd *userBddArray)
	Logical XOR of BDDs in argument null-terminated array of BDDs. More...

EXTERN Cal_Bdd	Cal_BddXnor (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
	Logical XNOR of argument BDDs. More...

EXTERN Cal_Bdd *	Cal_BddPairwiseAnd (Cal_BddManager bddManager, Cal_Bdd *userBddArray)
	Logical AND of BDD pairs in argument null-termiinated array of BDDs. More...

EXTERN Cal_Bdd *	Cal_BddPairwiseOr (Cal_BddManager bddManager, Cal_Bdd *userBddArray)
	Logical OR of BDD pairs in argument null-termiinated array of BDDs. More...

EXTERN Cal_Bdd *	Cal_BddPairwiseXor (Cal_BddManager bddManager, Cal_Bdd *userBddArray)
	Logical XOR of BDD pairs in argument null-termiinated array of BDDs. More...

EXTERN Cal_Bdd	Cal_BddSubstitute (Cal_BddManager bddManager, Cal_Bdd fUserBdd)
	Substitute a set of variables by functions. More...

EXTERN Cal_Bdd	Cal_BddVarSubstitute (Cal_BddManager bddManager, Cal_Bdd fUserBdd)
	Substitute a set of variables by set of another variables. More...

EXTERN Cal_Bdd	Cal_BddSwapVars (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd, Cal_Bdd hUserBdd)
	The function obtained by swapping two variables. More...

EXTERN Cal_Bdd	Cal_BddExists (Cal_BddManager bddManager, Cal_Bdd fUserBdd)
	Existentially quantification of some variables from the given BDD. More...

EXTERN Cal_Bdd	Cal_BddForAll (Cal_BddManager bddManager, Cal_Bdd fUserBdd)
	Universal quantification of some variables from the given BDD. More...

EXTERN Cal_Bdd	Cal_BddRelProd (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
	Logical AND of the argument BDDs and existentially quantifying some variables from the product. More...

EXTERN Cal_Bdd	Cal_BddCofactor (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd cUserBdd)
	Generalized cofactor of `f` with respect to `c`. More...

EXTERN Cal_Bdd	Cal_BddReduce (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd cUserBdd)
	A function that agrees with `f` for all valuations which satisfy `c`. More...

EXTERN Cal_Bdd	Cal_BddBetween (Cal_BddManager bddManager, Cal_Bdd fMinUserBdd, Cal_Bdd fMaxUserBdd)
	A function that contains `fMin` and is contained in `fMax`. More...

EXTERN Cal_Bdd	Cal_BddSatisfy (Cal_BddManager bddManager, Cal_Bdd fUserBdd)
	A satisfying assignment of `f`. More...

EXTERN Cal_Bdd	Cal_BddSatisfySupport (Cal_BddManager bddManager, Cal_Bdd fUserBdd)
	Returns a special cube contained in `f`. More...

EXTERN double	Cal_BddSatisfyingFraction (Cal_BddManager bddManager, Cal_Bdd fUserBdd)
	Fraction of valuations which make `f` true. More...

EXTERN int	Cal_BddType (Cal_BddManager bddManager, Cal_Bdd fUserBdd)
	The type of the given BDD (0, 1, +var, -var, overflow, nonterminal). More...

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

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

EXTERN Cal_Bdd	Cal_BddIf (Cal_BddManager bddManager, Cal_Bdd userBdd)
	A BDD corresponding to the top variable of the given BDD. More...

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

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

Pipelined BDD Manipulation
EXTERN int	Cal_PipelineInit (Cal_BddManager bddManager, Cal_BddOp_t bddOp)
	Initialize a BDD pipeline. More...

EXTERN void	Cal_PipelineQuit (Cal_BddManager bddManager)
	Resets the pipeline freeing all resources. More...

EXTERN void	Cal_PipelineSetDepth (Cal_BddManager bddManager, int depth)
	Set depth of a BDD pipeline. More...

EXTERN int	Cal_PipelineExecute (Cal_BddManager bddManager)
	Executes a pipeline. More...

EXTERN int	Cal_BddIsProvisional (Cal_BddManager bddManager, Cal_Bdd userBdd)
	Returns 1, if the given user BDD is a provisional BDD node. More...

EXTERN Cal_Bdd	Cal_PipelineCreateProvisionalBdd (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
	Create a provisional BDD in the pipeline. More...

EXTERN Cal_Bdd	Cal_PipelineUpdateProvisionalBdd (Cal_BddManager bddManager, Cal_Bdd provisionalBdd)
	Update a provisional BDD obtained during pipelining. More...

Constant declarations
#define	CAL_BDD_TYPE_NONTERMINAL 0

#define	CAL_BDD_TYPE_ZERO 1

#define	CAL_BDD_TYPE_ONE 2

#define	CAL_BDD_TYPE_POSVAR 3

#define	CAL_BDD_TYPE_NEGVAR 4

#define	CAL_BDD_TYPE_OVERFLOW 5

#define	CAL_BDD_TYPE_CONSTANT 6

#define	CAL_BDD_UNDUMP_FORMAT 1

#define	CAL_BDD_UNDUMP_OVERFLOW 2

#define	CAL_BDD_UNDUMP_IOERROR 3

#define	CAL_BDD_UNDUMP_EOF 4

#define	CAL_REORDER_NONE 0

#define	CAL_REORDER_SIFT 1

#define	CAL_REORDER_WINDOW 2

#define	CAL_REORDER_METHOD_BF 0

#define	CAL_REORDER_METHOD_DF 1

Macro declarations
#define	EXTERN extern

#define	Cal_BddNamingFnNone ((char ()(Cal_BddManager, Cal_Bdd, Cal_Pointer_t))0)
	Default BDD variable naming function.

#define	Cal_BddTerminalIdFnNone ((char ()(Cal_BddManager, Cal_Address_t, Cal_Address_t, Cal_Pointer_t))0)
	Default BDD terminal naming function.

#define	Cal_Assert(valid) assert(valid)

Detailed Description

CHeaderFile*****************************************************************

FileName [cal.h]

PackageName [cal]

Synopsis [Header CAL file for exported data structures and functions.]

Description []

SeeAlso [optional]

Author [Rajeev K. Ranjan (rajee.nosp@m.v@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u) Jagesh V. Sanghavi (sangh.nosp@m.avi@.nosp@m.eecs..nosp@m.berk.nosp@m.eley..nosp@m.edu)]

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

Revision [

Id: cal.h,v 1.6 1998/09/15 19:02:51 ravi Exp

]

Function Documentation

◆ Cal_AssociationInit()

EXTERN int Cal_AssociationInit	(	Cal_BddManager	bddManager,
		Cal_Bdd *	associationInfoUserBdds,
		int	pairs
	)

Creates or finds a variable association.

Parameters

associationInfoUserBdds	An array of BDD with Cal_BddNull(bddManager) as the end marker.
pairs	If 0, the array assumed to be an array of variables. Otherwise, it is interpreted as consecutive pairs of variables.

If pairs is non-zero, then associationInfoUserBdds must be of even length, the even numbered array elements should be variables, and the odd numbered elements should be the BDDs which they are mapped to.

Returns: 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.

◆ Cal_AssociationQuit()

EXTERN void Cal_AssociationQuit	(	Cal_BddManager	bddManager,
		int	associationId
	)

Deletes the variable association given by id.

Decrements the reference count of the variable association with identifier id, and frees it if the reference count becomes zero.

See also: Cal_AssociationInit

◆ Cal_AssociationSetCurrent()

EXTERN int Cal_AssociationSetCurrent	(	Cal_BddManager	bddManager,
		int	associationId
	)

Sets the current variable association to the one given.

Parameters

associationId The id of the association to currently use. Set it to -1 if the temporary association should be used.

Returns: ID of the prior association (if any). A return value of -1 indicates the temporary association.

◆ Cal_BddBetween()

EXTERN Cal_Bdd Cal_BddBetween	(	Cal_BddManager	bddManager,
		Cal_Bdd	fMinUserBdd,
		Cal_Bdd	fMaxUserBdd
	)

A function that contains fMin and is contained in fMax.

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`).

See also: Cal_BddReduce

◆ Cal_BddCofactor()

EXTERN Cal_Bdd Cal_BddCofactor	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd,
		Cal_Bdd	cUserBdd
	)

Generalized cofactor of f with respect to c.

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.

See also: Cal_BddReduce

◆ Cal_BddDumpBdd()

EXTERN int Cal_BddDumpBdd	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd,
		Cal_Bdd *	userVars,
		FILE *	fp
	)

Write a BDD to a file.

\userVars A null-terminated array of variables that include the support of f. These variables need not be in order of increasing index.

Parameters

fp	File to write to

Returns: A nonzero value if f was written to the file successfully.

◆ Cal_BddDynamicReordering()

EXTERN void Cal_BddDynamicReordering	(	Cal_BddManager	bddManager,
		int	technique,
		int	method
	)

Specify dynamic reordering technique and method.

See also: Cal_BddReorder

◆ Cal_BddElse()

EXTERN Cal_Bdd Cal_BddElse	(	Cal_BddManager	bddManager,
		Cal_Bdd	userBdd
	)

The negative cofactor of the argument BDD with respect to its top variable.

See also: Cal_BddThen

◆ Cal_BddExists()

EXTERN Cal_Bdd Cal_BddExists	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd
	)

Existentially quantification of some variables from the given BDD.

Returns the BDD for f with all the variables that are paired with something in the current variable association existentially quantified out.

See also: Cal_AssociationInit, Cal_AssociationSetCurrent, Cal_TempAssociationInit

◆ Cal_BddForAll()

EXTERN Cal_Bdd Cal_BddForAll	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd
	)

Universal quantification of some variables from the given BDD.

Returns the BDD for f with all the variables that are paired with something in the current variable association universally quantified out.

See also: Cal_AssociationInit, Cal_AssociationSetCurrent, Cal_TempAssociationInit

◆ Cal_BddFree()

EXTERN 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

◆ Cal_BddFunctionProfile()

EXTERN void Cal_BddFunctionProfile	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd,
		long *	funcCounts
	)

The number of subfunctions of f which may be obtained by restricting variables with an index lower than n.

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.

◆ Cal_BddFunctionProfileMultiple()

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

Similar to Cal_BddFunctionProfile for a null-terminated array of BDDs and accounting for sharing of nodes.

See also: Cal_BddFunctionProfile

◆ Cal_BddGetIfId()

EXTERN Cal_BddId_t Cal_BddGetIfId	(	Cal_BddManager	bddManager,
		Cal_Bdd	userBdd
	)

Returns the id of the top variable of the argument BDD.

See also: Cal_BddGetIfIndex

◆ Cal_BddGetIfIndex()

EXTERN Cal_BddId_t Cal_BddGetIfIndex	(	Cal_BddManager	bddManager,
		Cal_Bdd	userBdd
	)

Returns the index of the top variable of the argument BDD.

See also: Cal_BddGetIfId

◆ Cal_BddGetRegular()

EXTERN Cal_Bdd Cal_BddGetRegular	(	Cal_BddManager	bddManager,
		Cal_Bdd	userBdd
	)

Returns a BDD with positive from a given BDD with arbitrary phase.

\warn This does not increase the reference count of the BDD.

See also: Cal_BddNot

◆ Cal_BddIdentity()

EXTERN Cal_Bdd Cal_BddIdentity	(	Cal_BddManager	bddManager,
		Cal_Bdd	userBdd
	)

Duplicate of the argument BDD.

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

See also: Cal_BddNot

◆ Cal_BddIf()

EXTERN Cal_Bdd Cal_BddIf	(	Cal_BddManager	bddManager,
		Cal_Bdd	userBdd
	)

A BDD corresponding to the top variable of the given BDD.

See also: Cal_BddIfId, Cal_BddIfIndex

◆ Cal_BddImplies()

EXTERN 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).

\sideffect None

See also: Cal_BddIntersects

◆ Cal_BddIntersects()

EXTERN Cal_Bdd Cal_BddIntersects	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd,
		Cal_Bdd	gUserBdd
	)

Computes a BDD that implies conjunction of f and g.

\sideffect None

See also: Cal_BddImplies

◆ Cal_BddIsBddConst()

EXTERN 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.

See also: Cal_BddIsBddOne, Cal_BddIsBddZero

◆ Cal_BddIsBddOne()

EXTERN int Cal_BddIsBddOne	(	Cal_BddManager	bddManager,
		Cal_Bdd	userBdd
	)

Returns 1 if the argument BDD is constant one, 0 otherwise.

See also: Cal_BddIsBddZero, Cal_BddIsBddConst

◆ Cal_BddIsBddZero()

EXTERN int Cal_BddIsBddZero	(	Cal_BddManager	bddManager,
		Cal_Bdd	userBdd
	)

Returns 1 if the argument BDD is constant zero, 0 otherwise.

See also: Cal_BddIsBddOne, Cal_BddIsBddConst

◆ Cal_BddIsProvisional()

EXTERN int Cal_BddIsProvisional	(	Cal_BddManager	bddManager,
		Cal_Bdd	userBdd
	)

Returns 1, if the given user BDD is a provisional BDD node.

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

◆ Cal_BddITE()

EXTERN Cal_Bdd Cal_BddITE	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd,
		Cal_Bdd	gUserBdd,
		Cal_Bdd	hUserBdd
	)

Logical If-Then-Else.

Returns the BDD for the logical operation f ? g : h, i.e. f&g | ~f&h.

See also: Cal_BddAnd, Cal_BddNand, Cal_BddOr, Cal_BddNor, Cal_BddXor, Cal_BddXnor

◆ Cal_BddManagerGC()

EXTERN int Cal_BddManagerGC ( Cal_BddManager bddManager )

Invokes the garbage collection at the manager level.

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.

◆ Cal_BddManagerGetHooks()

EXTERN void* Cal_BddManagerGetHooks ( Cal_BddManager bddManager )

Returns the hooks field of the manager.

See also: Cal_BddManagerSetHooks

◆ Cal_BddManagerGetNumNodes()

EXTERN unsigned long Cal_BddManagerGetNumNodes ( Cal_BddManager bddManager )

Returns the number of BDD nodes.

See also: Cal_BddTotalSize

◆ Cal_BddManagerGetVarWithId()

EXTERN Cal_Bdd Cal_BddManagerGetVarWithId	(	Cal_BddManager	bddManager,
		Cal_BddId_t	id
	)

The variable with the specified id, null if no such variable exists.

See also: Cal_BddManagerGetVarWithIndex

◆ Cal_BddManagerGetVarWithIndex()

EXTERN Cal_Bdd Cal_BddManagerGetVarWithIndex	(	Cal_BddManager	bddManager,
		Cal_BddIndex_t	index
	)

The variable with the specified index, null if no such variable exists.

See also: Cal_BddManagerGetVarWithId

◆ Cal_BddManagerInit()

EXTERN Cal_BddManager Cal_BddManagerInit ( )

Creates and initializes a new BDD manager.

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.

See also: Cal_BddManagerQuit

◆ Cal_BddManagerQuit()

EXTERN int Cal_BddManagerQuit ( Cal_BddManager bddManager )

Frees the BDD manager and all the associated allocations.

See also: Cal_BddManagerInit

◆ Cal_BddManagerSetGCLimit()

EXTERN void Cal_BddManagerSetGCLimit ( Cal_BddManager manager )

Sets the limit of the garbage collection.

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

◆ Cal_BddManagerSetHooks()

EXTERN void Cal_BddManagerSetHooks	(	Cal_BddManager	bddManager,
		void *	hooks
	)

Sets the hooks field of the manager.

Side effects:: Hooks field changes.

See also: Cal_BddManagerGetHooks

◆ Cal_BddManagerSetParameters()

EXTERN void Cal_BddManagerSetParameters	(	Cal_BddManager	bddManager,
		long	reorderingThreshold,
		long	maxForwardedNodes,
		double	repackAfterGCThreshold,
		double	tableRepackThreshold
	)

Sets appropriate fields of BDD Manager.

This function is used to set the parameters which are used to control the reordering process. 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.

Parameters

reorderingThreshold	The number of nodes below which reordering will NOT be invoked.
maxForwardedNodes	The maximum number of forwarded nodes which are allowed (at that point the cleanup must be done)
repackAfterGCThreshold	The fraction of the page utilized that garbage collection has to achieve.
tableRepackThreshold	The fraction of the page utilized below which repacking has to be invoked.

◆ Cal_BddMultiwayAnd()

EXTERN Cal_Bdd Cal_BddMultiwayAnd	(	Cal_BddManager	bddManager,
		Cal_Bdd *	userBddArray
	)

Logical AND of BDDs in argument null-terminated array of BDDs.

See also: Cal_BddAnd

◆ Cal_BddMultiwayOr()

EXTERN Cal_Bdd Cal_BddMultiwayOr	(	Cal_BddManager	bddManager,
		Cal_Bdd *	userBddArray
	)

Logical OR of BDDs in argument null-terminated array of BDDs.

See also: Cal_BddOr

◆ Cal_BddMultiwayXor()

EXTERN Cal_Bdd Cal_BddMultiwayXor	(	Cal_BddManager	bddManager,
		Cal_Bdd *	userBddArray
	)

Logical XOR of BDDs in argument null-terminated array of BDDs.

See also: Cal_BddXor

◆ Cal_BddNand()

EXTERN Cal_Bdd Cal_BddNand	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd,
		Cal_Bdd	gUserBdd
	)

Logical NAND of argument BDDs.

See also: Cal_BddAnd, Cal_BddNot

◆ Cal_BddNewVarBlock()

EXTERN Cal_Block Cal_BddNewVarBlock	(	Cal_BddManager	bddManager,
		Cal_Bdd	variable,
		long	length
	)

Creates and returns a variable block used for controlling dynamic reordering.

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.

◆ Cal_BddNodeLimit()

EXTERN 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_BddNor()

EXTERN Cal_Bdd Cal_BddNor	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd,
		Cal_Bdd	gUserBdd
	)

Logical NOR of argument BDDs.

See also: Cal_BddOr, Cal_BddNot

◆ Cal_BddNot()

EXTERN Cal_Bdd Cal_BddNot	(	Cal_BddManager	bddManager,
		Cal_Bdd	userBdd
	)

Complement of the argument BDD.

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

See also: Cal_BddIdentity

◆ Cal_BddOne()

EXTERN Cal_Bdd Cal_BddOne ( Cal_BddManager bddManager )

The BDD for the constant one.

See also: Cal_BddZero

◆ Cal_BddOverflow()

EXTERN int Cal_BddOverflow ( Cal_BddManager bddManager )

Returns 1 if the node limit has been exceeded, 0 otherwise.

Side effects:: The overflow flag is cleared.

See also: Cal_BddNodeLimit

◆ Cal_BddPairwiseAnd()

EXTERN Cal_Bdd* Cal_BddPairwiseAnd	(	Cal_BddManager	bddManager,
		Cal_Bdd *	userBddArray
	)

Logical AND of BDD pairs in argument null-termiinated array of BDDs.

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

See also: Cal_BddPairwiseOr, Cal_BddPairwiseXor

◆ Cal_BddPairwiseOr()

EXTERN Cal_Bdd* Cal_BddPairwiseOr	(	Cal_BddManager	bddManager,
		Cal_Bdd *	userBddArray
	)

Logical OR of BDD pairs in argument null-termiinated array of BDDs.

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

See also: Cal_BddPairwiseAnd, Cal_BddPairwiseXor

◆ Cal_BddPairwiseXor()

EXTERN Cal_Bdd* Cal_BddPairwiseXor	(	Cal_BddManager	bddManager,
		Cal_Bdd *	userBddArray
	)

Logical XOR of BDD pairs in argument null-termiinated array of BDDs.

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

See also: Cal_BddPairwiseAnd, Cal_BddPairwiseOr

◆ Cal_BddPrintBdd()

EXTERN 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 BDD in the human readable form.

Parameters

VarNamingFn	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 string 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 be null; in this case, default names are generated for all variables. The macro bddNamingFnNone is a null pointer of suitable type.
TerminalIdFn	A pointer to a function taking a bddManager, two longs, and 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.
fp	File to print the output to.

See also: Cal_BddNamingFnNone, Cal_BddTerminalIdFnNone

◆ Cal_BddPrintFunctionProfile()

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

Similar to Cal_BddPrintProfile but displays a function profile for f.

See also: Cal_BddPrintProfile, Cal_BddNamingFnNone

◆ Cal_BddPrintFunctionProfileMultiple()

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

Similar to Cal_BddPrintFunctionProfile but displays a function profile for a set of BDDs.

See also: Cal_BddPrintFunctionProfile, Cal_BddNamingFnNone

◆ Cal_BddPrintProfile()

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

Displays the node profile for f on fp.

Parameters

lineLength	The maximum line length.
varNamingFn	similar to `Cal_BddPrintBdd`.

See also: Cal_BddNamingFnNone

◆ Cal_BddPrintProfileMultiple()

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

Similar to Cal_BddPrintProfile but displays the profile for a set of BDDs.

See also: Cal_BddPrintProfile, Cal_BddNamingFnNone

◆ Cal_BddProfile()

EXTERN void Cal_BddProfile	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd,
		long *	levelCounts,
		int	negout
	)

The number of nodes at each level in f.

Parameters

levelCounts	An array of size `Cal_BddVars(bddManager)+1` to hold the profile.
negout	Similar as in `Cal_BddSize`.

◆ Cal_BddProfileMultiple()

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

Similar to Cal_BddProfile for a null-terminated array of BDDs and accounting for sharing of nodes.

See also: Cal_BddProfile

◆ Cal_BddReduce()

EXTERN Cal_Bdd Cal_BddReduce	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd,
		Cal_Bdd	cUserBdd
	)

A function that agrees with f for all valuations which satisfy c.

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.

See also: Cal_BddCofactor

◆ Cal_BddRelProd()

EXTERN Cal_Bdd Cal_BddRelProd	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd,
		Cal_Bdd	gUserBdd
	)

Logical AND of the argument BDDs and existentially quantifying some variables from the product.

See also: Cal_BddAnd, Cal_BddExists, Cal_AssociationInit, Cal_AssociationSetCurrent, Cal_TempAssociationInit

◆ Cal_BddReorder()

EXTERN void Cal_BddReorder ( Cal_BddManager bddManager )

Invoke the current dynamic reodering method.

Side effects:: Indexes of a variable may change due to reodering.

See also: Cal_BddDynamicReordering

◆ Cal_BddSatisfy()

EXTERN Cal_Bdd Cal_BddSatisfy	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd
	)

A satisfying assignment of f.

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.

See also: Cal_BddSatisfySupport

◆ Cal_BddSatisfyingFraction()

EXTERN double Cal_BddSatisfyingFraction	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd
	)

Fraction of valuations which make f true.

Remarks: This fraction is independent of whatever set of variables f is supposed to be a function of.

◆ Cal_BddSatisfySupport()

EXTERN Cal_Bdd Cal_BddSatisfySupport	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd
	)

Returns a special cube contained in f.

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.

See also: Cal_BddSatisfySupport

◆ Cal_BddSetGCMode()

EXTERN void Cal_BddSetGCMode	(	Cal_BddManager	bddManager,
		int	gcMode
	)

Sets the garbage collection mode.

Parameters

gcMode Set to 0 means the garbage collection should be turned off, while 1 means garbage collection should be on.

◆ Cal_BddSize()

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

BDD size of fUserBdd.

Parameters

negout If non-zero then the number of nodes in fUserBdd is counted. If zero, the counting pretends the BDDs do not have negative-output pointers.

◆ Cal_BddSubstitute()

EXTERN Cal_Bdd Cal_BddSubstitute	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd
	)

Substitute a set of variables by functions.

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.

See also: Cal_BddCompose, Cal_BddVarSubstitute

◆ Cal_BddSwapVars()

EXTERN Cal_Bdd Cal_BddSwapVars	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd,
		Cal_Bdd	gUserBdd,
		Cal_Bdd	hUserBdd
	)

The function obtained by swapping two variables.

Returns the BDD obtained by simultaneously substituting variable g by variable h and variable h and variable g in the BDD f.

See also: Cal_BddSubstitute

◆ Cal_BddThen()

EXTERN Cal_Bdd Cal_BddThen	(	Cal_BddManager	bddManager,
		Cal_Bdd	userBdd
	)

The positive cofactor of the argument BDD with respect to its top variable.

See also: Cal_BddElse

◆ Cal_BddTotalSize()

EXTERN unsigned long Cal_BddTotalSize ( Cal_BddManager bddManager )

Returns the number of nodes in the Unique table.

See also: Cal_BddManagerGetNumNodes

◆ Cal_BddType()

EXTERN int Cal_BddType	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd
	)

The type of the given BDD (0, 1, +var, -var, overflow, nonterminal).

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.

◆ Cal_BddUndumpBdd()

EXTERN Cal_Bdd Cal_BddUndumpBdd	(	Cal_BddManager	bddManager,
		Cal_Bdd *	userVars,
		FILE *	fp,
		int *	error
	)

Reads a BDD from a file.

If the same userVars is 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.

\params userVars 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.

\params fp File to load from.

Returns: The desired BDD or Null if the operation fails for some reason (node limit reached, I/O error, invalid file format, etc.). If it failed, 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

◆ Cal_BddUnFree()

EXTERN 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_BddVarBlockReorderable()

EXTERN void Cal_BddVarBlockReorderable	(	Cal_BddManager	bddManager,
		Cal_Block	block,
		int	reorderable
	)

Sets the reoderability of a particular block.

If a block is reorderable, the child blocks are recursively involved in swapping.

◆ Cal_BddVarSubstitute()

EXTERN Cal_Bdd Cal_BddVarSubstitute	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd
	)

Substitute a set of variables by set of another variables.

Returns a BDD for f using the substitution defined by current variable association. It is assumed that each variable is replaced by another variable.

Remarks: For the substitution of a variable by a function, use Cal::Substitute() instead.

See also: Cal_BddSubstitute

◆ Cal_BddXnor()

EXTERN Cal_Bdd Cal_BddXnor	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd,
		Cal_Bdd	gUserBdd
	)

Logical XNOR of argument BDDs.

See also: Cal_BddXor, Cal_BddNot

◆ Cal_BddZero()

EXTERN Cal_Bdd Cal_BddZero ( Cal_BddManager bddManager )

The BDD for the constant zero.

See also: Cal_BddOne

◆ Cal_PipelineCreateProvisionalBdd()

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

Create a provisional BDD in the pipeline.

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

◆ Cal_PipelineExecute()

EXTERN int Cal_PipelineExecute ( Cal_BddManager bddManager )

Executes a pipeline.

All the results are computed. User should update the BDDs of interest.

Todo:: This feature should eventually become transparent.

Returns: 1 if the pipeline was succesfull, 0 otherwise.

◆ Cal_PipelineInit()

EXTERN int Cal_PipelineInit	(	Cal_BddManager	bddManager,
		Cal_BddOp_t	bddOp
	)

Initialize a BDD pipeline.

Remarks: All the operations for this pipeline must be of the same kind.

See also: Cal_PipelineQuit

◆ Cal_PipelineQuit()

EXTERN void Cal_PipelineQuit ( Cal_BddManager bddManager )

Resets the pipeline freeing all resources.

Remarks: Make sure to update all provisional BDDs of interest before calling this routine.

See also: Cal_BddIsProvisional, Cal_PipelineUpdateProvisionalBdd

◆ Cal_PipelineSetDepth()

EXTERN void Cal_PipelineSetDepth	(	Cal_BddManager	bddManager,
		int	depth
	)

Set depth of a BDD pipeline.

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

◆ Cal_PipelineUpdateProvisionalBdd()

EXTERN Cal_Bdd Cal_PipelineUpdateProvisionalBdd	(	Cal_BddManager	bddManager,
		Cal_Bdd	provisionalBdd
	)

Update a provisional BDD obtained during pipelining.

The provisional BDD is automatically freed after quitting pipeline.

◆ Cal_TempAssociationAugment()

EXTERN void Cal_TempAssociationAugment	(	Cal_BddManager	bddManager,
		Cal_Bdd *	associationInfoUserBdds,
		int	pairs
	)

Adds to the temporary variable association.

Parameters

pairs Similar to Cal_TempAssociationInit.

◆ Cal_TempAssociationInit()

EXTERN void Cal_TempAssociationInit	(	Cal_BddManager	bddManager,
		Cal_Bdd *	associationInfoUserBdds,
		int	pairs
	)

Sets the temporary variable association.

Parameters

pairs Set this to 0 if the information represents only a list of variables rather than a full association.

See also: Cal_AssociationInit

◆ Cal_TempAssociationQuit()

EXTERN void Cal_TempAssociationQuit ( Cal_BddManager bddManager )

Cleans up temporary association.

See also: Cal_TempAssociationInit

Structure declarations

Type declarations

CAL Manager

BDD

Pipelined BDD Manipulation

Constant declarations

Macro declarations

Detailed Description

Function Documentation

◆ Cal_AssociationInit()

◆ Cal_AssociationQuit()

◆ Cal_AssociationSetCurrent()

◆ Cal_BddBetween()

◆ Cal_BddCofactor()

◆ Cal_BddDumpBdd()

◆ Cal_BddDynamicReordering()

◆ Cal_BddElse()

◆ Cal_BddExists()

◆ Cal_BddForAll()

◆ Cal_BddFree()

◆ Cal_BddFunctionProfile()

◆ Cal_BddFunctionProfileMultiple()

◆ Cal_BddGetIfId()

◆ Cal_BddGetIfIndex()

◆ Cal_BddGetRegular()

◆ Cal_BddIdentity()

◆ Cal_BddIf()

◆ Cal_BddImplies()

◆ Cal_BddIntersects()

◆ Cal_BddIsBddConst()

◆ Cal_BddIsBddOne()

◆ Cal_BddIsBddZero()

◆ Cal_BddIsProvisional()

◆ Cal_BddITE()

◆ Cal_BddManagerGC()

◆ Cal_BddManagerGetHooks()

◆ Cal_BddManagerGetNumNodes()

◆ Cal_BddManagerGetVarWithId()

◆ Cal_BddManagerGetVarWithIndex()

◆ Cal_BddManagerInit()

◆ Cal_BddManagerQuit()

◆ Cal_BddManagerSetGCLimit()

◆ Cal_BddManagerSetHooks()

◆ Cal_BddManagerSetParameters()

◆ Cal_BddMultiwayAnd()

◆ Cal_BddMultiwayOr()

◆ Cal_BddMultiwayXor()

◆ Cal_BddNand()

◆ Cal_BddNewVarBlock()

◆ Cal_BddNodeLimit()

◆ Cal_BddNor()

◆ Cal_BddNot()

◆ Cal_BddOne()

◆ Cal_BddOverflow()

◆ Cal_BddPairwiseAnd()

◆ Cal_BddPairwiseOr()

◆ Cal_BddPairwiseXor()

◆ Cal_BddPrintBdd()

◆ Cal_BddPrintFunctionProfile()

◆ Cal_BddPrintFunctionProfileMultiple()

◆ Cal_BddPrintProfile()

◆ Cal_BddPrintProfileMultiple()

◆ Cal_BddProfile()

◆ Cal_BddProfileMultiple()

◆ Cal_BddReduce()

◆ Cal_BddRelProd()

◆ Cal_BddReorder()

◆ Cal_BddSatisfy()

◆ Cal_BddSatisfyingFraction()

◆ Cal_BddSatisfySupport()

◆ Cal_BddSetGCMode()

◆ Cal_BddSize()

◆ Cal_BddSubstitute()

◆ Cal_BddSwapVars()

◆ Cal_BddThen()

◆ Cal_BddTotalSize()

◆ Cal_BddType()

◆ Cal_BddUndumpBdd()

◆ Cal_BddUnFree()

◆ Cal_BddVarBlockReorderable()