stp.Model

class stp.Model

A detached snapshot of the last check that answered sat. Survives every later solver operation; never mutates. Completion is explicit: m[t] is a mapping lookup and raises KeyError (naming the missing symbol) if evaluating t would need a symbol the solver never saw; m.eval(t) completes such symbols with their sort’s default; m.get(t, default) is the mapping idiom. A term of another manager is translated by name first.

manager()

__getitem__(t)

get(t, default=None)

eval(t, model_completion=True)

The value of t. model_completion=True (the default): symbols outside the core take their sort’s default (never None). model_completion=False: the core’s values are substituted, the result simplified, and symbols outside the core left in place (z3py).

evaluate(t, model_completion=True)

The value of t. model_completion=True (the default): symbols outside the core take their sort’s default (never None). model_completion=False: the core’s values are substituted, the result simplified, and symbols outside the core left in place (z3py).

values(ts)

decls()

in_core(symbol)

array_bytes(array, first_index, count)

count elements from first_index of a BV-indexed array of byte-multiple elements.

to_smt2()

sexpr()

__len__()

__iter__()

__contains__(t)

translate(tm)

static from_smt2(text, tm=None)

Rebuild a model from the text of to_smt2() on tm (a private TermManager with tm=None), through a scratch solver of its own; the solvers already live over tm are untouched. Lookups with terms of other managers translate them by name.

array_value(t)

copy()

fun_value(t)

num_symbols()

symbol(i)

symbols()

try_value(t)

The value of t, or None if completion would be needed.

value(t)

The value of t, completing symbols outside the core.