Z3求解器輸出令人滿意的模型？

Question

在Z3中，如果輸入腳本是以SMTLib格式編寫的，是否可以輸出模型（滿足模型的值賦值）？ get-model返回滿足約束條件的解釋。有沒有什麼辦法從這些解釋中提取具體的價值觀？我知道我們可以使用python/C++ API來獲取模型值。

Answer 1

你可能想使用get-value，這裏有一個小例子（rise4fun鏈接：http://rise4fun.com/Z3/wR81）：

(declare-fun x() Int) 
(declare-fun y() Int) 
(declare-fun z() Int) 
(assert (>= (* 2 x) (+ y z))) 
(declare-fun f (Int) Int) 
(declare-fun g (Int Int) Int) 
(assert (< (f x) (g x x))) 
(assert (> (f y) (g x x))) 
(check-sat) ; sat 
(get-model) ; returns: 
; (model 
; (define-fun z() Int 
; 0) 
; (define-fun y() Int 
; (- 38)) 
; (define-fun x() Int 
; 0) 
; (define-fun g ((x!1 Int) (x!2 Int)) Int 
; (ite (and (= x!1 0) (= x!2 0)) 0 
;  0)) 
; (define-fun f ((x!1 Int)) Int 
; (ite (= x!1 0) (- 1) 
; (ite (= x!1 (- 38)) 1 
;  (- 1)))) 
;) 
(get-value (x)) ; returns ((x 0)) 
(get-value ((f x))) ; returns (((f x) (- 1))) 

潛在那麼你有這個取決於你正在試圖做的，什麼等等解析

有關詳細信息，請查看SMT-LIB標準：

http://smtlib.cs.uiowa.edu/language.shtml

最新版本爲：http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r12.09.09.pdf

您可以在頁面39 /圖3.5中看到get-value的一些示例。