z3 - unsat コア トラックの SMT-LIB v2 形式からの名前付き用語のリスト

Question

「a_ uc _1」などの名前リストと名前リストの量で用語を記録または印刷するz3 APIの使用方法は?

Answer 1

残念ながら、あなたが望むことを行うための API はありません。この情報は内部で利用できますが、API では公開されません。この情報を抽出するために Z3 コードを変更することは難しくありません。内部的には、SMT-LIB v2 ファイルを解析するために次の関数が使用されます。

bool parse_smt2_commands(cmd_context & ctx, 
                         std::istream & is, 
                         bool interactive = false, 
                         params_ref const & p = params_ref());

ファイルで定義されていますsrc/parsers/smt2/smt2parser.h。

cmd_contextオブジェクトは object で定義されますsrc/cmd_context/cmd_context.h。

次のメソッドがあります。

ptr_vector<expr>::const_iterator begin_assertion_names() const;
ptr_vector<expr>::const_iterator end_assertion_names() const;

これら 2 つの方法を使用して、SMT-LIB v2 ファイル内のアサーションの名前付けに使用されるすべての名前をトラバースできます。各名前は内部的にブール変数として表されます。ctxが の場合cmd_context、次を使用してすべての名前をトラバースできます。

ptr_vector<expr>::const_iterator it = ctx.begin_assertion_names();
for (; it != ctx.end_assertion_names(); it++) {
   expr * n = *it;
   // do something
   // here, we just print the name
   std::cout << to_app(n)->get_decl()->get_name() << "\n";
}