smt2lib ayrıştırıcısının z3 ana kaynak kodunun anlaşılması ve izlenmesi

Question

z3 ana kaynak kodunu anlamak istiyorum.Için giriş tipi smt2 için ana dosyadan çağrıları takip etti. giriş ana dosya için bu tip aşağıdaki kod ile smtlib_frontend dosyası (hat 341) çağırır:

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

ve daha sonra, bu kullanımda, (hat 128) üzerinden smt2parser çağırır:

result = parse_smt2_commands(ctx, in); 

smt2parser.cpp içinde

ve adı yöntemde:

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(); 

}

I2 sorun vardır:İlk önce: p() ne anlama geliyor? ayrıştırıcı sınıfı sadece bir kurucuya sahiptir (ayrıştırıcı (ctx, is, etkileşimli, ps)) ve p adıyla herhangi bir yönteme sahip değildir.

saniye: bu yöntem çağrıldıktan sonra, bu dosya z3'teki smt2lib çözümlemesi için ana sınıftır ve "parse_cmd()" adında bir yönteme sahiptir. ayrıştırma işlemi. Ancak bu yönteme bir geri dönüş yoktur. kod

Answer 1

Bu çizgiler:

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

ortalama ve sonra işlev p.operator çağrı (4 argüman alır kurucu ile) "adı p olan bir tip smt2 nesne :: ayrıştırıcı yapı"() (argüman olmadan) ve sonucunu döndürür; bakınız here. (Parantezin ne anlama geldiğini yeniden tanımlamak "operatör aşırı yüklenmesi" olarak adlandırılır ve birçok dilde bulunan bir kavramdır.)

SMT2 bir komut dilidir, yani bir karşılaştırma dosyası, her biri bir parse_cmd çağrısı.