dReal SMT 求解器反例

Posted 2023-03-06

技术标签:

【中文标题】dReal SMT 求解器反例【英文标题】：dReal SMT solver counterexamples 【发布时间】：2017-02-24 13:15:35 【问题描述】：

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

【问题讨论】：

【参考方案1】：

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

例如：dReal --model微波1.smt2

【讨论】：

以上是关于dReal SMT 求解器反例的主要内容，如果未能解决你的问题，请参考以下文章