Объявление неинтерпретируемых полиадных функций с помощью Z3Py

Используя Z3Py, я пытаюсь написать функцию decl_func(fname, arity), которая принимает два аргумента: fname, имя объявляемой функции, и arity, ее количество аргументов, и возвращает соответствующую (не интерпретируемую) функцию Z3 над целыми числами. Проблема в том, что значение arity не может быть задано заранее, поэтому тело функции не может быть

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

or

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

как это было бы для унарных или бинарных функций. Вот один грубый обходной путь, который я рассмотрел:

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

но это не работает, по-видимому, из-за того, как exec обрабатывает объявления переменных (я использую Python 3, если это уместно).

Есть предположения?


python-3.x z3 z3py
person user287393    schedule 13.05.2016    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Этот вопрос касается вариативных функций в Python.

Вы можете использовать тот же синтаксис «*», чтобы применить функцию к существующему списку аргументов:

Поэтому что-то вроде этого должно работать:

sorts = [IntSort(), IntSort(), IntSort()]
return Function(fname, *sorts)
person iago    schedule 15.05.2016