1

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

Acad
  • 161
  • 5

1 Answers1

1

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:

  • I couldn't install dReal on my PC so I was not able to test this code
  • It's really important, how You import the packages. The functions sin and cos are contained in both packages, but this is not for all functions guaranteed. Also some sympy functions might print differently, than dReal expects, but this could bre remedied via something like from dreal import my_func as myFunc
  • Be very careful with variable names
AlexNe
  • 926
  • 6
  • 22