Czy liczenie odwołań Z3_ast zawiera odniesienia poza Z3?

Question

W Z3 dostępne są 2 tryby: automatyczne liczenie odniesień i ręczne.

Rozumiem, jak działa ręczne liczenie wyników. Dzięki przykładowi.

Ale w jaki sposób Z3 wie, kiedy usunąć węzeł AST w przypadku automatycznego liczenia powtórzeń? Ponieważ Z3_ast jest strukturą z języka C => niemożliwe jest śledzenie wszystkich zadań i zwyczajów Z3_ast poza Z3 po jego utworzeniu.

Czy tylko odniesienia do Z3 wewnątrz Z3? To nie jest aktualizacja dla liczników punktów, jeśli robisz na przykład: ast1 = ast2.

Answer 1

Tryb automatyczny wykorzystuje bardzo prostą zasadę. Za każdym razem, gdy AST zostaje zwrócony do użytkownika, Z3 przechowuje go na stosie S i zwiększa jego licznik referencyjny. Po wykonaniu funkcji Z3_push, Z3 zapisuje rozmiar stosu S. Po wykonaniu dopasowanego Z3_pop, rozmiar stosu S zostaje przywrócony, a licznik odwołań AST wyrzuconych ze stosu jest zmniejszany. Ten tryb jest bardzo łatwy w użyciu, ale ma główny problem: zużycie pamięci. Na przykład, jeśli nie są używane Z3_push i Z3_pop, wszystkie AST utworzone przez użytkownika nigdy nie zostaną usunięte.