Применение функции к домену множества Z3 - PullRequest
Новая
       8

Применение функции к домену множества Z3

0 голосов
/ 30 сентября 2019

Есть ли способ в Z3 применить функцию к каждому элементу набора, чтобы получить новый набор? На обычном языке программирования такая функция выглядит следующим образом: map :: (a -> b) -> Set a -> Set b

Мне известна функция map, но она применяет произвольную функцию к диапазону массивов. map Я ищу работы с доменом массивов (учитывая способ построения наборов Z3).

1 Ответ

1 голос
/ 30 сентября 2019

Это невозможно в SMTLib. Обратите внимание, что функция map, которую вы хотите, является функцией более высокого порядка, и SMTLib не поддерживает логику высшего порядка. Существует несколько предложенных расширений для включения таких функций, но по крайней мере z3 пока не поддерживает такие функции. Некоторые ссылки:

Сказав это, иногда вы можете уйти, симулируя более упорядоченные объекты, используя количественноаксиомы. Конечно, введение квантификаторов делает логику полуразрешимой, поэтому средство проверки может вернуть unknown (и, скорее всего, так и будет для любого интересного варианта использования), но это один из способов решения таких проблем. Вот пример: 

; declare two Int sets
(declare-fun S1 () (Array Int Bool))
(declare-fun S2 () (Array Int Bool))

; Function to increment "domain" by 1
(define-fun f ((a Int)) Int (+ a 1))

; Relate S2 to S1 by "mapping" on the domain
; In a higher-order language, this would be:
;      S2 = map f S1
(assert (forall ((x Int)) (= (select S2 x)
                             (select S1 (f x))
                          )))

; some tests:
(assert (= (select S2 4) (select S1 3)))

(check-sat)
(get-model)

Обратите внимание, как я использовал утверждение forall, чтобы выразить связь между S1 и S2. Это может быть невозможно вообще;и вам, возможно, придется также указать обратное значение f в общем случае, но оно может быть использовано для основных целей. Обратите внимание, что вы не сможете «передать» функцию ни одному из них: точно так же, как и f в приведенном выше примере, все функции, используемые в позиции «высшего порядка», должны иметь явное имя. Он довольно ограничен, но может выполнять работу в простых случаях.

Кроме того, хотя Z3 быстро решает этот конкретный тест, я не ожидаю, что он будет обрабатывать произвольные количественные случаи. Для рассуждений с функциями более высокого порядка Z3 (или любой другой SMT-решатель) просто не правильный инструмент. Если это ваша цель, посмотрите на теоремы, такие как Изабель, HOL, Coq, Agda, Lean;которые разработаны с нуля, чтобы иметь дело с функциями более высокого порядка. У них также есть прочные связи (то есть оракулы и механизмы воспроизведения доказательств), поэтому они могут использовать решатели SMT в качестве фоновых движков для завершения доказательств. Недостатком является, конечно, то, что они не кнопочные, и поэтому требуют ручного управления. (Хотя автоматизация стала действительно хорошей в последние годы.)

...