cprover
letify.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Introduce LET for common subexpressions
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
9
#ifndef CPROVER_SOLVERS_SMT2_LETIFY_H
10
#define CPROVER_SOLVERS_SMT2_LETIFY_H
11
12
#include <
util/irep_hash_container.h
>
13
#include <
util/std_expr.h
>
14
16
class
letifyt
17
{
18
public
:
19
exprt
operator()
(
const
exprt
&);
20
21
protected
:
22
// to produce a fresh ID for each new let
23
std::size_t
let_id_count
= 0;
24
25
struct
let_count_idt
26
{
27
let_count_idt
(std::size_t _count,
const
symbol_exprt
&_let_symbol)
28
:
count
(_count),
let_symbol
(_let_symbol)
29
{
30
}
31
32
std::size_t
count
;
33
symbol_exprt
let_symbol
;
34
};
35
36
#if HASH_CODE
37
using
seen_expressionst
= std::unordered_map<exprt, let_count_idt, irep_hash>;
38
#else
39
using
seen_expressionst
=
irep_hash_mapt<exprt, let_count_idt>
;
40
#endif
41
42
void
collect_bindings
(
43
const
exprt
&expr,
44
seen_expressionst
&map,
45
std::vector<exprt> &let_order);
46
47
static
exprt
letify
(
48
const
exprt
&expr,
49
const
std::vector<exprt> &let_order,
50
const
seen_expressionst
&map);
51
52
static
exprt
substitute_let
(
const
exprt
&expr,
const
seen_expressionst
&map);
53
};
54
55
#endif // CPROVER_SOLVERS_SMT2_LETIFY_H
letifyt
Introduce LET for common subexpressions.
Definition:
letify.h:17
letifyt::let_count_idt::let_count_idt
let_count_idt(std::size_t _count, const symbol_exprt &_let_symbol)
Definition:
letify.h:27
letifyt::let_id_count
std::size_t let_id_count
Definition:
letify.h:23
exprt
Base class for all expressions.
Definition:
expr.h:53
letifyt::collect_bindings
void collect_bindings(const exprt &expr, seen_expressionst &map, std::vector< exprt > &let_order)
Definition:
letify.cpp:17
symbol_exprt
Expression to hold a symbol (variable)
Definition:
std_expr.h:82
irep_hash_container.h
IREP Hash Container.
letifyt::let_count_idt::count
std::size_t count
Definition:
letify.h:32
irep_hash_mapt
Definition:
irep_hash_container.h:102
letifyt::substitute_let
static exprt substitute_let(const exprt &expr, const seen_expressionst &map)
Definition:
letify.cpp:90
letifyt::let_count_idt
Definition:
letify.h:26
letifyt::let_count_idt::let_symbol
symbol_exprt let_symbol
Definition:
letify.h:33
letifyt::operator()
exprt operator()(const exprt &)
Definition:
letify.cpp:80
letifyt::letify
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.
Definition:
letify.cpp:54
std_expr.h
API to expression classes.
solvers
smt2
letify.h
Generated by
1.8.20