bdd_exprt Class Reference

Conversion between exprt and bbdt This encapsulate a bdd_managert, thus BDDs created with this class should only be combined with BDDs created using the same instance of bdd_exprt . More...

#include <bdd_expr.h>

Collaboration diagram for bdd_exprt:

Public Member Functions
bddt	from_expr (const exprt &expr)
exprt	as_expr (const bddt &root) const

Protected Types
typedef std::unordered_map< exprt, bddt, irep_hash >	expr_mapt

Protected Member Functions
bddt	from_expr_rec (const exprt &expr)
exprt	as_expr (const bdd_nodet &r, std::unordered_map< bdd_nodet::idt, exprt > &cache) const
	Helper function for bddt to exprt conversion. More...

Protected Attributes
bdd_managert	bdd_mgr
expr_mapt	expr_map
std::vector< exprt >	node_map
	Mapping from BDD variables to expressions: the expression at index i of node_map corresponds to the i-th variable. More...

Detailed Description

Conversion between exprt and bbdt This encapsulate a bdd_managert, thus BDDs created with this class should only be combined with BDDs created using the same instance of bdd_exprt .

See unit tests in unit/solvers/prop/bdd_expr.cpp for examples.

Definition at line 33 of file bdd_expr.h.

Member Typedef Documentation

expr_mapt

typedef std::unordered_map<exprt, bddt, irep_hash> bdd_exprt::expr_mapt

protected

Definition at line 42 of file bdd_expr.h.

Member Function Documentation

as_expr() [1/2]

exprt bdd_exprt::as_expr ( const bdd_nodet &  r, std::unordered_map< bdd_nodet::idt, exprt > &  cache  ) const

protected

Helper function for bddt to exprt conversion.

Parameters

r	node to convert
cache	map of already computed values

Definition at line 107 of file bdd_expr.cpp.

as_expr() [2/2]

exprt bdd_exprt::as_expr

(

const bddt &

root

)

const

Definition at line 171 of file bdd_expr.cpp.

from_expr()

bddt bdd_exprt::from_expr

(

const exprt &

expr

)

Definition at line 87 of file bdd_expr.cpp.

from_expr_rec()

bddt bdd_exprt::from_expr_rec ( const exprt &  expr )

protected

Definition at line 19 of file bdd_expr.cpp.

Member Data Documentation

bdd_mgr

bdd_managert bdd_exprt::bdd_mgr

protected

Definition at line 40 of file bdd_expr.h.

expr_map

expr_mapt bdd_exprt::expr_map

protected

Definition at line 44 of file bdd_expr.h.

node_map

std::vector<exprt> bdd_exprt::node_map

protected

Mapping from BDD variables to expressions: the expression at index i of node_map corresponds to the i-th variable.

Definition at line 48 of file bdd_expr.h.

---

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

• /home/runner/work/cbmc/cbmc/src/solvers/prop/bdd_expr.h
• /home/runner/work/cbmc/cbmc/src/solvers/prop/bdd_expr.cpp