Il riferimento di conteggio riferimenti Z3_ast fa riferimento a Z3?

Question

In Z3 ci sono 2 modalità: conteggio automatico dei riferimenti e manuale.

Capisco come funziona il conteggio ref manuale. Grazie all'esempio.

Ma come fa Z3 a sapere quando eliminare il nodo AST nel caso di conteggio automatico dei casi? Poiché Z3_ast è una struct dal linguaggio C => è impossibile tenere traccia di tutti i compiti e gli usi di Z3_ast al di fuori di Z3 dopo la sua creazione.

O solo i riferimenti di traccia Z3 all'interno di Z3? Non si tratta di aggiornamenti ai contatori di riferimento se si fa ad esempio: ast1 = ast2.

Answer 1

La modalità automatica utilizza una politica molto semplice. Ogni volta che un AST viene restituito all'utente, Z3 lo memorizza su uno stack S e incrementa il suo contatore di riferimento. Quando viene eseguita la funzione Z3_push, Z3 salva la dimensione dello stack S. Quando viene eseguito il corrispondente Z3_pop, la dimensione dello stack S viene ripristinata e il contatore di riferimento degli AST spuntati dallo stack viene decrementato. Questa modalità è molto facile da usare, ma ha un problema principale: il consumo di memoria. Ad esempio, se non si utilizzano Z3_push e Z3_pop, tutti gli AST creati dall'utente non verranno mai eliminati.