Deklarieren uninterpretierte polyadische Funktionen mit Z3Py

Question

Mit Z3Py, Ich versuche, eine Funktion decl_func(fname, arity) zu schreiben, die in zwei Argumente nimmt: fname, der Name der Funktion erklärt und arity, die Zahl der Argumente werden, und gibt die entsprechenden (nicht interpretierte) Z3-Funktion über ganze Zahlen. Das Problem ist, dass der Wert von arity kann nicht vorgegeben werden, so dass der Funktionskörper nicht

sein kann

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

oder

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

wie es für unäre oder binäre Funktionen sei. Hier ist eine grobe Abhilfe, die ich in Betracht gezogen habe:

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

aber das funktioniert nicht, scheinbar aufgrund der Art und Weise exec Variablendeklarationen Griffe (Ich verwende Python 3, wenn es das ist relevant).

Irgendwelche Gedanken?

Answer 1

Diese Frage bezieht sich auf variadic functions in Python.

Sie können die gleiche "*" Syntax verwenden, um die Funktion zu einer bestehenden Liste von Argumenten gelten:

daher so etwas wie diese sollte Arbeit:

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