CBMC
Public Member Functions | Static Public Member Functions | Private Member Functions | Private Attributes | Friends | List of all members
bddt Class Reference

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: