问为了处理CVC4中的递归函数定义，需要为递归函数启用有限模型查找模式。
EN

Stack Overflow用户

提问于 2016-04-06 05:29:12

回答 1查看 132关注 0票数 0

我在安德鲁·雷诺兹和co -authors的论文中发现了以下信息：“SMT中递归函数的模型发现”

如果启用了CVC4 4的递归函数的有限模型查找模式(使用命令行选项-fmf-fun)

但我已经安装了目前版本的CVC4，-fmf-乐趣在CVC4 4中是不可用的?请您在这方面指导我。

回答已采纳

发布于 2016-04-06 19:04:49

在最新的稳定版本(1.4)中，这个选项--fmf是不可用的，但是，它在最新的开发版本中是可用的。

您可以在CVC4的http://cvc4.cs.nyu.edu/downloads/ (页面右侧)下载最新的开发版本。

票数 2

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

原文链接：

https://stackoverflow.com/questions/36442275

复制

相似问题

问为了处理CVC4中的递归函数定义，需要为递归函数启用有限模型查找模式。EN