cprover
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. 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 override
 Creates an if_expr corresponding to the result of accessing the array at the given index. More...
 
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 override
 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 optionalt< 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. 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, 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 94 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 101 of file string_refinement_util.h.

Referenced by of_expr().

◆ 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 116 of file string_refinement_util.cpp.

References sparse_arrayt::entries, and exprt::operands().

◆ 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 134 of file string_refinement_util.cpp.

References sparse_arrayt::entries, INVARIANT, numeric_cast(), exprt::operands(), PRECONDITION, and exprt::type().

◆ 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 132 of file string_refinement_util.h.

Member Function Documentation

◆ at()

exprt interval_sparse_arrayt::at ( std::size_t  index) const
overridevirtual

Get the value at the specified index.

Complexity is linear in the number of entries.

Reimplemented from sparse_arrayt.

Definition at line 163 of file string_refinement_util.cpp.

References sparse_arrayt::default_value, and sparse_arrayt::entries.

◆ 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 170 of file string_refinement_util.cpp.

References sparse_arrayt::default_value, sparse_arrayt::entries, from_integer(), index_type(), and exprt::type().

Referenced by string_refinementt::get().

◆ of_expr()

optionalt< 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 152 of file string_refinement_util.cpp.

References interval_sparse_arrayt().

Referenced by string_refinementt::get(), and get_array().

◆ to_if_expression()

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

Creates an if_expr corresponding to the result of accessing the array at the given index.

Reimplemented from sparse_arrayt.

Definition at line 99 of file string_refinement_util.cpp.

References CHECK_RETURN, sparse_arrayt::default_value, sparse_arrayt::entries, from_integer(), and exprt::type().

Referenced by substitute_array_access().


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