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作为带有default-options的命令行工具时,一切都运行良好.生成的模型包含:

;; 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只包含一个ini文件CASE_SPLIT=5.结果是一个奇怪的模型.在我看来,差异基本上是我的变量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)中,如果用户CASE_SPLIT=5在启用自动配置时尝试设置,我将使Z3显示警告消息.