我正在尝试对矩阵执行一些符号计算（将符号作为矩阵的条目），之后我将有一些可能的解决方案。我的目标是根据约束选择解决方案/解决方案。
例如，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)
【问题讨论】：
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
【讨论】：
一种可能性是将 sympy 表达式转换为 stings，修改它们以表示 z3 表达式，然后调用 python 的 eval 将它们评估为 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 表达式的方法：
【讨论】：