cprover
Loading...
Searching...
No Matches
boolbv_let.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "boolbv.h"
10
11#include <util/range.h>
12#include <util/replace_symbol.h>
13#include <util/std_expr.h>
14
16{
17 const auto &variables = expr.variables();
18 const auto &values = expr.values();
19
21 expr.type() == expr.where().type(),
22 "let must have the type of the 'where' operand");
23
24 // Check the types.
25 for(auto &binding : make_range(variables).zip(values))
26 {
28 binding.first.type() == binding.second.type(),
29 "let value must have the type of the let symbol");
30 }
31
32 // A let expression can bind multiple symbols simultaneously.
33 // This is a 'concurrent' binding, i.e., the symbols are not yet
34 // visible when evaluating the values. SMT-LIB also has this
35 // semantics. We therefore first convert all values,
36 // and only then assign them.
37 std::vector<bvt> converted_values;
38 converted_values.reserve(variables.size());
39
40 for(auto &value : values)
41 converted_values.push_back(convert_bv(value));
42
43 // get fresh bound symbols
45
46 // Now assign
47 for(const auto &binding : make_range(fresh_variables).zip(converted_values))
48 {
49 bool is_boolean = binding.first.type().id() == ID_bool;
50 const auto &identifier = binding.first.get_identifier();
51
52 // make the symbol visible
53 if(is_boolean)
54 {
55 DATA_INVARIANT(binding.second.size() == 1, "boolean values have one bit");
56 symbols[identifier] = binding.second[0];
57 }
58 else
59 map.set_literals(identifier, binding.first.type(), binding.second);
60 }
61
62 // for renaming the bound symbols
64
65 for(const auto &pair : make_range(variables).zip(fresh_variables))
66 replace_symbol.insert(pair.first, pair.second);
67
68 // rename the bound symbols in 'where'
69 exprt where_renamed = expr.where();
71
72 // recursive call
73 bvt result_bv = convert_bv(where_renamed);
74
75 // the mapping can now be deleted
76 for(const auto &entry : fresh_variables)
77 {
78 const auto &type = entry.type();
79 if(type.id() == ID_bool)
80 symbols.erase(entry.get_identifier());
81 else
82 map.erase_literals(entry.get_identifier(), type);
83 }
84
85 return result_bv;
86}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
void erase_literals(const irep_idt &identifier, const typet &type)
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
virtual bvt convert_let(const let_exprt &)
binding_exprt::variablest fresh_binding(const binding_exprt &)
create new, unique variables for the given binding
Definition boolbv.cpp:566
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:40
boolbv_mapt map
Definition boolbv.h:120
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
A let expression.
Definition std_expr.h:2973
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition std_expr.h:3054
operandst & values()
Definition std_expr.h:3043
exprt & where()
convenience accessor for binding().where()
Definition std_expr.h:3066
binding_exprt & binding()
Definition std_expr.h:3001
Replace expression or type symbols by an expression or type, respectively.
std::vector< literalt > bvt
Definition literal.h:201
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition range.h:524
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
API to expression classes.