Z3Pyで未解釈​​polyadic関数を宣言します

Question

Z3Pyを使用して、decl_func(fname, arity)という2つの引数をとります：fname、宣言する関数の名前、およびその引数の数arityを返します。 （解釈されていない）Z3の整数を超える。問題は、それが単項またはバイナリの機能のためであるように、関数本体は

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

又は

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

できないようarityの値が、所定のできないことです。一見によるexecは、変数の宣言を処理する方法（それが関連している場合、私は、Pythonの3を使用しています）に、

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

が、これは動作しません：ここで私が考えられてきた1つの、粗製の回避策です。

どのような考えですか？

Answer 1

この質問は約variadic functions in Pythonです。

あなたは、引数の既存のリストに関数を適用するには、同じ "*" 構文を使用することができます。

したがって、このはず仕事のようなもの：

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