Z3のSMT-LIB 2.0アサーションのラベル

Question

Z3 SMT-LIB 2.0ベンチマークでアサーションに名前を付ける方法を教えてください。 SMT-LIBの標準的な構文を使用することをお勧めしますが、Z3はそれを理解していないようであるため、Z3で作業するものを探しています。必要なのは、ラベルを備えたUNSATコアを取得することです。

これが私がテストしたベンチマークの例です。

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

矛盾（x <yおよびy <= x）のために、unstatコア{hyp4、hyp5}を期待していますが、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用ですが、違いはありません）。