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/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
44  auto fresh_variables = fresh_binding(expr.binding());
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
63  replace_symbolt replace_symbol;
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();
70  replace_symbol(where_renamed);
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 }
void erase_literals(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:118
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition: boolbv_map.cpp:75
virtual bvt convert_let(const let_exprt &)
Definition: boolbv_let.cpp:15
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
exprt & where()
convenience accessor for binding().where()
Definition: std_expr.h:3066
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition: std_expr.h:3054
binding_exprt & binding()
Definition: std_expr.h:3001
operandst & values()
Definition: std_expr.h:3043
Replace expression or type symbols by an expression or type, respectively.
void insert(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothi...
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.