使用截至 2018-07-10 的最新 cvc4,此代码:
(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 接受相同的数据类型声明。这不应该工作吗?那是一个错误吗?任何解决方法?