How can I define a function in z3 Python API since the new SMT-LIB standard?

Question

The new SMT-LIB standard allows for a function defintion command of the form:

(define-fun f ((x1 σ1) · · · (xn σn)) σ t) 

The spec clarifies that this is semantically equivalent to

(declare-fun f (σ1 · · · σn) σ)
(assert (forall ((x1 σ1) · · · (xn σn)) (= ( f x1 · · · xn) t))

At the moment I would define a function using the Python z3 API as follows:

s = z3.Solver()
f = z3.Function("f", [σ1 ... σn, σ])
s.add(z3.ForAll([x1, ...,xn], t == f(x1, ..., xn)))

Is that the cannonical way of doing it or is there a more straightforward or efficient way of handling this?

Answer 1

Typically, one simply uses a Python function instead. This function returns the result in term of its symbolic inputs, in a way unrolling the definition before z3 even sees it.

One exception to this is if you want to define a recursive function, whose termination depends on a symbolic argument. Note that you can use the same facility even if your function isn't recursive, which can solve your problem of definitions that come from other sources. For details see RecAddDefinition.