如何一起使用Z3py和Sympy

Question

我试图在矩阵上执行一些符号计算(用符号作为矩阵的条目),之后我会有一些可能的解决方案.我的目标是根据约束选择解决方案/解决方案.

例如,M是一个矩阵,其中一个元素作为symbol.该矩阵将具有2个特征值,一个是正的,一个是负的.使用z3我试图找出唯一的负值,但我无法这样做,因为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() 从 sympy 表达式生成字符串。
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：将字符串转换为表达式