Core Manager of everything BDDs, variables, and more. More...

#include <calObj.hh>

Public Types
enum	ReorderTechnique { None = CAL_REORDER_NONE , Sift = CAL_REORDER_SIFT , Window = CAL_REORDER_WINDOW }
	The possible methods (algorithms) for variable reordering. More...

enum	ReorderMethod { BF = CAL_REORDER_METHOD_BF , DF = CAL_REORDER_METHOD_DF }
	The possible technique to be used to execute each method (c.f. `Cal::ReorderTechnique`). More...

Public Member Functions
	Cal ()
	Initialize a new BDD Manager.

	Cal (unsigned int numVars)
	Initialize a new BDD Manager with variables `[1, numVars]`.

	Cal (const Cal &o)=delete

	Cal (Cal &&o)
	Move ownership of C object.

	~Cal ()
	Clear memory of BDD Manager. More...

void	SetParameters (long reorderingThreshold, long maxForwardedNodes, double repackAfterGCThreshold, double tableRepackThreshold)
	Sets appropriate fields of BDD Manager. More...

unsigned long	Nodes () const
	The number of BDD nodes. More...

long	Vars () const
	The number of BDD variables.

bool	Overflow () const
	`true` if the node limit has been exceeded, `false` otherwise. More...

unsigned long	TotalSize () const
	The number of nodes in the Unique table. More...

void	Stats (FILE *fp=stdout) const
	Prints miscellaneous BDD statistics.

long	NodeLimit (long newLimit)
	Sets the node limit to `newLimit` and returns the previous limit. More...

void	SetGCMode (bool enableGC)
	Enable or Disable garbage collection.

void	SetGCLimit ()
	Sets the limit of the garbage collection. More...

void	GC ()
	Invokes the garbage collection at the manager level. More...

void	DynamicReordering (ReorderTechnique technique, ReorderMethod method=ReorderMethod::DF)
	Specify dynamic reordering technique and method. More...

void	Reorder ()
	Invoke the current dynamic reodering method. More...

template<typename IT >
int	AssociationInit (IT begin, IT end, const bool pairs=false)
	Creates or finds a variable association. More...

int	AssociationSetCurrent (int i)
	Sets the current variable association to the one given. More...

void	AssociationQuit (int i)
	Deletes the variable association given by id. More...

template<typename IT >
void	TempAssociationInit (IT begin, const IT end, const bool pairs=false)
	Sets the temporary variable association. More...

template<typename IT >
void	TempAssociationAugment (IT begin, const IT end, const bool pairs=false)
	Adds to the temporary variable association. More...

void	TempAssociationQuit ()
	Cleans up temporary association. More...

BDD	Null () const
	The NULL BDD.

BDD	One () const
	The BDD for the constant one. More...

BDD	Zero () const
	The BDD for the constant zero. More...

BDD	Id (Id_t id) const
	The variable with the specified id, null if no such variable exists. More...

BDD	Index (Index_t idx) const
	The variable with the specified index, null if no such variable exists. More...

BDD	CreateNewVarFirst ()
	Create and obtain a new variable at the start of the variable order.

BDD	CreateNewVarLast ()
	Create and obtain a new variable at the end of the variable order.

BDD	CreateNewVarBefore (const BDD &x)
	Create and obtain a new variable before the specified one in the variable order.

BDD	CreateNewVarAfter (const BDD &x)
	Create and obtain a new variable after the specified one in the variable order.

bool	IsNull (const BDD &f) const
	`true` if the given BDD is NULL, `false` otherwise.

bool	IsOne (const BDD &f) const
	`true` if the given BDD is constant one, `false`otherwise. More...

bool	IsZero (const BDD &f) const
	`true` if the given BDD is constant zero, `false`otherwise. More...

bool	IsConst (const BDD &f) const
	`true` if the given BDD is either constant one or constant zero, otherwise returns `false`. More...

bool	IsCube (const BDD &f) const
	`true` if the given BDD is a cube, `false` otherwise.

bool	IsEqual (const BDD &f, const BDD &g) const
	`true` if the two BDDs are equal, `false` otherwise. More...

bool	DependsOn (const BDD &f, const BDD &var) const
	`true` if the BDD `f` depends on `var`, `false` otherwise. More...

double	SatisfyingFraction (const BDD &f)
	Fraction of valuations which make this BDD true. More...

unsigned long	Size (const BDD &f, bool negout=true)
	This BDD's size. More...

template<typename IT >
unsigned long	Size (IT begin, IT end, bool negout=true)
	Similar to `Cal::Size()` for an iterator of BDDs. But, this accounts for sharing of nodes. More...

