C++ wrapper for Cal_Bdd, managing reference count with RAII. More...

#include <calObj.hh>

Public Types
enum	Type_t { Zero = CAL_BDD_TYPE_ZERO , One = CAL_BDD_TYPE_ONE , Constant = CAL_BDD_TYPE_CONSTANT , Posvar = CAL_BDD_TYPE_POSVAR , Negvar = CAL_BDD_TYPE_NEGVAR , Overflow = CAL_BDD_TYPE_OVERFLOW , NonTerminal = CAL_BDD_TYPE_NONTERMINAL }
	Possible types a BDD can be. More...

using	Id_t = Cal_BddId_t
	Type of BDD identifiers, i.e. the variable name independent of the current variable ordering.

using	Index_t = Cal_BddIndex_t
	Type of BDD indices, i.e. their placement in the current variable ordering.

Public Member Functions
	BDD ()
	The `NULL` BDD.

	BDD (const BDD &other)
	Copies ownership of another BDD.

BDD &	operator= (const BDD &other)
	Copy ownership of another BDD during assignment.

	BDD (BDD &&other)
	Move ownership of another BDD.

BDD &	operator= (BDD &&other)
	Move ownership of another BDD during assignment.

	~BDD ()
	Decrement reference count upon leaving scope.

bool	IsOne () const
	`true` if the this BDD is constant one, `false`otherwise.

bool	IsZero () const
	`true` if the this BDD is constant zero, `false`otherwise.

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

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

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

bool	IsEqualTo (const BDD &other) const
	`true` if this BDD is equal to `other`, `false` otherwise.

bool	operator== (const BDD &other) const
	`true` if argument BDDs are equal, `false` otherwise.

bool	operator!= (const BDD &other) const
	`false` if argument BDDs are equal, `true` otherwise.

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

BDD	If () const
	BDD corresponding to the top variable of the this BDD.

Id_t	Id () const
	Returns the id of this BDD's top variable.

Index_t	Index () const
	Returns the index of this BDD's top variable.

BDD	Then () const
	The positive cofactor of this BDD with respect to its top variable.

BDD	Else () const
	The negative cofactor of this BDD with respect to its top variable.

Type_t	Type () const
	The BDD type (0, 1, +var, -var, overflow, nonterminal).

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

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

BDD	Identity () const
	Duplicate of this BDD.

BDD	Regular () const
	Returns a BDD in positive form (regardless of this BDDs phase).

BDD	Not () const
	Complement of this BDD.

BDD	operator~ () const

BDD	Compose (const BDD &g, const BDD &h) const
	Substitute a BDD variable by a function.

BDD	Intersects (const BDD &g) const
	Computes a BDD that implies conjunction of this and `g`.

BDD	Implies (const BDD &g) const
	Computes a BDD that implies conjunction of this and `g.Not()`.

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

BDD	And (const BDD &g) const
	Logical AND operation.

BDD	operator& (const BDD &other) const

BDD &	operator&= (const BDD &other)

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

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

BDD	operator\| (const BDD &other) const

BDD &	operator\|= (const BDD &other)

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

BDD	Xor (const BDD &g) const
	Logical XOR operation.

BDD	operator^ (const BDD &other) const

BDD &	operator^= (const BDD &other)

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

BDD	Diff (const BDD &g) const
	Logical Difference operation.

BDD	operator- (const BDD &other) const

BDD &	operator-= (const BDD &other)

BDD	Satisfy () const
	A satisfying assignment of this BDD.

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

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

BDD	Cofactor (const BDD &c) const
	Generalized cofactor of this with respect to `c`.

BDD	Reduce (const BDD &c) const
	A function that agrees with this for all valuations which satisfy `c`.

void	Print (FILE *fp=stdout) const
	Prints this BDD in the human readable form.

void	FunctionPrint (std::string &name) const
	Prints the function implemented by this BDD.

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

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

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

void	PrintFunctionProfile (int lineLength=79, FILE *fp=stdout) const
	Similar to `BDD::PrintProfile()` but displays a function profile for this.

int	RefCount () const
	The reference count of this BDD.

std::string	ToString () const
	String representation of this BDD node.

Protected Member Functions
	BDD (Cal_BddManager bddManager, Cal_Bdd bdd)
	Wrap C API `Cal_Bdd` to be managed by this new `BDD` object.

Detailed Description

C++ wrapper for Cal_Bdd, managing reference count with RAII.

These BDDs are created from a Cal object which owns the unique node table. Hence, the life-time of any BDD object should not outlast its parent Cal object. Doing so leads to undefined behaviour.

See also: Cal

Member Enumeration Documentation

◆ Type_t

enum BDD::Type_t

Possible types a BDD can be.

See also: BDD::Type()

Enumerator
Zero	The Zero terminal
One	The One terminal
Constant	Constant (Non-Boolean)
Posvar	Positive variable
Negvar	Negative variable
Overflow	Invalid/Missing result due to Overflow
NonTerminal	BDD type encompassing all other cases

Constructor & Destructor Documentation

◆ BDD()

BDD::BDD	(	Cal_BddManager	bddManager,
		Cal_Bdd	bdd
	)

inlineprotected

Wrap C API Cal_Bdd to be managed by this new BDD object.

This function does not increment the reference count of the given Cal_Bdd, assuming the C API operation already has done so.

Member Function Documentation

◆ Cofactor()

BDD BDD::Cofactor ( const BDD & c ) const

inline

Generalized cofactor of this with respect to c.

