z3 - Z3_ast 是否引用计数 Z3 之外的引用？

Question

Z3 有两种模式:自动引用计数和手动。

我了解手动引用计数的工作原理。感谢例子。

但是在自动引用计数的情况下，Z3 怎么知道什么时候删除 AST 节点呢？
由于 Z3_ast 是 C 语言中的一个结构体 => 不可能在 Z3 创建后跟踪 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 将永远不会被删除。