diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index cfc6297791a..ad3562ed4d4 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -237,6 +238,11 @@ void arrayst::collect_arrays(const exprt &a) else if(a.id() == ID_array_comprehension) { } + else if(auto let_expr = expr_try_dynamic_cast(a)) + { + arrays.make_union(a, let_expr->where()); + collect_arrays(let_expr->where()); + } else { DATA_INVARIANT( @@ -528,6 +534,33 @@ void arrayst::add_array_constraints( else if(expr.id()==ID_index) { } + else if(auto let_expr = expr_try_dynamic_cast(expr)) + { + // we got x=let(a=e, A) + // add x[i]=A[a/e][i] + + exprt where = let_expr->where(); + replace_symbolt replace_symbol; + for(const auto &binding : + make_range(let_expr->variables()).zip(let_expr->values())) + { + replace_symbol.insert(binding.first, binding.second); + } + replace_symbol(where); + + for(const auto &index : index_set) + { + index_exprt index_expr{expr, index}; + index_exprt where_indexed{where, index}; + + // add constraint + lazy_constraintt lazy{ + lazy_typet::ARRAY_LET, equal_exprt{index_expr, where_indexed}}; + + add_array_constraint(lazy, false); // added immediately + array_constraint_count[constraint_typet::ARRAY_LET]++; + } + } else { DATA_INVARIANT( @@ -875,6 +908,8 @@ std::string arrayst::enum_to_string(constraint_typet type) return "arrayComprehension"; case constraint_typet::ARRAY_EQUALITY: return "arrayEquality"; + case constraint_typet::ARRAY_LET: + return "arrayLet"; default: UNREACHABLE; } diff --git a/src/solvers/flattening/arrays.h b/src/solvers/flattening/arrays.h index 97ba49bef84..34aea006ca6 100644 --- a/src/solvers/flattening/arrays.h +++ b/src/solvers/flattening/arrays.h @@ -93,7 +93,8 @@ class arrayst:public equalityt ARRAY_OF, ARRAY_TYPECAST, ARRAY_CONSTANT, - ARRAY_COMPREHENSION + ARRAY_COMPREHENSION, + ARRAY_LET }; struct lazy_constraintt @@ -124,7 +125,8 @@ class arrayst:public equalityt ARRAY_TYPECAST, ARRAY_CONSTANT, ARRAY_COMPREHENSION, - ARRAY_EQUALITY + ARRAY_EQUALITY, + ARRAY_LET }; typedef std::map array_constraint_countt; diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index f63137fdeb7..b5c5366658c 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -4445,15 +4445,22 @@ void smt2_convt::convert_member(const member_exprt &expr) CHECK_RETURN_WITH_DIAGNOSTICS( width != 0, "failed to get union member width"); - unflatten(wheret::BEGIN, expr.type()); + if(use_datatypes) + { + unflatten(wheret::BEGIN, expr.type()); - out << "((_ extract " - << (width-1) - << " 0) "; - convert_expr(struct_op); - out << ")"; + out << "((_ extract " << (width - 1) << " 0) "; + convert_expr(struct_op); + out << ")"; - unflatten(wheret::END, expr.type()); + unflatten(wheret::END, expr.type()); + } + else + { + out << "((_ extract " << (width - 1) << " 0) "; + convert_expr(struct_op); + out << ")"; + } } else UNEXPECTEDCASE( @@ -4565,57 +4572,50 @@ void smt2_convt::unflatten( } else if(type.id() == ID_array) { - if(use_datatypes) + PRECONDITION(use_as_const); + + if(where == wheret::BEGIN) + out << "(let ((?ufop" << nesting << " "; + else { - PRECONDITION(use_as_const); + out << ")) "; - if(where == wheret::BEGIN) - out << "(let ((?ufop" << nesting << " "; - else - { - out << ")) "; + const array_typet &array_type = to_array_type(type); - const array_typet &array_type = to_array_type(type); + std::size_t subtype_width = boolbv_width(array_type.element_type()); - std::size_t subtype_width = boolbv_width(array_type.element_type()); + DATA_INVARIANT( + array_type.size().is_constant(), + "cannot unflatten arrays of non-constant size"); + mp_integer size = + numeric_cast_v(to_constant_expr(array_type.size())); - DATA_INVARIANT( - array_type.size().is_constant(), - "cannot unflatten arrays of non-constant size"); - mp_integer size = - numeric_cast_v(to_constant_expr(array_type.size())); + for(mp_integer i = 1; i < size; ++i) + out << "(store "; - for(mp_integer i = 1; i < size; ++i) - out << "(store "; + out << "((as const "; + convert_type(array_type); + out << ") "; + // use element at index 0 as default value + unflatten(wheret::BEGIN, array_type.element_type(), nesting + 1); + out << "((_ extract " << subtype_width - 1 << " " + << "0) ?ufop" << nesting << ")"; + unflatten(wheret::END, array_type.element_type(), nesting + 1); + out << ") "; - out << "((as const "; - convert_type(array_type); - out << ") "; - // use element at index 0 as default value + std::size_t offset = subtype_width; + for(mp_integer i = 1; i < size; ++i, offset += subtype_width) + { + convert_expr(from_integer(i, array_type.index_type())); + out << ' '; unflatten(wheret::BEGIN, array_type.element_type(), nesting + 1); - out << "((_ extract " << subtype_width - 1 << " " - << "0) ?ufop" << nesting << ")"; + out << "((_ extract " << offset + subtype_width - 1 << " " << offset + << ") ?ufop" << nesting << ")"; unflatten(wheret::END, array_type.element_type(), nesting + 1); - out << ") "; - - std::size_t offset = subtype_width; - for(mp_integer i = 1; i < size; ++i, offset += subtype_width) - { - convert_expr(from_integer(i, array_type.index_type())); - out << ' '; - unflatten(wheret::BEGIN, array_type.element_type(), nesting + 1); - out << "((_ extract " << offset + subtype_width - 1 << " " << offset - << ") ?ufop" << nesting << ")"; - unflatten(wheret::END, array_type.element_type(), nesting + 1); - out << ")"; // store - } - - out << ")"; // let + out << ")"; // store } - } - else - { - // nop, already a bv + + out << ")"; // let } } else if(type.id() == ID_struct || type.id() == ID_struct_tag) @@ -4767,19 +4767,22 @@ void smt2_convt::set_to(const exprt &expr, bool value) { out << "(define-fun " << smt2_identifier; out << " () "; + convert_type(equal_expr.lhs().type()); + out << ' '; if( equal_expr.lhs().type().id() != ID_array || use_array_theory(prepared_rhs)) { - convert_type(equal_expr.lhs().type()); + convert_expr(prepared_rhs); } else { - std::size_t width = boolbv_width(equal_expr.lhs().type()); - out << "(_ BitVec " << width << ")"; + unflatten(wheret::BEGIN, equal_expr.lhs().type()); + + convert_expr(prepared_rhs); + + unflatten(wheret::END, equal_expr.lhs().type()); } - out << ' '; - convert_expr(prepared_rhs); out << ')' << '\n'; }