template<typename Container >
unsigned long	Size (Container c, bool negout=true)
	Similar to `Cal::Size()` for a container of BDDs. But, this accounts for sharing of nodes. More...

BDD	Identity (const BDD &f)
	Duplicate of given BDD. More...

BDD	Regular (const BDD &f)
	The given BDD in positive form (regardless of its phase). More...

BDD	Not (const BDD &f)
	Complement of the given BDD.

BDD	Compose (const BDD &f, const BDD &g, const BDD &h)
	Substitute a BDD variable by a function, i.e. f[h/g]. More...

BDD	Intersects (const BDD &f, const BDD &g)
	Computes a BDD that implies the conjunction of both BDDs. More...

BDD	Implies (const BDD &f, const BDD &g)
	Computes a BDD that implies the conjunction of `f` and `g.Not()`. More...

BDD	ITE (const BDD &f, const BDD &g, const BDD &h)
	Logical If-Then-Else. More...

BDD	And (const BDD &f, const BDD &g)
	Logical AND operation. More...

template<typename IT >
BDD	And (IT begin, IT end)
	Logical AND of iterator of `BDD` or `int`. More...

template<typename Container >
BDD	And (const Container &c)
	Logical AND of container with `BDD`s or `int`s. More...

BDD	Nand (const BDD &f, const BDD &g)
	Logical Negated AND operation. More...

BDD	Or (const BDD &f, const BDD &g)
	Logical OR operation.

template<typename IT >
BDD	Or (IT begin, IT end)
	Logical OR of iterator of `BDD` or `int`. More...

template<typename Container >
BDD	Or (const Container &c)
	Logical OR of container with `BDD`s or `int`s. More...

BDD	Nor (const BDD &f, const BDD &g)
	Logical Negated OR operation. More...

BDD	Xor (const BDD &f, const BDD &g)
	Logical XOR operation.w.

template<typename IT >
BDD	Xor (IT begin, IT end)
	Logical XOR of iterator of `BDD` or `int`. More...

template<typename Container >
BDD	Xor (const Container &c)
	Logical XOR of container with `BDD`s or `int`s. More...

BDD	Xnor (const BDD &f, const BDD &g)
	Logical Negated XOR operation.

template<typename IT >
std::vector< BDD >	PairwiseAnd (IT begin, IT end)
	Pairwise AND of `BDD`s or `int`s provided by an iterator. More...

template<typename Container >
std::vector< BDD >	PairwiseAnd (const Container &c)
	Pairwise AND of `BDD`s or `int`s within a container. More...

template<typename IT >
std::vector< BDD >	PairwiseOr (IT begin, IT end)
	Pairwise OR of `BDD`s or `int`s provided by an iterator. More...

template<typename Container >
std::vector< BDD >	PairwiseOr (const Container &c)
	Pairwise OR of `BDD`s or `int`s within a container. More...

template<typename IT >
std::vector< BDD >	PairwiseXor (IT begin, IT end)
	Pairwise XOR of `BDD`s or `int`s provided by an iterator. More...

template<typename Container >
std::vector< BDD >	PairwiseXor (const Container &c)
	Pairwise XOR of `BDD`s or `int`s within a container. More...

BDD	Satisfy (const BDD &f)
	A satisfying assignment of this BDD. More...

BDD	SatisfySupport (const BDD &f)
	Returns a special cube contained in this. More...

BDD	Substitute (const BDD &f)
	Substitute a set of variables by functions. More...

BDD	VarSubstitute (const BDD &f)

BDD	SwapVars (const BDD &f, const BDD &g, const BDD &h)
	The function obtained by swapping two variables. More...

BDD	Exists (const BDD &f)
	Existentially quantification of some variables from the given BDD. More...

BDD	ForAll (const BDD &f)
	Universal quantification of some variables from the given BDD. More...

BDD	RelProd (const BDD &f, const BDD &g)
	Logical AND of the argument BDDs and existentially quantifying some variables from the product. More...

BDD	Cofactor (const BDD &f, const BDD &c)
	Generalized cofactor of `f` with respect to `c`. More...

BDD	Reduce (const BDD &f, const BDD &c)
	Function that agrees with `f` for all valuations that satisfy `c`. More...

BDD	Between (const BDD &fMin, const BDD &fMax)
	Function that contains `fMin` and is contained in `fMax`. More...

BDD	If (const BDD &f) const
	BDD corresponding to the top variable of the given BDD. More...

Id_t	IfId (const BDD &f) const
	Returns the id of the given BDD's top variable. More...

Index_t	IfIndex (const BDD &f) const
	Returns the index of this BDD's top variable. More...

