Loading...

Searching...

No Matches

Public Member Functions | Static Public Member Functions | List of all members

interval_sparse_arrayt Class Referencefinal

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:

[フレーム]

[legend]

+ Collaboration diagram for interval_sparse_arrayt:

[フレーム]

[legend]

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.

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.

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.

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.

exprt at (std::size_t index) const

Get the value at the specified index.

interval_sparse_arrayt (exprt default_value)

Array containing the same value at each index.

- 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.

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.

- 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.

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]

interval_sparse_arrayt::interval_sparse_arrayt ( const with_exprt & expr )

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.