(get-unsat-core) возвращает пустой в Z3

Question

Я использую Z3, чтобы извлечь ядро ​​из неудовлетворительной формулы. Я использую интерфейс Z3@Rise (веб-интерфейс), чтобы написать следующий код,

(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 корректно возвращает "unsat", но (get-unsat-core) возвращает пустое. Я пропускаю некоторые настройки / опции? Или я сделал пример сложным?

Answer 1

Вам нужно добавить метки имен в свои утверждения, чтобы get-unsat-core имел метки для использования в выводе ядра unsat. Напишите свои утверждения так:

(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 (файл PDF).