Skip to content

Commit

Permalink
Use concretize instead of fill_in_array
Browse files Browse the repository at this point in the history
This will allow to remove fill_in_array_expr which duplicates what
concretize does.
  • Loading branch information
romainbrenguier committed Apr 10, 2018
1 parent 052d503 commit 6d87233
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 3 deletions.
5 changes: 3 additions & 2 deletions src/solvers/refinement/string_refinement.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2264,8 +2264,9 @@ exprt string_refinementt::get(const exprt &expr) const
const exprt length = super_get(arr.length());
if(const auto n = numeric_cast<std::size_t>(length))
{
const array_exprt arr_model(array_typet(arr.type().subtype(), length));
return fill_in_array_expr(arr_model, generator.max_string_length);
const interval_sparse_arrayt sparse_array(
from_integer(CHARACTER_FOR_UNKNOWN, arr.type().subtype()));
return sparse_array.concretize(*n, length.type());
}
}
return arr;
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/refinement/string_refinement_util.h
Original file line number Diff line number Diff line change
Expand Up @@ -148,7 +148,7 @@ class interval_sparse_arrayt final : public sparse_arrayt
/// Complexity is linear in the number of entries.
exprt at(std::size_t index) const override;

private:
/// Array containing the same value at each index.
explicit interval_sparse_arrayt(exprt default_value)
: sparse_arrayt(default_value)
{
Expand Down

0 comments on commit 6d87233

Please sign in to comment.