z3 - Z3 能否处理包含由 declare-sort/define-sort 引入的排序的数据类型？

Question

我正在尝试定义一个数据类型，其中包含由 declare-sort 或 define-sort 引入的排序。但以下尝试会导致错误。

(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'

有办法吗？

提前致谢。

Answer 1

是的，它可以。顺便说一句，您似乎使用的是旧版本的 Z3。您应该尝试最新版本。Z3 3.x 支持参数类型。因此，声明数据类型的语法发生了一点变化。现在，你必须写:

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

在新语法中，您可以指定类型参数。由于 listA 不是参数化的，您只需提供类型参数的空列表 ()。有关 Z3 中数据类型的更多信息，请参阅 Z3 guide .

使用参数类型，您还可以将 listA 和 listB 编码为:

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