CODEWITHSUNDEEP
z3py
Pierre Carbonnelle
Pierre Carbonnelle

Reputation: 2615

How to define a function in Z3py?

How can I write the equivalent of this code using the Z3 python API ?

(define-fun mymax ((a Int) (b Int)) Int
  (ite (> a b) a b))

(assert (= (mymax 100 7) 100))

(check-sat)
(get-model)

Unfortunately, the Function method is the Python equivalent to declare_fun, not define_fun: it does not accept an argument containing the function definition. It would be nice if we could write something like:

mymax = Function('mymax', IntSort(), IntSort(), IntSort(),
                 Lambda([a,b], If(a>b, a, b))

(I could declare mymax and add an appropriate constraint for it, but, when the function is large and complex, z3 must search for its definition, which does not seem very efficient. I'd rather give z3 the definition)

Upvotes: 1

Views: 949

Answers (1)

alias
alias

Reputation: 30418

Typically, Function declarations are intended for introducing uninterpreted-names into the environment. That is, you tell the solver there's this function and maybe it obeys some rules; such as commutativity, associativity etc; but that's all you care about, i.e., no actual definition.

If you do know the definition, which seems to be your use case, the recommended method is actually to use directly a Python function itself; which manipulates symbolic expressions. In your example, it'd be:

def symMax(a, b):
  return If(a>b, a, b)

And then simply use this in your code and it'll expand to the right definition.

There's one exception to this: What happens if your function is recursive: You can use a recursive Python function, but it's likely that the expansion won't work in this case as the "termination" condition might be symbolic. In these cases, use RecAddDefinition: https://z3prover.github.io/api/html/namespacez3py.html#a7029cec3faf5bd7cdd9d9e0365f8a3b5

Note that you can also use RecAddDefinition when your definition isn't recursive at all; and maybe that's what you had in mind. But in those cases, defining a Python function is the preferred way, as you can more easily manipulate the terms.

See this question for an example use of RecAddDefinition: https://stackoverflow.com/a/68457868/936310

Upvotes: 3

Related Questions