#include <guard_bdd.h>
Collaboration diagram for guard_bddt:Public Member Functions | |
| guard_bddt (const exprt &e, bdd_exprt &manager) | |
| guard_bddt (const guard_bddt &other) | |
| guard_bddt & | operator= (const guard_bddt &other) |
| guard_bddt & | operator= (guard_bddt &&other) |
| guard_bddt & | add (const exprt &expr) |
| guard_bddt & | append (const guard_bddt &guard) |
| exprt | as_expr () const |
| exprt | guard_expr (exprt expr) const |
Return guard => dest or a simplified variant thereof if either guard or dest are trivial. More... | |
| bool | is_true () const |
| bool | is_false () const |
| guard_bddt | operator! () const |
| bool | disjunction_may_simplify (const guard_bddt &other_guard) |
Returns true if operator|= with other_guard may result in a simpler expression. More... | |
Static Public Attributes | |
| static constexpr bool | is_always_simplified = true |
| BDDs are always in a simplified form and thus no further simplification is required after calls to as_expr(). More... | |
Private Member Functions | |
| guard_bddt (bdd_exprt &manager, bddt bdd) | |
Private Attributes | |
| bdd_exprt & | manager |
| bddt | bdd |
Friends | |
| guard_bddt & | operator-= (guard_bddt &g1, const guard_bddt &g2) |
Transforms g1 into g1' such that ‘g1’ & g2 => g1 => g1'` and returns a reference to g1. More... | |
| guard_bddt & | operator|= (guard_bddt &g1, const guard_bddt &g2) |
Detailed Description
Definition at line 21 of file guard_bdd.h.
Constructor & Destructor Documentation
◆ guard_bddt() [1/3]
Definition at line 19 of file guard_bdd.cpp.
◆ guard_bddt() [2/3]
|
inline |
Definition at line 25 of file guard_bdd.h.
◆ guard_bddt() [3/3]
Definition at line 76 of file guard_bdd.h.
Member Function Documentation
◆ add()
| guard_bddt & guard_bddt::add | ( | const exprt & | expr | ) |
Definition at line 64 of file guard_bdd.cpp.
◆ append()
| guard_bddt & guard_bddt::append | ( | const guard_bddt & | guard | ) |
Definition at line 58 of file guard_bdd.cpp.
◆ as_expr()
| exprt guard_bddt::as_expr | ( | ) | const |
Definition at line 82 of file guard_bdd.cpp.
◆ disjunction_may_simplify()
|
inline |
Returns true if operator|= with other_guard may result in a simpler expression.
For bdd_exprt we always simplify maximally.
Definition at line 67 of file guard_bdd.h.
◆ guard_expr()
Return guard => dest or a simplified variant thereof if either guard or dest are trivial.
Definition at line 38 of file guard_bdd.cpp.
◆ is_false()
|
inline |
Definition at line 49 of file guard_bdd.h.
◆ is_true()
|
inline |
Definition at line 44 of file guard_bdd.h.
◆ operator!()
|
inline |
Definition at line 60 of file guard_bdd.h.
◆ operator=() [1/2]
| guard_bddt & guard_bddt::operator= | ( | const guard_bddt & | other | ) |
Definition at line 24 of file guard_bdd.cpp.
◆ operator=() [2/2]
| guard_bddt & guard_bddt::operator= | ( | guard_bddt && | other | ) |
Definition at line 31 of file guard_bdd.cpp.
Friends And Related Function Documentation
◆ operator-=
|
friend |
Transforms g1 into g1' such that ‘g1’ & g2 => g1 => g1'` and returns a reference to g1.
Definition at line 70 of file guard_bdd.cpp.
◆ operator|=
|
friend |
Definition at line 76 of file guard_bdd.cpp.
Member Data Documentation
◆ bdd
|
private |
Definition at line 74 of file guard_bdd.h.
◆ is_always_simplified
|
staticconstexpr |
BDDs are always in a simplified form and thus no further simplification is required after calls to as_expr().
This can vary according to the guard implementation.
Definition at line 38 of file guard_bdd.h.
◆ manager
|
private |
Definition at line 73 of file guard_bdd.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/analyses/guard_bdd.h
- /home/runner/work/cbmc/cbmc/src/analyses/guard_bdd.cpp
