bdd.h File Reference

#include <stdio.h>

Go to the source code of this file.

Data Structures
struct	s_bddPair
	Data type for representing a set of variable substitutions for use with bdd_replace. More...
struct	s_bddStat
	Status information about the bdd package. More...
struct	s_bddGbcStat
	Status information about garbage collections. More...
struct	s_bddCacheStat
	Status information about cache usage. More...
Defines
#define	bddop_and   0
#define	bddop_xor   1
#define	bddop_or   2
#define	bddop_nand   3
#define	bddop_nor   4
#define	bddop_imp   5
#define	bddop_biimp   6
#define	bddop_diff   7
#define	bddop_less   8
#define	bddop_invimp   9
#define	bddop_not   10
#define	bddop_simplify   11
#define	bdd_relprod(a, b, var)   bdd_appex((a),(b),bddop_and,(var))
	Relational product.
#define	BDD_REORDER_NONE   0
#define	BDD_REORDER_WIN2   1
#define	BDD_REORDER_WIN2ITE   2
#define	BDD_REORDER_SIFT   3
#define	BDD_REORDER_SIFTITE   4
#define	BDD_REORDER_WIN3   5
#define	BDD_REORDER_WIN3ITE   6
#define	BDD_REORDER_RANDOM   7
#define	BDD_REORDER_FREE   0
#define	BDD_REORDER_FIXED   1
#define	BDD_MEMORY   (-1)
	Out of memory.
#define	BDD_VAR   (-2)
	Unknown variable.
#define	BDD_RANGE   (-3)
	Variable value out of range (not in domain).
#define	BDD_DEREF   (-4)
	Removing external reference to unknown node.
#define	BDD_RUNNING   (-5)
	Called bdd_init() twice whithout bdd_done().
#define	BDD_FILE   (-6)
	Some file operation failed.
#define	BDD_FORMAT   (-7)
	Incorrect file format.
#define	BDD_ORDER   (-8)
	Vars.
#define	BDD_BREAK   (-9)
	User called break.
#define	BDD_VARNUM   (-10)
	Different number of vars.
#define	BDD_NODES   (-11)
	Tried to set max. than there already has been allocated.
#define	BDD_OP   (-12)
	Unknown operator.
#define	BDD_VARSET   (-13)
	Illegal variable set.
#define	BDD_VARBLK   (-14)
	Bad variable block operation.
#define	BDD_DECVNUM   (-15)
	Trying to decrease the number of variables.
#define	BDD_REPLACE   (-16)
	Replacing to already existing variables.
#define	BDD_NODENUM   (-17)
	Number of nodes reached user defined maximum.
#define	BDD_ILLBDD   (-18)
	Illegal bdd argument.
#define	BDD_SIZE   (-19)
	Illegal size argument.
#define	BVEC_SIZE   (-20)
	Mismatch in bitvector size.
#define	BVEC_SHIFT   (-21)
	Illegal shift-left/right parameter.
#define	BVEC_DIVZERO   (-22)
	Division by zero.
#define	BDD_ERRNUM   24
Typedefs
typedef int	BDD
	Data type for representing BDDs.
typedef BDD	bdd
	Alternative name for data type for representing BDDs.
typedef s_bddPair	bddPair
	Data type for representing a set of variable substitutions for use with bdd_replace.
typedef s_bddStat	bddStat
	Status information about the bdd package.
typedef s_bddGbcStat	bddGbcStat
	Status information about garbage collections.
typedef s_bddCacheStat	bddCacheStat
	Status information about cache usage.
typedef void(*)	bddinthandler (int)
	Data type for error handlers for use with bdd_error_hook.
typedef void(*)	bddgbchandler (int, bddGbcStat *)
	Data type for garbage collection handlers for use with bdd_gbc_hook.
typedef void(*)	bdd2inthandler (int, int)
	Data type for node table resize handlers for use with bdd_resize_hook.
typedef int(*)	bddsizehandler (void)
	Data type for BDD minimization handlers for use with bdd_resize_hook.
typedef void(*)	bddfilehandler (FILE *, int)
	Data type for printing handlers for use with bdd_file_hook.
typedef void(*)	bddallsathandler (char *, int)
	Data type for satisfying assignment handlers for use with bdd_allsat.
Functions
bddinthandler	bdd_error_hook (bddinthandler handler)
	Set a handler for error conditions.
bddgbchandler	bdd_gbc_hook (bddgbchandler handler)
	Set a handler for garbage collections.
bdd2inthandler	bdd_resize_hook (bdd2inthandler handler)
	Set a handler for nodetable resizes.
bddinthandler	bdd_reorder_hook (bddinthandler handler)
	Sets a handler for automatic reorderings.
bddfilehandler	bdd_file_hook (bddfilehandler handler)
	Specifies a printing callback handler.
int	bdd_init (int nodesize, int cachesize)
	Initializes the bdd package.
void	bdd_done (void)
	Resets the bdd package.
