Is it possible to get the equisatisfiable boolean formula of a QF_UF formula using existing SMT solvers?

Question

In eager SMT solvers, a SMT formula is encoded as a equisatisfiable boolean formula which is fed to a SAT solver. Typically, for QF_UF formulae, uninterpreted functions are reduced by Ackermann's reduction or Bryant's reduction, and then a equisatisfiable boolean formula is constructed by equality graph approach.

So I want to know if it is possible to invoke an existing SMT solver to get the equisatisfiable boolean formula given a QF_UF formula without hacking the low-level implementation of the solver. For example, Z3 has some tactics to transform the input problem (such as tseitin-cnf and elim-term-ite), and is there a tactic for such translation?

Answer 1

In z3 you can dump DIMACS with a patch like https://gist.github.com/nunoplopes/8cd9fb433b2663c99cb34c8a95ae812f

You can also use the bit-blast tactic to get the SAT formula, which will be over Boolean Z3 variables. I don't think that's guaranteed to be in CNF or NNF or whatever form.