z3 - sort Seq的定义

Question

我想知道sort Seq的定义是什么。我在 Z3 SMT 2.0 指南中找不到它的定义。我意识到 Seq 已经定义了，因为我试图定义一个名为 Seq 的排序。是否有一些与 Seq 相关的断言？

谢谢！！

马克西

Answer 1

是的Seq，，RegEx（正则表达式）和FP（浮点数）在 Z3 4.0 中是“保留的”。它们尚未实施，但将在未来的版本中提供。例如，Z3 将具有内置函数，例如：、seq-last和许多其他函数。在 Z3 4.0 中，这些排序和函数只是“存根”，其行为类似于未解释的排序和函数。这就是为什么我们没有他们的任何文件。seq-concatseq-length