Etichetta su SMT-lib 2.0 asserzioni in Z3

Question

Potrebbe dirmi come denominare asserzioni in un punto di riferimento Z3 SMT-LIB 2.0? Io preferirei utilizzare la sintassi standard di SMT-LIB, ma come Z3 sembra non capire, sto solo cercando un lavoro con Z3. Il bisogno è quello di ottenere nuclei UNSAT con le etichette.

Ecco un esempio di punto di riferimento che ho provato:

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

Mi aspetto il nucleo UNSAT {hyp4, hyp5} a causa della contraddizione (x

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

Capisco che Z3 non capisce questo modo di nominare, ma non riuscivo a trovare un altro modo nella documentazione z3.

Mi può aiutare per favore?

Answer 1

Se cambio il tuo primo comando da

(set-option enable-cores)

a

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

e che quindi eseguire lo script:

z3 -smt2 script.smt2

ottengo come uscita

unsat
(hyp4 hyp5)

che è credo che quello che ti aspettavi. Si noti che sto usando Z3 3.2 (per Linux, ma che non dovrebbe fare alcuna differenza).