cprover
sparse_arrayt Class Reference

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>

Inheritance diagram for sparse_arrayt:
[legend]
Collaboration diagram for sparse_arrayt:
[legend]

Public Member Functions

 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...
 
virtual exprt to_if_expression (const exprt &index) const
 Creates an if_expr corresponding to the result of accessing the array at the given index. More...
 
virtual exprt at (std::size_t index) const
 Get the value at the specified index. More...
 

Protected Member Functions

 sparse_arrayt (exprt default_value)
 

Protected Attributes

exprt default_value
 
std::map< std::size_t, exprtentries
 

Detailed Description

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

Constructor & Destructor Documentation

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

References can_cast_expr< with_exprt >(), default_value, entries, expr_dynamic_cast(), and PRECONDITION.

◆ sparse_arrayt() [2/2]

sparse_arrayt::sparse_arrayt ( exprt  default_value)
inlineexplicitprotected

Definition at line 85 of file string_refinement_util.h.

Member Function Documentation

◆ at()

exprt sparse_arrayt::at ( std::size_t  index) const
virtual

Get the value at the specified index.

Complexity is linear in the number of entries.

Reimplemented in interval_sparse_arrayt.

Definition at line 93 of file string_refinement_util.cpp.

References default_value, and entries.

◆ to_if_expression()

exprt sparse_arrayt::to_if_expression ( const exprt index) const
virtual

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

Reimplemented in interval_sparse_arrayt.

Definition at line 76 of file string_refinement_util.cpp.

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

Referenced by substitute_array_access().

Member Data Documentation

◆ default_value

◆ entries


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