understanding and following z3 master source code of smt2lib parser -


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