int	bdd_setvarnum (int num)
	Set the number of used bdd variables.
int	bdd_extvarnum (int num)
	Add extra bdd variables.
int	bdd_isrunning (void)
	Test whether the package is started or not.
int	bdd_setmaxnodenum (int size)
	Set the maximum available number of bdd nodes.
int	bdd_setmaxincrease (int size)
	Set maximum number of nodes used to increase node table.
int	bdd_setminfreenodes (int mf)
	Set minimum number of nodes to be reclaimed after gbc (as a percentage).
int	bdd_getnodenum (void)
	Get the number of active nodes in use.
int	bdd_getallocnum (void)
	Get the number of allocated nodes.
char *	bdd_versionstr (void)
	Returns a text string with version information.
int	bdd_versionnum (void)
	Returns the version number of the bdd package.
void	bdd_stats (bddStat *stat)
	Returns some status information about the bdd package.
void	bdd_cachestats (bddCacheStat *s)
	Fetch cache access usage.
void	bdd_fprintstat (FILE *f)
	Print cache statistics to a file.
void	bdd_printstat (void)
	Print cache statistics to stdout.
void	bdd_default_gbchandler (int, bddGbcStat *)
	Default garbage collection handler.
void	bdd_default_errhandler (int e)
	Default error handler.
const char *	bdd_errstring (int)
	Converts an error code to a string.
void	bdd_clear_error (void)
	Clears an error condition in the kernel.
BDD	bdd_true (void)
	Returns the constant true bdd.
BDD	bdd_false (void)
	Returns the constant false bdd.
int	bdd_varnum (void)
	Returns the number of defined variables.
BDD	bdd_ithvar (int var)
	Returns a bdd representing the i'th variable.
BDD	bdd_nithvar (int var)
	Returns a bdd representing the negation of the i'th variable.
int	bdd_var (BDD r)
	Gets the variable labeling the bdd.
BDD	bdd_low (BDD r)
	Gets the false branch of a bdd.
BDD	bdd_high (BDD r)
	Gets the true branch of a bdd.
BDD	bdd_addref (BDD r)
	Increases the reference count on a node.
BDD	bdd_delref (BDD r)
	Decreases the reference count on a node.
void	bdd_gbc (void)
	Performs a manual garbage collection.
int	bdd_scanset (BDD a, int **varset, int *varnum)
	Returns an integer representation of a variable set.
BDD	bdd_makeset (int *varset, int varnum)
	Builds a bdd variable set from an integer array.
bddPair *	bdd_newpair (void)
	Creates an empty variable pair table.
int	bdd_setpair (bddPair *pair, int oldvar, int newvar)
	Set one variable pair.
int	bdd_setpairs (bddPair *pair, int *oldvar, int *newvar, int size)
	Defines a whole set of pairs.
int	bdd_setbddpair (bddPair *pair, int oldvar, BDD newvar)
	Set one variable pair.
int	bdd_setbddpairs (bddPair *pair, int *olvar, BDD *newvar, int size)
	Defines a whole set of pairs.
void	bdd_resetpair (bddPair *p)
	Clear all variable pairs.
void	bdd_freepair (bddPair *p)
	Frees a table of pairs.
int	bdd_setcacheratio (int r)
	Sets the cache ratio for the operator caches.
BDD	bdd_buildcube (int value, int width, BDD *var)
	Build a cube from an array of variables specified by a BDD array.
BDD	bdd_ibuildcube (int value, int width, int *var)
	Build a cube from an array of variables.
BDD	bdd_not (BDD r)
	Negates a bdd.
BDD	bdd_apply (BDD l, BDD r, int op)
	Basic bdd operations.
BDD	bdd_and (BDD l, BDD r)
	The logical 'and' of two bdds.
BDD	bdd_or (BDD l, BDD r)
	The logical 'or' of two bdds.
BDD	bdd_xor (BDD l, BDD r)
	The logical 'xor' of two bdds.
BDD	bdd_imp (BDD l, BDD r)
	The logical 'implication' between two bdds.
BDD	bdd_biimp (BDD l, BDD r)
	The logical 'bi-implication' between two bdds.
BDD	bdd_ite (BDD f, BDD g, BDD h)
	If-then-else operator.
BDD	bdd_restrict (BDD r, BDD var)
	Restric a set of variables to constant values.
BDD	bdd_constrain (BDD f, BDD c)
	Generalized cofactor.
BDD	bdd_replace (BDD r, bddPair *pair)
	Replaces variables with other variables.
BDD	bdd_compose (BDD f, BDD g, BDD v)
	Functional composition.
BDD	bdd_veccompose (BDD g, bddPair *pair)
	Simultaneous functional composition.
BDD	bdd_simplify (BDD f, BDD d)
	Coudert and madre's restrict function.
BDD	bdd_exist (BDD r, BDD var)
	Existential quantification of variables.
BDD	bdd_forall (BDD r, BDD var)
	Universal quantification of variables.
