CODEWITHSUNDEEP
z3
Shambo
Shambo

Reputation: 946

Extracting SMT-LIB Formula

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.

Upvotes: 2

Views: 457

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

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;
    }

Upvotes: 4

Related Questions