Z3_ast引用計數是否在Z3外計數引用？

Question

在Z3中有兩種模式：自動參考計數和手動。

我瞭解手動參考計數是如何工作的。感謝例子。

但是Z3如何知道何時在自動重新計數情況下刪除AST節點？ 由於Z3_ast是C語言中的一個結構，所以不可能在Z3創建後追蹤Z3之外的所有分配和用法。

或者Z3只在Z3中追蹤引用？這是沒有更新的ref計數器，如果你做，例如：ast1 = ast2。

Answer 1

自動模式使用一個非常簡單的策略。每當AST返回給用戶時，Z3將其存儲在堆棧S上並遞增其引用計數器。 執行Z3_push函數時，Z3保存堆棧的大小S。當匹配Z3_pop被執行時，堆棧S的大小被恢復，並且從堆棧彈出的AST的引用計數器遞減。 此模式非常易於使用，但它有一個主要問題：內存消耗。例如，如果不使用Z3_push和Z3_pop，則用戶創建的所有AST將不會被刪除。