2

SMT-LIB 版本 2.6的草案指定了一个(declare-datatypes)声明。在此功能的原始公告中提到，建议的语法与当时 Z3 和 CVC4 支持的语法不同。

是否有任何具有 SMT-LIB 支持的 SMT 求解器当前支持 SMT-LIB 2.6 草案中的建议语法，或者是否有补丁为求解器添加了对建议语法的支持？

我感兴趣的逻辑是 QF_ABV 加上简单 n 元组的数据类型。我不需要高级数据类型功能，例如递归数据类型或参数数据类型。

4

1 回答 1

4

我在 CVC4 的最新开发版本中添加了对 SMT LIB 2.6 版数据类型的支持（提交 594301e6f2893ebe9baba5083ff084933b1e9da9）。默认情况下不启用 2.6 语法，但您可以使用：

cvc4 --lang=smt2.6 [输入]

希望这会有所帮助，安德鲁

于 2017-03-16T18:32:37.007 回答