Étiquette sur SMT-LIB 2.0 assertions z3

Question

Pourriez-vous me dire comment nommer des affirmations dans une référence z3 SMT-LIB 2.0? Je préférerais utiliser la syntaxe standard de SMT-LIB, mais comme z3 ne semble pas comprendre, je suis à la recherche d'un travail avec z3. Le besoin est d'obtenir des noyaux UNSAT avec des étiquettes.

Voici un exemple de référence I testé:

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

J'attends le noyau unsat {hyp4, hyp5} à cause de la contradiction (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
()

Je comprends que z3 ne comprend pas cette façon de nommer, mais je ne pouvais pas trouver une autre façon dans la documentation z3.

Pourriez-vous me aider s'il vous plaît?

Answer 1

Si je change votre première commande de

(set-option enable-cores)

à

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

et que je lance alors votre script:

z3 -smt2 script.smt2

Je reçois en sortie

unsat
(hyp4 hyp5)

qui est je crois ce que vous attendiez. Notez que j'utilise Z3 3.2 (pour Linux, mais cela ne devrait pas faire de différence).