Z3 устанавливает значение по умолчанию массива в ноль - PullRequest
Новая
       7

Z3 устанавливает значение по умолчанию массива в ноль

0 голосов
/ 25 февраля 2019

Я пытаюсь найти модели для выражений массива, где значения по умолчанию для массива равны 0.

Например, я пытаюсь решить этот пример, но все время получаю неизвестные результаты 

(declare-const arr (Array Int Int))
(declare-const arr2 (Array Int Int))
(declare-const a Int)
(declare-const b Int)

(assert (forall ((x Int)) (= (select arr x) 0)))

(assert (> a 0))
(assert (<= a 10))

(assert (= arr2 (store arr a 1337)))

(assert (> b 0))
(assert (<= b 10))


(assert (= (select arr2 b) 0))

(check-sat)
(get-model)

1 Ответ

0 голосов
/ 25 февраля 2019

Советы Патрика о том, что не следует использовать квантификаторы, незаменимы!Они сделают вашу жизнь сложнее.Однако вам повезло, потому что z3 поддерживает константы-массивы для вашего случая использования, что довольно часто.Синтаксис: 

(assert (= arr ((as const (Array Int Int)) 0)))

Это гарантирует, что arr будет иметь все свои записи как 0;количественная оценка не требуется, и z3 прекрасно с ней справляется.

Итак, ваш эталонный тест будет: 

(declare-const arr (Array Int Int))
(declare-const arr2 (Array Int Int))
(declare-const a Int)
(declare-const b Int)

(assert (= arr ((as const (Array Int Int)) 0)))

(assert (> a 0))
(assert (<= a 10))

(assert (= arr2 (store arr a 1337)))

(assert (> b 0))
(assert (<= b 10))


(assert (= (select arr2 b) 0))

(check-sat)
(get-model)

, который решается в кратчайшие сроки.Таким образом, вы можете начать весь массив с 0 и изменить интересующий вас диапазон;которая может зависеть от переменных, как обычно, и не требуется знать заранее.

...