Etikett für SMT-LIB 2.0-Behauptungen in Z3
Frage
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?
Lösung
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).