z3 - 根据求解器的决定执行get-model或unsat-core

我想知道，SMT-LIB 2.0脚本中是否有可能访问求解器的最后一个可满足性决策（星期六，星期六，...）。例如，以下代码：

(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返回：

unsat
(error "model generation not enabled")

在MathSAT 5中，它只是中断（获取模型），甚至没有到达（获取非核心）。
如果决策是SAT，是否有非核心功能，如果决策是UNSAT，是否有SMT-LIB 2.0语言来建模？例如，解决方案可能如下所示：

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

我搜索了SMT-LIB 2.0语言文档，但没有发现任何提示。

编辑：
我也尝试了下面的代码，但不幸的是它没有用。

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

最佳答案

SMT语言不允许您编写这样的命令。
Boogie等工具处理此问题的方式是使用
双向文本管道：它从（check-sat）读取结果。
如果结果字符串为“ unsat”，则无法使用模型，但是
核心是支票是否使用假设。如果产生
字符串是“ sat”，该工具可以预期（get-model）命令
成功。