问SMT求解器支持SMT-LIB 2.6 declare-datatypes语句
EN

Stack Overflow用户

提问于 2017-03-13 20:20:37

回答 1查看 461关注 0票数 2

SMT-LIB版本2.6的draft指定了一个(declare-datatypes)语句。在此功能的original announcement中提到，所提出的语法与当时Z3和CVC4支持的语法不同。

是否有任何SMT解算器支持SMT-LIB，当前支持SMT-LIB2.6草案中的建议语法，或者有补丁将对建议语法的支持添加到求解器中？

我感兴趣的逻辑是简单n元组的QF_ABV +数据类型。我不需要高级数据类型特性，比如递归数据类型或参数数据类型。

回答已采纳

发布于 2017-03-17 02:32:37

我在CVC4的最新开发版本(commit 594301e6f2893ebe9baba5083ff084933b1e9da9)中添加了对SMT LIB version2.6数据类型的支持。默认情况下，2.6语法未启用，但您可以使用：

cvc4 --lang=smt2.6输入

希望这对你有帮助，安德鲁

票数 4

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/42763520

复制

相似问题

问SMT求解器支持SMT-LIB 2.6 declare-datatypes语句EN