CBMC
Loading...
Searching...
No Matches
free_symbols.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Free Symbols
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
11
12#include "free_symbols.h"
13
14#include <util/std_expr.h>
15
16#include <unordered_set>
17
18static void free_symbols_rec(
19 const std::unordered_set<symbol_exprt, irep_hash> &bound_symbols,
20 const exprt &src,
21 const std::function<void(const symbol_exprt &)> &f)
22{
23 if(src.id() == ID_symbol)
24 {
25 const auto &symbol_expr = to_symbol_expr(src);
26 auto b_it = bound_symbols.find(symbol_expr);
27 if(b_it == bound_symbols.end())
28 f(symbol_expr);
29 }
30 else if(
31 src.id() == ID_forall || src.id() == ID_exists || src.id() == ID_lambda)
32 {
33 // bindings may hide symbols
34 const auto &binding_expr = to_binding_expr(src);
35
36 auto new_bound_symbols = bound_symbols; // copy
37
38 for(const auto &s : binding_expr.variables())
39 new_bound_symbols.insert(s);
40
42 }
43 else if(src.id() == ID_let)
44 {
45 // bindings may hide symbols
46 const auto &let_expr = to_let_expr(src);
47
48 for(const auto &v : let_expr.values())
50
51 auto new_bound_symbols = bound_symbols; // copy
52
53 for(const auto &s : let_expr.variables())
54 new_bound_symbols.insert(s);
55
57 }
58 else
59 {
60 for(const auto &op : src.operands())
62 }
63}
64
66 const exprt &expr,
67 const std::function<void(const symbol_exprt &)> &f)
68{
69 std::unordered_set<symbol_exprt, irep_hash> free_symbols, bound_symbols;
71}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
operandst & operands()
Definition expr.h:94
const irep_idt & id() const
Definition irep.h:388
Expression to hold a symbol (variable)
Definition std_expr.h:131
static void free_symbols_rec(const std::unordered_set< symbol_exprt, irep_hash > &bound_symbols, const exprt &src, const std::function< void(const symbol_exprt &)> &f)
void free_symbols(const exprt &expr, const std::function< void(const symbol_exprt &)> &f)
Free Symbols.
API to expression classes.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3456
const binding_exprt & to_binding_expr(const exprt &expr)
Cast an exprt to a binding_exprt.
Definition std_expr.h:3304
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272