smt_array_theoryt::selectt Struct Reference

#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:

• /home/runner/work/cbmc/cbmc/src/solvers/smt2_incremental/theories/smt_array_theory.h
• /home/runner/work/cbmc/cbmc/src/solvers/smt2_incremental/theories/smt_array_theory.cpp