smt_bit_vector_theoryt::extractt Struct Reference

#include <smt_bit_vector_theory.h>

Public Member Functions
smt_sortt	return_sort (const smt_termt &operand) const
std::vector< smt_indext >	indices () const
void	validate (const smt_termt &operand) const

Static Public Member Functions
static const char *	identifier ()

Public Attributes
std::size_t	i
std::size_t	j

Detailed Description

Definition at line 19 of file smt_bit_vector_theory.h.

Member Function Documentation

identifier()

const char * smt_bit_vector_theoryt::extractt::identifier ( )

static

Definition at line 54 of file smt_bit_vector_theory.cpp.

indices()

std::vector< smt_indext > smt_bit_vector_theoryt::extractt::indices

(

)

const

Definition at line 65 of file smt_bit_vector_theory.cpp.

return_sort()

smt_sortt smt_bit_vector_theoryt::extractt::return_sort

(

const smt_termt &

operand

)

const

Definition at line 60 of file smt_bit_vector_theory.cpp.

validate()

void smt_bit_vector_theoryt::extractt::validate

(

const smt_termt &

operand

)

const

Definition at line 70 of file smt_bit_vector_theory.cpp.

Member Data Documentation

i

std::size_t smt_bit_vector_theoryt::extractt::i

Definition at line 21 of file smt_bit_vector_theory.h.

j

std::size_t smt_bit_vector_theoryt::extractt::j

Definition at line 22 of file smt_bit_vector_theory.h.

---

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

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