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