Z3 是否支持 Real-to-Int 转换? [英] Does Z3 support Real-to-Int conversions?

问题描述

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

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.

推荐答案

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

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)

这篇关于Z3 是否支持 Real-to-Int 转换?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！