Low level access to the structure of the BDD, read-only. More...
#include <bdd_cudd.h>
Collaboration diagram for bdd_nodet:Public Types | |
| using | indext = unsigned int |
| Type of indexes of Boolean variables. More... | |
| using | idt = DdNode * |
| Return type for id() More... | |
| using | indext = std::size_t |
| Type of indexes of Boolean variables. More... | |
| using | idt = mini_bdd_nodet * |
| Return type for id() More... | |
Public Member Functions | |
| bool | is_constant () const |
| bool | is_complement () const |
| indext | index () const |
| Label on the node, corresponds to the index of a Boolean variable. More... | |
| bdd_nodet | then_branch () const |
| bdd_nodet | else_branch () const |
| idt | id () const |
| Unique identifier of the node. More... | |
| bool | is_constant () const |
is_constant has to be true for true and false and to distinguish between the two, is_complement has to be true for the constant false. More... | |
| bool | is_complement () const |
| indext | index () const |
| Label on the node, corresponds to the index of a Boolean variable. More... | |
| bdd_nodet | then_branch () const |
| bdd_nodet | else_branch () const |
| idt | id () const |
| Unique identifier of the node. More... | |
Private Member Functions | |
| bdd_nodet (DdNode *node) | |
| bdd_nodet (mini_bdd_nodet *node, const std::unordered_map< std::size_t, std::size_t > &bdd_var_to_index) | |
Private Attributes | |
| DdNode * | node |
| mini_bdd_nodet * | node |
| const std::unordered_map< std::size_t, std::size_t > & | bdd_var_to_index |
Friends | |
| class | bdd_managert |
Detailed Description
Low level access to the structure of the BDD, read-only.
Definition at line 27 of file bdd_cudd.h.
Member Typedef Documentation
◆ idt [1/2]
| using bdd_nodet::idt = DdNode * |
Return type for id()
Definition at line 60 of file bdd_cudd.h.
◆ idt [2/2]
| using bdd_nodet::idt = mini_bdd_nodet * |
Return type for id()
Definition at line 62 of file bdd_miniBDD.h.
◆ indext [1/2]
| using bdd_nodet::indext = unsigned int |
Type of indexes of Boolean variables.
Definition at line 41 of file bdd_cudd.h.
◆ indext [2/2]
| using bdd_nodet::indext = std::size_t |
Type of indexes of Boolean variables.
Definition at line 43 of file bdd_miniBDD.h.
Constructor & Destructor Documentation
◆ bdd_nodet() [1/2]
|
inlineexplicitprivate |
Definition at line 70 of file bdd_cudd.h.
◆ bdd_nodet() [2/2]
|
inlineexplicitprivate |
Definition at line 76 of file bdd_miniBDD.h.
Member Function Documentation
◆ else_branch() [1/2]
|
inline |
Definition at line 54 of file bdd_cudd.h.
◆ else_branch() [2/2]
|
inline |
Definition at line 56 of file bdd_miniBDD.h.
◆ id() [1/2]
|
inline |
Unique identifier of the node.
Definition at line 63 of file bdd_cudd.h.
◆ id() [2/2]
|
inline |
Unique identifier of the node.
Definition at line 65 of file bdd_miniBDD.h.
◆ index() [1/2]
|
inline |
Label on the node, corresponds to the index of a Boolean variable.
Definition at line 44 of file bdd_cudd.h.
◆ index() [2/2]
|
inline |
Label on the node, corresponds to the index of a Boolean variable.
Definition at line 46 of file bdd_miniBDD.h.
◆ is_complement() [1/2]
|
inline |
Definition at line 35 of file bdd_cudd.h.
◆ is_complement() [2/2]
|
inline |
Definition at line 37 of file bdd_miniBDD.h.
◆ is_constant() [1/2]
|
inline |
Definition at line 30 of file bdd_cudd.h.
◆ is_constant() [2/2]
|
inline |
is_constant has to be true for true and false and to distinguish between the two, is_complement has to be true for the constant false.
Definition at line 32 of file bdd_miniBDD.h.
◆ then_branch() [1/2]
|
inline |
Definition at line 49 of file bdd_cudd.h.
◆ then_branch() [2/2]
|
inline |
Definition at line 51 of file bdd_miniBDD.h.
Friends And Related Function Documentation
◆ bdd_managert
|
friend |
Definition at line 73 of file bdd_cudd.h.
Member Data Documentation
◆ bdd_var_to_index
|
private |
Definition at line 74 of file bdd_miniBDD.h.
◆ node [1/2]
|
private |
Definition at line 69 of file bdd_cudd.h.
◆ node [2/2]
|
private |
Definition at line 71 of file bdd_miniBDD.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
