时间戳

首页 > 解决方案 > 是否可以在 CVC4 中使用自定义数据类型的数组？

smt - 是否可以在 CVC4 中使用自定义数据类型的数组？

问题描述

使用截至 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 接受相同的数据类型声明。这不应该工作吗？那是一个错误吗？任何解决方法？

标签： smtcvc4

解决方案

推荐阅读