首页 文章

整数除法给出错误的结果

提问于
浏览 次
0

我尝试检查 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)
)
z3

1 回答

  • 1

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

    还支持真正的除法（从这里：http://smtlib.cs.uiowa.edu/theories/Reals.smt2），你提到的除零问题包括：“因为在SMT-LIB逻辑中，所有函数符号都被解释为总函数，所以形式（/ t 0）的术语是有意义的在Reals的每个实例中 . 但是，声明对它们的值没有任何限制 . 这尤其意味着 - 对于每个实例理论T和 - 对于排序Real的每个闭合项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)
    回复于

相关问题