BDD	Then (const BDD &f)
	The positive cofactor of the given BDD with respect to its top variable. More...

BDD	Else (const BDD &f)
	The negative cofactor of the given BDD with respect to its top variable. More...

void	Print (const BDD &f, FILE *fp=stdout) const
	Prints a BDD in the human readable form. More...

void	FunctionPrint (const BDD &f, std::string &name) const
	Prints the function implemented by the given BDD. More...

std::vector< long >	Profile (const BDD &f, bool negout=true) const
	Obtain a vector with the number of nodes at each level in f. More...

template<typename IT >
std::vector< long >	Profile (IT begin, IT end, bool negout=true) const
	Similar to `Cal::Profile()` for an iterator of BDDs. But, this accounts for sharing of nodes. More...

template<typename Container >
std::vector< long >	Profile (const Container &c, bool negout=true) const
	Similar to `Cal::Profile()` for a container of BDDs. But, this accounts for sharing of nodes. More...

void	PrintProfile (const BDD &f, int lineLength=79, FILE *fp=stdout) const
	Prints a BDD in the human readable form. More...

template<typename IT >
void	PrintProfile (IT begin, IT end, int lineLength=79, FILE *fp=stdout) const
	Similar to `Cal::PrintProfile()` for an iterator of BDDs. But, this accounts for sharing of nodes. More...

template<typename Container >
void	PrintProfile (const Container &c, int lineLength=79, FILE *fp=stdout) const
	Similar to `Cal::PrintProfile` for a container of BDDs. But, this accounts for sharing of nodes.AssociationSetCurrent. More...

std::vector< long >	FunctionProfile (const BDD &f) const
	The number of subfunctions of the given BDD which may be obtained by restricting variables with an index lower than n. More...

template<typename IT >
std::vector< long >	FunctionProfile (IT begin, IT end) const
	Similar to `Cal::FunctionProfile` for an iterator of BDDs. But, this accounts for sharing of nodes. More...

template<typename Container >
std::vector< long >	FunctionProfile (const Container &c) const
	Similar to `Cal::FunctionProfile` for a container of BDDs. But, this accounts for sharing of nodes. More...

void	PrintFunctionProfile (const BDD &f, int lineLength=79, FILE *fp=stdout) const
	Similar to `Cal::PrintProfile()` but displays a function profile for the given BDD. More...

template<typename IT >
void	PrintFunctionProfile (IT begin, IT end, int lineLength=79, FILE *fp=stdout) const
	Similar to `Cal::PrintFunctionProfile` for an iterator of BDDs. But, this accounts for sharing of nodes. More...

template<typename Container >
void	PrintFunctionProfile (const Container &c, int lineLength=79, FILE *fp=stdout) const
	Similar to `Cal::PrintFunctionProfile` for a container of BDDs. But, this accounts for sharing of nodes. More...

Detailed Description

Core Manager of everything BDDs, variables, and more.

Remarks: The Cal class is designed based on non-sharing ownership. You can move the ownership to someone else, but you cannot create a copy of this class to have multiple owners of the same BDD Manager. Please use C++ references instead.

Member Enumeration Documentation

◆ ReorderMethod

enum Cal::ReorderMethod

The possible technique to be used to execute each method (c.f. Cal::ReorderTechnique).

See also: Cal::DynamicReordering, Cal::ReorderTechnique

◆ ReorderTechnique

enum Cal::ReorderTechnique

The possible methods (algorithms) for variable reordering.

See also: Cal::DynamicReordering, Cal::ReorderMethod

Constructor & Destructor Documentation

◆ ~Cal()

Cal::~Cal ( )

inline

Clear memory of BDD Manager.

If this object owns a Cal_BddManager from the C API, then that one is properly reset and freed.

Member Function Documentation

◆ And() [1/3]

BDD Cal::And	(	const BDD &	f,
		const BDD &	g
	)

inline

Logical AND operation.

See also: BDD::And()

◆ And() [2/3]

template<typename Container >

BDD Cal::And ( const Container & c )

inline

Logical AND of container with BDDs or ints.

If the container is of ints, the integers are converted into a BDD with Cal::Id().

Parameters

c	Container of BDDs or integers which supports `begin()` and `end()` iterators.

See also: BDD::And()

◆ And() [3/3]

template<typename IT >

BDD Cal::And	(	IT	begin,
		IT	end
	)

inline

Logical AND of iterator of BDD or int.

If IT::value_type is int then the integers are converted into a BDD with Cal::Id().

Parameters

begin	Iterator pointing to the start of the given range of BDDs or integers.
end	Iterator pointing to the end of the given range.

See also: BDD::And()

