Does Z3 support Real-to-Int conversions?
z3
Solution
Yes, Z3 has a `to_int` function that converts a Real into an integer. The semantics of `to_int` is defined in the SMT 2.0 standard. Here is an example: http://rise4fun.com/Z3/uJ3J
(declare-fun x () Real)
(assert (= (to_int x) 2))
(assert (not (= x 2.0)))
(check-sat)
(get-model)
Problem
In Z3 you have to_real to obtain the Real equivalent of an Int. Is there some support to the inverse conversions, i.e., to truncation, rounding or like? In the negative case, what could be the most Z3-friendly way of defining them, if any? Many thanks to everyone will answer.