问dReal SMT求解器反例
EN

Stack Overflow用户

提问于 2017-02-24 21:15:35

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

dReal SMT求解器是否返回反例？我见过这样的例子:produce models是正确的，但我不知道如何生成反例。此外，可视化工具有一个-- dReach选项，因此dReal似乎需要生成一些模型信息。但是，当我在.smt2文件上运行它时，我似乎找不到查看反例的方法。

发布于 2017-02-24 23:34:56

好吧，这是微不足道的:)模型不遵循通常的.smt2使用约定( get -model)，但是您可以使用命令行选项--model来获取模型。

例如: dReal --模型微波1.smt2

票数 1

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

原文链接：

https://stackoverflow.com/questions/42439578

复制

相似问题

问dReal SMT求解器反例EN