整数除法给出不正确的结果

Question

我尝试检查x div y == 2 和x / y == 2 的可满足性，但两次都得到了不正确的结果。貌似 Z3 还不支持这些？

(declare-fun x () Int)
(declare-fun y () Int)

(assert (=  (div x y ) 2))

(check-sat)
(get-model)
(exit)

sat
(model 
  (define-fun y () Int
    0)
  (define-fun x () Int
    38)
)



(declare-fun x () Int)
(declare-fun y () Int)

(assert (=  (/ x y ) 2))

(check-sat)
(get-model)
(exit)

sat
(model 
  (define-fun y () Int
    0)
  (define-fun x () Int
    1)
)

Answer 1

支持整数除法，见：http://smtlib.cs.uiowa.edu/theories/Ints.smt2

还支持真正的除法（来自这里：http://smtlib.cs.uiowa.edu/theories/Reals.smt2），您提到的除零问题已涵盖： “由于在 SMT-LIB 逻辑中所有函数符号都被解释为总函数，因此 (/t 0) 形式的术语在 Reals 的每个实例中都是有意义的。但是，声明对其值没有施加任何限制. 这尤其意味着 - 对于每个实例理论 T 和 - 对于每一个实数类型的封闭项 t1 和 t2， 有一个 T 的模型满足 (= t1 (/t2 0))。”

您应该添加一个除数不等于零的断言。

(assert (not (= y 0)))

这是示例（rise4fun 链接：http://rise4fun.com/Z3/IUDE）：

(declare-fun x () Int)
(declare-fun y () Int)

(assert (not (= y 0)))

(push)
(assert (=  (div x y ) 2))
(check-sat)
(get-model) ; gives x = 2, y = 1
(pop)

(push)
(assert (=  (/ x y ) 2))
(check-sat)
(get-model) ; gives x = -2, y = -1
(pop)