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

Question

在我的任务中，我使用了两个SMT解算器，z3和dReal。虽然我在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包含在两个包中，但这并不是所有函数都有保证的。另外，一些同情函数的打印方式可能与dReal预期的不同，但这可以通过诸如from dreal import my_func as myFunc
• 之类的方法进行补救，对于变量名称

要非常小心。