The constrain operator given by Coudert et al (ICCAD90) is used to find the generalized cofactor.

See also: BDD::Reduce()

◆ Compose()

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

inline

Substitute a BDD variable by a function.

Parameters

g	Variable to be substituted.
h	Function to substitute.

◆ FunctionProfile()

std::vector< long > BDD::FunctionProfile ( ) const

inline

The number of subfunctions of this 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.

◆ Id()

Id_t BDD::Id ( ) const

inline

Returns the id of this BDD's top variable.

See also: BDD::Index()

◆ Identity()

BDD BDD::Identity ( ) const

inline

Duplicate of this BDD.

See also: BDD::Not()

◆ If()

BDD BDD::If ( ) const

inline

BDD corresponding to the top variable of the this BDD.

See also: Bdd::Id(), BDD::Index()

◆ Implies()

BDD BDD::Implies ( const BDD & g ) const

inline

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

See also: BDD::Intersects()

◆ Index()

Index_t BDD::Index ( ) const

inline

Returns the index of this BDD's top variable.

See also: BDD::Id()

◆ Intersects()

BDD BDD::Intersects ( const BDD & g ) const

inline

Computes a BDD that implies conjunction of this and g.

See also: BDD::Implies()

◆ IsConst()

bool BDD::IsConst ( ) const

inline

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

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

◆ IsOne()

bool BDD::IsOne ( ) const

inline

true if the this BDD is constant one, falseotherwise.

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

◆ IsZero()

bool BDD::IsZero ( ) const

inline

true if the this BDD is constant zero, falseotherwise.

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

◆ ITE()

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

inline

Logical If-Then-Else.

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

See also: BDD::And(), BDD::Nand(), BDD::Or(), BDD::Nor(), BDD::Xor(), BDD::Xnor()

◆ operator!=()

bool BDD::operator!= ( const BDD & other ) const

inline

false if argument BDDs are equal, true otherwise.

See also: BDD::IsEqualTo()

◆ operator&()

BDD BDD::operator& ( const BDD & other ) const

inline

See also: BDD::And()

◆ operator&=()

BDD & BDD::operator&= ( const BDD & other )

inline

See also: BDD::And()

◆ operator-()

BDD BDD::operator- ( const BDD & other ) const

inline

See also: BDD::Diff()

◆ operator-=()

BDD & BDD::operator-= ( const BDD & other )

inline

See also: BDD::Diff()

◆ operator==()

bool BDD::operator== ( const BDD & other ) const

inline

true if argument BDDs are equal, false otherwise.

See also: BDD::IsEqualTo()

◆ operator^()

BDD BDD::operator^ ( const BDD & other ) const

inline

See also: BDD::Xor()

◆ operator^=()

BDD & BDD::operator^= ( const BDD & other )

inline

See also: BDD::Xor()

◆ operator|()

BDD BDD::operator| ( const BDD & other ) const

inline

See also: BDD::Or()

◆ operator|=()

BDD & BDD::operator|= ( const BDD & other )

inline

See also: BDD::Or()

◆ operator~()

BDD BDD::operator~ ( ) const

inline

See also: BDD::Not()

◆ PrintFunctionProfile()

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

inline

Similar to BDD::PrintProfile() but displays a function profile for this.

Parameters

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

◆ PrintProfile()

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

inline

Prints a BDD in the human readable form.

Parameters

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

◆ Profile()

std::vector< long > BDD::Profile ( bool negout = true ) const

inline

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

Parameters

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

◆ Reduce()

BDD BDD::Reduce ( const BDD & c ) const

inline

A function that agrees with this for all valuations which 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::Cofactor()

◆ RefCount()

int BDD::RefCount ( ) const

inline

The reference count of this BDD.

The reference count is a value between 0 and 255. If a reference count is 255 then incrementing or decrementing it has no effect. This is to safe-guard constants and variables from being garbage collected.

◆ Regular()

BDD BDD::Regular ( ) const

inline

Returns a BDD in positive form (regardless of this BDDs phase).

See also: BDD::Not()

◆ Satisfy()

BDD BDD::Satisfy ( ) const

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.

◆ SatisfyingFraction()

double BDD::SatisfyingFraction ( ) const

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 BDD::SatisfySupport ( ) const

inline

Returns a special cube contained in this.

The returned BDD which implies this, 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.

◆ Size()

unsigned long BDD::Size ( bool negout = true ) const

inline

This BDD's size.

Parameters

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

◆ SwapVars()

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

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 this BDD.

See also: BDD::Substitute()

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

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

Public Types

Public Member Functions

Protected Member Functions

Detailed Description

Member Enumeration Documentation

◆ Type_t

Constructor & Destructor Documentation

◆ BDD()

Member Function Documentation

◆ Cofactor()

◆ Compose()

◆ FunctionProfile()

◆ Id()

◆ Identity()

◆ If()

◆ Implies()

◆ Index()

◆ Intersects()

◆ IsConst()

◆ IsOne()

◆ IsZero()

◆ ITE()

◆ operator!=()

◆ operator&()

◆ operator&=()

◆ operator-()

◆ operator-=()

◆ operator==()

◆ operator^()

◆ operator^=()

◆ operator|()

◆ operator|=()

◆ operator~()

◆ PrintFunctionProfile()

◆ PrintProfile()

◆ Profile()

◆ Reduce()

◆ RefCount()

◆ Regular()

◆ Satisfy()

◆ SatisfyingFraction()

◆ SatisfySupport()

◆ Size()

◆ SwapVars()