CBMC
Public Member Functions | Private Attributes | List of all members
bdd_managert Class Reference

Manager for BDD creation. More...

#include <bdd_cudd.h>

+ Inheritance diagram for bdd_managert:
+ Collaboration diagram for bdd_managert:

Public Member Functions

 bdd_managert ()
 
 bdd_managert (const bdd_managert &)=delete
 
bddt bdd_true ()
 
bddt bdd_false ()
 
bddt bdd_variable (bdd_nodet::indext index)
 
bdd_nodet bdd_node (const bddt &bdd) const
 
bddt bdd_true ()
 
bddt bdd_false ()
 
bddt bdd_variable (bdd_nodet::indext index)
 
bdd_nodet bdd_node (const bddt &bdd) const
 
 bdd_managert (const bdd_managert &)=delete
 
 bdd_managert ()=default
 

Private Attributes

Cudd cudd
 
std::unordered_map< std::size_t, bddt > index_to_bdd
 
std::unordered_map< std::size_t, std::size_t > bdd_var_to_index
 
- Private Attributes inherited from mini_bdd_mgrt
var_tablet var_table
 
nodest nodes
 
mini_bddt true_bdd
 
mini_bddt false_bdd
 
reverse_mapt reverse_map
 
freet free
 

Additional Inherited Members

- Private Types inherited from mini_bdd_mgrt
typedef std::vector< var_table_entryt > var_tablet
 
typedef std::list< mini_bdd_nodet > nodest
 
typedef std::map< reverse_keyt, mini_bdd_nodet * > reverse_mapt
 
typedef std::stack< mini_bdd_nodet * > freet
 
- Private Member Functions inherited from mini_bdd_mgrt
 mini_bdd_mgrt ()
 
 ~mini_bdd_mgrt ()
 
mini_bddt Var (const std::string &label)
 
void DumpDot (std::ostream &out, bool supress_zero=false) const
 
void DumpTikZ (std::ostream &out, bool supress_zero=false, bool node_numbers=true) const
 
void DumpTable (std::ostream &out) const
 
const mini_bddt & True () const
 
const mini_bddt & False () const
 
mini_bddt mk (unsigned var, const mini_bddt &low, const mini_bddt &high)
 
std::size_t number_of_nodes ()
 

Detailed Description

Manager for BDD creation.

Definition at line 136 of file bdd_cudd.h.

Constructor & Destructor Documentation

◆ bdd_managert() [1/4]

bdd_managert::bdd_managert ( )
inline

Definition at line 139 of file bdd_cudd.h.

◆ bdd_managert() [2/4]

bdd_managert::bdd_managert ( const bdd_managert &  )
delete

◆ bdd_managert() [3/4]

bdd_managert::bdd_managert ( const bdd_managert &  )
delete

◆ bdd_managert() [4/4]

bdd_managert::bdd_managert ( )
default

Member Function Documentation

◆ bdd_false() [1/2]

bddt bdd_managert::bdd_false ( )
inline

Definition at line 150 of file bdd_cudd.h.

◆ bdd_false() [2/2]

bddt bdd_managert::bdd_false ( )
inline

Definition at line 159 of file bdd_miniBDD.h.

◆ bdd_node() [1/2]

bdd_nodet bdd_managert::bdd_node ( const bddt &  bdd) const
inline

Definition at line 160 of file bdd_cudd.h.

◆ bdd_node() [2/2]

bdd_nodet bdd_managert::bdd_node ( const bddt &  bdd) const
inline

Definition at line 175 of file bdd_miniBDD.h.

◆ bdd_true() [1/2]

bddt bdd_managert::bdd_true ( )
inline

Definition at line 145 of file bdd_cudd.h.

◆ bdd_true() [2/2]

bddt bdd_managert::bdd_true ( )
inline

Definition at line 154 of file bdd_miniBDD.h.

◆ bdd_variable() [1/2]

bddt bdd_managert::bdd_variable ( bdd_nodet::indext  index)
inline

Definition at line 155 of file bdd_cudd.h.

◆ bdd_variable() [2/2]

bddt bdd_managert::bdd_variable ( bdd_nodet::indext  index)
inline

Definition at line 164 of file bdd_miniBDD.h.

Member Data Documentation

◆ bdd_var_to_index

std::unordered_map<std::size_t, std::size_t> bdd_managert::bdd_var_to_index
private

Definition at line 185 of file bdd_miniBDD.h.

◆ cudd

Cudd bdd_managert::cudd
private

Definition at line 166 of file bdd_cudd.h.

◆ index_to_bdd

std::unordered_map<std::size_t, bddt> bdd_managert::index_to_bdd
private

Definition at line 184 of file bdd_miniBDD.h.

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