cprover
|
Represents arrays of the form array_of(x) with {i:=a} with {j:=b} ...
by a default value x
and a list of entries (i,a)
, (j,b)
etc.
More...
#include <string_refinement_util.h>
Public Member Functions | |
sparse_arrayt (const with_exprt &expr) | |
Initialize a sparse array from an expression of the form array_of(x) with {i:=a} with {j:=b} ... This is the form in which array valuations coming from the underlying solver are given. More... | |
virtual exprt | to_if_expression (const exprt &index) const |
Creates an if_expr corresponding to the result of accessing the array at the given index. More... | |
virtual exprt | at (std::size_t index) const |
Get the value at the specified index. More... | |
Protected Member Functions | |
sparse_arrayt (exprt default_value) | |
Protected Attributes | |
exprt | default_value |
std::map< std::size_t, exprt > | entries |
Represents arrays of the form array_of(x) with {i:=a} with {j:=b} ...
by a default value x
and a list of entries (i,a)
, (j,b)
etc.
Definition at line 65 of file string_refinement_util.h.
|
explicit |
Initialize a sparse array from an expression of the form array_of(x) with {i:=a} with {j:=b} ...
This is the form in which array valuations coming from the underlying solver are given.
Definition at line 60 of file string_refinement_util.cpp.
References can_cast_expr< with_exprt >(), default_value, entries, expr_dynamic_cast(), and PRECONDITION.
|
inlineexplicitprotected |
Definition at line 85 of file string_refinement_util.h.
|
virtual |
Get the value at the specified index.
Complexity is linear in the number of entries.
Reimplemented in interval_sparse_arrayt.
Definition at line 93 of file string_refinement_util.cpp.
References default_value, and entries.
Creates an if_expr corresponding to the result of accessing the array at the given index.
Reimplemented in interval_sparse_arrayt.
Definition at line 76 of file string_refinement_util.cpp.
References CHECK_RETURN, default_value, entries, from_integer(), and exprt::type().
Referenced by substitute_array_access().
|
protected |
Definition at line 83 of file string_refinement_util.h.
Referenced by at(), interval_sparse_arrayt::at(), interval_sparse_arrayt::concretize(), sparse_arrayt(), to_if_expression(), and interval_sparse_arrayt::to_if_expression().
|
protected |
Definition at line 84 of file string_refinement_util.h.
Referenced by at(), interval_sparse_arrayt::at(), interval_sparse_arrayt::concretize(), interval_sparse_arrayt::interval_sparse_arrayt(), sparse_arrayt(), to_if_expression(), and interval_sparse_arrayt::to_if_expression().