Extracting SMT-LIB Formula

Question

Is there any way to extract a SMT-LIB formula, including all the declarations, definitions and constraints into a .smt2 file from the solver/model/context class of the C++ API. I.e. opposite of what the function "Z3_parse_smtlib2_string" does.

Answer 1

Good point. C++ lacks this function. The Python binding now has it for the solver class.

Here is a possible sketch:

    std::string to_smt2() {
        expr_vector es = assertions();
        ast* const* fmls = es.ptr();
        unsigned sz = es.size();
        if (sz > 0) {
            --sz;
            fml = fmls[sz];
        }
        else {
            fml = ctx().bool_val(true);
        }
        std::string result;
        result = Z3_benchmark_to_smtlib_string(ctx(),
                                               "", "", "", "", 
                                               sz, 
                                               fmls, 
                                               fml);
        return result;
    }