【发布时间】：2016-05-18 17:37:05
【问题描述】：
我想做什么：我想打电话给(check-sat)，然后如果结果是unknown，就打电话给(check-sat-using qfnra-nlsat)。
我为什么要这样做？：对于我的应用程序，使用 (check-sat) 应用的 Z3 默认策略优于我使用 (check-sat-using) 设计的任何策略。但是，在少数情况下(check-sat) 返回unknown，但(check-sat-using ...) 采用明智选择的策略会找到结果。这是一个例子：
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun k () Int)
(assert (= z (* x y)))
(assert (= k (* i j)))
(assert (< k z))
; This returns unknown
(check-sat)
; This gives a solution
(check-sat-using qfnra-nlsat)
(get-value (x y z i j k))
我尝试了什么？： 我在单个 SMT 文件中最接近的是(check-sat-using (or-else smt qfnra-nlsat)). 不幸的是，就我的目的而言，(check-sat-using smt) 的性能不如 (check-sat)，所以这个不是一个选项。
【问题讨论】：
-
如果之前的结果是
unknown，您不能简单地读取(check-sat)的结果然后发出(check-sat-using qfnra-nlsat)吗？我一直通过 stdio 使用 Z3。 -
@MalteSchwerhoff 如果我在交互模式下使用 Z3，那么我可以这样做，是的。我正在使用的当前过程是编写一个完整的 .smt2 文件，以我的 .smt2 文件作为输入调用 Z3，然后读取结果。与让我的软件以交互方式或通过更复杂的 API 使用 Z3 相比，这具有一些优势。不过，您的建议也不错。