◆ AssociationInit()

template<typename IT >

int Cal::AssociationInit	(	IT	begin,
		IT	end,
		const bool	pairs = `false`
	)

inline

Creates or finds a variable association.

Parameters

begin	Iterator pointing to the start of the given range.
end	Iterator pointing to the end of the given range.
pairs	If `false`, the array assumed to be an array of variables. If `true`, it is interpreted as consecutive pairs of variables (and hence it must be of even length).

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.

See also: Cal::AssociationSetCurrent()

◆ AssociationQuit()

void Cal::AssociationQuit ( int i )

inline

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

◆ AssociationSetCurrent()

int Cal::AssociationSetCurrent ( int i )

inline

Sets the current variable association to the one given.

Parameters

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

See also: Cal::AssociationQuit()

◆ Between()

BDD Cal::Between	(	const BDD &	fMin,
		const BDD &	fMax
	)

inline

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::Cofactor(), Cal::Reduce()

◆ Cofactor()

BDD Cal::Cofactor	(	const BDD &	f,
		const BDD &	c
	)

inline

Generalized cofactor of f with respect to c.

Returns the generalized cofactor of f with respect to BDD c. The constrain operator given by Coudert et al (ICCAD90) is used to find the generalized cofactor.

See also: BDD::Cofactor(), Cal::Reduce()

◆ Compose()

BDD Cal::Compose	(	const BDD &	f,
		const BDD &	g,
		const BDD &	h
	)

inline

Substitute a BDD variable by a function, i.e. f[h/g].

See also: BDD::Compose()

◆ DependsOn()

bool Cal::DependsOn	(	const BDD &	f,
		const BDD &	var
	)		const

inline

true if the BDD f depends on var, false otherwise.

See also: BDD::DependsOn()

◆ DynamicReordering()

void Cal::DynamicReordering	(	ReorderTechnique	technique,
		ReorderMethod	method = `ReorderMethod::DF`
	)

inline

Specify dynamic reordering technique and method.

See also: Cal::Reorder()

◆ Else()

BDD Cal::Else ( const BDD & f )

inline

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

See also: BDD::Else()

◆ Exists()

BDD Cal::Exists ( const BDD & f )

inline

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::TempAssociationInit()

◆ ForAll()

BDD Cal::ForAll ( const BDD & f )

inline

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::TempAssociationInit()

◆ FunctionPrint()

void Cal::FunctionPrint	(	const BDD &	f,
		std::string &	name
	)		const

inline

Prints the function implemented by the given BDD.

See also: BDD::FunctionPrint()

◆ FunctionProfile() [1/3]

std::vector<long> Cal::FunctionProfile ( const BDD & f ) const

inline

The number of subfunctions of the given BDD 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 this which may be obtained by restricting the variables whose index is less than n. An entry of zero indicates that this is independent of the variable with the corresponding index.

See also: BDD::FunctionProfile()

◆ FunctionProfile() [2/3]

template<typename Container >

std::vector<long> Cal::FunctionProfile ( const Container & c ) const

inline

Similar to Cal::FunctionProfile for a container of BDDs. But, this accounts for sharing of nodes.

Parameters

c	Container of BDDs which supports `begin()` and `end()` iterators.

See also: BDD::FunctionProfile()

◆ FunctionProfile() [3/3]

template<typename IT >

std::vector<long> Cal::FunctionProfile	(	IT	begin,
		IT	end
	)		const

inline

Similar to Cal::FunctionProfile for an iterator of BDDs. But, this accounts for sharing of nodes.

Parameters

begin	Iterator pointing to the start of the given range of BDDs.
end	Iterator pointing to the end of the given range.

See also: BDD::FunctionProfile()

◆ GC()

void Cal::GC ( )

inline

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.

◆ Id()

BDD Cal::Id ( Id_t id ) const

inline

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

See also: Cal::Index()

◆ Identity()

BDD Cal::Identity ( const BDD & f )

inline

Duplicate of given BDD.

See also: BDD::Identity(), Cal::Not()

◆ If()

BDD Cal::If ( const BDD & f ) const

inline

BDD corresponding to the top variable of the given BDD.

See also: Bdd::If(), Cal::IfId(), Cal::IfIndex()

◆ IfId()

Id_t Cal::IfId ( const BDD & f ) const

inline

Returns the id of the given BDD's top variable.

See also: BDD::Id(), Cal::IfIndex()

◆ IfIndex()

Index_t Cal::IfIndex ( const BDD & f ) const

inline

Returns the index of this BDD's top variable.

See also: BDD::Index(), Cal::IfId()

◆ Implies()

