Cuando se ejecuta Z3 sin lógica especificada, y(check-sat) se emite, la lógica endefault_tactic.cpp se utiliza para invocar condicionalmente al "mejor" solucionador. Me gustaría acceder a esta táctica predeterminada desde la interfaz SMT-LIB 2.

Intenté traducir la lógica de default_tactic.cpp a SMT-LIB, y se me ocurrió esto:

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

Esto "casi" funciona, en eso, si elimina las líneas connra, lirayqffpa, Z3 ejecutará esto sin problemas. Parece que esas tres tácticas no están expuestas con la interfaz SMT-LIB 2 de Z3 4.4.1. Sin embargo, otro problema con esto es que si la táctica predeterminada se actualiza en una futura revisión de Z3, cualquier estrategia codificada como la que escribí anteriormente no se actualizará.

Lo que realmente me gustaría hacer es emitir un comando como(check-sat-using default), o algo similar, y obtenga el mismo resultado que el obtenido con(check-sat). es posible?