Classes

struct let_count_idt

Public Member Functions

exprt operator() (const exprt &)

Protected Types

using seen_expressionst = std::unordered_map< exprt, let_count_idt, irep_hash >

Protected Member Functions

void collect_bindings (const exprt &expr, seen_expressionst &map, std::vector< exprt > &let_order)

Static Protected Member Functions

static exprt letify (const exprt &expr, const std::vector< exprt > &let_order, const seen_expressionst &map)

Construct a nested let expression for expressions in let_order that are used more than once.

static exprt substitute_let (const exprt &expr, const seen_expressionst &map)

Protected Attributes

std::size_t let_id_count = 0

Detailed Description

Introduce LET for common subexpressions.

Definition at line 15 of file letify.h.

Member Typedef Documentation

◆ seen_expressionst

using letifyt::seen_expressionst = std::unordered_map<exprt, let_count_idt, irep_hash>

protected

Definition at line 36 of file letify.h.

Member Function Documentation

◆ collect_bindings()

void letifyt::collect_bindings ( const exprt & expr,

seen_expressionst & map,

std::vector< exprt > & let_order

)

protected

Definition at line 16 of file letify.cpp.

◆ letify()

exprt letifyt::letify ( const exprt & expr,

const std::vector< exprt > & let_order,

const seen_expressionst & map

)

staticprotected

Construct a nested let expression for expressions in let_order that are used more than once.

Definition at line 53 of file letify.cpp.

◆ operator()()

exprt letifyt::operator() ( const exprt & expr )

Definition at line 79 of file letify.cpp.

◆ substitute_let()

exprt letifyt::substitute_let ( const exprt & expr,

const seen_expressionst & map

)

staticprotected

Definition at line 89 of file letify.cpp.

Member Data Documentation

◆ let_id_count

std::size_t letifyt::let_id_count = 0

protected

Definition at line 22 of file letify.h.

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

/home/runner/work/cbmc/cbmc/src/solvers/smt2/letify.h
/home/runner/work/cbmc/cbmc/src/solvers/smt2/letify.cpp