(check-sat-using default) or similar?

Question

When Z3 is run with no logic specified, and (check-sat) is issued, the logic in default_tactic.cpp is used to conditionally invoke the "best" solver. I would like to access this default tactic from the SMT-LIB 2 interface.

I tried translating the logic from default_tactic.cpp into SMT-LIB, and I came up with this:

(check-sat-using (and-then simplify
    (cond is-qfbv qfbv
    (cond is-qflia qflia
    (cond is-qflra qflra
    (cond is-qfnra qfnra
    (cond is-qfnia qfnia
    (cond is-nra nra
    (cond is-lira lira
    (cond is-qffpabv qffpa
    smt))))))))))

This "almost" works, in that, if you delete the lines with nra, lira, and qffpa, then Z3 will execute this without issue. It seems that those three tactics are not exposed with the SMT-LIB 2 interface of Z3 4.4.1. Another problem with this, though, is that if the default tactic is updated in a future revision of Z3, then any hard-coded strategy like what I wrote above would not be updated.

What I would really like to do is issue a command like (check-sat-using default), or something similar, and get the same result as as obtained with (check-sat). Is this possible?

Answer 1

The file you refer to is very old. Z3 has since moved to GitHub and the latest version of default_tactic.cpp is here.

The default tactic for QF_FP is now called qffp, the lira tactic has since been exported as well and I just exported nra as well (as of this commit).

---

Edit: As of this commit, the default tactic has also been exported, so it's now possible to write (check-sat-using default) as requested.