如何将Z3py与Sympy一起使用

Question

我正在尝试对矩阵进行一些符号计算，也就是说，矩阵里的元素是符号。完成这些计算后，我会得到一些可能的解。我的目标是根据一些限制条件来选择合适的解。

举个例子，M是一个矩阵，其中有一个元素是symbol（符号）。这个矩阵会有两个特征值，一个是正的，一个是负的。我想用z3这个工具找出负值，但我遇到问题，因为a被定义为一个符号，除非我把它转换成真实的数值，否则我无法把它作为限制条件来使用。

我该怎么办呢？有没有办法把a（符号）转换成真实数或整数，这样我就可以用它来作为限制条件，比如s.add(a>0)？

from sympy import* 
from z3 import* 
from math import*

a=Symbol('a')

M=Matrix([[a,2],[3,4]]) m=M.eigenvals();

s=Solver()

s.add(m<0)
print(s.check())
model = s.model() print(model)

Answer 1

一种方法是把sympy表达式转换成字符串，然后修改这些字符串使它们变成z3表达式，最后用Python的eval来计算这些z3表达式。具体步骤如下：

1. 把你的sympy表达式转换成字符串。你可以通过调用Python的str()来生成这些字符串。
2. 在每个字符串后面加上不等式或等式的符号（比如 ' > 0', ' < 0', ' >= 0 ', 或 ' <= 0'）。
3. 把字符串中所有sympy和z3不匹配的地方进行替换。例如，把所有的"sqrt"改成"z3.Sqrt"。
4. 调用Python的eval()，它可以接受这些字符串并将它们计算成z3表达式。
5. 现在你就进入了z3的世界。

下面是我写的一个函数，用来把一系列字符串从sympy表达式转换成z3的不等式系统。

import z3
import sympy

###################################
def sympy_to_z3(str_ineq_list, syms):
# converts a list of strings representing sympy expressions (inequalities)
# to a conjunction of z3 expressions in order to be processed by the solver
system_str = 'z3.And('
for str_ineq in str_ineq_list:
    system_str += str_ineq.replace('sqrt', 'z3.Sqrt') + ', '
system_str += ')'
for sym in syms:
    # this initializes the symbols (x1, x2,..) as real variables
    exec(str(sym) + ', = z3.Reals("' + str(sym) + '")')
system = eval(system_str)
return system

我并不是特别喜欢这种方法，因为它涉及到字符串的处理和动态调用eval()和exec()，如果你是动态生成系统的话，这会让计算变得相当慢，但这是我能想到的办法。

关于将字符串转换为z3表达式的更多信息：

• Z3与字符串表达式
• z3python：将字符串转换为表达式

Answer 2

一个替代 eval 和 exec 的方法是遍历 sympy 表达式，然后构建相应的 z3 表达式。下面是一些代码：

from z3 import Real, Sqrt 
from sympy.core import Mul, Expr, Add, Pow, Symbol, Number

def sympy_to_z3(sympy_var_list, sympy_exp):
    'convert a sympy expression to a z3 expression. This returns (z3_vars, z3_expression)'

    z3_vars = []
    z3_var_map = {}

    for var in sympy_var_list:
        name = var.name
        z3_var = Real(name)
        z3_var_map[name] = z3_var
        z3_vars.append(z3_var)

    result_exp = _sympy_to_z3_rec(z3_var_map, sympy_exp)

    return z3_vars, result_exp

def _sympy_to_z3_rec(var_map, e):
    'recursive call for sympy_to_z3()'

    rv = None

    if not isinstance(e, Expr):
        raise RuntimeError("Expected sympy Expr: " + repr(e))

    if isinstance(e, Symbol):
        rv = var_map.get(e.name)

        if rv == None:
            raise RuntimeError("No var was corresponds to symbol '" + str(e) + "'")

    elif isinstance(e, Number):
        rv = float(e)
    elif isinstance(e, Mul):
        rv = _sympy_to_z3_rec(var_map, e.args[0])

        for child in e.args[1:]:
            rv *= _sympy_to_z3_rec(var_map, child)
    elif isinstance(e, Add):
        rv = _sympy_to_z3_rec(var_map, e.args[0])

        for child in e.args[1:]:
            rv += _sympy_to_z3_rec(var_map, child)
    elif isinstance(e, Pow):
        term = _sympy_to_z3_rec(var_map, e.args[0])
        exponent = _sympy_to_z3_rec(var_map, e.args[1])

        if exponent == 0.5:
            # sqrt
            rv = Sqrt(term)
        else:
            rv = term**exponent

    if rv == None:
        raise RuntimeError("Type '" + str(type(e)) + "' is not yet implemented for convertion to a z3 expresion. " + \
                            "Subexpression was '" + str(e) + "'.")

    return rv

这里有一个使用这些代码的例子：

from sympy import symbols
from z3 import Solver, sat

var_list = x, y = symbols("x y")

sympy_exp = -x**2 + y + 1
z3_vars, z3_exp = sympy_to_z3(var_list, sympy_exp)

z3_x = z3_vars[0]
z3_y = z3_vars[1]

s = Solver()
s.add(z3_exp == 0) # add a constraint with converted expression
s.add(z3_y >= 0) # add an extra constraint

result = s.check()

if result == sat:
    m = s.model()

    print "SAT at x={}, y={}".format(m[z3_x], m[z3_y])
else:
    print "UNSAT"

运行这个代码会得到一个结果，解决了约束条件 y >= 0 和 -x^2 + y + 1 == 0：

SAT at x=2, y=3