Подсчитывает ли Z3_ast подсчет ссылок за пределами Z3?

Question

В Z3 есть 2 режима: автоматический подсчет ссылок и ручной.

Я понимаю, как работает ручной подсчет ссылок. Благодаря примеру.

Но как Z3 узнает, когда удалять узел AST в случае автоматического повторного подсчета? Поскольку Z3_ast является структурой из языка C =>, невозможно отследить все назначения и использования Z3_ast за пределами Z3 после его создания.

Или ссылки трека Z3 только внутри Z3? То есть обновления счетчиков ссылок не выполняются, если вы, например, выполните: ast1 = ast2.

Answer 1

Автоматический режим использует очень простую политику.Всякий раз, когда AST возвращается пользователю, Z3 сохраняет его в стеке S и увеличивает его счетчик ссылок.При выполнении функции Z3_push Z3 сохраняет размер стека S.Когда выполняется сопоставление Z3_pop, размер стека S восстанавливается и счетчик ссылок AST, извлеченных из стека, уменьшается.Этот режим очень прост в использовании, но у него есть главная проблема: потребление памяти.Например, если Z3_push и Z3_pop не используются, то все AST, созданные пользователем, никогда не будут удалены.