z3 C++インターフェイスでプルーフを有効にするにはどうすればよいですか？

Question

Z3のC++インターフェイスを使って校正を有効にするにはどうすればよいですか？私は次のように設定しようとしました：プロダクトプルーフをtrueにしましたが、そのラインのコメントを外すと、プルーフ（）を呼び出すラインのコメントを外す前に、ソリューションに推測を追加しようとするとクラッシュしました。例えば、C++ファイル内の関数に基づいて：

 void prove_example2(std::ostream& os) { 
     os << "prove_example2\n"; 

     context c; 
     solver s(c); 
     params p(c); 
     //p.set(":produce-proofs", true); 
     s.set(p); 

     expr x = c.int_const("x"); 
     expr y = c.int_const("y"); 
     expr z = c.int_const("z"); 
     sort I = c.int_sort(); 
     func_decl g = function("g", I, I); 

     expr conjecture1 = implies(g(g(x) - g(y)) != g(z) && x + z <= y && y <= x, 
      z < 0); 


     s.add(!conjecture1); 
     os << "conjecture 1:\n" << conjecture1 << "\n"; 
     if (s.check() == unsat) { 
      os << "proved" << "\n"; 
      // Needs setup before calling 
      //os << s.proof() << "\n"; 
     } 
     else 
      os << "failed to prove" << "\n"; 
} 

Answer 1

はtest_capi.cでmk_proof_contextを参照してください。証明は、ソルバとコンテキストの両方で有効にする必要があります。 C++では、コンテキストやソルバーを作成する前に、

z3::set_param("proof", "true"); 

でグローバルデフォルトパラメータを設定するのが最も簡単な方法です。