CODEWITHSUNDEEP
python-3.xz3z3py
user287393
user287393

Reputation: 1251

Declaring uninterpreted polyadic functions with Z3Py

Using Z3Py, I'm trying to write a function decl_func(fname, arity) which takes in two arguments : fname, the name of the function to be declared, and arity, its number of arguments, and returns the corresponding (uninterpreted) Z3 function over integers. The problem is that the value of arity cannot be predetermined, so the function body cannot be

return Function(fname, IntSort(), IntSort())

or

return Function(fname, IntSort(), IntSort(), IntSort())

as it would be for unary or binary functions. Here's one crude workaround I've considered :

exec('f = Function(\'%s\', %s)' % (fname, ('IntSort(), ' * arity + 'IntSort()')))
return f

but this does not work, seemingly due to the way exec handles variable declarations (I'm using Python 3, if that is relevant).

Any thoughts?

Upvotes: 0

Views: 125

Answers (1)

iago
iago

Reputation: 277

This question is about variadic functions in Python.

You can use the same "*" syntax to apply the function to an existing list of arguments:

Therefore, something like this should work:

sorts = [IntSort(), IntSort(), IntSort()]
return Function(fname, *sorts)

Upvotes: 1

Related Questions