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显示警告信息。