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:128
typet & type()
Definition: expr.h:56
exprt & where()
Definition: std_expr.h:4734
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
void erase_literals(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:150
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition: boolbv_map.cpp:121
API to expression classes.
virtual bvt convert_let(const let_exprt &)
Definition: boolbv_let.cpp:14
API to type classes.
exprt & value()
Definition: std_expr.h:4724
symbol_exprt & symbol()
Definition: std_expr.h:4714
boolbv_mapt map
Definition: boolbv.h:99
A let expression.
Definition: std_expr.h:4705
std::vector< literalt > bvt
Definition: literal.h:200