为什么 Z3 中的运算符 '/' 和 'div' 给出不同的结果？答案

【问题标题】：Why operators '/' and 'div' in Z3 give different results?为什么 Z3 中的运算符 '/' 和 'div' 给出不同的结果？
【发布时间】：2014-09-24 22:30:45
【问题描述】：

我试图用两个整数表示一个实数，将它们用作实数的分子和分母。我写了以下程序：

(declare-const a Int)
(declare-const b Int)
(declare-const f Real)

(assert (= f (/ a b)))
(assert (= f 0.5))
(assert (> b 2))
(assert (> b a))

(check-sat)
(get-model)

程序返回SAT结果如下：

sat
(model 
  (define-fun f () Real
    (/ 1.0 2.0))
  (define-fun b () Int
    4)
  (define-fun a () Int
    2)
)

但是，如果我写 '(assert (= f (div a b)))' 而不是 '(assert (= f (/ a b)))'，那么结果是 UNSAT。为什么 div 不返回相同的结果？

此外，我最关心的是，我没有找到在 z3 .Net API 中使用运算符“/”的方法。我只能看到函数 MkDiv，它实际上是用于操作员 'div' 的。有没有办法让我可以在 z3 .Net API 的情况下应用运算符'/'？提前谢谢你。

【问题讨论】：

标签： z3

【解决方案1】：

严格来说，这些公式都不符合 SMT-LIB2，因为 / 是一个接受两个 Real 输入并产生一个 Real 输出的函数，而 div 是一个接受两个 Int 输入并产生一个 Int (见SMT-LIB Theories)。 Z3 更轻松，并自动转换这些对象。如果我们启用选项smtlib2_compliant=true，那么它确实会在两种情况下都报错。

div版本不能满足的原因是f根据@987654327@的整数确实没有解，但是确实没有整数满足(= f 0.5)

【讨论】：