z3 - 为什么 0 = 0.5？

Question

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

如果我这样做 (assert (= 0 0.5))它将是令人满意的。但是，如果我切换顺序并执行 (assert (= 0.5 0))它不能满足。

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

Answer 1

我认为这是缺乏类型检查的结果； z3 太宽容了。它应该简单地拒绝这样的查询，因为它们的格式不正确。

根据 SMT-Lib 标准，v2 ( http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r10.12.21.pdf )；第 30 页；核心理论是这样定义的:

(theory Core
:sorts ((Bool 0))
:funs ((true Bool) (false Bool) (not Bool Bool)
      (=> Bool Bool Bool :right-assoc) (and Bool Bool Bool :left-assoc)
      (or Bool Bool Bool :left-assoc) (xor Bool Bool Bool :left-assoc)
      (par (A) (= A A Bool :chainable))
      (par (A) (distinct A A Bool :pairwise))
      (par (A) (ite Bool A A A))
      )
:definition
"For every expanded signature Sigma, the instance of Core with that signature
is the theory consisting of all Sigma-models in which:
  - the sort Bool denotes the set {true, false} of Boolean values;
  - for all sorts s in Sigma,
       - (= s s Bool) denotes the function that
         returns true iff its two arguments are identical;
       - (distinct s s Bool) denotes the function that
         returns true iff its two arguments are not identical;
       - (ite Bool s s) denotes the function that
         returns its second argument or its third depending on whether
         its first argument is true or not;
       - the other function symbols of Core denote the standard Boolean operators
         as expected.
       "
  :values "The set of values for the sort Bool is {true, false}."
)

因此，根据定义，相等性要求输入排序相同；因此上述查询应被拒绝为无效。

可能会切换到 z3 或其他一些强制比默认情况下更严格的类型检查的设置；但我希望即使使用最轻松的实现也会发现这种情况。