Term¶

class Term¶

A term is one intrusive pointer to a hash-consed engine node. Equal terms are the same node. The node pins its manager. A value term (kind() == VALUE) is a term like any other: it can be asserted, compared and decoded. A symbol prints as its declared name, or as prefix!k if made by mk_fresh.

Public Functions

Term() noexcept¶: the null term

Term(const Term&) noexcept¶

Term(Term&&) noexcept¶

Term &operator=(const Term&) noexcept¶

Term &operator=(Term&&) noexcept¶

~Term()¶

bool is_null() const noexcept¶

explicit operator bool() const = delete¶

Kind kind() const¶

Sort sort() const¶

std::size_t num_children() const¶

Term child(std::size_t i) const¶: INDEX_OUT_OF_RANGE.

std::vector<Term> children() const¶

std::vector<std::uint32_t> indices() const¶: empty unless indexed

std::uint64_t id() const noexcept¶: unique within the manager; never reused

TermManager manager() const¶

bool is_value() const noexcept¶: kind() == VALUE

bool is_const() const noexcept¶: kind() == CONSTANT (including defined functions)

bool is_defined_function() const noexcept¶: a parameterized define-fun handle

std::optional<std::string> symbol() const¶: the declared name, if any

bool to_bool() const¶

bool fits_uint64() const¶

bool fits_int64() const¶: int64: two’s complement of the BV’s own width

std::uint64_t to_uint64() const¶: DOES_NOT_FIT if width > 64 and too big.

std::int64_t to_int64() const¶

std::string to_bv_string(int base = 2, bool pad = true) const¶: base 2, 10 or 16; padded to the width for 2 and 16 (ceil(n/4) hex digits)

std::vector<std::uint64_t> to_bv_limbs() const¶: LSB-first, ceil(w/64)

std::vector<std::uint8_t> to_bv_bytes(bool little_endian = true) const¶

FloatValue to_fp() const¶

RoundingMode to_rm() const¶

RationalValue to_rational() const¶

std::uint64_t to_uninterpreted_index() const¶: element index in its sort

Term operator[](const Term &index) const¶: select

Term operator()(std::initializer_list<Term> args) const¶: APPLY.

Term operator()(const std::vector<Term> &args) const¶

template<class ...Ts> inline Term operator()(const Term &first, const Ts&... rest) const¶

Term substitute(const std::vector<std::pair<Term, Term>> &map) const¶

std::string str() const¶: SMT-LIB 2, untruncated, no let-sharing; any depth

std::string to_string(Format f, bool share_subterms = true) const¶: SMT-LIB 2 with let-sharing, DOT or GDL through the engine’s printers, which recurse once per level of the term: one some ten thousand levels deep can overflow the stack there (str() cannot).

bool same_as(const Term&) const noexcept¶: structural: the same node

Friends

friend Term operator==(const Term&, const Term&)¶: EQUAL.

friend Term operator!=(const Term&, const Term&)¶: DISTINCT.

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

struct Less¶

by id; std::less<Term> is this

Subclassed by std::less< stp::api::Term >

Public Functions

bool operator()(const Term&, const Term&) const noexcept¶