CODEWITHSUNDEEP
z3smt
Douglas B. Staple
Douglas B. Staple

Reputation: 10946

(check-sat) then (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).

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))

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.

Upvotes: 0

Views: 289

Answers (1)

Douglas B. Staple
Douglas B. Staple

Reputation: 10946

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))

This feature should be available with Z3 4.4.2 and greater.

Upvotes: 1

Related Questions