z3中SMT-LIB 2.0聲明的標籤

您能否告訴我如何在z3 SMT-LIB 2.0基準中命名聲明？我寧願使用SMT-LIB的標準語法，但由於z3似乎並不理解它，我只是在尋找一個與z3一起工作的人。需要的是獲得不帶標籤的核心。z3中SMT-LIB 2.0聲明的標籤

這裏是我測試基準的一個例子：

(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），但Z3返回的不飽和度核心{hyp4，hyp5}：

(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文檔中找到另一種方式。

請問您能幫我嗎？

來源

2011-10-18 ygu

如果我從

(set-option enable-cores)

改變你的第一個命令

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

和我然後運行腳本：

z3 -smt2 script.smt2

我得到的輸出

unsat 
(hyp4 hyp5)

這是我相信你所期待的。請注意，我使用的是Z3 3.2（對於Linux，但不應該有任何區別）。

來源

2011-10-18 10:22:46 Philippe

謝謝，但我之前嘗試過，並且在未知的ID上收到同樣的錯誤，並加上以下消息：「（錯誤」第20行第16列：核心尚未啓用，請使用（set-option enable-cores）「）「，這就是爲什麼我嘗試使用上述選項的原因。我認爲z3的版本是問題所在。我在Linux上使用Z3 2.19。我會去獲取你的版本並嘗試。 – ygu

事實上：如果你看[發行註記]（http://research.microsoft.com/en-us/um/redmond/projects/z3/releasenotes.html），你會發現很多事情已經改變關於Z3 2.19以來的SMT-LIB 2.0支持。 – Philippe

我剛試過。它與Z3 3.2一起工作。再次感謝@菲利普。 – ygu

z3中SMT-LIB 2.0聲明的標籤

回答

相關問題