From cb105500481b5db07b49049b5454d5aa062d1933 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 3 Apr 2018 15:02:29 +0100 Subject: [PATCH] Use sparse arrays in substitute_array_access The obtained expression can be exponentially smaller, because sparse array representation avoids repetitions. --- src/solvers/refinement/string_refinement.cpp | 28 ++++---------------- 1 file changed, 5 insertions(+), 23 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index fed05e00478..27f6db950e0 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -1188,6 +1188,8 @@ exprt fill_in_array_expr(const array_exprt &expr, std::size_t string_max_length) /// expressions: for instance in array access `arr[index]`, where: /// `arr := {12, 24, 48}` the constructed expression will be: /// `index==0 ? 12 : index==1 ? 24 : 48` +/// Avoids repetition so `arr := {12, 12, 24, 48}` will give +/// `index<=1 ? 12 : index==1 ? 24 : 48` static exprt substitute_array_access( const array_exprt &array_expr, const exprt &index, @@ -1195,29 +1197,9 @@ static exprt substitute_array_access( &symbol_generator) { const typet &char_type = array_expr.type().subtype(); - const typet &index_type = to_array_type(array_expr.type()).size().type(); - const std::vector &operands = array_expr.operands(); - - exprt result = symbol_generator("out_of_bound_access", char_type); - - for(std::size_t i = 0; i < operands.size(); ++i) - { - // Go in reverse order so that smaller indexes appear first in the result - const std::size_t pos = operands.size() - 1 - i; - const equal_exprt equals(index, from_integer(pos, index_type)); - if(operands[pos].type() != char_type) - { - INVARIANT( - operands[pos].id() == ID_unknown, - string_refinement_invariantt( - "elements can only have type char or " - "unknown, and it is not char type")); - result = if_exprt(equals, exprt(ID_unknown, char_type), result); - } - else - result = if_exprt(equals, operands[pos], result); - } - return result; + const exprt default_val = symbol_generator("out_of_bound_access", char_type); + const interval_sparse_arrayt sparse_array(array_expr, default_val); + return sparse_array.to_if_expression(index); } static exprt substitute_array_access(