Метка на утверждениях SMT-LIB 2.0 в Z3

Question

Не могли бы вы сказать мне, как назвать утверждения в эталоне Z3 SMT-LIB 2.0? Я бы предпочел использовать стандартный синтаксис SMT-LIB, но, как кажется, Z3 не понимает, я просто ищу одного, работающего с Z3. Необходимость состоит в том, чтобы получить невысокие ядра с этикетками.

Вот пример теста, который я проверил:

(set-option enable-cores)
(set-logic AUFLIA)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (! (<= 0 x) :named hyp1))
(assert (! (<= 0 y) :named hyp2))
(assert (! (<= 0 z) :named hyp3))
(assert (! (< x y) :named hyp4))
(assert (! (and (<= 0 y) (<= y x)) :named hyp5))
(assert (! (not (= x z)) :named goal))
(check-sat)
(get-unsat-core)

Я ожидаю непревзойденного ядра {hyp4, hyp5} из -за противоречия (x <y и y <= x), но Z3 возвращает:

(error "ERROR: line 10 column 31: could not locate id  hyp1.")
(error "ERROR: line 11 column 31: could not locate id  hyp2.")
(error "ERROR: line 12 column 31: could not locate id  hyp3.")
(error "ERROR: line 13 column 30: could not locate id  hyp4.")
(error "ERROR: line 16 column 36: could not locate id  hyp5.")
(error "ERROR: line 18 column 35: could not locate id  goal.")
sat
()

Я понимаю, что Z3 не понимает такого способа именования, но я не мог найти другой способ документации Z3.

Не могли бы вы мне помочь, пожалуйста?

Answer 1

Если я изменю вашу первую команду с

(set-option enable-cores)

к

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

и что я затем запускаю ваш сценарий:

z3 -smt2 script.smt2

Я получаю как вывод

unsat
(hyp4 hyp5)

Что я верю в то, что вы ожидали. Обратите внимание, что я использую Z3 3.2 (для Linux, но это не должно иметь никакого значения).