I would like to create a constraint that makes sure that a Real value is quantized to some tick value.
TICK = 0.5
x = Real('x')
solve(x % TICK == 0)
Unfortunately, this does not work with Real numbers (it works with Int and FP). Another solution that I thought of was to create a set of valid numbers and check whether the number is part of the set, however the set would need to be really big.
Is there any other solution?
As Christoph mentioned, computing the modulus of a real-number isn't really meaningful. But your question is still valid: You're asking if x is an integer multiple of TICK. You can do this as follows:
from z3 import *
TICK = 0.5
x = Real('x')
k = Int('k')
solve(x == 1, ToReal(k) * TICK == x)
solve(x == 1.2, ToReal(k) * TICK == x)
This prints:
[k = 2, x = 1]
no solution
Note that unless x is a constant, this'll lead to a mixed integer-real arithmetic, and it might give rise to non-linear constraints. This can make it hard for the solver to answer your query, i.e., it can return unknown or take too long to respond. It all depends on what other constraints you have on x.