Loading...

Searching...

No Matches

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

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.

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.

Protected Member Functions

sparse_arrayt (exprt default_value)

Protected Attributes

exprt default_value

std::map< std::size_t, exprt > entries

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 73 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 67 of file string_refinement_util.cpp.

◆ sparse_arrayt() [2/2]

sparse_arrayt::sparse_arrayt ( exprt default_value )

inlineexplicitprotected

Definition at line 89 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 84 of file string_refinement_util.cpp.

Member Data Documentation

◆ default_value

exprt sparse_arrayt::default_value

protected

Definition at line 87 of file string_refinement_util.h.

◆ entries

std::map<std::size_t, exprt> sparse_arrayt::entries

protected

Definition at line 88 of file string_refinement_util.h.

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

/home/runner/work/cbmc/cbmc/src/solvers/strings/string_refinement_util.h
/home/runner/work/cbmc/cbmc/src/solvers/strings/string_refinement_util.cpp