我正在尝试在 Z3 中使用数组和量词来查找给定文本中的子字符串。
我的代码如下：
(declare-const a (Array Int Int))
(declare-const x Int)
;; a|A
(assert (or (= (select a 0) 61) (= (select a 0) 41)))
;; b|B
(assert (or (= (select a 1) 62) (= (select a 1) 42)))
;; c|C
(assert (or (= (select a 2) 63) (= (select a 2) 43)))
(assert (>= x 0))
(assert (< x 3))
(assert (exists ((i Int)) (= (select a i) 72) ))
(check-sat)
Z3 在不应该的时候说那是 SAT。我对 Z3 和 SMT 理论相当陌生，我无法弄清楚我的代码有什么问题。
在您的示例中，实际上可以通过将 i 设为 0、1、2 范围之外的任何自然数来满足。因此，例如，如果您让 i = 3，因为您没有以任何方式限制索引 3 处的数组， a[3] 可能是 72。
这是一个链接，显示了 Z3@Rise 界面上您的示例的令人满意的分配（模型），以及接下来描述的修复：http ://rise4fun.com/Z3/E6YI
为了防止这种情况发生，一种方法是将 i 的范围限制为您已经分配的数组索引之一。也就是说，将 i 限制在 0 和 2 之间。
(declare-const a (Array Int Int))
(declare-const x Int)
;; a|A
(assert (or (= (select a 0) 61) (= (select a 0) 41)))
;; b|B
(assert (or (= (select a 1) 62) (= (select a 1) 42)))
;; c|C
(assert (or (= (select a 2) 63) (= (select a 2) 43)))
(assert (>= x 0))
(assert (< x 3))
(assert (exists ((i Int)) (= (select a i) 72)))
(check-sat)
(get-model) ; model gives i == 3 with a[i] == 72
(assert (exists ((i Int)) (and (>= i 0) (<= i 2) (= (select a i) 72) )))
(check-sat)