(get-unsat-core) Z3

Question

में खाली लौटाता है मैं एक असंतुष्ट सूत्र के असंतुलित कोर को निकालने के लिए Z3 का उपयोग कर रहा हूं। मैं जेड 3 उपयोग कर रहा हूँ @ वृद्धि इंटरफेस (वेब ​​आधारित) निम्नलिखित कोड लिखने के लिए,

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

जांच शनिवार को सही ढंग से वापस आती है 'unsat' लेकिन (मिल-unsat कोर) खाली देता है। क्या मुझे कुछ विन्यास/विकल्प याद आ रहा है? या मैंने उदाहरण जटिल बना दिया है?

Answer 1

आपको अपने दावों में नाम लेबल जोड़ने की आवश्यकता है ताकि असुरक्षित कोर में असतत कोर आउटपुट में लेबल का उपयोग किया जा सके। इस तरह के अपने दावे लिखें:

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

और get-unsat-core एक असुरक्षित कोर मुद्रित करेगा।

इस वाक्यविन्यास के लिए दस्तावेज़ीकरण SMTLIB tutorial (पीडीएफ फाइल) में पाया जा सकता है।