cprover
bdd_exprt Class Reference

TO_BE_DOCUMENTED. More...

#include <bdd_expr.h>

+ Collaboration diagram for bdd_exprt:

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 32 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 45 of file bdd_expr.h.

◆ node_mapt

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

Definition at line 47 of file bdd_expr.h.

Constructor & Destructor Documentation

◆ bdd_exprt()

bdd_exprt::bdd_exprt ( const namespacet _ns)
inlineexplicit

Definition at line 35 of file bdd_expr.h.

Member Function Documentation

◆ as_expr() [1/2]

exprt bdd_exprt::as_expr ( ) const

Definition at line 134 of file bdd_expr.cpp.

◆ as_expr() [2/2]

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

Definition at line 98 of file bdd_expr.cpp.

◆ from_expr()

void bdd_exprt::from_expr ( const exprt expr)

Definition at line 93 of file bdd_expr.cpp.

◆ from_expr_rec()

mini_bddt bdd_exprt::from_expr_rec ( const exprt expr)
protected

Definition at line 21 of file bdd_expr.cpp.

Member Data Documentation

◆ bdd_mgr

mini_bdd_mgrt bdd_exprt::bdd_mgr
protected

Definition at line 42 of file bdd_expr.h.

◆ expr_map

expr_mapt bdd_exprt::expr_map
protected

Definition at line 46 of file bdd_expr.h.

◆ node_map

node_mapt bdd_exprt::node_map
protected

Definition at line 48 of file bdd_expr.h.

◆ ns

const namespacet& bdd_exprt::ns
protected

Definition at line 41 of file bdd_expr.h.

◆ root

mini_bddt bdd_exprt::root
protected

Definition at line 43 of file bdd_expr.h.


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