(get-unsat-core) zwraca pustą wartość w Z3

Question

Używam Z3, aby wyodrębnić rdzeń niezadowalającej formuły. Używam Z3 @ Rise interfejsu (Web Based) napisać następujący kod,

(set-logic QF_LIA) 
(set-option :produce-unsat-cores true) 

(declare-fun ph1() Int) 
(declare-fun ph1p() Int) 
(declare-fun ph3() Int) 
(declare-fun ph3p() Int) 
(declare-fun ph4() Int) 
(declare-fun ph4p() Int) 

(define-fun one() Bool (= ph3p (+ ph1 1))) 
(define-fun two() Bool (= ph3 (+ ph1 1))) 
(define-fun three() Bool (= ph1p (+ ph1 1))) 
(define-fun four() Bool (= ph4p (+ ph1p 1))) 
(define-fun five() Bool (>= ph1 0)) 
(define-fun six() Bool (>= ph4 0)) 

(define-fun secondpartA() Bool (or (= ph4 0) (<= ph3 ph4))) 
(define-fun secondpartB() Bool (or (= ph3p 0) (<= ph4p ph3p))) 


(assert one) 
(assert two) 
(assert three) 
(assert four) 
(assert five) 
(assert six) 
(assert secondpartA) 
(assert secondpartB) 
(check-sat) 
(get-unsat-core) 

check-sat poprawnie zwraca 'unsat' ale (get-unsat-core) zwraca pusty. Czy brakuje mi jakiejś konfiguracji/opcji? A może skomplikowałem przykład?

Answer 1

Musisz dodać etykiety nazw do swoich zapewnień, więc get-unsat-core ma etykiety do użycia w niezamaskowanych wyjściach rdzenia. Napisz swoje twierdzenia w ten sposób:

(assert (! one :named a1)) 
(assert (! two :named a2)) 
(assert (! three :named a3)) 
(assert (! four :named a4)) 
(assert (! five :named a5)) 
(assert (! six :named a6)) 
(assert (! secondpartA :named spA)) 
(assert (! secondpartB :named spB)) 

oraz get-unsat-core wydrukuje niezatwierdzony rdzeń.

Dokumentacja dla tej składni znajduje się w SMTLIB tutorial (plik PDF).