cprover
bdd_exprt Class Reference

TO_BE_DOCUMENTED. More...

#include <bdd_expr.h>

Collaboration diagram for bdd_exprt:
[legend]

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_hashexpr_mapt
 
typedef std::map< unsigned, exprtnode_mapt
 

Protected Member Functions

mini_bddt from_expr_rec (const exprt &expr)
 
exprt as_expr (const mini_bddt &r) const
 

Protected Attributes

const namespacetns
 
mini_bdd_mgrt bdd_mgr
 
mini_bddt root
 
expr_mapt expr_map
 
node_mapt node_map
 

Detailed Description

TO_BE_DOCUMENTED.

Definition at line 30 of file bdd_expr.h.

Member Typedef Documentation

§ expr_mapt

typedef std::unordered_map<exprt, mini_bddt, irep_hash> bdd_exprt::expr_mapt
protected

Definition at line 43 of file bdd_expr.h.

§ node_mapt

typedef std::map<unsigned, exprt> bdd_exprt::node_mapt
protected

Definition at line 45 of file bdd_expr.h.

Constructor & Destructor Documentation

§ bdd_exprt()

bdd_exprt::bdd_exprt ( const namespacet _ns)
inlineexplicit

Definition at line 33 of file bdd_expr.h.

References as_expr(), and from_expr().

Member Function Documentation

§ as_expr() [1/2]

exprt bdd_exprt::as_expr ( ) const

Definition at line 138 of file bdd_expr.cpp.

References mini_bddt::is_initialized(), and root.

Referenced by as_expr(), and bdd_exprt().

§ as_expr() [2/2]

exprt bdd_exprt::as_expr ( const mini_bddt r) const
protected

§ from_expr()

void bdd_exprt::from_expr ( const exprt expr)

Definition at line 97 of file bdd_expr.cpp.

References from_expr_rec(), and root.

Referenced by bdd_exprt(), and from_expr_rec().

§ from_expr_rec()

Member Data Documentation

§ bdd_mgr

mini_bdd_mgrt bdd_exprt::bdd_mgr
protected

Definition at line 40 of file bdd_expr.h.

Referenced by from_expr_rec().

§ expr_map

expr_mapt bdd_exprt::expr_map
protected

Definition at line 44 of file bdd_expr.h.

Referenced by from_expr_rec().

§ node_map

node_mapt bdd_exprt::node_map
protected

Definition at line 46 of file bdd_expr.h.

Referenced by as_expr(), and from_expr_rec().

§ ns

const namespacet& bdd_exprt::ns
protected

Definition at line 39 of file bdd_expr.h.

Referenced by from_expr_rec().

§ root

mini_bddt bdd_exprt::root
protected

Definition at line 41 of file bdd_expr.h.

Referenced by as_expr(), and from_expr().


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