Skip to content

(interval_)sparse_arrayt: Remove unnecessary use of "virtual" and further cleanup #2566

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Jul 12, 2018
Merged

(interval_)sparse_arrayt: Remove unnecessary use of "virtual" and further cleanup #2566

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/solvers/refinement/string_refinement.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1067,7 +1067,7 @@ static exprt substitute_array_access(
const bool left_propagate)
{
return left_propagate ? interval_sparse_arrayt(expr).to_if_expression(index)
: sparse_arrayt(expr).to_if_expression(index);
: sparse_arrayt::to_if_expression(expr, index);
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@romainbrenguier This is the code that does explicitly distinguish sparse_arrayt vs interval_sparse_arrayt

}

/// Create an equivalent expression where array accesses are replaced by 'if'
Expand Down
18 changes: 8 additions & 10 deletions src/solvers/refinement/string_refinement_util.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,12 +73,16 @@ sparse_arrayt::sparse_arrayt(const with_exprt &expr)
default_value = expr_dynamic_cast<array_of_exprt>(ref.get()).what();
}

exprt sparse_arrayt::to_if_expression(const exprt &index) const
exprt sparse_arrayt::to_if_expression(
const with_exprt &expr,
const exprt &index)
{
sparse_arrayt sparse_array(expr);

return std::accumulate(
entries.begin(),
entries.end(),
default_value,
sparse_array.entries.begin(),
sparse_array.entries.end(),
sparse_array.default_value,
[&](
const exprt if_expr,
const std::pair<std::size_t, exprt> &entry) { // NOLINT
Expand All @@ -90,12 +94,6 @@ exprt sparse_arrayt::to_if_expression(const exprt &index) const
});
}

exprt sparse_arrayt::at(const std::size_t index) const
{
const auto it = entries.find(index);
return it != entries.end() ? it->second : default_value;
}

exprt interval_sparse_arrayt::to_if_expression(const exprt &index) const
{
return std::accumulate(
Expand Down
12 changes: 4 additions & 8 deletions src/solvers/refinement/string_refinement_util.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,11 +73,7 @@ class sparse_arrayt

/// Creates an if_expr corresponding to the result of accessing the array
/// at the given index
virtual exprt to_if_expression(const exprt &index) const;

/// Get the value at the specified index.
/// Complexity is linear in the number of entries.
virtual exprt at(std::size_t index) const;
static exprt to_if_expression(const with_exprt &expr, const exprt &index);

protected:
exprt default_value;
Expand Down Expand Up @@ -114,7 +110,7 @@ class interval_sparse_arrayt final : public sparse_arrayt
const array_list_exprt &expr,
const exprt &extra_value);

exprt to_if_expression(const exprt &index) const override;
exprt to_if_expression(const exprt &index) const;

/// If the expression is an array_exprt or a with_exprt uses the appropriate
/// constructor, otherwise returns empty optional.
Expand All @@ -125,8 +121,8 @@ class interval_sparse_arrayt final : public sparse_arrayt
array_exprt concretize(std::size_t size, const typet &index_type) const;

/// Get the value at the specified index.
/// Complexity is linear in the number of entries.
exprt at(std::size_t index) const override;
/// Complexity is logarithmic in the number of entries.
exprt at(std::size_t index) const;

/// Array containing the same value at each index.
explicit interval_sparse_arrayt(exprt default_value)
Expand Down
3 changes: 1 addition & 2 deletions unit/solvers/refinement/string_refinement/sparse_array.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,6 @@ SCENARIO("sparse_array", "[core][solvers][refinement][string_refinement]")

WHEN("It is converted to a sparse array")
{
const sparse_arrayt sparse_array(input_expr);
THEN("The resulting if expression is index=100?z:index=4?x:index=1?y:0")
{
const symbol_exprt index("index", int_type);
Expand All @@ -57,7 +56,7 @@ SCENARIO("sparse_array", "[core][solvers][refinement][string_refinement]")
charx,
if_exprt(
equal_exprt(index, index1), chary, from_integer(0, char_type))));
REQUIRE(sparse_array.to_if_expression(index) == expected);
REQUIRE(sparse_arrayt::to_if_expression(input_expr, index) == expected);
}
}

Expand Down