[Python] Most Precise way to approximate e^x using z3

I'm working on formal verification problems pertaining to transcendental functions like e^x. I am trying to secure either exact arithmetic or symbolic reasoning throughout the code. So far this is what my code looks like:

from z3 import *
import gmpy2

gmpy2.get_context().precision = 100

def prec_exp(x):
frac = x.as_fraction()
return RealVal(str(gmpy2.exp(gmpy2.mpfr(frac.numerator) / gmpy2.mpfr(frac.denominator))))

# Example Usage
x = RealVal(-0.254)
e_x = prec_exp(x)
print(f"e^x: {e_x}")


And this code outputs

e^x: 9696147525580950428294296600753/12500000000000000000000000000000


For purposes of formal verification, I was told that this isn't precise enough and was wondering if there was a better way to represent e^x in z3. My goal is to define a line from points (0,0) to (x,e^x) to use in my solver.

Continue reading...