Represents arrays by the indexes up to which the value remains the same. More...
#include <string_refinement_util.h>
Inheritance diagram for interval_sparse_arrayt: Collaboration diagram for interval_sparse_arrayt:Public Member Functions | |
| interval_sparse_arrayt (const with_exprt &expr) | |
An expression of the form array_of(x) with {i:=a} with {j:=b} is converted to an array arr where for all index k smaller than i, arr[k] is a, for all index between i (exclusive) and j it is b and for the others it is x. More... | |
| interval_sparse_arrayt (const array_exprt &expr, const exprt &extra_value) | |
Initialize an array expression to sparse array representation, avoiding repetition of identical successive values and setting the default to extra_value. More... | |
| interval_sparse_arrayt (const array_list_exprt &expr, const exprt &extra_value) | |
Initialize a sparse array from an array represented by a list of index-value pairs, and setting the default to extra_value. More... | |
| exprt | to_if_expression (const exprt &index) const |
| array_exprt | concretize (std::size_t size, const typet &index_type) const |
| Convert to an array representation, ignores elements at index >= size. More... | |
| exprt | at (std::size_t index) const |
| Get the value at the specified index. More... | |
| interval_sparse_arrayt (exprt default_value) | |
| Array containing the same value at each index. More... | |
| Public Member Functions inherited from sparse_arrayt | |
| 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... | |
Static Public Member Functions | |
| static std::optional< interval_sparse_arrayt > | of_expr (const exprt &expr, const exprt &extra_value) |
| If the expression is an array_exprt or a with_exprt uses the appropriate constructor, otherwise returns empty optional. More... | |
| Static Public Member Functions inherited from sparse_arrayt | |
| static exprt | to_if_expression (const with_exprt &expr, const exprt &index) |
| Creates an if_expr corresponding to the result of accessing the array at the given index. More... | |
Additional Inherited Members | |
| Protected Member Functions inherited from sparse_arrayt | |
| sparse_arrayt (exprt default_value) | |
| Protected Attributes inherited from sparse_arrayt | |
| exprt | default_value |
| std::map< std::size_t, exprt > | entries |
Detailed Description
Represents arrays by the indexes up to which the value remains the same.
For instance ‘{'a’, 'a', 'a', 'b', 'b', 'c'}‘ would be represented by by ('a’, 2) ; ('b', 4), ('c', 5). This is particularly useful when the array is constant on intervals.
Definition at line 98 of file string_refinement_util.h.
Constructor & Destructor Documentation
◆ interval_sparse_arrayt() [1/4]
|
inlineexplicit |
An expression of the form array_of(x) with {i:=a} with {j:=b} is converted to an array arr where for all index k smaller than i, arr[k] is a, for all index between i (exclusive) and j it is b and for the others it is x.
Definition at line 105 of file string_refinement_util.h.
◆ interval_sparse_arrayt() [2/4]
| interval_sparse_arrayt::interval_sparse_arrayt | ( | const array_exprt & | expr, |
| const exprt & | extra_value | ||
| ) |
Initialize an array expression to sparse array representation, avoiding repetition of identical successive values and setting the default to extra_value.
Definition at line 122 of file string_refinement_util.cpp.
◆ interval_sparse_arrayt() [3/4]
| interval_sparse_arrayt::interval_sparse_arrayt | ( | const array_list_exprt & | expr, |
| const exprt & | extra_value | ||
| ) |
Initialize a sparse array from an array represented by a list of index-value pairs, and setting the default to extra_value.
Indexes must be constant expressions, and negative indexes are ignored.
Definition at line 140 of file string_refinement_util.cpp.
◆ interval_sparse_arrayt() [4/4]
|
inlineexplicit |
Array containing the same value at each index.
Definition at line 136 of file string_refinement_util.h.
Member Function Documentation
◆ at()
| exprt interval_sparse_arrayt::at | ( | std::size_t | index | ) | const |
Get the value at the specified index.
Complexity is logarithmic in the number of entries.
Definition at line 169 of file string_refinement_util.cpp.
◆ concretize()
| array_exprt interval_sparse_arrayt::concretize | ( | std::size_t | size, |
| const typet & | index_type | ||
| ) | const |
Convert to an array representation, ignores elements at index >= size.
Definition at line 176 of file string_refinement_util.cpp.
◆ of_expr()
|
static |
If the expression is an array_exprt or a with_exprt uses the appropriate constructor, otherwise returns empty optional.
Definition at line 158 of file string_refinement_util.cpp.
◆ to_if_expression()
Definition at line 105 of file string_refinement_util.cpp.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/solvers/strings/string_refinement_util.h
- /home/runner/work/cbmc/cbmc/src/solvers/strings/string_refinement_util.cpp
