如何一起使用 Z3py 和 Sympy [英] How to use Z3py and Sympy together

问题描述

我正在尝试对矩阵执行一些符号计算(使用符号作为矩阵的条目)，然后我将有许多可能的解决方案.我的目标是根据约束选择解决方案/解决方案.

I am trying to perform some symbolic calculation on matrices (with symbols as an entries of matrices), and after that I will have a number of possible solution. My goal is to select solutions/ solution based upon constraints.

例如，M是一个矩阵，它有一个元素作为symbol.该矩阵将有 2 个特征值，一个为正，一个为负.使用 z3 我试图仅找出负值，但我无法这样做，因为 a 被定义为一个符号，除非我将其转换为实数，否则我无法将其写为约束.

for example, M is a matrix which have one element as a symbol. This matrix will have 2 eigenvalues one is positive an one is negative. Using z3 I am trying to find out only negative value, but I am unable to do so as a is defined as a symbol and I cannot write it as a constraint unless I convert it to a real value.

我该怎么办?有什么方法可以将(符号)转换为实数或整数，以便我可以将其用作约束 s.add(a>0)

what should I do? is there any way to convert a (symbol) in to real or integer so that I can use it as a constraint 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 表达式.这是一些代码:

An alternative to eval and exec is to walk the sympy expression and construct the corresponding z3 expression. Here's some code:

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 的输出:

Running this produces the output that solves the constraints y >= 0 and -x^2 + y + 1 == 0:

SAT at x=2, y=3

这篇关于如何一起使用 Z3py 和 Sympy的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！