Does Z3 support Real-to-Int conversions?

Question

In Z3, you need to_real to get the real equivalent of Int. Is there any support for inverse transforms i.e. Truncation, rounding or the like? In the negative case, what could be the most Z3-convenient way to determine them, if any? Many thanks to everyone who answers.

Answer 1

Yes, Z3 has a to_int function that converts Real to an integer. The semantics of to_int 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)