Recorrido del árbol Z3_ast en C/C++

Question

En resumen, necesito poder atravesar el árbol Z3_ast y acceder a los datos asociados a sus nodos. Parece que no puede encontrar ninguna documentación/ejemplos sobre cómo hacer eso. Cualquier indicador será de ayuda.

Por fin, necesito analizar las fórmulas del tipo smt2lib en Z3, hacer algunas sustituciones variables constantes y luego reproducir la fórmula en una estructura de datos que sea compatible con otra sora SMT no relacionada (mistral para ser específico, no lo hago Creo que los detalles acerca de mistral son importantes para esta pregunta, pero curiosamente no tiene una interfaz de línea de comandos donde pueda alimentar las fórmulas de texto. Simplemente tiene una API de C). He pensado que para generar la fórmula en el formato de mistral, necesitaría atravesar el árbol Z3_ast y reconstruir la fórmula en el formato deseado. Parece que no puedo encontrar ninguna documentación/ejemplos que demuestren cómo hacerlo. Cualquier indicador será de ayuda.

Answer 1

Considere el uso de las clases auxiliares de C++ definidas en z3++.h. La distribución Z3 también incluye un ejemplo usando estas clases. Aquí hay un pequeño fragmento de código que atraviesa una expresión Z3. Si sus fórmulas no contienen cuantificadores, entonces ni siquiera necesita manejar las ramas is_quantifier() y 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); 
}