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 }
boolbv_mapt::erase_literals
void erase_literals(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:118
boolbvt::map
boolbv_mapt map
Definition: boolbv.h:118
bvt
std::vector< literalt > bvt
Definition: literal.h:201
boolbvt::fresh_binding
binding_exprt::variablest fresh_binding(const binding_exprt &)
create new, unique variables for the given binding
Definition: boolbv.cpp:562
replace_symbol.h
prop_conv_solvert::symbols
symbolst symbols
Definition: prop_conv_solver.h:117
exprt
Base class for all expressions.
Definition: expr.h:54
let_exprt::variables
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition: std_expr.h:3000
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
range.h
Ranges: pair of begin and end iterators, which can be initialized from containers,...
replace_symbolt::insert
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...
Definition: replace_symbol.cpp:24
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:40
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:2989
let_exprt::where
exprt & where()
convenience accessor for binding().where()
Definition: std_expr.h:3012
std_expr.h
API to expression classes.
let_exprt::binding
binding_exprt & binding()
Definition: std_expr.h:2947
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
let_exprt
A let expression.
Definition: std_expr.h:2919
boolbv_mapt::set_literals
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition: boolbv_map.cpp:75
replace_symbolt
Replace expression or type symbols by an expression or type, respectively.
Definition: replace_symbol.h:25