根据求解器的决定执行 get-model 或 unsat-core [英] Executing get-model or unsat-core depending on solver's decision

问题描述

我想知道，在 SMT-LIB 2.0 脚本中是否有可能访问求解器的最后一个可满足性决策(sat、unsat、...).例如下面的代码:

I wonder, if there is a possibility in a SMT-LIB 2.0 script to access the last satisfiability decision of a solver (sat, unsat, ...). For example, the following code:

(set-option :produce-unsat-cores true)
(set-option :produce-models true)
(set-logic QF_UF)
(declare-fun p () Bool)
(declare-fun q () Bool)
(declare-fun r () Bool)

(assert (! (=> p q) :named PQ))
(assert (! (=> q r) :named QR))
(assert (! (not (=> p r)) :named nPR))

(check-sat)
(get-model)
(get-unsat-core)

跑在 Z3 返回:

unsat
(error "line 15 column 10: model is not available")
(PQ QR nPR)

并在 MathSAT 中运行返回:

and ran in MathSAT returns:

unsat
(error "model generation not enabled")

在 MathSAT 5 中，它只是中断 (get-model)，甚至没有达到 (get-unsat-core).SMT-LIB 2.0 语言中是否有任何方法可以获取模型如果该决定是 SAT 并且 unsat-core 如果该决定是 UNSAT?例如，解决方案可能如下所示:

In MathSAT 5 it just breaks on (get-model) and doesn't even reach (get-unsat-core). Is there any way in SMT-LIB 2.0 language to get-model iff the decision was SAT and unsat-core iff the decision was UNSAT? Solution could for example look like this:

(check-sat)
(ite (= (was-sat) true) (get-model) (get-unsat-core))

我搜索了 SMT-LIB 2.0 语言文档，但没有找到任何提示.

I searched SMT-LIB 2.0 language documentation, but I did not found any hint.

我也试过下面的代码，可惜没用.

I also tried the code below, and unfortunately it did not work.

(ite (= (check-sat) "sat") (get-model) (get-unsat-core))

推荐答案

SMT 语言不允许您编写这样的命令.工具(例如 Boogie)处理此问题的方式是使用双向文本管道:它从 (check-sat) 读回结果.如果结果字符串是unsat"，则模型不可用，但如果检查使用假设，则核心将是.如果由此产生字符串是sat"工具可以期望(get-model)命令成功.

The SMT language does not let you write commands like this. The way that tools, such as Boogie, deal with this is to use a two-way text pipe: It reads back the result from (check-sat). If the resulting string is "unsat" models are not available, but cores would be if the check uses asssumptions. If the resulting string is "sat" the tool can expect that a (get-model) command succeeds.

这篇关于根据求解器的决定执行 get-model 或 unsat-core的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！