Etikett für SMT-LIB 2.0-Behauptungen in Z3

Question

Könnten Sie mir sagen, wie man Behauptungen in einem Z3 SMT-LIB 2.0-Benchmark nennt? Ich würde es vorziehen, die Standardsyntax von SMT-Lib zu verwenden, aber da Z3 es nicht zu verstehen scheint, suche ich nur nach einem, der mit Z3 arbeitet. Das Bedürfnis besteht darin, uns mit Etiketten zu entfernen.

Hier ist ein Beispiel für den von mir getesteten Benchmark:

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

Ich erwarte den UNSAT -Kern (Hyp4, Hyp5} wegen des Widerspruchs (x <y und y <= x), aber Z3 kehrt zurück:

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

Ich verstehe, dass Z3 diese Art der Benennung nicht versteht, aber ich konnte in Z3 -Dokumentation keinen anderen Weg finden.

Kannst du mir bitte helfen?

Answer 1

Wenn ich Ihren ersten Befehl aus ändere von

(set-option enable-cores)

zu

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

Und dass ich dann dein Skript ausführe:

z3 -smt2 script.smt2

Ich bekomme als Ausgabe

unsat
(hyp4 hyp5)

Welches ist ich glaube, was Sie erwartet haben. Beachten Sie, dass ich Z3 3.2 verwende (für Linux, das sollte jedoch keinen Unterschied machen).