Z3 - arguments for check-sat-using

Question

Apologies if this is a stupid question - I'm quite new to using Z3 (and SMT in general) - but I am a bit stumped.

Say I have two files in the SMT2 input language, with minor differences, summarized as:

(define-fun T ((i Int)) Bool (... - too long to paste completely, but does define $prop)
(assert (T 0))
(declare-fun assum1 () Bool)
(assert (=> assum1 (not (and ($prop 0)))))
(check-sat assum1)

Now, one of these (the simpler one) returns "sat", the variant with more complex non-linear math returns "unknown".

I think that the more complex variant could be solved with a non-linear solver such as qfnra-nlsat (or perhaps other strategies), but trying to use it with check-sat-using:

(check-sat-using qfnra-nlsat assum1)

returns:

(error "line 246 column 29: invalid command argument, keyword expected")

However, not explicitly naming function assum1

(check-sat-using qfnra-nlsat)

runs, but gives me an "unknown" result.

So, my question is - how can I choose my solver and apply it specifically to the function "assum1"?

Thanks for your help.

Answer 1

The arguments for check-sat and check-sat-using are not the same. While check-sat takes a set of assumptions (Boolean literals), check-sat-using expects a tactic that is to be applied to the current goal (like the 'apply' command), it does not take assumptions. The difference between apply and check-sat-using is that the latter applies the tactic and then checks whether the result is the empty goal or a false goal. (For more information about goals and tactics in Z3 see the strategies tutorial.)

For this particular example, I think it would be easiest to assert assum1 into the goal before you apply qfnra-nlsat (which means you would have to construct a new goal if any of the assumptions change).

The nlsat tactic is also applied by default if the problem is in QF_NRA, but it might require an explicit

(set-logic QF_NRA)

in the beginning of the file to make sure that it is applied.