BDD Cal::Implies	(	const BDD &	f,
		const BDD &	g
	)

inline

Computes a BDD that implies the conjunction of f and g.Not().

See also: BDD::Implies(), Cal::Intersects()

◆ Index()

BDD Cal::Index ( Index_t idx ) const

inline

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

See also: Cal::Id()

◆ Intersects()

BDD Cal::Intersects	(	const BDD &	f,
		const BDD &	g
	)

inline

Computes a BDD that implies the conjunction of both BDDs.

See also: BDD::Intersects(), Cal::Implies()

◆ IsConst()

bool Cal::IsConst ( const BDD & f ) const

inline

true if the given BDD is either constant one or constant zero, otherwise returns false.

See also: BDD::IsConst(), Cal::IsOne(), Cal::isZero()

◆ IsEqual()

bool Cal::IsEqual	(	const BDD &	f,
		const BDD &	g
	)		const

inline

true if the two BDDs are equal, false otherwise.

See also: BDD::IsEqualTo()

◆ IsOne()

bool Cal::IsOne ( const BDD & f ) const

inline

true if the given BDD is constant one, falseotherwise.

See also: BDD::IsOne, Cal::IsZero(), Cal::IsConst()

◆ IsZero()

bool Cal::IsZero ( const BDD & f ) const

inline

true if the given BDD is constant zero, falseotherwise.

See also: BDD::IsZero(), Cal::IsOne(), Cal::IsConst()

◆ ITE()

BDD Cal::ITE	(	const BDD &	f,
		const BDD &	g,
		const BDD &	h
	)

inline

Logical If-Then-Else.

See also: BDD::ITE()

◆ Nand()

BDD Cal::Nand	(	const BDD &	f,
		const BDD &	g
	)

inline

Logical Negated AND operation.

See also: BDD::Nand()

◆ NodeLimit()

long Cal::NodeLimit ( long newLimit )

inline

Sets the node limit to newLimit and returns the previous limit.

Side effects:: Threshold for garbage collection may change.

See also: Cal::SetGCLimit(), Cal::GC()

◆ Nodes()

unsigned long Cal::Nodes ( ) const

inline

The number of BDD nodes.

See also: Cal::TotalSize()

◆ Nor()

BDD Cal::Nor	(	const BDD &	f,
		const BDD &	g
	)

inline

Logical Negated OR operation.

See also: BDD::Nor()

◆ One()

BDD Cal::One ( ) const

inline

The BDD for the constant one.

See also: Cal::Zero()

◆ Or() [1/2]

template<typename Container >

BDD Cal::Or ( const Container & c )

inline

Logical OR of container with BDDs or ints.

If the container is of ints, the integers are converted into a BDD with Cal::Id().

Parameters

c	Container of BDDs or integers which supports `begin()` and `end()` iterators.

See also: BDD::Or()

◆ Or() [2/2]

template<typename IT >

BDD Cal::Or	(	IT	begin,
		IT	end
	)

inline

Logical OR of iterator of BDD or int.

If IT::value_type is int then the integers are converted into a BDD with Cal::Id().

Parameters

begin	Iterator pointing to the start of the given range of BDDs or integers.
end	Iterator pointing to the end of the given range.

See also: BDD::Or()

◆ Overflow()

bool Cal::Overflow ( ) const

inline

true if the node limit has been exceeded, false otherwise.

Side effects:: The overflow flag is cleared.

See also: Cal::NodeLimit()

◆ PairwiseAnd() [1/2]

template<typename Container >

std::vector<BDD> Cal::PairwiseAnd ( const Container & c )

inline

Pairwise AND of BDDs or ints within a container.

If the container is of ints, the integers are converted into a BDD with Cal::Id().

Parameters

c	Container of BDDs or integers which supports `begin()` and `end()` iterators.

See also: BDD::And()

◆ PairwiseAnd() [2/2]

template<typename IT >

std::vector<BDD> Cal::PairwiseAnd	(	IT	begin,
		IT	end
	)

inline

Pairwise AND of BDDs or ints provided by an iterator.

If IT::value_type is int then the integers are converted into a BDD with Cal::Id().

Parameters

begin	Iterator pointing to the start of the given range of BDDs or integers.
end	Iterator pointing to the end of the given range.

See also: BDD::And()

◆ PairwiseOr() [1/2]

template<typename Container >

std::vector<BDD> Cal::PairwiseOr ( const Container & c )

inline

Pairwise OR of BDDs or ints within a container.

If the container is of ints, the integers are converted into a BDD with Cal::Id().

Parameters

c	Container of BDDs or integers which supports `begin()` and `end()` iterators.

