z3 - 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 绑定(bind)到节点 n0。

然后我使用 z3 和一个只包含 CASE_SPLIT=5 的 ini 文件。 .
结果是一个奇怪的模型。在我看来，区别基本上是
我的变量 m0_1 没有绑定(bind)到我的任何节点 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绑定(bind)到这个新节点？我认为我的一个断言( (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 配置。
因此，在您的示例中，会发生以下情况:

您提供选项 CASE_SPLIT=5

当 Z3 验证命令行选项时，相关性传播被禁用，并且不会生成警告消息。

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 显示警告消息。启用自动配置时。