python - 用 Z3 中的表达式替换函数

Question

我正在与 Z3 合作Python API，我想采用一个表达式，并将其替换为声明的函数。也就是说，我想做如下的事情:

from z3 import *

x, y = Ints('x y')

# In practice, this could be a dynamically
# generated expression
expr = x + y * 2

f = Function('f', IntSort(), IntSort(), IntSort())

# Not sure how to implement this
function_substitute(f(x, y) == f(y, x) + f(4,0), (f, [x,y], expr))
# Results in x + y * 2 == y + x * 2 + 4

最初，我以为我想要一个包装 expr 的函数(Levent 对此提供了一个很好的答案)，但经过考虑，这对于替代方法来说并不是特别有帮助，并且绝对感觉有点老套。

任何帮助或建议将不胜感激!

Answer 1

这是一件不寻常的事情，但这里有一个解决方案:

from z3 import *

def functionFromExpr(args, expr):
    return lambda *fargs: substitute(expr, zip (args, fargs))

x, y = Ints ('x y')
expr = x + y

f = functionFromExpr([x, y], expr)

print (f (x, y))
print (f (x, IntVal(4)))
print (f (IntVal(3), IntVal(4)))

打印:

x + y
x + 4
3 + 4

请注意，您需要通过在调用站点自行适当转换表达式来显式传递表达式。如果您想避免这种情况，可以执行以下操作:

def mkExpr(a):
    if is_expr(a):
        return a
    elif isinstance(a, int):
        return IntVal(a)
    elif isinstance(a, float):
        return FPVal(a)
    else:
        raise Exception("Don't know how to convert: %s"  % a.__repr__())

def functionFromExpr(args, expr):
    return lambda *fargs: substitute(expr, zip (args, [mkExpr(e) for  e in fargs]))

x, y = Ints ('x y')
expr = x + y

f = functionFromExpr([x, y], expr)

print (f (x, y))
print (f (x, 4))
print (f (3, 4))

显然，您必须适当修改 mkExpr 以处理您可能传递的各种常量。