¿Z3_ast referencias de conteo de conteo fuera de Z3?

Question

En Z3 hay 2 modos: conteo automático de referencias y manual.

Entiendo cómo funciona el recuento manual de ref. Gracias al ejemplo.

Pero, ¿cómo sabe Z3 cuándo eliminar el nodo AST en el caso de recuento de ref automático? Dado que Z3_ast es una estructura de lenguaje C => es imposible realizar un seguimiento de todas las asignaciones y usos de Z3_ast fuera de Z3 después de su creación.

¿O referencias de seguimiento Z3 dentro de Z3 solamente? Eso no es actualizaciones para ref contadores se hacen si lo hace, por ejemplo: ast1 = ast2.

Answer 1

El modo automático utiliza una política muy simple. Cada vez que se devuelve un AST al usuario, Z3 lo almacena en una pila S e incrementa su contador de referencia. Cuando se ejecuta la función Z3_push, Z3 guarda el tamaño de la pila S. Cuando se ejecuta la coincidencia Z3_pop, se restaura el tamaño de la pila S, y se reduce el contador de referencia de los AST que salieron de la pila. Este modo es muy fácil de usar, pero tiene un problema principal: el consumo de memoria. Por ejemplo, si no se utilizan Z3_push y Z3_pop, entonces nunca se eliminarán todos los AST creados por el usuario.