4

SMT2 标准规定调用 get-value 仅在调用 check-sat 并且仅当 check-sat 返回“sat”或“unknown”时才合法。

下面是一个 unsat 问题的简单示例：

(set-option :produce-models true)
(set-logic QF_BV)
(set-info :smt-lib-version 2.0)
(declare-fun a ()(_ BitVec 4))
(declare-fun b ()(_ BitVec 4))
(declare-fun c ()(_ BitVec 4))
(declare-fun z ()(_ BitVec 4))
(assert (= #b1111 z))
(assert (= a b))
(assert (= (bvxor a z) c))
(assert (= b c))
(check-sat)
(get-value ( a ))
(get-value ( b ))
(get-value ( c ))

由于问题未解决，因此 get-value 命令是非法的。取出任何一个断言，它就会变成 sat 并且 get-value 命令变得合法。所以我的问题是，你如何编写一个 SMT2 脚本来检查 check-sat 的返回值，并且只在它返回 sat 时才调用 get-value？

非法调用 get-value 对我来说是一个问题，因为我在一个流程中运行不同的 smt 求解器并检查程序的返回值，然后解析它们的输出。如果非法调用 get-value，CVC4 会将其返回值更改为错误状态。

4

2 回答 2

3

如果您想要一个“SMT”文件来管理整个交易，我认为没有什么好方法。

这个问题在与其他语言的 SMT 求解器交互时经常出现。我采用的解决方案是，我与求解器保持一个开放的管道，并将脚本的行提供给它，阅读响应，并根据我得到的响应决定接下来要发送什么。本质上是程序化的交互。（例如，这就是 Haskell SBV 库所做的。）

但是，我确实同意这是一种痛苦。如果有一种 SMT2-lib 认可的方式来处理这种常见的交互，那就太好了。

于 2014-06-25T17:32:02.350 回答
1

对于从命令行运行的 CVC4，添加标志

--dump-models          output models after every SAT/INVALID/UNKNOWN
                       response [*]

这不像 get-value 那样具体。此选项是非标准的，CVC4 当前不支持从 SMT2 解析器设置此标志。（让我们知道您是否希望得到支持。）

于 2014-06-25T18:14:12.923 回答