잘못된 결과 from z3

Z3 SMT Solver를 사용하여 다음을 증명하려고합니다 : ((x*x) + x) = ((~x * ~x) + ~x). C 프로그래밍 언어의 오버플로 의미 때문에 올바릅니다. Z3에서잘못된 결과 from z3

(declare-fun a() Int) 

(define-fun myadd ((x Int) (y Int)) Int (mod (+ x y) 4294967296)) 
(define-fun mynot ((x Int))   Int (- 4294967295 (mod x 4294967296))) 
(define-fun mymul ((x Int) (y Int)) Int (mod (* x y) 4294967296)) 

(define-fun myfun1 ((x Int)) Int (myadd (mynot x) (mymul (mynot x) (mynot x)))) 
(define-fun myfun2 ((x Int)) Int (myadd x (mymul x x))) 

(simplify (myfun1 0)) 
(simplify (myfun2 0)) 

(assert (= (myfun1 a) (myfun2 a))) 
(check-sat) 
(exit)

출력은 다음과 같습니다 :

는 이제 다음과 같은 SMT-LIB 코드를 작성했습니다

0 
0 
unsat

이제 내 질문 : 왜 결과가 "unsat"인가? 내 코드의 simplify 명령은 myfun1과 myfun2가 동일한 결과를 갖도록 유효한 할당을 얻을 수 있음을 보여줍니다.

내 코드에 문제가 있거나 z3의 버그입니까?

제발 누구든지 나를 도울 수 있습니다. Thx

출처

2012-01-25 Thomas

C와 유사한 정수로 작업한다면 수동 인코딩의 연습이 아니라면 수학 정수가 아닌 비트 벡터를 사용하는 것이 좋습니다. – Philippe

빠른 설명 :이 잘못된 결과는 Z3 수식 전처리 기의 버그 때문입니다. 이 문제는 수정되어 다음 릴리스에서 사용할 수 있습니다. 이 버그는'(mod (+ a b))'또는'(mod (* a b)) '형식의 수식을 사용하는 벤치 마크에 영향을줍니다. –

@GManNickG : 좋은 지적입니다. –

잘못된 결과는 Z3 수식/식 전 처리기 버그로 인한 것입니다. 이 버그는 수정되었으며 현재 릴리스 (v4.3.1)의 일부입니다. 이 버그는 (mod (+ a b)) 또는 (mod (* a b)) 형식의 수식을 사용하는 벤치 마크에 영향을주었습니다.

예제 온라인 here을 다시 시도하고 예상되는 결과를 얻을 수 있습니다.

출처

2013-02-02 13:36:37

잘못된 결과 from z3

답변

관련 문제