Loading...

Searching...

No Matches

bddt Class Reference

Logical operations on BDDs. More...

#include <bdd_cudd.h>

+ Inheritance diagram for bddt:

[フレーム]

[legend]

+ Collaboration diagram for bddt:

[フレーム]

[legend]

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)

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 Symbol 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