z3 smt2에서 정수 나누기를 사용할 때 알려지지 않음

Question

penta (n) = (n * (3n-1))/2 함수에 대한 해답을 찾고, penta (z) = penta (a) + 펜타 (b)는 모든 수의 양성 반응을 나타낸다. 정수 나누기 (div) 정의의 일부가 될 때까지 작동하지만 정의에 추가 할 때 제한 시간이 또는 알 수 없음 있습니다. 나는 8, 7, 4를 얻을 것으로 예상 할 것입니다. 내가 잘못한 것에 대해 어떤 생각을 가지고 있습니까?

(declare-const a Int) 
(declare-const b Int) 
(declare-const z Int) 

(define-fun penta ((n Int)) Int (div (* (- (* 3 n) 1) n) 2)) 

(assert (= (penta z) (+ (penta a) (penta b)) )) 
(assert (> a 1)) 
(assert (> b 1)) 
(assert (> z 1)) 

(check-sat) 
(get-model) 

나는 http://rise4fun.com/Z3 웹 사이트의 버전과 버전 4.1 (64)를 사용하고 있습니다.

Answer 1

문제는 두 개의 숫자가 아닌 인수 사이에 정수 곱셈을 사용한다는 것이 가장 큰 문제입니다. 일반적인 Diophantine 문제에 대한 의사 결정 절차가 없으므로 Z3은 최선의 노력을 수행하므로 모델 열거를 선호하지 않습니다.

정수 나누기를 사용하지 않으면 Z3에서 을 기반으로 부분 휴리스틱을 시도하여 문제를 유한 도메인 비트 벡터로 변환하여 모델을 찾습니다. 수식에 대해 구문 검사를 수행하여이 추론을 호출합니다. 구문 분석은 연산자 (div .. 2)를 사용할 때 실패합니다. 당신은 (DIV의 × 2)를 인코딩 할 수 있도록 발견은 새로운 변수를 도입하고이를 경계하여 문제 을 선택합니다 :

(declare-const penta_z Int) 
(declare-const penta_a Int) 
(declare-const penta_b Int) 
(assert (or (= (* 2 penta_z) (penta z)) (= (+ 1 (* 2 penta_z)) (penta z)))) 
(assert (or (= (* 2 penta_a) (penta a)) (= (+ 1 (* 2 penta_a)) (penta a)))) 
(assert (or (= (* 2 penta_b) (penta b)) (= (+ 1 (* 2 penta_b)) (penta b)))) 
(assert (= penta_z (+ penta_a penta_b) )) 
(assert (> a 1)) 
(assert (> b 1)) 
(assert (> z 1)) 
(assert (>= penta_z 0)) 
(assert (<= penta_z 100)) 

또한 직접이 때문에 오류가 발생하기 쉬운 점점 시작하지만 비트 벡터를 사용하여 문제를 인코딩 할 수 있습니다 오버 플로우를 처리하는 방법을 다루어야합니다.