Sort¶

class Sort¶

Public Functions

Sort() noexcept¶: the null sort; is_null() is true

Sort(const Sort&) noexcept¶

Sort(Sort&&) noexcept¶

Sort &operator=(const Sort&) noexcept¶

Sort &operator=(Sort&&) noexcept¶

~Sort()¶

bool is_null() const noexcept¶

explicit operator bool() const = delete¶: no implicit truthiness

SortKind kind() const¶

bool is_bool() const¶

bool is_bv() const¶

bool is_fp() const¶

bool is_rm() const¶

bool is_real() const¶

bool is_array() const¶

bool is_fun() const¶

bool is_uninterpreted() const¶

std::uint32_t bv_size() const¶: INVALID_ARGUMENT unless is_bv()

std::uint32_t fp_exp_size() const¶: INVALID_ARGUMENT unless is_fp()

std::uint32_t fp_sig_size() const¶: includes the hidden bit (SMT-LIB)

Sort array_index() const¶

Sort array_element() const¶

std::vector<Sort> fun_domain() const¶

Sort fun_codomain() const¶

std::uint32_t fun_arity() const¶

std::string name() const¶: uninterpreted sorts only

std::uint64_t id() const noexcept¶: manager-unique, never reused

TermManager manager() const¶

std::string str() const¶: SMT-LIB 2.

Friends

friend bool operator==(const Sort&, const Sort&) noexcept¶

friend bool operator!=(const Sort&, const Sort&) noexcept¶

friend bool operator<(const Sort&, const Sort&) noexcept¶

friend std::ostream &operator<<(std::ostream&, const Sort&)¶