cprover
Loading...
Searching...
No Matches
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:
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.
 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_arraytof_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, exprtentries

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.

◆ 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]

interval_sparse_arrayt::interval_sparse_arrayt ( exprt default_value)
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()

std::optional< interval_sparse_arrayt > interval_sparse_arrayt::of_expr ( const exprt & expr,
const exprt & extra_value )
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()

exprt interval_sparse_arrayt::to_if_expression ( const exprt & index) const

Definition at line 105 of file string_refinement_util.cpp.


The documentation for this class was generated from the following files: