z3 SMT-LIB 2.0 ベンチマークでアサーションに名前を付ける方法を教えてください。SMT-LIB の標準構文を使用したいのですが、z3 はそれを理解していないようなので、z3 で動作するものを探しています。必要なのは、ラベル付きの未飽和コアを取得することです。
私がテストしたベンチマークの例を次に示します。
(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 and y <= x) のため unsat コア {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 のドキュメントで別の方法を見つけることができませんでした。
私を手伝ってくれますか？