Z3 ForAll on Arrays

Question

Мне удалось создать массив записей с использованием Z3, но теперь я пытаюсь увидеть синтаксис, который мне нужен для выполнения операции $ \ forall $ в массиве ... вот пример фрагмента SMT -LIB2-код, который у меня есть.

(declare-datatypes() ((rec (mk-R5 (age Int) (area Int) (married Bool))))) 
(declare-const recs (Array Int rec)) 
(declare-const r1 rec) 
(assert(= (age r1) 15)) 
(assert(= (area r1) 10001)) 
(assert(= (married r1) true)) 
(declare-const r2 rec) 
(assert(= (age r2) 35)) 
(assert(= (area r2) 2845)) 
(assert(= (married r2) true)) 
(declare-const x Int) 
(declare-const y Int) 
(assert (= recs (store recs x r1))) 
(assert (= recs (store recs y r2))) 
(assert(forall ((i rec)) (= (married i) true))) 
(check-sat) 
(get-model) 

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

Как выполнить операцию $ \ forall $ над массивом, который у меня есть?

Answer 1

Похоже, вы пытаетесь поместить две записи в массив, а затем сказать что-то об этих элементах. К сожалению, ваша кодировка не совсем означает это.

Первое, что нужно обратить внимание, это значение следующей строки:

(declare-const recs (Array Int rec)) 

Это говорит о том, что recs массив индексируется всех целых чисел. То есть, домен представляет собой набор всех значений Int. Вероятно, это не то, что вы имели в виду.

Кроме того, линии:

(assert (= recs (store recs x r1))) 
(assert (= recs (store recs y r2))) 

лучше написано так:

(assert (= (select recs x) r1)) 
(assert (= (select recs y) r2)) 

Думай о нем, как говорят, что вы знаете об индексе x и y; в отличие от некоторых императивных утверждений присваивания, чтобы «изменить» recs, когда вы пытались написать. Не существует понятия изменения любых значений в smt-lib; вы просто заявляете, что вы знаете, о модели, которую вы строите.

Один из способов исправить ForAll-утверждение было бы написать так:

(assert (forall ((i Int)) 
       (implies (or (= i x) (= i y)) 
         (= (married (select recs i)) true)))) 

Мы количественно по индексам, и сказать, что если индекс i или y, то эти записи имеют married людей , С учетом этих изменений, Z3 отвечает:

sat 
(model 
    (define-fun r2() rec 
    (mk-R5 35 2845 true)) 
    (define-fun recs() (Array Int rec) 
    (_ as-array k!0)) 
    (define-fun y() Int 
    1) 
    (define-fun x() Int 
    0) 
    (define-fun r1() rec 
    (mk-R5 15 10001 true)) 
    (define-fun k!0!2 ((x!0 Int)) rec 
    (ite (= x!0 1) (mk-R5 35 2845 true) 
     (mk-R5 15 10001 true))) 
    (define-fun k!1 ((x!0 Int)) Int 
    (ite (= x!0 0) 0 
     1)) 
    (define-fun k!0 ((x!0 Int)) rec 
    (k!0!2 (k!1 x!0))) 
) 

, который немного трудно читать, но это даст вам модель, как указано.

Мне кажется, однако, что это не совсем то, что вы пытались моделировать; но с вашего вопроса трудно сказать. Если вы описываете фактическую проблему, которую пытаетесь решить, ответы могут быть более полезными.