提取SMT-LIB公式

Question

是否有任何方法从C++ API的solver/model/context类中提取SMT-LIB公式，包括将所有声明，定义和约束条件提取到.smt2文件中。即与函数“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; 
    }