How can I limit the decimal places a real variable can have in Z3 Theorem Prover?

Question

I will provide a simple example below to further explain the question:

from z3 import *

s = Solver()
x = Real('x')

#
# Here I would establish constraints that limit the
# nunber of decimal places x can have.
# I.E. x -> 1.2; where x can have up to 1 decimal place
#

s.add(x > 1.89, x < 1.91)

if s.check() == unsat:
    print("No solution")

print("x = %s" % str(s.model()[x]))

Here the result would be: x = 19/10.. Which converted to a float would be x = 1.9..

In this case x has 1 decimal place as there is only 1 digit after the .

So, I am wondering if there is a way to limit the variable x (in the smt solver: Z3 Theorem Prover) so that it can only have y number of decimal places.

Note that the code shown above is python code, hence, I am interacting with z3 with python.

Answer 1

I don't think you can work with reals like this, but if you multiply everything by 100, you will get integers. So you could require that x is an integer, add the constraint 198 < x < 190, and ask for a solution. If you get it, the real number you were looking for is x/100.