Подставим функцию с выражением в Z3 - PullRequest
Новая
       18

Подставим функцию с выражением в Z3

1 голос
/ 24 мая 2019

Я работаю с 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 (на что Левент дал отличный ответ), но подумав об этом, это не особенно полезно с помощью метода замены и определенно чувствует себя немного хакерским.

Любая помощь или совет будет принята с благодарностью!

1 Ответ

1 голос
/ 25 мая 2019

Это необычная вещь, но есть одно решение: 

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 для обработки всех видов констант, которые вы можете передавать.

...