Traversing Z3_ast tree in C/C++

Question

W skrócie, potrzebuję móc przemierzać drzewo Z3_ast i uzyskiwać dostęp do danych powiązanych z jego węzłami. Nie można znaleźć żadnej dokumentacji/przykładów, jak to zrobić. Wszelkie wskazówki byłyby pomocne.

W końcu, muszę przeanalizować formuły typu smt2lib w Z3, wprowadzić zmienną do stałych zastępstw, a następnie odtworzyć formułę w strukturze danych, która jest kompatybilna z innym niespokrewnionym sovlerem SMT (mistral za konkretny, ja nie mysle, ze informacje na temat mistrala sa wazne dla tego pytania, ale na tyle zabawnie, ze nie ma interfejsu wiersza polece, w ktorym mozna podac formuly tekstowe. Ma po prostu API C). Doszedłem do wniosku, że aby wygenerować formułę w formacie mistral, będę musiał przejść drzewo Z3_ast i zrekonstruować formułę w pożądanym formacie. Nie mogę znaleźć żadnej dokumentacji/przykładów, które pokazują, jak to zrobić. Wszelkie wskazówki byłyby pomocne.

Answer 1

Rozważ użycie klas pomocniczych C++ zdefiniowanych pod z3++.h. Dystrybucja Z3 zawiera również przykład użycia tych klas. Oto mały fragment kodu, który przechodzi przez wyrażenie Z3. Jeśli formuły nie zawierają kwantyfikatorów, nie musisz nawet obsługiwać gałęzi is_quantifier() i is_var().

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