BDD	bdd_unique (BDD, BDD)
	Unique quantification of variables.
BDD	bdd_appex (BDD l, BDD r, int opr, BDD var)
	Apply operation and existential quantification.
BDD	bdd_appall (BDD l, BDD r, int opr, BDD var)
	Apply operation and universal quantification.
BDD	bdd_appuni (BDD l, BDD r, int opr, BDD var)
	Apply operation and unique quantification.
BDD	bdd_support (BDD r)
	Returns the variable support of a bdd.
BDD	bdd_satone (BDD r)
	Finds one satisfying variable assignment.
BDD	bdd_satoneset (BDD r, BDD var, BDD pol)
	Finds one satisfying variable assignment.
BDD	bdd_fullsatone (BDD r)
	Finds one satisfying variable assignment.
void	bdd_allsat (BDD r, bddallsathandler handler)
	Finds all satisfying variable assignments.
double	bdd_satcount (BDD r)
	Calculates the number of satisfying variable assignments.
double	bdd_satcountset (BDD, BDD)
	Calculates the number of satisfying variable assignments for a given set of variables.
double	bdd_satcountln (BDD r)
	Calculates the logarithm of the number of satisfying variable assignments.
double	bdd_satcountlnset (BDD r, BDD varset)
	Calculates the logarithm of the number of satisfying variable assignments for a given set of variables.
int	bdd_nodecount (BDD r)
	Counts the number of nodes used for a bdd.
int	bdd_anodecount (BDD *r, int num)
	Counts the number of shared nodes in an array of bdds.
int *	bdd_varprofile (BDD r)
	Returns a variable profile.
double	bdd_pathcount (BDD r)
	Count the number of paths leading to the true terminal.
void	bdd_printall (void)
	Prints all used entries in the node table to stdout.
void	bdd_fprintall (FILE *ofile)
	Prints all used entries in the node table to a file.
void	bdd_fprinttable (FILE *ofile, BDD r)
	Prints the node table entries used by a bdd to a file.
void	bdd_printtable (BDD r)
	Prints the node table entries used by a bdd to stdout.
void	bdd_fprintset (FILE *ofile, BDD r)
	Prints the set of truth assignments specified by a bdd to a file.
void	bdd_printset (BDD r)
	Prints the set of truth assignments specified by a bdd to stdout.
int	bdd_fnprintdot (char *fname, BDD r)
	Prints a description of a bdd in dot format to a file specified by filename.
void	bdd_fprintdot (FILE *ofile, BDD r)
	Prints a description of a bdd in dot format to a file.
void	bdd_printdot (BDD r)
	Prints a description of a bdd in dot format to stdout.
int	bdd_fnsave (char *fname, BDD r)
	Saves a bdd to a file specified by filename.
int	bdd_save (FILE *ofile, BDD r)
	Saves a bdd to a file.
int	bdd_fnload (char *fname, BDD *r)
	Loads a bdd from a file specified by filename.
int	bdd_load (FILE *ifile, BDD *r)
	Loads a bdd from a file.
int	bdd_swapvar (int v1, int v2)
	Swap two bdd variables.
void	bdd_default_reohandler (int prestate)
	Default reorder handler.
void	bdd_reorder (int method)
	Start dynamic reordering.
int	bdd_reorder_gain (void)
	Calculate the gain in size after a reordering.
bddsizehandler	bdd_reorder_probe (bddsizehandler handler)
	Define a handler for minimization of bdds.
void	bdd_clrvarblocks (void)
	Clears all variable blocks.
int	bdd_addvarblock (BDD b, int fixed)
	Adds a new variable block for reordering.
int	bdd_intaddvarblock (int first, int last, int fixed)
	Adds a new variable block for reordering.
void	bdd_varblockall (void)
	Add a variable block for all variables.
bddfilehandler	bdd_blockfile_hook (bddfilehandler handler)
	Specifies a printing callback handler.
int	bdd_autoreorder (int method)
	Enables automatic reordering.
int	bdd_autoreorder_times (int method, int num)
	Enables automatic reordering.
int	bdd_var2level (int var)
	Fetch the level of a specific bdd variable.
int	bdd_level2var (int level)
	Fetch the variable number of a specific level.
int	bdd_getreorder_times (void)
	Fetch the current number of allowed reorderings.
int	bdd_getreorder_method (void)
	Fetch the current reorder method.
void	bdd_enable_reorder (void)
	Enables automatic reordering.
void	bdd_disable_reorder (void)
	Disable automatic reordering.
int	bdd_reorder_verbose (int value)
	Enables verbose information about reorderings.
void	bdd_setvarorder (int *neworder)
	Set a specific variable order.
void	bdd_printorder (void)
	Prints the current order to stdout.
void	bdd_fprintorder (FILE *ofile)
	Prints the current order to a file.
Variables
const BDD	bddfalse
	The constant false bdd.
const BDD	bddtrue
	The constant true bdd.

---

Detailed Description

Definition in file bdd.h.

---