Вы отвечаете на вопрос, который возникает на регулярной основе:
как я могу смешивать типы данных и массивы (как наборы, мульти-наборы или
типы данных в диапазоне)?
Как указано выше, Z3 не поддерживает смешивание типов данных.
и массивы в одной декларации.
Решение состоит в том, чтобы разработать собственный решатель для
смешанный тип данных + теория массивов. Z3 содержит программный
API для разработки пользовательских решателей.
Все еще полезно разработать этот пример
проиллюстрировать возможности и ограничения
кодирования теорий с квантификаторами и триггерами.
Позвольте мне упростить ваш пример, просто используя A.
В качестве обходного пути вы можете определить вспомогательный вид.
Обходной путь не идеален, все же. Это иллюстрирует некоторые
Аксиома «взлом». Он опирается на операционную семантику
о том, как квантификаторы создаются во время поиска.
(set-option :model true) ; We are going to display models.
(set-option :auto-config false)
(set-option :mbqi false) ; Model-based quantifier instantiation is too powerful here
(declare-sort SetA) ; Declare a custom fresh sort SetA
(declare-datatypes () ((A f1 (cons (value Int) (a SetA)))))
(define-sort Set (T) (Array T Bool))
Затем определите биекции между (набор A), набор A.
(declare-fun injSA ((Set A)) SetA)
(declare-fun projSA (SetA) (Set A))
(assert (forall ((x SetA)) (= (injSA (projSA x)) x)))
(assert (forall ((x (Set A))) (= (projSA (injSA x)) x)))
Это почти то, что указано в объявлении типа данных.
Для обеспечения обоснованности вы можете связать порядковый номер с членами A
и обеспечить, чтобы члены SetA были меньше в обоснованном порядке:
(declare-const v Int)
(declare-const s1 SetA)
(declare-const a1 A)
(declare-const sa1 (Set A))
(declare-const s2 SetA)
(declare-const a2 A)
(declare-const sa2 (Set A))
С аксиомами до сих пор a1 может быть членом самого себя.
(push)
(assert (select sa1 a1))
(assert (= s1 (injSA sa1)))
(assert (= a1 (cons v s1)))
(check-sat)
(get-model)
(pop)
Теперь мы связываем порядковый номер с членами A.
(declare-fun ord (A) Int)
(assert (forall ((x SetA) (v Int) (a A))
(=> (select (projSA x) a)
(> (ord (cons v x)) (ord a)))))
(assert (forall ((x A)) (> (ord x) 0)))
По умолчанию создание экземпляров квантификатора в Z3 основано на шаблонах.
Первое количественное утверждение выше не будет реализовано на всех
соответствующие случаи. Вместо этого можно утверждать:
(assert (forall ((x1 SetA) (x2 (Set A)) (v Int) (a A))
(! (=> (and (= (projSA x1) x2) (select x2 a))
(> (ord (cons v x1)) (ord a)))
:pattern ((select x2 a) (cons v x1)))))
Аксиомы, подобные этим, которые используют два паттерна (называемые мульти-паттернами)
довольно дорогие. Они производят экземпляры для каждой пары
из (выберите х2 а) и (минусы v х1)
Ограничение членства с прежних времен неудовлетворительно.
(push)
(assert (select sa1 a1))
(assert (= s1 (injSA sa1)))
(assert (= a1 (cons v s1)))
(check-sat)
(pop)
но модели еще не обязательно хорошо сформированы.
значением по умолчанию для набора является 'true', что
будет означать, что модель подразумевает, что существует цикл членства
когда его нет.
(push)
(assert (not (= (cons v s1) a1)))
(assert (= (projSA s1) sa1))
(assert (select sa1 a1))
(check-sat)
(get-model)
(pop)
Мы можем приблизить более точные модели, используя
следующий подход для обеспечения того, что наборы, которые
используемые в данных типы являются конечными.
Например, когда есть проверка членства на множестве x2,
мы устанавливаем, что значением по умолчанию для этого набора является «ложь».
(assert (forall ((x2 (Set A)) (a A))
(! (not (default x2))
:pattern ((select x2 a)))))
В качестве альтернативы, всякий раз, когда набор встречается в конструкторе типа данных
конечно
(assert (forall ((v Int) (x1 SetA))
(! (not (default (projSA x1)))
:pattern ((cons v x1)))))
(push)
(assert (not (= (cons v s1) a1)))
(assert (= (projSA s1) sa1))
(assert (select sa1 a1))
(check-sat)
(get-model)
(pop)
На протяжении включения дополнительных аксиом,
Z3 дает ответ «неизвестно» и, кроме того,
модель, которая производится, указывает, что домен SetA
конечно (синглтон). Таким образом, пока мы можем исправить настройки по умолчанию
эта модель до сих пор не удовлетворяет аксиомам. Удовлетворяет
аксиомы только по модулю инстанциации.