Skip to content

Commit 6d87233

Browse files
Use concretize instead of fill_in_array
This will allow to remove fill_in_array_expr which duplicates what concretize does.
1 parent 052d503 commit 6d87233

File tree

2 files changed

+4
-3
lines changed

2 files changed

+4
-3
lines changed

src/solvers/refinement/string_refinement.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2264,8 +2264,9 @@ exprt string_refinementt::get(const exprt &expr) const
22642264
const exprt length = super_get(arr.length());
22652265
if(const auto n = numeric_cast<std::size_t>(length))
22662266
{
2267-
const array_exprt arr_model(array_typet(arr.type().subtype(), length));
2268-
return fill_in_array_expr(arr_model, generator.max_string_length);
2267+
const interval_sparse_arrayt sparse_array(
2268+
from_integer(CHARACTER_FOR_UNKNOWN, arr.type().subtype()));
2269+
return sparse_array.concretize(*n, length.type());
22692270
}
22702271
}
22712272
return arr;

src/solvers/refinement/string_refinement_util.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -148,7 +148,7 @@ class interval_sparse_arrayt final : public sparse_arrayt
148148
/// Complexity is linear in the number of entries.
149149
exprt at(std::size_t index) const override;
150150

151-
private:
151+
/// Array containing the same value at each index.
152152
explicit interval_sparse_arrayt(exprt default_value)
153153
: sparse_arrayt(default_value)
154154
{

0 commit comments

Comments
 (0)