smt2libパーサーのz3マスターソースコードを理解し、それに従う

Question

私はz3マスターソースコードを理解したいと思います。私はメインファイルからsmt2の入力種別の呼び出しに従いました。入力主このタイプのファイルについては、以下のコードを介してsmtlib_frontendファイル（ライン341）を呼び出し：

case IN_SMTLIB_2: 
memory::exit_when_out_of_memory(true, "(error \"out of memory\")"); 
return_value = read_smtlib2_commands(g_input_file); 
break; 

をし、この方法は、（ライン128）を介してsmt2parserを呼び出し：

result = parse_smt2_commands(ctx, in); 

smt2parser.cppで

と呼ばれる方法で：：

bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool 
interactive, params_ref const & ps) { 
    smt2::parser p(ctx, is, interactive, ps); 
    return p(); 

}

私は2問題を抱えています最初に：p（）はどういう意味ですか？パーサークラスには1つのコンストラクター（パーサー（ctx、is、interactive、ps））があり、pという名前のメソッドはありません。

second：呼び出し元のグラフは、このファイルがz3のsmt2libを解析するためのメインクラスである間に切断され、その名前が "parse_cmd（）"というメソッドを持ちます。構文解析操作。この方法には言及していません。

Answer 1

これらのコード行：

smt2::parser p(ctx, is, interactive, ps); 
return p(); 

）は平均「型SMT2のオブジェクトを構築::名前Pとパーサー」（4つの引数を取るコンストラクタを介して）、次いで、（機能p.operatorを呼び出します（引数なし）、その結果を返します。 hereを参照してください。

SMT2はコマンド言語です。つまり、ベンチマークファイルに一連のコマンドが含まれています。これらのコマンドのそれぞれは、コマンドをトリガします。 parse_cmdを呼び出します。