See also: BDD::Or()

◆ PairwiseOr() [2/2]

template<typename IT >

std::vector<BDD> Cal::PairwiseOr	(	IT	begin,
		IT	end
	)

inline

Pairwise OR of BDDs or ints provided by an iterator.

If IT::value_type is int then the integers are converted into a BDD with Call::Id().

Parameters

begin	Iterator pointing to the start of the given range of BDDs or integers.
end	Iterator pointing to the end of the given range.

See also: BDD::Or()

◆ PairwiseXor() [1/2]

template<typename Container >

std::vector<BDD> Cal::PairwiseXor ( const Container & c )

inline

Pairwise XOR of BDDs or ints within a container.

If the container is of ints, the integers are converted into a BDD with Cal::Id().

Parameters

c	Container of BDDs or integers which supports `begin()` and `end()` iterators.

◆ PairwiseXor() [2/2]

template<typename IT >

std::vector<BDD> Cal::PairwiseXor	(	IT	begin,
		IT	end
	)

inline

Pairwise XOR of BDDs or ints provided by an iterator.

If IT::value_type is int then the integers are converted into a BDD with Cal::Id().

◆ Print()

void Cal::Print	(	const BDD &	f,
		FILE *	fp = `stdout`
	)		const

inline

Prints a BDD in the human readable form.

Parameters

f	BDD to be printed.
fp	Pointer to the `FILE` to output to (default `stdout`).

See also: BDD::Print()

◆ PrintFunctionProfile() [1/3]

void Cal::PrintFunctionProfile	(	const BDD &	f,
		int	lineLength = `79`,
		FILE *	fp = `stdout`
	)		const

inline

Similar to Cal::PrintProfile() but displays a function profile for the given BDD.

Parameters

f	BDD to be printed.
lineLength	The maximum line length.
fp	Pointer to the `FILE` to output to (default `stdout`).

See also: BDD::PrintFunctionProfile()

◆ PrintFunctionProfile() [2/3]

template<typename Container >

void Cal::PrintFunctionProfile	(	const Container &	c,
		int	lineLength = `79`,
		FILE *	fp = `stdout`
	)		const

inline

Similar to Cal::PrintFunctionProfile for a container of BDDs. But, this accounts for sharing of nodes.

Parameters

c	Container of BDDs which supports `begin()` and `end()` iterators.
lineLength	The maximum line length.
fp	Pointer to the `FILE` to output to (default `stdout`).

See also: BDD::PrintFunctionProfile()

◆ PrintFunctionProfile() [3/3]

template<typename IT >

void Cal::PrintFunctionProfile	(	IT	begin,
		IT	end,
		int	lineLength = `79`,
		FILE *	fp = `stdout`
	)		const

inline

Similar to Cal::PrintFunctionProfile for an iterator of BDDs. But, this accounts for sharing of nodes.

Parameters

begin	Iterator pointing to the start of the given range of BDDs.
end	Iterator pointing to the end of the given range.
lineLength	The maximum line length.
fp	Pointer to the `FILE` to output to (default `stdout`).

See also: BDD::PrintFunctionProfile()

◆ PrintProfile() [1/3]

void Cal::PrintProfile	(	const BDD &	f,
		int	lineLength = `79`,
		FILE *	fp = `stdout`
	)		const

inline

Prints a BDD in the human readable form.

Parameters

f	BDD to be printed.
lineLength	The maximum line length.
fp	Pointer to the `FILE` to output to (default `stdout`).

◆ PrintProfile() [2/3]

template<typename Container >

void Cal::PrintProfile	(	const Container &	c,
		int	lineLength = `79`,
		FILE *	fp = `stdout`
	)		const

inline

Similar to Cal::PrintProfile for a container of BDDs. But, this accounts for sharing of nodes.AssociationSetCurrent.

Parameters

c	Container of BDDs which supports `begin()` and `end()` iterators.
lineLength	The maximum line length.
fp	Pointer to the `FILE` to output to (default `stdout`).

◆ PrintProfile() [3/3]

template<typename IT >

void Cal::PrintProfile	(	IT	begin,
		IT	end,
		int	lineLength = `79`,
		FILE *	fp = `stdout`
	)		const

inline

Similar to Cal::PrintProfile() for an iterator of BDDs. But, this accounts for sharing of nodes.

Parameters

begin	Iterator pointing to the start of the given range of BDDs.
end	Iterator pointing to the end of the given range.
lineLength	The maximum line length.
fp	Pointer to the `FILE` to output to (default `stdout`).

◆ Profile() [1/3]

std::vector<long> Cal::Profile	(	const BDD &	f,
		bool	negout = `true`
	)		const

