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>
|
| | 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...
|
| |
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 73 of file string_refinement_util.h.
◆ sparse_arrayt() [1/2]
| sparse_arrayt::sparse_arrayt |
( |
const with_exprt & |
expr | ) |
|
|
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 67 of file string_refinement_util.cpp.
◆ sparse_arrayt() [2/2]
| sparse_arrayt::sparse_arrayt |
( |
exprt |
default_value | ) |
|
|
inlineexplicitprotected |
◆ to_if_expression()
Creates an if_expr corresponding to the result of accessing the array at the given index.
Definition at line 84 of file string_refinement_util.cpp.
◆ default_value
| exprt sparse_arrayt::default_value |
|
protected |
◆ entries
| std::map<std::size_t, exprt> sparse_arrayt::entries |
|
protected |
The documentation for this class was generated from the following files:
Inheritance diagram for sparse_arrayt: