z3 - Z3 是否支持 Real-to-Int 转换？

Question

在 Z3 中，您必须 to_real 才能获得 Int 的 Real 等价物。是否支持逆转换，即截断、舍入等？在否定的情况下，如果有的话，最适合 Z3 的定义它们的方式是什么？非常感谢大家会回答。

Answer 1

是的，Z3 有一个to_int将 Real 转换为整数的函数。的语义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)