Z3 支持实数到整数的转换吗？

Question

在 Z3 中，您必须 to_real 才能获得 Int 的 Real 等价物。是否有一些对逆转换的支持，即截断、舍入或类似转换？在消极的情况下，Z3 最友好的定义方式是什么（如果有的话）？非常感谢大家的解答。

Answer 1

是的，Z3 有一个to_int将实数转换为整数的函数。的语义在SMT 2.0 标准to_int中定义。这是一个例子： http: //rise4fun.com/Z3/uJ3J

(declare-fun x () Real)

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

(check-sat)
(get-model)