TermManager

class TermManager

A shared handle. Copies share one manager. The manager is destroyed when the last handle, term, sort, solver and model referring to it is destroyed.

Names passed to declare_sort, declare and bind_symbol, and prefixes passed to mk_fresh_sort and mk_fresh, must be representable as SMT-LIB quoted symbols: no NUL, ‘|’, backslash, DEL, or ASCII control characters other than tab, newline and carriage return. Spaces and non-ASCII bytes (including UTF-8) are allowed; the printer quotes where needed. Names and prefixes beginning with ‘@’ or ‘.’ are reserved for solver use. Violations are INVALID_ARGUMENT before any name is recorded. Names must be nonempty; fresh-name prefixes may be empty.

Public Functions

TermManager()

Config{}.

explicit TermManager(const Config&)

explicit TermManager(const Options &manager_options)

The same three entries by registry name; a solver-scoped entry that is SET in it is OPTION_VALUE.

TermManager(const TermManager&) noexcept

TermManager(TermManager&&) noexcept

TermManager &operator=(const TermManager&) noexcept

TermManager &operator=(TermManager&&) noexcept

~TermManager()

std::uint64_t id() const noexcept

process-unique

bool simplify() const noexcept

construction-time folding; fixed

RoundingMode default_rounding_mode() const noexcept

void set_default_rounding_mode(RoundingMode)

std::uint32_t uf_sort_width() const noexcept

Sort mk_bool_sort()

Sort mk_bv_sort(std::uint32_t width)

INVALID_ARGUMENT if width == 0.

Sort mk_fp_sort(std::uint32_t exp_size, std::uint32_t sig_size)

each >= 2

Sort mk_fp16_sort()

Sort mk_fp32_sort()

Sort mk_fp64_sort()

Sort mk_fp128_sort()

Sort mk_rm_sort()

Sort mk_real_sort()

Sort mk_array_sort(const Sort &index, const Sort &element)

UNSUPPORTED for combinations the engine lacks.

Sort mk_fun_sort(const std::vector<Sort> &domain, const Sort &codomain)

Sort declare_sort(std::string_view name)

named uninterpreted sort, keyed by name; INVALID_ARGUMENT for a sort SMT-LIB predefines (Bool, Real, …)

Sort mk_fresh_sort(std::string_view prefix = "")

anonymous, printed as prefix!k

Term declare(std::string_view name, const Sort&)

A named symbol, keyed by name in the manager’s one name table: the same name and sort give the same term whether it comes from this call, from Python’s BitVec(‘x’, 32), from a parsed script or from bind_symbol; SORT_MISMATCH if the name is already declared at another sort. In addition to the name rules above, a symbol SMT-LIB’s theories predefine cannot be declared (true, select, bvadd, RNE, +, …): INVALID_ARGUMENT, since |true| and true are the same symbol and no printed script could tell the two apart. INVALID_ARGUMENT for a name retained by define-fun; retrieve it with symbol() instead.

Term mk_fresh(const Sort&, std::string_view prefix = "")

An anonymous symbol that never enters the name table: fresh on every call, printed as prefix!k with a manager-unique k.

std::optional<Term> symbol(std::string_view name) const

Name lookup, including retained define-fun names: a nullary definition returns its body; a parameterized one returns a callable FUN term whose applications expand its body.

std::vector<Term> symbols() const

Declared symbols and parameterized definitions, each identity once. Nullary definitions name expressions, so are found only with symbol().

std::vector<Sort> declared_sorts() const

every declared sort, declaration order

void bind_symbol(std::string_view name, const Term&)

a symbol under a second name: SORT_MISMATCH if taken, INVALID_ARGUMENT for a compound term or a predefined name

Term term_from_id(std::uint64_t id) const

INVALID_ARGUMENT if no live term has that id.

Term mk_true()

Term mk_false()

Term mk_bool(bool)

Term mk_bv(std::uint32_t width, std::uint64_t value)

VALUE_OUT_OF_RANGE unless value < 2^width.

Term mk_bv_signed(std::uint32_t width, std::int64_t value)

two’s complement range

Term mk_bv(std::uint32_t width, std::string_view digits, int base)

base 2/10/16; optional #b/#x/0x; ‘-’ in base 10; ‘_’ between two digits separates them

Term mk_bv_limbs(std::uint32_t width, const std::vector<std::uint64_t> &lsb_first)

Term mk_bv_bytes(std::uint32_t width, const std::vector<std::uint8_t> &bytes, bool little_endian = true)

Term mk_bv_wrapped(std::uint32_t width, std::uint64_t value)

value mod 2^width

Term mk_bv_zero(std::uint32_t width)

Term mk_bv_ones(std::uint32_t width)

Term mk_bv_min_signed(std::uint32_t width)

Term mk_bv_max_signed(std::uint32_t width)

Term mk_fp_from_bits(const Sort &fp, const Term &bv_value)

NaN canonicalised.

Term mk_fp_from_bits(const Sort &fp, std::string_view bits)

“0b..”, “0x..” or bare binary

Term mk_fp(const Term &sign, const Term &exponent, const Term &significand)

(fp …); symbolic allowed

Term mk_fp_pos_zero(const Sort &fp)

Term mk_fp_neg_zero(const Sort &fp)

Term mk_fp_pos_inf(const Sort &fp)

Term mk_fp_neg_inf(const Sort &fp)

Term mk_fp_nan(const Sort &fp)

the canonical quiet NaN of the format

Term mk_fp(const Sort &fp, RoundingMode rm, double value)

exact, then rounded once under rm

Term mk_fp(const Sort &fp, RoundingMode rm, std::string_view decimal_or_rational)

“0.1”, “1/3”, “-2.5e-3”

Term mk_rm(RoundingMode)

Term mk_real(std::int64_t)

Term mk_real(std::int64_t numerator, std::int64_t denominator)

INVALID_ARGUMENT if 0.

Term mk_real(std::string_view literal)

“-3/7”, “0.25”, “12”

Term mk_const_array(const Sort &array_sort, const Term &element)

element: a value (no symbol in it), UNSUPPORTED otherwise

Term mk_term(Kind, const std::vector<Term> &args, const std::vector<std::uint32_t> &indices = {}, std::optional<Sort> result_sort = std::nullopt)

Term mk_term(Kind, std::initializer_list<Term> args, std::initializer_list<std::uint32_t> indices = {})

Term simplify(const Term&) const

local rewrites only; touches no solver; an unspecified floating-point case (fp.min of +0 and -0, fp.to_ubv of NaN, …) stays as it is

Friends

friend bool operator==(const TermManager&, const TermManager&) noexcept

friend bool operator!=(const TermManager&, const TermManager&) noexcept

struct Config

Public Members

bool simplify = true

RoundingMode default_rounding_mode = RoundingMode::RNE

std::uint32_t uf_sort_width = 16