Значения для терминов Array в моделях z3 - PullRequest
Новая
       5

Значения для терминов Array в моделях z3

2 голосов
/ 30 декабря 2011

Я использую z3 для своего исследования, и у меня есть следующая проблема.Я анализирую модель выполнимой формулы, которая содержит массивы и неинтерпретированные функции.Я хотел бы проверить, проверить конкретные записи массива.

В примерах из руководства по z3 можно получить доступ к таким значениям.
Например, для вопросов типа 

(get-value ((select my_array 0)))

можно получить ответы.как 

(((select my_array 0) 1))

, указывающее, что значение my_array в позиции 0 равно 1.

Однако полученный ответ выглядит как 

(((select my_array 0) (select Array!val!0 0)))

что не очень помогает.

Кроме того, в начале модели я получаю блок, который выглядит следующим образом: 

  ;; universe for (Array Int Int):
  ;;   Array!val!10 Array!val!6 Array!val!0 Array!val!5 Array!val!9 Array!val!1 Array!val!11 Array!val!4 Array!val!2 Array!val!7 Array!val!3 Array!val!8 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun Array!val!10 () (Array Int Int))
  (declare-fun Array!val!6 () (Array Int Int))
  (declare-fun Array!val!0 () (Array Int Int))
  (declare-fun Array!val!5 () (Array Int Int))
  (declare-fun Array!val!9 () (Array Int Int))
  (declare-fun Array!val!1 () (Array Int Int))
  (declare-fun Array!val!11 () (Array Int Int))
  (declare-fun Array!val!4 () (Array Int Int))
  (declare-fun Array!val!2 () (Array Int Int))
  (declare-fun Array!val!7 () (Array Int Int))
  (declare-fun Array!val!3 () (Array Int Int))
  (declare-fun Array!val!8 () (Array Int Int))
  ;; cardinality constraint:
  (forall ((x (Array Int Int)))
          (and (= x Array!val!10)
               (= x Array!val!6)
               (= x Array!val!0)
               (= x Array!val!5)
               (= x Array!val!9)
               (= x Array!val!1)
               (= x Array!val!11)
               (= x Array!val!4)
               (= x Array!val!2)
               (= x Array!val!7)
               (= x Array!val!3)
               (= x Array!val!8)))
  ;; -----------

Я действительно не понимаю значенияэто, но каким-то образом это, кажется, связано с моей проблемой, так как подобный блок не появляется для простых примеров в руководстве.Кто-нибудь знает, что вызывает такое поведение z3 или как его можно избежать?

После некоторых экспериментов я нашел «минимальный» пример, демонстрирующий нежелательное поведение.Кажется, что-то связано с использованием неинтерпретированных функций в индексных выражениях. 

(declare-fun my_function ((Int)(Int)) Int)
(declare-fun my_array () (Array Int Int))

(assert
  (=
    (select my_array (my_function 0 1))
    (select my_array (my_function 1 0))
  )
)

(check-sat)  
(get-model)
(get-value ((select my_array (my_function 0 1))))
(get-value ((my_function 0 1)))

z3 отвечает на это: 

sat 
(model
 ;; universe for (Array Int Int):
 ;; Array!val!0
 ;; -----------
 ;; definitions for universe elements:
 (declare-fun Array!val!0 () (Array Int Int))
 ;; cardinality constraint:
 (forall ((x (Array Int Int))) (= x Array!val!0))
 ;; -----------
 (define-fun my_array () (Array Int Int)
 Array!val!0)
 (define-fun my_function ((x!1 Int) (x!2 Int)) Int
 (ite (and (= x!1 0) (= x!2 1)) 2
 (ite (and (= x!1 1) (= x!2 0)) 3
 2)))
 )
 (((select my_array (my_function 0 1)) (select Array!val!0 2)))
 (((my_function 0 1) 2))

1 Ответ

3 голосов
/ 30 декабря 2011

В SMT «логика» указывает, какие теории доступны для построения формул.Например, если используется команда (set-logic QF_UFLIA), доступны неинтерпретированные функции и линейная целочисленная арифметика.Когда логика не указана с помощью команды set-logic.Z3 пытается угадать логику автоматически для пользователя, и только «устанавливает» необходимые теории.В вашем примере Z3 неправильно полагает, что вашему примеру не нужна теория массива.Таким образом, (Array Int Int) рассматривается как неинтерпретированная сортировка.Вот почему Z3 предполагает (Array Int Int) неинтерпретируемую сортировку и предоставляет интерпретацию для нее в сгенерированной модели.Это ошибка, я исправлю ее в следующем выпуске.Тем временем вы можете использовать один из следующих подходов, чтобы избежать этой ошибки:

  • Укажите логику, которая содержит теорию массивов.Пример: добавьте (set-logic QF_AUFLIA) в начале вашего примера.

  • Отключите автоматическую настройку (Z3 установит все доступные теории).Добавить команду (set-option :auto-config false).

...