2

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.

1
  • I think you will have to wrap it in class like the car class example
    – 0x90
    Mar 28, 2014 at 20:08

1 Answer 1

2

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

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.