z3 - 仅当 check-sat 返回 "sat"时才动态调用 get-value

Question

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 会将其返回值更改为错误状态。

Answer 1

我不认为有什么好方法，如果你想要的是有一个“SMT”文件来统治整个交易。

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

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