提取SMT-LIB公式

Question

是否有任何方法从.smt2 API的求解器/模型/上下文类中提取SMT公式，包括所有的声明、定义和约束到C++文件中。即与"Z3_parse_smtlib2_string“函数相反的功能。

Answer 1

说得好。C++缺乏此功能。Python绑定现在为解决器类提供了它。

下面是一个可能的草图：

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