Z3_ast ağacında geçiş C/C++

Question

Kısacası, Z3_ast ağacından geçebilmeli ve düğümleri ile ilişkili verilere erişebilmem gerekir. Bunun nasıl yapılacağı konusunda herhangi bir doküman/örnek bulamıyor. Herhangi bir işaretçi yardımcı olacaktır. Uzunluğunda, smt2lib tip formüllerini Z3'e ayırmam, bazı değişkenleri sabit sübstitüsyonlar haline getirmem ve daha sonra başka bir ilgisiz SMT sovler ile uyumlu bir veri yapısında formül üretmem gerekir. Bu soru için önemli olan, bu soru için önemli, ancak metin formülleriyle besleyebildiğim bir komut satırı arabirimine sahip olmak yeterli değil. Sadece bir C API'si var). Bu formülü mistral formatında üretmek için, Z3_ast ağacını çaprazlamak ve formülü istenen formatta yeniden yapılandırmak zorunda kalacağım. Bunun nasıl yapılacağını gösteren herhangi bir belge/örnek bulamıyorum. Herhangi bir işaretçi yardımcı olacaktır.

Answer 1

z3++.h'da tanımlanan C++ yardımcı sınıflarını kullanmayı düşünün. Z3 dağılımı ayrıca bu sınıfları kullanan bir örnek içerir. İşte bir Z3 ifadesini geçen küçük bir kod parçası. Formüllerinizde niceleyiciler yoksa, is_quantifier() ve is_var() dallarını tutmanıza bile gerek yoktur.

void visit(expr const & e) { 
    if (e.is_app()) { 
     unsigned num = e.num_args(); 
     for (unsigned i = 0; i < num; i++) { 
      visit(e.arg(i)); 
     } 
     // do something 
     // Example: print the visited expression 
     func_decl f = e.decl(); 
     std::cout << "application of " << f.name() << ": " << e << "\n"; 
    } 
    else if (e.is_quantifier()) { 
     visit(e.body()); 
     // do something 
    } 
    else { 
     assert(e.is_var()); 
     // do something 
    } 
} 

void tst_visit() { 
    std::cout << "visit example\n"; 
    context c; 

    expr x = c.int_const("x"); 
    expr y = c.int_const("y"); 
    expr z = c.int_const("z"); 
    expr f = x*x - y*y >= 0; 

    visit(f); 
}