Массивы и квантификатор

Я пытаюсь использовать массив и квантификатор в 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 и не могу понять, что не так с моим кодом.


z3 smt
person 0mer    schedule 28.08.2012    source источник

Ответы (1)


arrow_upward
2
arrow_downward

В вашем примере это фактически выполнимо, если принять 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)
person Taylor T. Johnson    schedule 28.08.2012
comment
Похоже, вы пытались добиться этого с помощью x. Вместо ограничения, которое я наложил, вы можете сделать то же самое (при условии, что 0 ‹= x‹ 3, как у вас есть): (assert (exists ((i Int)) (and (= i x) (= (select a i) 72) ))) - person Taylor T. Johnson; 28.08.2012