diff --git a/regression/smt2_solver/let1/let-scoping1.desc b/regression/smt2_solver/let/let-scoping1.desc similarity index 100% rename from regression/smt2_solver/let1/let-scoping1.desc rename to regression/smt2_solver/let/let-scoping1.desc diff --git a/regression/smt2_solver/let1/let-scoping1.smt2 b/regression/smt2_solver/let/let-scoping1.smt2 similarity index 100% rename from regression/smt2_solver/let1/let-scoping1.smt2 rename to regression/smt2_solver/let/let-scoping1.smt2 diff --git a/regression/smt2_solver/let-with-bv1/test.desc b/regression/smt2_solver/let/let-with-bv1.desc similarity index 100% rename from regression/smt2_solver/let-with-bv1/test.desc rename to regression/smt2_solver/let/let-with-bv1.desc diff --git a/regression/smt2_solver/let-with-bv1/let-with-bv1.smt2 b/regression/smt2_solver/let/let-with-bv1.smt2 similarity index 100% rename from regression/smt2_solver/let-with-bv1/let-with-bv1.smt2 rename to regression/smt2_solver/let/let-with-bv1.smt2 diff --git a/regression/smt2_solver/let/let-with-bv2.desc b/regression/smt2_solver/let/let-with-bv2.desc new file mode 100644 index 00000000000..c63bb4ec8b4 --- /dev/null +++ b/regression/smt2_solver/let/let-with-bv2.desc @@ -0,0 +1,7 @@ +CORE +let-with-bv2.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- diff --git a/regression/smt2_solver/let/let-with-bv2.smt2 b/regression/smt2_solver/let/let-with-bv2.smt2 new file mode 100644 index 00000000000..f9c61e09ff2 --- /dev/null +++ b/regression/smt2_solver/let/let-with-bv2.smt2 @@ -0,0 +1,26 @@ +(set-logic QF_BV) + +(define-fun x () (_ BitVec 8) #x12) + +; let hides the function 'x' +(define-fun let1 () Bool (let ((x #x4567)) (= x #x4567))) + +; the binding isn't visible immediately +(define-fun let2 () Bool (= (let ((x x)) x) #x12)) + +; parallel let +(define-fun let3 () Bool (= (let ((x #x45) (y x)) y) #x12)) + +; limited scope +(define-fun let4 () Bool (and (let ((x true)) x) (= x #x12))) + +; all must be true + +(assert (not (and + let1 + let2 + let3 + let4 + ))) + +(check-sat) diff --git a/regression/smt2_solver/let1/test.desc b/regression/smt2_solver/let/let1.desc similarity index 100% rename from regression/smt2_solver/let1/test.desc rename to regression/smt2_solver/let/let1.desc diff --git a/regression/smt2_solver/let1/let1.smt2 b/regression/smt2_solver/let/let1.smt2 similarity index 100% rename from regression/smt2_solver/let1/let1.smt2 rename to regression/smt2_solver/let/let1.smt2 diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 0104a04ba69..1dd793bb7f7 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -271,6 +271,9 @@ class boolbvt:public arrayst // strings numberingt string_numbering; + + // scopes + std::size_t scope_counter = 0; }; #endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_H diff --git a/src/solvers/flattening/boolbv_let.cpp b/src/solvers/flattening/boolbv_let.cpp index 32422e2540d..e192b85902c 100644 --- a/src/solvers/flattening/boolbv_let.cpp +++ b/src/solvers/flattening/boolbv_let.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" #include +#include #include bvt boolbvt::convert_let(const let_exprt &expr) @@ -16,25 +17,76 @@ bvt boolbvt::convert_let(const let_exprt &expr) const auto &variables = expr.variables(); const auto &values = expr.values(); + DATA_INVARIANT( + expr.type() == expr.where().type(), + "let must have the type of the 'where' operand"); + + // Check the types. for(auto &binding : make_range(variables).zip(values)) { - const bvt value_bv = convert_bv(binding.second); + DATA_INVARIANT( + binding.first.type() == binding.second.type(), + "let value must have the type of the let symbol"); + } + + // A let expression can bind multiple symbols simultaneously. + // This is a 'concurrent' binding, i.e., the symbols are not yet + // visible when evaluating the values. SMT-LIB also has this + // semantics. We therefore first convert all values, + // and only then assign them. + std::vector converted_values; + converted_values.reserve(variables.size()); + + for(auto &value : values) + converted_values.push_back(convert_bv(value)); + + scope_counter++; + + // for renaming the bound symbols + replace_symbolt replace_symbol; + + // Now assign + for(const auto &binding : make_range(variables).zip(converted_values)) + { + bool is_boolean = binding.first.type().id() == ID_bool; + const auto &old_identifier = binding.first.get_identifier(); + + // produce a new identifier + const irep_idt new_identifier = + "boolbvt::scope::" + std::to_string(scope_counter) + + "::" + id2string(old_identifier); - // We expect the identifiers of the bound symbols to be unique, - // and thus, these can go straight into the symbol to literal map. - // This property also allows us to cache any subexpressions. - const irep_idt &id = binding.first.get_identifier(); + // make the symbol visible + if(is_boolean) + { + DATA_INVARIANT(binding.second.size() == 1, "boolean values have one bit"); + symbols[new_identifier] = binding.second[0]; + } + else + map.set_literals(new_identifier, binding.first.type(), binding.second); - // the symbol shall be visible during the recursive call - // to convert_bv - map.set_literals(id, binding.first.type(), value_bv); + // remember the renaming + replace_symbol.insert( + binding.first, symbol_exprt(new_identifier, binding.first.type())); } - bvt result_bv=convert_bv(expr.where()); + // rename the bound symbols in 'where' + exprt where_renamed = expr.where(); + replace_symbol(where_renamed); - // now remove, no longer needed - for(auto &variable : variables) - map.erase_literals(variable.get_identifier(), variable.type()); + // recursive call + bvt result_bv = convert_bv(where_renamed); + + // the mapping can now be deleted + for(const auto &entry : replace_symbol.get_expr_map()) + { + const auto &new_symbol = to_symbol_expr(entry.second); + const auto &type = new_symbol.type(); + if(type.id() == ID_bool) + symbols.erase(new_symbol.get_identifier()); + else + map.erase_literals(new_symbol.get_identifier(), type); + } return result_bv; } diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp index 81fbcdf5d5a..aec587abdf2 100644 --- a/src/solvers/prop/prop_conv_solver.cpp +++ b/src/solvers/prop/prop_conv_solver.cpp @@ -172,8 +172,8 @@ literalt prop_conv_solvert::convert(const exprt &expr) literalt literal = convert_bool(expr); // insert into cache - result.first->second = literal; + if(freeze_all && !literal.is_constant()) prop.set_frozen(literal); @@ -295,41 +295,6 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr) return equal ? prop.lequal(tmp1, tmp2) : prop.lxor(tmp1, tmp2); } } - else if(expr.id() == ID_let) - { - const let_exprt &let_expr = to_let_expr(expr); - const auto &variables = let_expr.variables(); - const auto &values = let_expr.values(); - - // first check whether this is all boolean - const bool all_boolean = - let_expr.where().type().id() == ID_bool && - std::all_of(values.begin(), values.end(), [](const exprt &e) { - return e.type().id() == ID_bool; - }); - - if(all_boolean) - { - for(auto &binding : make_range(variables).zip(values)) - { - literalt value_converted = convert(binding.second); - - // We expect the identifier of the bound symbols to be unique, - // and thus, these can go straight into the symbol map. - // This property also allows us to cache any subexpressions. - const irep_idt &id = binding.first.get_identifier(); - symbols[id] = value_converted; - } - - literalt result = convert(let_expr.where()); - - // remove again - for(auto &variable : variables) - symbols.erase(variable.get_identifier()); - - return result; - } - } return convert_rest(expr); }