0

I'm using SymPy expressions to compute expressions such as a + 3 * b that then I want to verify with Z3 (for example, a + 3 * b > 0 for all positive a, b).

I can't find a way to replace a, b and in general SymPy symbols with Z3 objects.

import sympy
from z3 import *

a = sympy.Symbol('a')
b = sympy.Symbol('b')

t = Real('t')
w = Real('w')

e = a + 3 * b
e = e.subs({a:t, b:w})  # does nothing?
e = e.replace(a, t).replace(b, w)  # e = t + 3 * w

And(True, e > 0)  # raises z3.z3types.Z3Exception

The exception is thrown also by replacing 3 with RealVal('3').

I'm currently operating on strings and finally using exec to change types and expressions as above, but I'm planning to stop using exec.

yokke
  • 99
  • 7

1 Answers1

1

You cannot mix and match sympy expressions with z3py expressions. They are different internal data-structures. However, you can walk through the sympy expression and create a corresponding z3 expression, but it has to be done separately. Note that the call to subs is doing a substitution in the sympy world: The substitution is happening, but the resulting expression is still a sympy expression. (And most likely an illegal one: if you actually do try to use any sympy functions on it, you'll most likely get a similar exception from sympy itself.)

You need to develop a function that takes a sympy expression and gives you a z3py expression.

As far as I know there is no "official" function to do this, but see this (somewhat dated) answer for details: How to use Z3py and Sympy together You might be able to use the code from there to serve your purposes. (A rough guess: Doing a full converter from sympy to z3py might very well be impossible due to the richness of sympy and the inevitable mismatches, but you can most likely get a converter that handles your use cases.)

alias
  • 28,120
  • 2
  • 23
  • 40