z3求解器使用Sympy符号

Question

我试图使用Z3来确定表达式是否可满足。我已经创建了所有的方程，我想使用SymPy作为约束，变量是符号。例如

"f1==(x -y >= 0 )"
"f2 == (x_y >= 1)"
"f3 == f1 -f2> =0"

我希望解算器返回x,y,f1,f2,f3的正确值，使方程可满足…

s = z3.Solver()
for m,n in zip((allvariables[3:len(allvariables)-1]),allequations):
print('variable',m)
print('equations',n)
s.add(m==(n))

print('solver check', s.check())
while s.check() == sat:
print(s)

Answer 1

一般情况下，不能混合匹配z3和Sympy符号。他们生活在不同的世界，不能轻易交换。

实际上，您必须解析SymPy表达式，并根据z3对其进行重构。这可以通过多种方式实现，但这不是一件便宜/容易的事情，因为您需要分析大量的SymPy代码。然而，如果你的表达式是"简单的"足够了，也许你可以用一个简单的翻译。首先看看如何将SymPy表达式转换为解析树。这是一个很好的起点:https://docs.sympy.org/latest/tutorials/intro-tutorial/manipulation.html