Я хочу использовать одностороннюю функцию в z3 программе Python.Я бы хотел, чтобы z3 соблюдал следующие свойства / тактику:
- , если
x = y, то f(x) = f(y) f - это вычислимая функция Python, которую я могу предоставить, когдаx известно - , если
f(x) = y, попытаться разрешить путем сопоставления f(*y) = f(x), подразумевая x = *y из предыдущих назначений (никогда не пытайтесь угадать x, который вычисляется в y)
Существуют ли встроенные функции для поддержки этой конструкции или что-нибудь еще, что может помочь ее представить?