Z3에서 나누기위한 버그입니까?

Question

나는 다음과 같은 두 가지 스크립트 rise4fun에 시도 :

스크립트 (1) :

(declare-const a Int) 
(declare-const b Int) 
(assert (= 1 (/ a b))) ; division 
(check-sat) 
(get-model) 

스크립트 (2) :

(declare-const a Int) 
(declare-const b Int) 
(assert (= 1 (rem a b))) ; remainder 
(check-sat) 
(get-model) 

Z3는 (나에게 준 = 0, B = 0)을 (1)과 (a = 38, b = 0)의 모델로 사용하고 있습니다. 이 솔루션은 Z3에 몇 가지 버그를 나타 냅니까? 감사!

Answer 1

이것은 버그가 아니며 함수가 SMT 및 Z3에서 수학적으로 정의되는 방식 때문입니다. 문제는 분모가 0이 아니라는 주장이 없기 때문에 두 경우 모두 0으로 나누는 것입니다. b이 0이 아닌 제약 조건을 추가하면 예상 결과가 더 높아집니다. 여기에 더 많은 기대 결과 (: http://rise4fun.com/Z3/Xokpp rise4fun 링크) :주는 업데이트 된 예는

(declare-const a Int) 
(declare-const b Int) 
(assert (= 1 (/ a b))) ; 
(check-sat) 
(get-model) ; gives a = 0, b = 0 

(assert (not (= b 0))) 
(check-sat) 
(get-model) ; gives a = -1, b = -1 

그리고 (rise4fun 링크 : http://rise4fun.com/Z3/x5Is) : 자세한 내용은

(declare-const a Int) 
(declare-const b Int) 
(assert (= 1 (rem a b))) 
(check-sat) 
(get-model) ; gives b = 0, a = 38 

(assert (not (= b 0))) 
(check-sat) 
(get-model) ; gives b = 2, a = 1 

,이 질문과 대답을 참조 (그것은 실수에 대한 자세한 내용을 이야기하지만, 상황은 정수 비슷하고, 정수 이론 부문이 실제 이론적으로 처리하는 방법을 말한다) :

integer division gives incorrect result