Quando o Z3 é executado sem lógica especificada, e(check-sat) é emitida, a lógica emdefault_tactic.cpp é usado para invocar condicionalmente o "melhor" solucionador. Gostaria de acessar essa tática padrão na interface SMT-LIB 2.

Tentei traduzir a lógica do default_tactic.cpp para o SMT-LIB e criei o seguinte:

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

Isso "quase" funciona, pois, se você excluir as linhas comnra, liraeqffpa, o Z3 executará isso sem problemas. Parece que essas três táticas não estão expostas com a interface SMT-LIB 2 do Z3 4.4.1. Outro problema com isso, porém, é que, se a tática padrão for atualizada em uma revisão futura do Z3, qualquer estratégia codificada como a que escrevi acima não será atualizada.

O que eu realmente gostaria de fazer é emitir um comando como(check-sat-using default)ou algo semelhante e obtenha o mesmo resultado que o obtido com(check-sat). Isso é possível?