z3python: using math library

Question

I was trying to use python's math library with z3python, what I did was

import z3
import math
a,b = z3.Reals('a b')
solve(b == math.factorial(a), b == 6)

The error message it returns is AttributeError: ArithRef instance has no attribute 'float'.

My purpose is not really using the factorial function in Z3, rather I am curious if the functions from the math library can be used with Z3 in general. Any suggestion is appreciated.

Answer 1

In general, no, this is not possible. The reason is that there is no translation for Python functions to logical constraints (which in theory could be done, e.g., via the fixed-point engine), but it would require substantial effort and essentially an encoding of (in general undecidable) model-checking problems. See also Leo's excellent answer to a related question here).

In this particular example, note that a is symbolic, i.e., it represents any possible real number. math.factorial does not know what to do with this information, because it's implementation only handles concrete real numbers.

For some particular functions, it may of course be possible to provide a precise encoding to Z3. For example, Z3 supports exponentiation and the Python API provides a __pow__ operator. Note that this operator however, may not have exactly the same semantics as Python's __pow__ on (floating-point abstractions of) real numbers, and it is not derived from Python's implementation of __pow__.