我正在使用 Z3 构建有界模型检查器。在尝试实施完整性测试时,我遇到了一个奇怪的性能问题。完整性测试必须确保所有状态,每条路径最多包含每个状态一次。如果仍有满足此属性的路径,则 Z3 很快就会给出答案,但是在考虑了所有路径的情况下,Z3 似乎呈指数级缓慢。
我已将测试用例简化为以下内容:
; Set the problem size (length of path)
(define-fun sz () Int 5)
; Used to define valid states
(define-fun limit ((s Int)) Bool
(and (>= s 0)
(<= s sz)))
; Constructs a path of a given length
(define-fun path-of-len ((path (Array Int Int)) (len Int)) Bool
(forall ((i Int))
(=> (and (>= i 0)
(< i len))
(limit (select path i)))))
; Asserts that a given path only contains unique states
(define-fun loop-free ((path (Array Int Int)) (len Int)) Bool
(forall ((i Int) (j Int))
(=> (and (>= i 0)
(>= j 0)
(< i len)
(< j len)
(not (= i j)))
(not (= (select path i) (select path j))))))
; Construct a unique path of a given length
(define-fun path ((path (Array Int Int)) (len Int)) Bool
(and (path-of-len path len)
(loop-free path len)))
; Declare a concrete path
(declare-const tpath (Array Int Int))
; Assert that the path is loop free
(assert (path tpath (+ sz 2)))
(check-sat)
在我的计算机上,这会导致以下运行时间(取决于路径长度):
- 3:0.057s
- 4:0.561s
- 5:42.602s
- 6:>15m(中止)
如果我从 Int 切换到大小为 64 的位向量,性能会稍微好一些,但似乎仍然呈指数级:
- 3:0.035s
- 4:0.053s
- 5:0.061s
- 6:0.106s
- 7:0.467s
- 8:1.809s
- 9:2m49.074s
奇怪的是,长度为 10 只需要 2m34.197s。如果我切换到更小尺寸的位向量,性能会好一点,但仍然是指数级的。
所以我的问题是:这是可以预料的吗?有没有更好的方法来制定这种“无循环”约束?