cprover
|
TO_BE_DOCUMENTED. More...
#include <bdd_expr.h>
Public Member Functions | |
bdd_exprt (const namespacet &_ns) | |
void | from_expr (const exprt &expr) |
exprt | as_expr () const |
Protected Types | |
typedef std::unordered_map< exprt, mini_bddt, irep_hash > | expr_mapt |
typedef std::map< unsigned, exprt > | node_mapt |
Protected Member Functions | |
mini_bddt | from_expr_rec (const exprt &expr) |
exprt | as_expr (const mini_bddt &r) const |
Protected Attributes | |
const namespacet & | ns |
mini_bdd_mgrt | bdd_mgr |
mini_bddt | root |
expr_mapt | expr_map |
node_mapt | node_map |
TO_BE_DOCUMENTED.
Definition at line 32 of file bdd_expr.h.
|
protected |
Definition at line 45 of file bdd_expr.h.
|
protected |
Definition at line 47 of file bdd_expr.h.
|
inlineexplicit |
Definition at line 35 of file bdd_expr.h.
exprt bdd_exprt::as_expr | ( | ) | const |
Definition at line 140 of file bdd_expr.cpp.
References mini_bddt::is_initialized(), and root.
Referenced by as_expr().
Definition at line 104 of file bdd_expr.cpp.
void bdd_exprt::from_expr | ( | const exprt & | expr | ) |
Definition at line 99 of file bdd_expr.cpp.
References from_expr_rec(), and root.
Definition at line 20 of file bdd_expr.cpp.
References bdd_mgr, if_exprt::cond(), expr_map, mini_bdd_mgrt::False(), if_exprt::false_case(), format(), irept::id(), exprt::is_constant(), exprt::is_false(), make_binary(), node_map, unary_exprt::op(), exprt::op0(), exprt::op1(), exprt::operands(), to_equal_expr(), to_if_expr(), to_implies_expr(), to_not_expr(), mini_bdd_mgrt::True(), if_exprt::true_case(), exprt::type(), and mini_bdd_mgrt::Var().
Referenced by from_expr().
|
protected |
Definition at line 42 of file bdd_expr.h.
Referenced by from_expr_rec().
|
protected |
Definition at line 46 of file bdd_expr.h.
Referenced by from_expr_rec().
|
protected |
Definition at line 48 of file bdd_expr.h.
Referenced by as_expr(), and from_expr_rec().
|
protected |
Definition at line 41 of file bdd_expr.h.
|
protected |
Definition at line 43 of file bdd_expr.h.
Referenced by as_expr(), and from_expr().