Z3Py: получение функции, соответствующей каждому оператору, например. '*', '==', '-'

Question

Я хочу генерировать уравнения/неравенства в Z3Py автоматически используя алгоритм, который я разрабатываю. Для этого мне нужно использовать такие операторы, как ==, +, * как функции.

Например, в Sympy, я могу добавить два символа следующим образом

import sympy as sp 
sp.Add(x, y) 

, что приводит к x + y.

Могу ли я сделать то же самое в Z3Py?

Для скорости вычислений я считаю, что преобразовать из или в строковое представление выражения нехорошо.

Answer 1

Я не могу найти никакой документации (и я предполагаю, что вы не можете либо) для непосредственной поддержки z3py, однако все неявные операции в питоне есть вызываемые функции в модуле operator :

import operator 

x,y = Ints("x y") 

a = operator.add(x,y) 

, если вы хотите, чтобы отобразить функции их символов, которые вы можете использовать Dict:

ops = {"+":operator.add, "*":operator.mul} #etc. 

Answer 2

Как насчет:

import z3 

x, y = z3.Ints('x y') 
print z3.ExprRef.__eq__(x, y)