ini-option CASE_SPLIT產生奇怪的模型

Question

在用z3工作我的碩士論文時，我發現了一些我無法理解的奇怪東西。 我希望你能幫助我。 :)

的SMT-文件我寫了這個樣子的：

(set-logic QF_UF) 
(set-info :smt-lib-version 2.0) 

;Declare sort Node and its objects. 
(declare-sort Node 0) 
(declare-fun n0() Node) 
(declare-fun n1() Node) 

;Predicate 
(declare-fun dead_0 (Node) Bool) 
;Abbreviation 
(declare-fun I() Bool) 

;initial configuration 
(assert(= I (and 
(not(= n0 n1)) 
(not(dead_0 n0)) 
(dead_0 n1)))) 

;Predicate 
(declare-fun dead_1 (Node) Bool) 
;variable 
(declare-fun m0_1() Node) 

;Abbreviation for Transformation 
(declare-fun TL1_1() Bool) 

;Transformation1neuerKnoten1 
(assert(or (= m0_1 n0)(= m0_1 n1))) 

;Is the whole formula satisfiable? 
(assert(= (and I TL1_1) true)) 
(check-sat) 
(get-model) 

一切都運行得很好，而使用Z3作爲默認選項的命令行工具。 生成的模型包含：

;; universe for Node: 
;; Node!val!0 Node!val!1 
;; ----------- 

和

(define-fun n0() Node 
Node!val!0) 
(define-fun n1() Node 
Node!val!1) 
(define-fun m0_1() Node 
Node!val!0) 

所以我的變量m0_1綁定到節點N0。

然後我用z3和一個只包含CASE_SPLIT=5的ini文件。 結果是一個奇怪的模型。在我看來，差異基本上是 ，我的變量m0_1沒有綁定到我的任何節點n0或n1。 產生的模型包含：

;; universe for Node: 
;; Node!val!2 Node!val!0 Node!val!1 
;; ----------- 

和

(define-fun n0() Node 
Node!val!0) 
(define-fun n1() Node 
Node!val!1) 
(define-fun m0_1() Node 
Node!val!2) 

所以我的問題是：爲什麼Z3創建另一個節點（Node!val!2）爲什麼是綁定到這個新的節點我的變量m0_1？我認爲我的一個斷言（(assert(or (= m0_1 n0)(= m0_1 n1)))）會禁止這一點。

在此先感謝！ :)

Answer 1

Z3有一個稱爲「相關性傳播」的功能。這個特性對於含有量詞的問題是非常有效的，但是對於無量詞的問題來說，這通常是開銷的。命令行選項RELEVANCY=0禁用相關性傳播，RELEVANCY=2或RELEVANCY=1啓用它。 選項CASE_SPLIT=5假定啓用相關傳播。 如果我們提供CASE_SPLIT=5 RELEVANCY=0，然後將Z3生成一個警告消息

WARNING: relevacy must be enabled to use option CASE_SPLIT=3, 4 or 5 

，並忽略的選項。

此外，默認情況下，Z3使用「自動配置」功能。此功能掃描輸入公式並調整給定實例的Z3配置。 所以，在你的榜樣，會發生以下情況：

1. 您提供的選項CASE_SPLIT=5
2. 當Z3驗證命令行選項，關聯性傳播被禁用，並且不產生警告消息。
3. Z3運行自動配置程序，由於您的示例是免費量化的，因此會禁用相關性傳播RELEVANCY=0。現在，使用不一致的配置，Z3產生錯誤的結果。

爲了避免這個問題，如果你使用CASE_SPLIT=5，那麼你也應該用AUTO_CONFIG=false（禁用自動配置）和RELEVANCY=2（使相關的傳播）。因此，在命令行應該是：

z3 CASE_SPLIT=5 AUTO_CONFIG=false RELEVANCY=2 file.smt2 

在下一版本（Z3 4.2），我會向Z3如果用戶嘗試啓用自動配置時設置CASE_SPLIT=5顯示警告信息。