desafortunadamente no tengo suficiente reputación para comentar las respuestas de otras preguntas. Así que tengo que empezar una nueva pregunta.

Esencialmente tengo el mismo problema que el descritoaquí. Quiero usar Z3 para resolución incremental. Para obtener las restricciones en Z3, uso cadenas smtlib2. Todo funciona bien para el primer conjunto de restricciones, donde puedo poner las declaraciones de variables, etc. directamente en la cadena smtlib2. Al agregar restricciones adicionales de forma incremental, Z3_parse_smtlib2_string necesita recibir el número de declaraciones anteriores (num_decls sin signo), las declaraciones (Z3_func_decl const decls []) y sus nombres (Z3_symbol const decl_names []). Para las cadenas smtlib, la interfaz del analizador ofrece funciones para recuperar esta información, por ejemplo, "Z3_get_smtlib_num_decls" y "Z3_get_smtlib_decl". Sin embargo, no funcionan para cadenas smtlib2.

Había una solución utilizando modelos. Para esta solución, Z3 debe devolver modelos que incluyan cada variable declarada ("modelos completos"), lo que parece no ser el caso por defecto. Se ha descrito una solución para este problema.aquí (para Z3 4.0). Desafortunadamente, esto ya no funciona para Z3 4.3.

¿Alguien tiene una idea de cómo puedo obtener modelos completos de Z3 que no dependen tanto de la versión utilizada? O incluso mejor: ¿Hay formas más directas de recuperar las declaraciones mientras tanto? Hace aproximadamente un año, Leonardo de Moura mencionó que habrá objetos "Parser" en el futuro que tendrán soporte para recuperar decls, fórmulas, etc. (verZ3 4.0: obtener el modelo completo). ¿Hay algo nuevo aquí que todavía no haya descubierto en la documentación?

¡Muchas gracias!

Elisabeth