FunctionValue

class FunctionValue

Public Functions

Sort sort() const

bool is_tabular() const

True for an uninterpreted function’s finite table. A define-fun has a symbolic body instead: size, entry, entries and else_value are UNSUPPORTED; apply evaluates the body in this snapshot.

std::size_t size() const

Entry entry(std::size_t i) const

std::vector<Entry> entries() const

Term else_value() const

always ground: a VALUE of the codomain

Term apply(const std::vector<Term> &arg_values) const

Term as_ite_term(const std::vector<Term> &formal_args) const

The interpretation over the supplied arguments, with free symbols and uninterpreted functions replaced by their snapshot values. A definition can produce a general expression rather than an ITE. UNSUPPORTED for parameter-dependent partial FP operations; apply still evaluates them.

FunctionValue(const FunctionValue&) noexcept

FunctionValue &operator=(const FunctionValue&) noexcept

~FunctionValue()

struct Entry

An application the model records; every other one is else_value().

Public Members

std::vector<Term> args

Term value