Probe is-unbounded vs. is-lia, is-nia, etc

[bobismijnnaam]

I have a question about the is-unbounded probe. If this probe is true, does that mean that none of the support of z3 for the lia/nia/nra/lra/nira fragments can be used? Or does the is-unbounded probe mean, you have some unbounded constants in your smt file (goals?), but z3 will still try to use specialized support lia/nia/etc. proof goals.

I'm interested in this because we'd like our tool to give feedback to the user when smt is generated that goes into a harder fragment. More specifically, we're interested in knowing when the solver starts reasoning about nonlinear arithmetic, as this is usually problematic. However we'd also be interested to know when, e.g., z3 starts reasoning in a real fragment.

(For context, even more generally: we'd like to give the user some information about what z3 is having a hard time with, and we thought maybe knowing what fragment z3 is considering is a good start. We're also considering axiom profiler to debug quantifiers, but that seems difficult, as axiom profiler seems to freeze when it imports logs emitted by z3.)

Finally, is it intentional that the probes are strictly exclusive? Meaning, that either the is-nia probe is true, OR the is-nira, but not both. Intuitively I would say they overlap a bit but in practice z3 seems to consider them strictly separate.

[NikolajBjorner]

The specification of is-unbounded is that the goal contains a real or integer variable that either does not have an upper or lower bound. If every variable (uninterpreted sub-term of type int/real) have both a lower and upper bound assertion, the probe returns false.

lia tactics use this to probe a goal whether it can be translated to SAT (finite domains).
If a goal is bounded and contains only integers the default tactic for QF_LIA attempts to throw the problem at a SAT solver (bit-vector formulation). It can also translate unbounded problems into SAT, as an under-approximation.

The output of tactics used is currently only really available if you run z3 in verbose=10 and above.
It prints names of tactics that are applied to std-err.

I would like to graduate from the axiom profiler. The alternative mechanism is to set solver.proof.log=z3prooflog.smt2.
It dumps all generated clauses in SMTLIB2 format.
You can use z3 to parse the log and add callbacks to post-process what it parses.
https://microsoft.github.io/z3guide/programming/Proof%20Logs
There are some examples of how to use post-process proof logs from Python.
A disclaimer is that proof log reparsing remains to have some work in progress: it doesn't reliably create re-parsable output when you use recursive functions (maybe fixed), lambdas, sequences, but has been harnessed for pure benchmark categories.

I think the intent with the probes named after benchmark categories is-nia, is-nira is to establish proper classification according to the conventions used in SMTLIB.
So is-nira requires some occurrence of a real, integer and non-linear multiplication.

[bobismijnnaam]

Thank you for the explanation! That clears it up for me. The proof logs look very promising.