inline

Obtain a vector with the number of nodes at each level in f.

Parameters

f	BDD of interest.
negout	If `false` then counting pretends the BDD does not have negative-output pointers (complement edges).

See also: BDD::Profile()

◆ Profile() [2/3]

template<typename Container >

std::vector<long> Cal::Profile	(	const Container &	c,
		bool	negout = `true`
	)		const

inline

Similar to Cal::Profile() for a container of BDDs. But, this accounts for sharing of nodes.

Parameters

negout	If `false` then counting pretends the BDD does not have negative-output pointers (complement edges).
c	Container of BDDs which supports `begin()` and `end()` iterators.

See also: BDD::Profile()

◆ Profile() [3/3]

template<typename IT >

std::vector<long> Cal::Profile	(	IT	begin,
		IT	end,
		bool	negout = `true`
	)		const

inline

Similar to Cal::Profile() for an iterator of BDDs. But, this accounts for sharing of nodes.

Parameters

begin	Iterator pointing to the start of the given range of BDDs.
end	Iterator pointing to the end of the given range.
negout	If `false` then counting pretends the BDD does not have negative-output pointers (complement edges).

See also: BDD::Profile()

◆ Reduce()

BDD Cal::Reduce	(	const BDD &	f,
		const BDD &	c
	)

inline

Function that agrees with f for all valuations that satisfy c.

The result is usually smaller in terms of number of BDD nodes than this. 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: BDD::Reduce(), Cal::Cofactor()

◆ Regular()

BDD Cal::Regular ( const BDD & f )

inline

The given BDD in positive form (regardless of its phase).

See also: BDD::Regular()

◆ RelProd()

BDD Cal::RelProd	(	const BDD &	f,
		const BDD &	g
	)

inline

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::And(), Cal::Exists(), Cal::AssociationInit(), Cal::AssociationSetCurrent(), Cal::TempAssociationInit()

◆ Reorder()

void Cal::Reorder ( )

inline

Invoke the current dynamic reodering method.

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

See also: Cal::DynamicReordering()

◆ Satisfy()

BDD Cal::Satisfy ( const BDD & f )

inline

A satisfying assignment of this BDD.

Returns a BDD which implies this, true for some valuation on which f is true, and which has at most one node at each level.

See also: BDD::Satisfy()

◆ SatisfyingFraction()

double Cal::SatisfyingFraction ( const BDD & f )

inline

Fraction of valuations which make this BDD true.

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

◆ SatisfySupport()

BDD Cal::SatisfySupport ( const BDD & f )

inline

Returns a special cube contained in this.

Returns a BDD which implies this, true for some valuation on which f is true, and which has at most one node at each level.

See also: BDD::SatisfySupport()

◆ SetGCLimit()

void Cal::SetGCLimit ( )

inline

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

See also: Cal::NodeLimit()

◆ SetParameters()

void Cal::SetParameters	(	long	reorderingThreshold,
		long	maxForwardedNodes,
		double	repackAfterGCThreshold,
		double	tableRepackThreshold
	)

inline

Sets appropriate fields of BDD Manager.

Parameters

reorderingThreshold	The number of nodes below which reordering will NOT beinvoked.
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.

◆ Size() [1/3]

unsigned long Cal::Size	(	const BDD &	f,
		bool	negout = `true`
	)

inline

This BDD's size.

Parameters

f	BDD of interest.
negout	If `false` then counting pretends the BDD does not have negative-output pointers (complement edges).

◆ Size() [2/3]

template<typename Container >

unsigned long Cal::Size	(	Container	c,
		bool	negout = `true`
	)

inline

Similar to Cal::Size() for a container of BDDs. But, this accounts for sharing of nodes.

Parameters

c	Container of BDDs which supports `begin()` and `end()` iterators.
negout	If `false` then counting pretends the BDD does not have negative-output pointers (complement edges).

◆ Size() [3/3]

template<typename IT >

unsigned long Cal::Size	(	IT	begin,
		IT	end,
		bool	negout = `true`
	)

inline

Similar to Cal::Size() for an iterator of BDDs. But, this accounts for sharing of nodes.

Parameters

begin	Iterator pointing to the start of the set of BDDs.
end	Iterator pointing to the end.
negout	If `false` then counting pretends the BDD does not have negative-output pointers (complement edges).

◆ Substitute()

BDD Cal::Substitute ( const BDD & f )

inline

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::Compose(), Cal::VarSubstitute(), Cal::AssociationInit(), Cal::TempAssociationInit()

◆ SwapVars()

BDD Cal::SwapVars	(	const BDD &	f,
		const BDD &	g,
		const BDD &	h
	)

