Z3是否支持实时对诠释转换？(Does Z3 support Real-to-Int convers

在Z3你to_real获得Int的真实等同。 有逆转换，即一定的支撑，以截断，舍入或喜欢？ 在否定的情况下，这可能是定义它们，如果有最Z3友好的方式？ 非常感谢大家会回答。

Answer 1:

是的，Z3拥有to_int一个真正转换成整数的功能。 的语义to_int在定义SMT 2.0标准 。 下面是一个例子： http://rise4fun.com/Z3/uJ3J

(declare-fun x () Real)

(assert (= (to_int x) 2))
(assert (not (= x 2.0)))

(check-sat)
(get-model)

文章来源: Does Z3 support Real-to-Int conversions?