Z3中的獲取任務

（獲取分配）命令應該返回符號列表以及它們的真/假值，如果它們是Bool類型的。根據我的理解，這隻能在以下情況下完成：produce-assignments設置爲true，並且（check-sat）返回時。但是，當我運行一個小腳本在Z3上測試這個時，（get-assignment）只返回（） - 空白。這裏是我的腳本：Z3中的獲取任務

(set-option :produce-assignments true) 
(set-logic QF_UF) 
(declare-fun a() Bool) 
(declare-fun b() Bool) 
(assert (= a b)) 
(check-sat) 
(get-assignment)

來源

2013-05-03 user2345614

對於它的價值，我可以證實這種行爲Z3 [4.3.2版 - 64位 - 編譯哈希碼96f4606a7f2d]。有趣的是，將'（set-option：produce-models true）'放入前導中並在'（check-sat）'後放置'（get-value（ab））'產生'（（false）（b false）） '，所以該作業似乎可用（請參閱http://rise4fun.com/Z3/zGH7）。它看起來好像'（get-assignment）'不被支持，並且好像使用它不會引發錯誤。 – 2013-05-03 06:57:19

的get-assignment語義並不直觀。它顯示named子公式的值。從SMT 2.0 reference（第62頁）：

get-assignment 是一種重量輕，並獲得價值的受限版本，要求針對選定的一組以前真值賦值進入公式（29）同樣的幾個。其他已經討論過的命令（例如，get-proof），只有當產生分配選項（默認爲false）被設置爲真時（參見下面的第5.1.7節）時才能發出該命令。求解器不需要支持這個選項。像get-value一樣，只有在檢查sat命令後，纔會發出該命令，或者可選地還會報告未知的命令，而不會插入斷言集命令。命令返回所有對（fb）的序列，其中b爲真或假並且f是所有斷言的集合中的形式（t命名爲f）的（子）項的標籤，其中t排序布爾。與獲取值類似，當最近一次check-sat命令的響應爲sat，並且只有時，所有斷言的集合都保證具有與返回的真值分配一致的模型（在邏輯中）。

下面是使用兩個命名的子式（也可在網上here）相同的例子：

(set-option :produce-assignments true) 
(set-logic QF_UF) 
(declare-fun a() Bool) 
(declare-fun b() Bool) 
(assert (! (= (! a :named a_val) b) :named eq_val)) 
(check-sat) 
(get-assignment)

來源

2013-05-08 14:22:27

Z3中的獲取任務

回答

相關問題