i want understand z3 master source code.i followed calls main file input kind of smt2. type of input main file calls smtlib_frontend file via below code(line 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;
and method calls smt2parser via(line 128) :
result = parse_smt2_commands(ctx, in);
in smt2parser.cpp , in called method :
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();
}
i have 2 problem : first : p() mean? parser class has 1 constructor (parser (ctx, is, interactive, ps)) , don't have method name of p.
second : after calling method, caller graph disconnected while file main class parsing smt2lib in z3 , has method name "parse_cmd()" seems main method starting parsing operation. there no refrence method.
these lines of code:
smt2::parser p(ctx, is, interactive, ps); return p();
mean "construct object of type smt2::parser name p" (via constructor takes 4 arguments) , call function p.operator() (with no arguments) , return result; see here. (redefining parentheses mean called "operator overloading" , concept exists in many languages.)
smt2 command language, i.e., benchmark file contains series of commands, each of trigger call parse_cmd.
Comments
Post a Comment