为什么0=0.5？

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

If I do (assert (= 0 0.5))就会得到满足。但是，如果我改变顺序并执行(assert (= 0.5 0))这是不能令人满意的。

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

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

根据SMT-Lib标准，v2（http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r10​​.12.21.pdf 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 或其他一些设置，强制进行比默认情况更严格的类型检查；但我预计即使采用最宽松的实现方式也会发现这种情况。