为什么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) 
) 

不过，如果我写 '（断言（= F（DIV AB）））' 而不是“（ assert（= f（/ ab）））'，那么结果是UNSAT。为什么div不会返回相同的结果？另外，对于我来说主要关心的是，我没有找到在z3 .Net API中使用运算符'/'的方法。我只能看到函数MkDiv，它实际上是运算符'div'。有没有办法让我可以在z3 .Net API的情况下应用运算符'/'？先谢谢你。

Answer 1

严格地说既不这些公式是SMT-LIB2柔顺的，因为/是一个函数，它有两个实输入，并产生一个真正的输出，而div是一个函数，它两个int输入，并产生一个Int（见SMT-LIB Theories） 。 Z3更放松并自动转换这些对象。如果我们启用选项smtlib2_compliant=true那么它确实会在两种情况下报告错误。

的原因div版本为不可满足的是，有确实没有解决方案，其中f是根据(= f (/ a b))的整数，但确实没有整数，其满足(= f 0.5)