ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
smtlib_smt_sort Class Reference

#include <smtlib_conv.h>

Inheritance diagram for smtlib_smt_sort:
[legend]

Public Member Functions

 smtlib_smt_sort (smt_sort_kind k, unsigned int w)
 smtlib_smt_sort (smt_sort_kind k, unsigned int w1, unsigned int w2)
 smtlib_smt_sort (smt_sort_kind k)
 smtlib_smt_sort (smt_sort_kind k, const smtlib_smt_sort *dom, const smtlib_smt_sort *rag)
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

const smtlib_smt_sort * domain
const smtlib_smt_sort * range
Public Attributes inherited from smt_sort
smt_sort_kind id
 Identifies what /kind/ of sort this is.

Constructor & Destructor Documentation

◆ smtlib_smt_sort() [1/4]

smtlib_smt_sort::smtlib_smt_sort ( smt_sort_kind k,
unsigned int w )
inlineexplicit

◆ smtlib_smt_sort() [2/4]

smtlib_smt_sort::smtlib_smt_sort ( smt_sort_kind k,
unsigned int w1,
unsigned int w2 )
inlineexplicit

◆ smtlib_smt_sort() [3/4]

smtlib_smt_sort::smtlib_smt_sort ( smt_sort_kind k)
inlineexplicit

◆ smtlib_smt_sort() [4/4]

smtlib_smt_sort::smtlib_smt_sort ( smt_sort_kind k,
const smtlib_smt_sort * dom,
const smtlib_smt_sort * rag )
inlineexplicit

Member Data Documentation

◆ domain

const smtlib_smt_sort* smtlib_smt_sort::domain

◆ range

const smtlib_smt_sort* smtlib_smt_sort::range

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