Loading...

Searching...

No Matches

Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes | List of all members

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:

[フレーム]

[legend]

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.

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.

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