Logical operations on BDDs. More...

#include <bdd_cudd.h>

Inheritance diagram for bddt:

Collaboration diagram for bddt:

Public Member Functions
bool	equals (const bddt &other) const

bool	is_true () const

bool	is_false () const

bddt	bdd_not () const

bddt	bdd_or (const bddt &other) const

bddt	bdd_and (const bddt &other) const

bddt	bdd_xor (const bddt &other) const

bddt	constrain (const bddt &other)

bddt &	operator= (const bddt &other)=default

bool	equals (const bddt &other) const

bool	is_true () const

bool	is_false () const

bddt	bdd_not () const

bddt	bdd_or (const bddt &other) const

bddt	bdd_and (const bddt &other) const

bddt	bdd_xor (const bddt &other) const

bddt	constrain (const bddt &other)

bddt &	operator= (const bddt &other)

Static Public Member Functions
static bddt	bdd_ite (const bddt &i, const bddt &t, const bddt &e)

static bddt	bdd_ite (const bddt &i, const bddt &t, const bddt &e)

Private Member Functions
	bddt (BDD bdd)

	bddt (const mini_bddt &bdd)

Private Member Functions inherited from mini_bddt
	mini_bddt ()

	mini_bddt (const mini_bddt &x)

	~mini_bddt ()

mini_bddt	operator! () const

mini_bddt	operator^ (const mini_bddt &) const

mini_bddt	operator== (const mini_bddt &) const

mini_bddt	operator& (const mini_bddt &) const

mini_bddt	operator\| (const mini_bddt &) const

mini_bddt &	operator= (const mini_bddt &)

bool	is_constant () const

bool	is_true () const

bool	is_false () const

unsigned	var () const

const mini_bddt &	low () const

const mini_bddt &	high () const

unsigned	node_number () const

void	clear ()

bool	is_initialized () const

	mini_bddt (class mini_bdd_nodet *_node)

Private Attributes
BDD	bdd

Private Attributes inherited from mini_bddt
class mini_bdd_nodet *	node

Friends
class	bdd_managert

Detailed Description

Logical operations on BDDs.

Definition at line 77 of file bdd_cudd.h.

Constructor & Destructor Documentation

◆ bddt() [1/2]

bddt::bddt ( BDD bdd )

inlineexplicitprivate

Definition at line 130 of file bdd_cudd.h.

◆ bddt() [2/2]

bddt::bddt ( const mini_bddt & bdd )

inlineexplicitprivate

Definition at line 145 of file bdd_miniBDD.h.

Member Function Documentation

◆ bdd_and() [1/2]

bddt bddt::bdd_and ( const bddt & other ) const

inline

Definition at line 105 of file bdd_cudd.h.

◆ bdd_and() [2/2]

bddt bddt::bdd_and ( const bddt & other ) const

inline

Definition at line 115 of file bdd_miniBDD.h.

◆ bdd_ite() [1/2]

static bddt bddt::bdd_ite	(	const bddt &	i,
		const bddt &	t,
		const bddt &	e
	)

inlinestatic

Definition at line 115 of file bdd_cudd.h.

◆ bdd_ite() [2/2]

static bddt bddt::bdd_ite	(	const bddt &	i,
		const bddt &	t,
		const bddt &	e
	)

inlinestatic

Definition at line 125 of file bdd_miniBDD.h.

◆ bdd_not() [1/2]

bddt bddt::bdd_not ( ) const

inline

Definition at line 95 of file bdd_cudd.h.

◆ bdd_not() [2/2]

bddt bddt::bdd_not ( ) const

inline

Definition at line 105 of file bdd_miniBDD.h.

◆ bdd_or() [1/2]

bddt bddt::bdd_or ( const bddt & other ) const

inline

Definition at line 100 of file bdd_cudd.h.

◆ bdd_or() [2/2]

bddt bddt::bdd_or ( const bddt & other ) const

inline

Definition at line 110 of file bdd_miniBDD.h.

◆ bdd_xor() [1/2]

bddt bddt::bdd_xor ( const bddt & other ) const

inline

Definition at line 110 of file bdd_cudd.h.

◆ bdd_xor() [2/2]

bddt bddt::bdd_xor ( const bddt & other ) const

inline

Definition at line 120 of file bdd_miniBDD.h.

◆ constrain() [1/2]

bddt bddt::constrain ( const bddt & other )

inline

Definition at line 120 of file bdd_cudd.h.

◆ constrain() [2/2]

bddt bddt::constrain ( const bddt & other )

inline

Definition at line 130 of file bdd_miniBDD.h.

◆ equals() [1/2]

bool bddt::equals ( const bddt & other ) const

inline

Definition at line 80 of file bdd_cudd.h.

◆ equals() [2/2]

bool bddt::equals ( const bddt & other ) const

inline

Definition at line 90 of file bdd_miniBDD.h.

◆ is_false() [1/2]

bool bddt::is_false ( ) const

inline

Definition at line 90 of file bdd_cudd.h.

◆ is_false() [2/2]

bool bddt::is_false ( ) const

inline

Definition at line 100 of file bdd_miniBDD.h.

◆ is_true() [1/2]

bool bddt::is_true ( ) const

inline

Definition at line 85 of file bdd_cudd.h.

◆ is_true() [2/2]

bool bddt::is_true ( ) const

inline

Definition at line 95 of file bdd_miniBDD.h.

◆ operator=() [1/2]

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

inline

Definition at line 136 of file bdd_miniBDD.h.

◆ operator=() [2/2]

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

default

Friends And Related Function Documentation

◆ bdd_managert

bdd_managert

friend

Definition at line 129 of file bdd_cudd.h.

Member Data Documentation

◆ bdd

BDD bddt::bdd

private

Definition at line 128 of file bdd_cudd.h.

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

/home/runner/work/cbmc/cbmc/src/solvers/bdd/bdd_cudd.h
/home/runner/work/cbmc/cbmc/src/solvers/bdd/bdd_miniBDD.h

Public Member Functions

Static Public Member Functions

Private Member Functions

Private Attributes

Friends

Detailed Description

Constructor & Destructor Documentation

◆ bddt() [1/2]

◆ bddt() [2/2]

Member Function Documentation

◆ bdd_and() [1/2]

◆ bdd_and() [2/2]

◆ bdd_ite() [1/2]

◆ bdd_ite() [2/2]

◆ bdd_not() [1/2]

◆ bdd_not() [2/2]

◆ bdd_or() [1/2]

◆ bdd_or() [2/2]

◆ bdd_xor() [1/2]

◆ bdd_xor() [2/2]

◆ constrain() [1/2]

◆ constrain() [2/2]

◆ equals() [1/2]

◆ equals() [2/2]

◆ is_false() [1/2]

◆ is_false() [2/2]

◆ is_true() [1/2]

◆ is_true() [2/2]

◆ operator=() [1/2]

◆ operator=() [2/2]

Friends And Related Function Documentation

◆ bdd_managert

Member Data Documentation

◆ bdd