Z3 behaviour if inapplicable tactic is used?

Question

What is Z3's behavior in general if a tactic is applied that aught not be appropriate to the specific problem? For example:

(declare-fun x () Real)
(declare-fun y () Real)
(assert (= x (* y y)))
(check-sat-using qflia)

This specific example returns sat. I'm surprised by this, because the problem is not in QFLIA. I would have expected either an error, or unknown.

Is it safe to apply a tactic even if you don't know whether the tactic you're applying is actually applicable to the specific problem instance?

Douglas B. Staple Douglas B. Staple · Accepted Answer · 2016-05-27T13:21:33

Issuing (help-tactic) over the SMT-LIB 2 API gives a huge amount of information about the different built-in tactics and the options they support. Somewhere in there, you'll find:

- qflia builtin strategy for solving QF_LIA problems.
    add_bound_lower (rational) (default: -2) lower bound to be added to unbounded variables.
    add_bound_upper (rational) (default: 2) upper bound to be added to unbounded variables.
    ...
    fail_if_inconclusive (bool) (default: true) fail if found unsat (sat) for under (over) approximated goal.

An interesting parameter here is fail_if_inconclusive. As I understand it, this parameter means that, when using under-approximations such as add_bound_lower, unsat results will be converted to unknown. In fact, it seems to be impossible to get an unsat result when add_bounds is used.

I am not sure about this, but it seems that applying the qflia tactic to a goal not in QFLIA may also be treated as an under-approximation. This is less clear-cut than when using add-bounds, because really trivial unsat goals do indeed return unsat with qflia, even though they're outside QFLIA. For example, this returns unsat:

(declare-fun x () Real)
(assert (distinct x x))
(assert (= (* x x) 2.0))
(check-sat-using (using-params qflia :fail_if_inconclusive true))

My guess for the reason behind this surprising result is that probably (distinct x x) is enough to make the whole goal unsatisfiable in a preprocessing step.

Overall the strategy API seems to work as follows: it may be that useful results are obtained by using a seemingly inappropriate tactic, if that tactic includes an over or under approximation of the goal. If the goal becomes unsat or sat due to a mismatch between the tactic and the goal, then Z3 will fail (return unknown).

Z3 behaviour if inapplicable tactic is used?

1 Answers