cprover
boolbv_let.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "boolbv.h"
10 
11 #include <util/std_expr.h>
12 #include <util/std_types.h>
13 
15 {
16  const bvt value_bv=convert_bv(expr.value());
17 
18  // We expect the identifiers of the bound symbols to be unique,
19  // and thus, these can go straight into the symbol to literal map.
20  // This property also allows us to cache any subexpressions.
21  const irep_idt &id=expr.symbol().get_identifier();
22 
23  // the symbol shall be visible during the recursive call
24  // to convert_bv
25  map.set_literals(id, expr.symbol().type(), value_bv);
26  bvt result_bv=convert_bv(expr.where());
27 
28  // now remove, no longer needed
29  map.erase_literals(id, expr.symbol().type());
30 
31  return result_bv;
32 }
const irep_idt & get_identifier() const
Definition: std_expr.h:176
typet & type()
Return the type of the expression.
Definition: expr.h:68
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
exprt & where()
Definition: std_expr.h:4666
void erase_literals(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:158
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition: boolbv_map.cpp:126
API to expression classes.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
virtual bvt convert_let(const let_exprt &)
Definition: boolbv_let.cpp:14
Pre-defined types.
exprt & value()
Definition: std_expr.h:4656
symbol_exprt & symbol()
Definition: std_expr.h:4646
boolbv_mapt map
Definition: boolbv.h:101
A let expression.
Definition: std_expr.h:4635
std::vector< literalt > bvt
Definition: literal.h:200