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/range.h>
12 #include <util/std_expr.h>
13 #include <util/std_types.h>
14 
16 {
17  const auto &variables = expr.variables();
18  const auto &values = expr.values();
19 
20  for(auto &binding : make_range(variables).zip(values))
21  {
22  const bvt value_bv = convert_bv(binding.second);
23 
24  // We expect the identifiers of the bound symbols to be unique,
25  // and thus, these can go straight into the symbol to literal map.
26  // This property also allows us to cache any subexpressions.
27  const irep_idt &id = binding.first.get_identifier();
28 
29  // the symbol shall be visible during the recursive call
30  // to convert_bv
31  map.set_literals(id, binding.first.type(), value_bv);
32  }
33 
34  bvt result_bv=convert_bv(expr.where());
35 
36  // now remove, no longer needed
37  for(auto &variable : variables)
38  map.erase_literals(variable.get_identifier(), variable.type());
39 
40  return result_bv;
41 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
boolbv_mapt::erase_literals
void erase_literals(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:155
boolbvt::map
boolbv_mapt map
Definition: boolbv.h:104
bvt
std::vector< literalt > bvt
Definition: literal.h:201
let_exprt::variables
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition: std_expr.h:4246
std_types.h
Pre-defined types.
range.h
Ranges: pair of begin and end iterators, which can be initialized from containers,...
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:119
boolbvt::convert_let
virtual bvt convert_let(const let_exprt &)
Definition: boolbv_let.cpp:15
boolbv.h
let_exprt::values
operandst & values()
Definition: std_expr.h:4235
let_exprt::where
exprt & where()
convenience accessor for binding().where()
Definition: std_expr.h:4258
std_expr.h
API to expression classes.
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
let_exprt
A let expression.
Definition: std_expr.h:4165
boolbv_mapt::set_literals
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition: boolbv_map.cpp:123