cprover
Loading...
Searching...
No Matches
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)
bddtoperator= (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)
bddtoperator= (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_bddtoperator= (const mini_bddt &)
bool is_constant () const
bool is_true () const
bool is_false () const
unsigned var () const
const mini_bddtlow () const
const mini_bddthigh () 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_nodetnode

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]

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]

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

◆ 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: