Выражение отношения подтипа между типами перечисления в Z3 - PullRequest
Новая
       17

Выражение отношения подтипа между типами перечисления в Z3

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

Как лучше всего выразить отношение подтипа между типами перечисления в Z3?

В частности, я хочу сделать что-то вроде следующего: 

(declare-datatypes () ((Animal Eagle Snake Scorpion)))

, а затем создать новый подтип: 

(declare-datatypes () ((Mammal Cat Rat Bat)))

так что утверждение о том, что есть 4 различных константы типа Animal, является SAT, а утверждение о том, что есть 4 различных константы типа Mammal, является UNSAT.

1 Ответ

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

Z3 не имеет прямой поддержки отношений подтипов (подортов).Я вижу два способа их моделирования в Z3.

Например, у вас может быть сортировка перечисления Animal, которая содержит всех животных.Затем вы определяете предикаты, такие как: is-mammal, is-reptile и т. Д.

Вот сценарий, который использует этот подход: 

(set-option :produce-models true)
(declare-datatypes () ((Animal Eagle Snake Scorpion Cat Rat Man)))

(define-fun is-mammal ((x Animal)) Bool
        (or (= x Cat) (= x Rat) (= x Man)))

(declare-const a1 Animal)
(declare-const a2 Animal)
(declare-const a3 Animal)
(declare-const a4 Animal)


(assert (distinct a1 a2 a3 a4))
(check-sat)
; sat
(get-model)

; now, we constraint a1, a2, a3 and a4 to be mammals.
(assert (is-mammal a1))
(assert (is-mammal a2))
(assert (is-mammal a3))
(assert (is-mammal a4))
(check-sat)
; unsat

Другое решение использует типы данных для определения видов перечисленияи союз родов.То есть мы объявляем один тип данных для каждого класса животных: MammalType, ReptileType и т. Д. Каждый из них является типом перечисления.Затем мы объявляем тип данных union: AnimalType.Этот тип данных содержит конструктор для каждого класса животных: Mammal, Reptile и т. Д. Z3 автоматически создает предикат is-[constructor-name] (распознаватель) для каждого конструктора: is-Mammal, is-Reptile и т. Д. Мы называем методы доступа как "Animal2Class ": Animal2Mammal, Animal2Reptile и т. Д. Более подробную информацию о типах данных можно найти по адресу http://rise4fun.com/z3/tutorial/guide. Вот скрипт, использующий эту кодировку: 

(set-option :produce-models true)

(declare-datatypes () ((AveType Eagle Sparrow)))
(declare-datatypes () ((ReptileType Snake)))
(declare-datatypes () ((ArachnidType Scorpion Spider)))
(declare-datatypes () ((MammalType Cat Rat Man)))

(declare-datatypes () ((AnimalType 
                        (Ave (Animal2Ave AveType))
                        (Reptile (Animal2Reptile ReptileType))
                        (Arachnid (Animal2Arachnid ArachnidType))
                        (Mammal (Animal2Mammal MammalType)))))

(declare-const a1 AnimalType)
(declare-const a2 AnimalType)
(declare-const a3 AnimalType)
(declare-const a4 AnimalType)

(assert (distinct a1 a2 a3 a4))
(check-sat)
; sat
(get-model)

; now, we constraint a1, a2, a3 and a4 to be mammals.
(assert (is-Mammal a1))
(assert (is-Mammal a2))
(assert (is-Mammal a3))
(assert (is-Mammal a4))
(check-sat)
; unsat
...