pythondreal

Converting type() of a symbolic variable that is compatible with another toolbox in Python

For my assignment, I use two SMT solvers, z3 and dReal. While I do computations in z3 by introducing variables as symbolic variables (sympy), However, dReal requires its own custom variable type called "dreal._dreal_py.Variable".

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

The result is

dreal._dreal_py.Variable

I have a really long SymPy expression that has trigonometric terms involving multiple variables, for example:

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)

Output: sympy.core.add.Add

I have to add this as a condition to dReal solver.

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

However, since dReal does not accept symbolic variable type, it gives the following error:

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

I need to know how to convert one arbitrary symbolic data type into any other so that I can use the long expression directly as an input to my solver. If there isn't, what is the possible fix to my problem?

Thanks in advance

Solution

  • As a workaround, try evaluating strings as code:

    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)

    Note three things here: