0

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)

Pierre Carbonnelle
  • 2,305
  • 19
  • 25

1 Answers1

2

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

alias
  • 28,120
  • 2
  • 23
  • 40
  • Thanks for the tips. I guess a python function and RecAddDefinition are quite similar in terms of processing, but when the function is complex and used frequently, I suspect that ` RecAddDefinition` will be relatively faster, because a call to it will be interpreted in C++ instead of in Python. – Pierre Carbonnelle Aug 07 '21 at 18:23
  • The two methods are actually quite different. With `RecAddDefinition`, you're registering this as a function with the solver; which will process it as such and expand definitions based on what the solver needs. With the Python version, every call will be completely unrolled before you even pass it to the solver. (Hence it'll have problems if recursive and does not symbolically terminate.) You can't reasonable talk about "efficiency" in either method; I'd actually think the Python version would be faster if always applied to ground terms. They are complementary techniques. – alias Aug 07 '21 at 19:29