整数除法给出不正确的结果 [英] integer division gives incorrect result

问题描述

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

I try to check satisfiability of x div y == 2 and x / y == 2 but got incorrect results both times. Looks like Z3 doesn't support these yet ?

(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)
)

推荐答案

支持整数除法，参见: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))."

Real division is also supported (from here: http://smtlib.cs.uiowa.edu/theories/Reals.smt2), the issue with division by zero you mention is covered: "Since in SMT-LIB logic all function symbols are interpreted as total functions, terms of the form (/ t 0) are meaningful in every instance of Reals. However, the declaration imposes no constraints on their value. This means in particular that - for every instance theory T and - for every closed terms t1 and t2 of sort Real, there is a model of T that satisfies (= t1 (/ t2 0))."

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

You should add an assertion that the divisor is not equal to zero.

(assert (not (= y 0)))

示例如下(rise4fun 链接:http://rise4fun.com/Z3/IUDE):

Here's the example (rise4fun link: 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)

这篇关于整数除法给出不正确的结果的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！