Разве нельзя использовать массив пользовательских типов данных с CVC4?

Используя последнюю версию cvc4 по состоянию на 2018-07-10, этот код:

(set-info :smt-lib-version 2.6)
(set-logic ALL)
(declare-datatypes
  ( (Type 0) )
  ( ((bool) (number)
     (tuple (tuple-type (Array Int Type)))) ))

производит этот вывод из cvc4:

(error "Parse Error: Symbol 'Type' not declared as a type
   (tuple (tuple-type (Array Int Type)))) ))
                                 ^
")

Такая же декларация типа данных принята Z3. Разве это не должно работать? Это ошибка? Любой обходной путь?

0 ответов

Другие вопросы по тегам