为什么 0 = 0.5? [英] Why does 0 = 0.5?

问题描述

在处理 .smt2 文件时，我注意到 Z3 4.3.1 的一些奇怪行为.

I noticed some strange behavior with Z3 4.3.1 when working with .smt2 files.

如果我这样做 (assert (= 0 0.5)) 它将是可满足的.但是，如果我切换顺序并执行 (assert (= 0.5 0)) 则无法满足.

If I do (assert (= 0 0.5)) it will be satisfiable. However, if I switch the order and do (assert (= 0.5 0)) it's not satisfiable.

我对发生的事情的猜测是，如果第一个参数是一个整数，它会将它们都转换为整数(将 0.5 向下舍入为 0)，然后进行比较.如果我将0"更改为0.0"，它会按预期工作.这与我使用过的大多数编程语言形成对比，如果其中一个参数是浮点数，则它们都被转换为浮点数并进行比较.这真的是 Z3 中的预期行为吗?

My guess as to what is happening is that if the first parameter is an integer, it casts both of them to integers (rounding 0.5 down to 0), then does the comparison. If I change "0" to "0.0" it works as expected. This is in contrast to most programming languages I've worked with where if either of the parameters is a floating-point number, they are both cast to floating-point numbers and compared. Is this really the expected behavior in Z3?

推荐答案

严格来说，Z3 默认不符合 SMT 2.0，这就是其中一种情况.我们可以添加

Strictly speaking, Z3 is not SMT 2.0 compliant by default, and this is one of those cases. We can add

(set-option :smtlib2-compliant true) 

然后这个查询确实被正确拒绝了.

and then this query is indeed rejected correctly.

这篇关于为什么 0 = 0.5?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！