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.
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.)