Skip to content

Commit 4da9fad

Browse files
Daniel Kroeningkroening
Daniel Kroening
authored andcommitted
boolbvt: introduce scopes
This is the biggest change to the solver interface since it got added to the codebase. Currently, bound identifiers (exists, forall, let, lambda, array_comprehension_exprt) must be unique; the solver loses soundness if that assumption is violated. This change introduces scopes for let, i.e., the uniqueness requirement is dropped. Nested scoping works as expected. This matches what SMT-LIB does, i.e., the renaming done in the SMT-LIB front-end can be dropped.
1 parent 028ac2c commit 4da9fad

File tree

2 files changed

+67
-12
lines changed

2 files changed

+67
-12
lines changed

src/solvers/flattening/boolbv.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -271,6 +271,9 @@ class boolbvt:public arrayst
271271

272272
// strings
273273
numberingt<irep_idt> string_numbering;
274+
275+
// scopes
276+
std::size_t scope_counter = 0;
274277
};
275278

276279
#endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_H

src/solvers/flattening/boolbv_let.cpp

Lines changed: 64 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -9,32 +9,84 @@ Author: Daniel Kroening, [email protected]
99
#include "boolbv.h"
1010

1111
#include <util/range.h>
12+
#include <util/replace_symbol.h>
1213
#include <util/std_expr.h>
1314

1415
bvt boolbvt::convert_let(const let_exprt &expr)
1516
{
1617
const auto &variables = expr.variables();
1718
const auto &values = expr.values();
1819

20+
DATA_INVARIANT(
21+
expr.type() == expr.where().type(),
22+
"let must have the type of the 'where' operand");
23+
24+
// Check the types.
1925
for(auto &binding : make_range(variables).zip(values))
2026
{
21-
const bvt value_bv = convert_bv(binding.second);
27+
DATA_INVARIANT(
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+
scope_counter++;
44+
45+
// for renaming the bound symbols
46+
replace_symbolt replace_symbol;
47+
48+
// Now assign
49+
for(const auto &binding : make_range(variables).zip(converted_values))
50+
{
51+
bool is_boolean = binding.first.type().id() == ID_bool;
52+
const auto &old_identifier = binding.first.get_identifier();
53+
54+
// produce a new identifier
55+
const irep_idt new_identifier =
56+
"boolbvt::scope::" + std::to_string(scope_counter) +
57+
"::" + id2string(old_identifier);
2258

23-
// We expect the identifiers of the bound symbols to be unique,
24-
// and thus, these can go straight into the symbol to literal map.
25-
// This property also allows us to cache any subexpressions.
26-
const irep_idt &id = binding.first.get_identifier();
59+
// make the symbol visible
60+
if(is_boolean)
61+
{
62+
DATA_INVARIANT(binding.second.size() == 1, "boolean values have one bit");
63+
symbols[new_identifier] = binding.second[0];
64+
}
65+
else
66+
map.set_literals(new_identifier, binding.first.type(), binding.second);
2767

28-
// the symbol shall be visible during the recursive call
29-
// to convert_bv
30-
map.set_literals(id, binding.first.type(), value_bv);
68+
// remember the renaming
69+
replace_symbol.insert(
70+
binding.first, symbol_exprt(new_identifier, binding.first.type()));
3171
}
3272

33-
bvt result_bv=convert_bv(expr.where());
73+
// rename the bound symbols in 'where'
74+
exprt where_renamed = expr.where();
75+
replace_symbol(where_renamed);
3476

35-
// now remove, no longer needed
36-
for(auto &variable : variables)
37-
map.erase_literals(variable.get_identifier(), variable.type());
77+
// recursive call
78+
bvt result_bv = convert_bv(where_renamed);
79+
80+
// the mapping can now be deleted
81+
for(const auto &entry : replace_symbol.get_expr_map())
82+
{
83+
const auto &new_symbol = to_symbol_expr(entry.second);
84+
const auto &type = new_symbol.type();
85+
if(type.id() == ID_bool)
86+
symbols.erase(new_symbol.get_identifier());
87+
else
88+
map.erase_literals(new_symbol.get_identifier(), type);
89+
}
3890

3991
return result_bv;
4092
}

0 commit comments

Comments
 (0)