CBMC
Static Public Member Functions | List of all members
smt_array_theoryt::selectt Struct Referencefinal

#include <smt_array_theory.h>

Static Public Member Functions

static const char * identifier ()
 
static smt_sortt return_sort (const smt_termt &array, const smt_termt &index)
 
static std::vector< std::string > validation_errors (const smt_termt &array, const smt_termt &index)
 
static void validate (const smt_termt &array, const smt_termt &index)
 

Detailed Description

Definition at line 11 of file smt_array_theory.h.

Member Function Documentation

◆ identifier()

const char * smt_array_theoryt::selectt::identifier ( )
static

Definition at line 5 of file smt_array_theory.cpp.

◆ return_sort()

smt_sortt smt_array_theoryt::selectt::return_sort ( const smt_termt &  array,
const smt_termt &  index 
)
static

Definition at line 10 of file smt_array_theory.cpp.

◆ validate()

void smt_array_theoryt::selectt::validate ( const smt_termt &  array,
const smt_termt &  index 
)
static

Definition at line 29 of file smt_array_theory.cpp.

◆ validation_errors()

std::vector< std::string > smt_array_theoryt::selectt::validation_errors ( const smt_termt &  array,
const smt_termt &  index 
)
static

Definition at line 17 of file smt_array_theory.cpp.

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