ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
solver_smt_sort< solver_sort > Class Template Reference

#include <smt_sort.h>

Inheritance diagram for solver_smt_sort< solver_sort >:
[legend]

Public Member Functions

 solver_smt_sort (smt_sort_kind i, solver_sort _s)
 solver_smt_sort (smt_sort_kind i, solver_sort _s, const type2tc &_tupletype)
 solver_smt_sort (smt_sort_kind i, solver_sort _s, unsigned int w)
 solver_smt_sort (smt_sort_kind i, solver_sort _s, unsigned int w, unsigned int sw)
 solver_smt_sort (smt_sort_kind i, solver_sort _s, std::size_t dw, const smt_sort *_rangesort)
 solver_smt_sort (smt_sort_kind i, solver_sort _s, const type2tc &type, std::size_t width, smt_sortt range_sort)
 ~solver_smt_sort () override=default
Public Member Functions inherited from smt_sort
 smt_sort (smt_sort_kind i)
 smt_sort (smt_sort_kind i, const type2tc &type)
 smt_sort (smt_sort_kind i, std::size_t width)
 smt_sort (smt_sort_kind i, std::size_t width, std::size_t sigwidth)
 smt_sort (smt_sort_kind i, std::size_t dom_width, smt_sortt range_sort)
 smt_sort (smt_sort_kind i, const type2tc &type, std::size_t dom_width, smt_sortt range_sort)
size_t get_data_width () const
size_t get_domain_width () const
smt_sortt get_range_sort () const
size_t get_significand_width () const
size_t get_exponent_width () const
const type2tc & get_tuple_type () const
virtual ~smt_sort ()=default

Public Attributes

solver_sort s
Public Attributes inherited from smt_sort
smt_sort_kind id
 Identifies what /kind/ of sort this is.

Constructor & Destructor Documentation

◆ solver_smt_sort() [1/6]

template<typename solver_sort>
solver_smt_sort< solver_sort >::solver_smt_sort ( smt_sort_kind i,
solver_sort _s )
inline

◆ solver_smt_sort() [2/6]

template<typename solver_sort>
solver_smt_sort< solver_sort >::solver_smt_sort ( smt_sort_kind i,
solver_sort _s,
const type2tc & _tupletype )
inline

◆ solver_smt_sort() [3/6]

template<typename solver_sort>
solver_smt_sort< solver_sort >::solver_smt_sort ( smt_sort_kind i,
solver_sort _s,
unsigned int w )
inline

◆ solver_smt_sort() [4/6]

template<typename solver_sort>
solver_smt_sort< solver_sort >::solver_smt_sort ( smt_sort_kind i,
solver_sort _s,
unsigned int w,
unsigned int sw )
inline

◆ solver_smt_sort() [5/6]

template<typename solver_sort>
solver_smt_sort< solver_sort >::solver_smt_sort ( smt_sort_kind i,
solver_sort _s,
std::size_t dw,
const smt_sort * _rangesort )
inline

◆ solver_smt_sort() [6/6]

template<typename solver_sort>
solver_smt_sort< solver_sort >::solver_smt_sort ( smt_sort_kind i,
solver_sort _s,
const type2tc & type,
std::size_t width,
smt_sortt range_sort )
inline

◆ ~solver_smt_sort()

template<typename solver_sort>
solver_smt_sort< solver_sort >::~solver_smt_sort ( )
overridedefault

Member Data Documentation

◆ s

template<typename solver_sort>
solver_sort solver_smt_sort< solver_sort >::s
The documentation for this class was generated from the following file: