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

Question

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

(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 指南。

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

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