Z3py: received error while parsing small real numbers

Question

I am trying to integrate z3py into my application. Statements exist that include small real numbers, such as

solver.add(x <= 1e-6) 

Then I got the following error:

 File "~/src/solver/z3.py", line 2001, in __le__ a, b = _coerce_exprs(self, other) File "~/src/solver/z3.py", line 846, in _coerce_exprs b = s.cast(b) File "~/src/solver/z3.py", line 1742, in cast return RealVal(val, self.ctx) File "~/src/solver/z3.py", line 2526, in RealVal return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx) File "~/src/solver/z3core.py", line 1774, in Z3_mk_numeral raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err)) src.solver.z3types.Z3Exception: 'parser error' 

Bye statement

 solver.add(x <= 1e-4) 

seems beautiful.

Therefore, I assume that in z3 there is some kind of limitation of accuracy. If so, is it possible to resolve the first statement?

Thanks.

Answer 1

There is no precision limitation in Z3. It can represent arbitrary precision rational numbers and algebraic numbers. Here is an example:

 print RealVal('1/10000000000000000000000000000') print simplify((RealVal('1/10') ** RealVal('10')) ** RealVal('10')) 

You can try it online at: http://rise4fun.com/Z3Py/ahJQ

The RealVal(a) function RealVal(a) Python value to a real Z3 value. To do this, use the API Z3 C Z3_mk_numeral . This code is available in the z3.py file included with the Z3 distribution. The Z3_mk_numeral API expects a string that encodes a rational number in decimal format (for example, "1.3") or fractional format (for example, "1/3"). Please note that scientific notation is not supported. To make RealVal(a) convenient for python users, we use the str(a) method to convert a to a string before calling Z3_mk_numeral . Thus, users can also write RealVal(1) , RealVal(1.2) , etc.

The second bit of information is that the operator solver.add(x <= 1e-4) is essentially a short hand for solver.add(x <= RealVal(1e-4)) .

Now we may ask why the example works for 1e-4 , but not for 1e-6 . The problem is implementing str in Python. str(1e-4) returns the string "0.0001" in decimal notation, which is supported by Z3 Z3_mk_numeral , but str(1e-6) returns the string "1e-6" in scientific notation, which is not supported by Z3_mk_numeral .

 print str(1e-4) print str(1e-6) 

Here is the link to the example above: http://rise4fun.com/Z3Py/C02q

To avoid this problem, we must avoid numbers in scientific notation when creating Z3 expressions. I will see if I have time to add support for scientific notation in Z3_mk_numeral for the next version of Z3.