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

Question

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

(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 的情况下应用运算符“/”？预先感谢您。

Answer 1

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

div版本无法满足的原因是，根据(= f (/a b))，确实没有f为整数的解，但确实没有满足(= f 0.5)

的整数