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

Static Public Member Functions

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

Member Function Documentation

◆ to_if_expression()

exprt sparse_arrayt::to_if_expression ( const with_exprt expr,
const exprt index 
)
static

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

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: