我想知道 SMT-LIB 2.0 脚本中是否有可能访问求解器的最后一个可满足性决策(sat、unsat,...)。例如,以下代码:
(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 中,它只是中断 (get-model),甚至达不到 (get-unsat-core)。
SMT-LIB 2.0 语言中是否有任何方法可以在决策为 SAT 时获取模型并在决策为 UNSAT 时获取 unsat-core ?例如,解决方案可能如下所示:
(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) 命令
成功了。
本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)