为什么 Z3 中的运算符 '/' 和 'div' 给出不同的结果? [英] Why operators '/' and 'div' in Z3 give different results?

问题描述

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

I was trying to represent a real number with two integer numbers as using them as the numerator and the denominator of the real number. I wrote the following program:

(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结果如下:

The program returned SAT result as follows:

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 不返回相同的结果?

However, if I write '(assert (= f (div a b)))' instead of '(assert (= f (/ a b)))', then the result is UNSAT. Why does not div return the same result?

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

Moreover, and the main concern for me, I did not find a way to use operator '/' in z3 .Net API. I can see only function MkDiv, which actually for operator 'div'. Is there a way so that I can apply operator '/' in the case of z3 .Net API? Thank you in advance.

推荐答案

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

Strictly speaking neither of these formulas is SMT-LIB2 compliant, because / is a function that takes two Real inputs and produces a Real output, whereas div is a function that takes two Int inputs and produces an Int (see SMT-LIB Theories). Z3 is more relaxed and automatically converts those objects. If we enable the option smtlib2_compliant=true then it will indeed report an error in both cases.

div 版本不满意的原因是确实没有解f根据(= f(/ab))为整数，但确实没有满足(= f 0.5)

The reason for the div version being unsatisfiable is that there is indeed no solution where f is an integer according to (= f (/ a b)), but there is indeed no integer that satisfies (= f 0.5)

这篇关于为什么 Z3 中的运算符 '/' 和 'div' 给出不同的结果?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！