为什么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或其他一些设置,强制进行比默认更严格的类型检查; 但我希望即使是最放松的实现,也能抓住这个案例.

Answer 2

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

(set-option :smtlib2-compliant true) 

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