inline

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

See also: BDD::SwapVars(), Cal::Substitute()

◆ TempAssociationAugment()

template<typename IT >

void Cal::TempAssociationAugment	(	IT	begin,
		const IT	end,
		const bool	pairs = `false`
	)

inline

Adds to the temporary variable association.

Parameters

begin	Iterator pointing to the start of the given range.
end	Iterator pointing to the end of the given range.
pairs	Similar to `Cal::AssociationInit()`.

See also: Cal::TempAssociationInit(), Cal::AssociationInit()

◆ TempAssociationInit()

template<typename IT >

void Cal::TempAssociationInit	(	IT	begin,
		const IT	end,
		const bool	pairs = `false`
	)

inline

Sets the temporary variable association.

Parameters

begin	Iterator pointing to the start of the given range.
end	Iterator pointing to the end of the given range.
pairs	Similar to `Cal::AssociationInit()`.

See also: Cal::AssociationInit()

◆ TempAssociationQuit()

void Cal::TempAssociationQuit ( )

inline

Cleans up temporary association.

See also: Cal::TempAssociationInit()

◆ Then()

BDD Cal::Then ( const BDD & f )

inline

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

See also: BDD::Then()

◆ TotalSize()

unsigned long Cal::TotalSize ( ) const

inline

The number of nodes in the Unique table.

See also: Cal::Nodes()

◆ Xor() [1/2]

template<typename Container >

BDD Cal::Xor ( const Container & c )

inline

Logical XOR of container with BDDs or ints.

If the container is of ints, the integers are converted into a BDD with Cal::Id().

Parameters

c	Container of BDDs or integers which supports `begin()` and `end()` iterators.

See also: BDD::Xor()

◆ Xor() [2/2]

template<typename IT >

BDD Cal::Xor	(	IT	begin,
		IT	end
	)

inline

Logical XOR of iterator of BDD or int.

If the container is of ints, the integers are converted into a BDD with Cal::Id().

Parameters

begin	Iterator pointing to the start of the given range of BDDs or integers.
end	Iterator pointing to the end of the given range.

See also: BDD::Xor()

◆ Zero()

BDD Cal::Zero ( ) const

inline

The BDD for the constant zero.

See also: Cal::One()

The documentation for this class was generated from the following file:

/home/runner/work/cal/cal/src/calObj.hh

Public Types

Public Member Functions

Detailed Description

Member Enumeration Documentation

◆ ReorderMethod

◆ ReorderTechnique

Constructor & Destructor Documentation

◆ ~Cal()

Member Function Documentation

◆ And() [1/3]

◆ And() [2/3]

◆ And() [3/3]

◆ AssociationInit()

◆ AssociationQuit()

◆ AssociationSetCurrent()

◆ Between()

◆ Cofactor()

◆ Compose()

◆ DependsOn()

◆ DynamicReordering()

◆ Else()

◆ Exists()

◆ ForAll()

◆ FunctionPrint()

◆ FunctionProfile() [1/3]

◆ FunctionProfile() [2/3]

◆ FunctionProfile() [3/3]

◆ GC()

◆ Id()

◆ Identity()

◆ If()

◆ IfId()

◆ IfIndex()

◆ Implies()

◆ Index()

◆ Intersects()

◆ IsConst()

◆ IsEqual()

◆ IsOne()

◆ IsZero()

◆ ITE()

◆ Nand()

◆ NodeLimit()

◆ Nodes()

◆ Nor()

◆ One()

◆ Or() [1/2]

◆ Or() [2/2]

◆ Overflow()

◆ PairwiseAnd() [1/2]

◆ PairwiseAnd() [2/2]

◆ PairwiseOr() [1/2]

◆ PairwiseOr() [2/2]

◆ PairwiseXor() [1/2]

◆ PairwiseXor() [2/2]

◆ Print()

◆ PrintFunctionProfile() [1/3]

◆ PrintFunctionProfile() [2/3]

◆ PrintFunctionProfile() [3/3]

◆ PrintProfile() [1/3]

◆ PrintProfile() [2/3]

◆ PrintProfile() [3/3]

◆ Profile() [1/3]

◆ Profile() [2/3]

◆ Profile() [3/3]

◆ Reduce()

◆ Regular()

◆ RelProd()

◆ Reorder()

◆ Satisfy()

◆ SatisfyingFraction()

◆ SatisfySupport()

◆ SetGCLimit()

◆ SetParameters()

◆ Size() [1/3]

◆ Size() [2/3]

◆ Size() [3/3]

◆ Substitute()

◆ SwapVars()

◆ TempAssociationAugment()