Может ли Z3 обрабатывать типы данных, которые содержат сортировки, введенные функциейещать-сортировать / определять-сортировать? - PullRequest
Новая
       6

Может ли Z3 обрабатывать типы данных, которые содержат сортировки, введенные функциейещать-сортировать / определять-сортировать?

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

Я пытаюсь определить тип данных, который содержит сортировки, введенные в описании-объявлении или определении-сортировке.Но следующая попытка приводит к ошибкам. 

(declare-sort A)
(define-sort B () Int)
(declare-datatypes ((listA (nilA) (consA (hdA A) (tlA listA))))) ;=> unknown sort 'A'
(declare-datatypes ((listB (nilB) (consB (hdB B) (tlB listB))))) ;=> unknown sort 'B'

Есть ли способ сделать это?

Заранее спасибо.

1 Ответ

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

Да, это возможно. Кстати, кажется, вы используете старую версию Z3. Вы должны попробовать последнюю версию. Z3 3.x поддерживает параметрические типы. Итак, синтаксис объявления типов данных немного изменился. Теперь вы должны написать: 

(declare-datatypes () ((listA (nilA) (consA (hdA A) (tlA listA)))))

В новом синтаксисе вы можете указать параметры типа. Поскольку listA не является параметрическим, вы просто предоставили пустой список () параметров типа. Для получения дополнительной информации о типах данных в Z3 см. Руководство Z3 .

Используя параметрические типы, вы также можете кодировать listA и listB как: 

(declare-datatypes (T) ((list (nil) (cons (hd T) (tl list))))) 
(define-sort listA () (list A))
(define-sort listB () (list B))
...