(check-sat) 然后 (check-sat-using qfnra-nlsat) [英] (check-sat) then (check-sat-using qfnra-nlsat)

问题描述

我想做什么:我想调用(check-sat)，然后如果结果是unknown，调用(check-sat-using qfnra-nlsat).

What I want to do: I would like to call (check-sat), and then if the result is unknown, call (check-sat-using qfnra-nlsat).

我为什么要这样做?:对于我的应用程序，使用 (check-sat) 应用的 Z3 默认策略优于我使用 (check-sat-using).但是，在某些情况下，(check-sat) 返回 unknown，但 (check-sat-using ...) 会明智地返回选择的策略找到结果.下面是一个例子:

Why do I want to do this?: For my application the Z3 default tactics applied with (check-sat) are superior to anything I have devised using (check-sat-using). However, there are a few situations where (check-sat) returns unknown, but (check-sat-using ...) with judiciously chosen tactics finds a result. Here is an example:

(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)，所以这不是一个选项.

What have I tried?: The closest I've come in a single SMT file is(check-sat-using (or-else smt qfnra-nlsat)). Unfortunately (check-sat-using smt) does not perform as well as (check-sat) for my purposes, so this is not an option.

推荐答案

这不能直接使用 (check-sat)，而是 default 使用的策略 代码>(check-sat) 在这个问题之后公开.所以，在Z3当前的master分支中，可以这样写:

This is not possible directly using (check-sat), but the default tactic used by (check-sat) was exposed following this question. So, in the current master branch of Z3, it's possible to write:

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

Z3 4.4.2 及更高版本应提供此功能.

This feature should be available with Z3 4.4.2 and greater.

这篇关于(check-sat) 然后 (check-sat-using qfnra-nlsat)的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！