(check-sat) 然后 (check-sat-using qfnra-nlsat)

Question

我想做的事情：我想调用(check-sat)，然后如果结果是unknown，调用(check-sat-using qfnra-nlsat) .

我为什么要这样做？： 对于我的应用程序，使用 (check-sat) 应用的 Z3 默认策略优于我使用 [=15= 设计的任何策略].但是，在某些情况下 (check-sat) returns 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) 出于我的目的，所以这不是一个选项。

Answer 1

直接使用 (check-sat) 是不可能的，但是 (check-sat) 使用的 default 策略在之后暴露出来了。所以，在Z3当前的master分支中，可以这样写：

(check-sat-using (or-else default qfnra-nlsat))

此功能应适用于 Z3 4.4.2 及更高版本。

(check-sat) 然后 (check-sat-using qfnra-nlsat)

(check-sat) then (check-sat-using qfnra-nlsat)

smt

z3