了解并遵循 smt2lib 解析器的 z3 master 源代码

Question

我想了解 z3 主源代码 code.I 跟随主文件对 smt2 输入类型的调用。对于这种类型的输入主文件，通过以下代码（第 341 行）调用 smtlib_frontend 文件：

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() 是什么意思？ parser class 只有一个构造函数（parser (ctx, is, interactive, ps)）并且没有任何名为 p.

的方法

第二个：调用此方法后，调用者图将断开连接，而此文件是主要的 class 用于在 z3 中解析 smt2lib 并且有一个名称为 "parse_cmd()" 的方法似乎是开始解析操作的主要方法。但是没有参考这个方法。

Answer 1

这些代码行：

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

mean "construct an object of type smt2::parser with name p"（通过带 4 个参数的构造函数）然后调用函数 p.operator()（不带参数）和 return 结果；参见 here。（重新定义括号的意思叫"operator overloading"，是很多语言都存在的概念。）

SMT2 是一种命令语言，即基准文件包含一系列命令，每个命令都会触发对 parse_cmd 的调用。

了解并遵循 smt2lib 解析器的 z3 master 源代码

understanding and following z3 master source code of smt2lib parser

z3