Does Z3 support Real-to-Int conversions?

问题:

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.

回答1:

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)