python - 转换与 Python 中的另一个工具箱兼容的符号变量的 type()

Question

对于我的作业，我使用两个 SMT 求解器:z3 和 dReal。虽然我通过引入变量作为符号变量 (sympy) 在 z3 中进行计算，但是 dReal 需要自己的自定义变量类型，称为“dreal._dreal_py.Variable”。

from dreal import * 
s=Variable('x')
type(s)

结果是

dreal._dreal_py.Variable

我有一个非常长的 SymPy 表达式，其中包含涉及多个变量的三角项，例如:

from sympy import *
x=symbols('x')
y=symbols('y')
z=symbols('z') 
P=sin(x-y)+x**2+y**3+sin(y-z) 
type(P)

输出: sympy.core.add.Add

我必须将其作为条件添加到 dReal 求解器。

cond=And(x < 3, 4 < x, y < 3, 4 < y, 0 < z, 0 < P)

但是，由于 dReal 不接受符号变量类型，因此会出现以下错误:

unsupported operand type(s) for -: 'Add' and 'dreal._dreal_py.Expression'

我需要知道如何将一种任意符号数据类型转换为任何其他符号数据类型，以便我可以直接使用长表达式作为求解器的输入。如果没有，我的问题可能的解决办法是什么？

提前致谢

Answer 1

作为解决方法，请尝试将字符串作为代码进行评估:

import sympy as sy  #don't import any functions, that could cover up dreal's
from dreal import * #need to import everything from dreal

s_x=sy.symbols('x')
s_y=sy.symbols('y')
s_z=sy.symbols('z') 
P=sy.sin(s_x-s_y)+s_x**2+s_y**3+sy.sin(s_y-s_z)

x = Variable('x')
y = Variable('y')
z = Variable('z')

#Here, the magic happens
reP = eval(str(P))

cond=And(x < 3, 4 < x, y < 3, 4 < y, 0 < z, 0 < reP)

这里请注意三件事:

• 我无法在我的电脑上安装 dReal，因此无法测试此代码
• 如何导入包非常重要。函数 sin 和 cos 均包含在两个包中，但这并不保证适用于所有函数。另外，一些 sympy 函数的打印结果可能与 dReal 预期的不同，但这可以通过 from dreal import my_func as myFunc
• 对变量名称要非常小心