如何使预定义的 Python 函数与 Z3py 一起使用？

Question

作为 Z3 的初学者，我想知道是否有办法让 Z3Py 使用预定义的 Python 函数。以下是一个解释我的问题的小例子。

from z3 import *

def f(x):
    if x > 0:
        print " > 0"
        return 1
    else:
        print " <= 0"
        return 0

a=Int('a')
s=Solver()
s.insert(f(a) == 0)

t = s.check()
print t
print a
m = s.model()
print m

f(x) 是在 python 中定义的函数。当 x s.insert(f(a) == 0) 并希望 Z3 可以为变量“a”找到合适的值（例如 -3）。但是这些代码不能正常工作。应该怎么改？

（请注意我需要在Z3之外定义f(x)，然后被Z3调用。）

我要做的是调用图形库提供的预定义函数而不将其转换为 Z3。我正在使用 NetworkX 库，一些代码如下：

import networkx as nx

G1=nx.Graph()
G1.add_edge(0,1)

G2=nx.Graph()
G2.add_edge(0,1)
G2.add_edge(1,2)

print(nx.is_isomorphic(G1, G2))
#False

我需要 Z3 来帮助我在 G2 中找到一个顶点，这样在删除该顶点后，G2 与 G1 同构。例如

G2.remove_node(0)
print(nx.is_isomorphic(G1, G2))
#True

Answer 1

我认为如果f 是一个通用函数（例如，如果它是递归的怎么办？），这将是困难的，尽管如果您假设它具有某种结构（例如，if then else），您也许可以编写一个简单的翻译器。问题在于 Z3 的函数本质上是数学函数，并不直接等同于 Python 函数（请参阅 http://en.wikipedia.org/wiki/Uninterpreted_function ）。如果可能出于您的目的，我建议采取相反的方向：根据 Z3 构造定义您的函数f，然后在您的程序中对其进行评估（例如，使用此方法：Z3/Python getting python values from model）。如果这对您不起作用，请提供一些有关如何使用该功能的其他详细信息。这是一个最小的例子（rise4fun 链接：http://rise4fun.com/Z3Py/pslw）：

def f(x):
    return If(x > 0, 1, 0)

a=Int('a')
s=Solver()
P = (f(a) == 0)
s.add(P)

t = s.check()
print t
print a
m = s.model()
print m

res = simplify(f(m[a])) # evaluate f at the assignment to a found by Z3

print "is_int_value(res):", is_int_value(res)

print res.as_long() == 0 # Python 0

print f(1)
print simplify(f(1)) # Z3 value of 1, need to convert as above