数组和量化器

Question

我试图在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理论还很陌生，我不知道我的代码出了什么问题。

Answer 1

在您的示例中，将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)