stp.FuncInterp

class stp.FuncInterp

A function in a saved model. Uninterpreted functions have entries and an else value; define-fun functions have a symbolic body. Both are callable; is_tabular() tells whether table inspection is supported.

arity()

else_value()

num_entries()

entry(i)

((arg values…), value)

entries()

__len__()

__iter__()

__call__(*arg_values)

Call self as a function.

as_ite(*formals)

apply(arg_values)

is_tabular()

size()

sort()