Model¶

class Model¶

A detached snapshot. One snapshot exists per successful check, taken at the first model()/value() call (or before the solver’s state changes) and shared by every Model handle afterwards. Never refuses, never mutates.

Public Functions

TermManager manager() const¶

Term value(const Term&) const¶: A VALUE of the term’s sort; any term of this manager, built before or after the check; symbols outside the core are COMPLETED with their sort’s default. An array’s value is a term with no symbol in it: the constant array of its default under a store per cell (array_value(t).as_term()). A function has no value term: SORT_MISMATCH, read it with function_value.

std::optional<Term> try_value(const Term&) const¶: nullopt instead of completing; an array is complete when its base is an array in the core (default included) or a constant array

std::vector<Term> values(const std::vector<Term>&) const¶: batch (completing)

bool bool_value(const Term&) const¶

std::uint64_t uint64_value(const Term&) const¶: DOES_NOT_FIT.

std::int64_t int64_value(const Term&) const¶

std::string bv_string(const Term&, int base = 2, bool pad = true) const¶

std::vector<std::uint64_t> bv_limbs(const Term&) const¶

std::vector<std::uint8_t> bv_bytes(const Term&, bool little_endian = true) const¶

FloatValue fp_value(const Term&) const¶

RoundingMode rm_value(const Term&) const¶

RationalValue real_value(const Term&) const¶

std::uint64_t uninterpreted_index(const Term&) const¶

ArrayValue array_value(const Term&) const¶: any array-sorted term

FunctionValue function_value(const Term&) const¶: any function-sorted term

void array_bytes(const Term &array, std::uint64_t first_index, std::size_t count, std::uint8_t *out) const¶: Dense read of a BV-indexed, BV-element array whose element width is a multiple of 8: elements [first_index, first_index + count) as little-endian bytes per element, completed by the model’s array fill rule. INVALID_ARGUMENT when the interval leaves the index sort.

std::vector<Term> symbols() const¶: the model core: symbols the solver assigned

bool in_core(const Term &symbol) const¶: false: value() would complete it

std::string to_smt2() const¶: the whole model

Model(const Model&) noexcept¶

Model &operator=(const Model&) noexcept¶

~Model()¶

Friends

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