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

Question

Z3有2种模式：自动引用计数和手动。

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

但是在自动引用计数的情况下，Z3 是如何知道何时删除 AST 节点的呢？ 由于 Z3_ast 是来自 C 语言的结构 => 不可能在 Z3 之外跟踪 Z3_ast 在创建后的所有分配和使用。

还是仅 Z3 内部的 Z3 轨道参考？如果您这样做，则不会对 ref 计数器进行更新：ast1 = ast2。

Answer 1

自动模式使用非常简单的策略。每当 AST 返回给用户时，Z3 将其存储在堆栈中S并递增其引用计数器。当Z3_push函数执行时，Z3 保存栈的大小S。当Z3_pop执行匹配时，栈的大小S被恢复，从栈中弹出的 AST 的引用计数器递减。这种模式非常好用，但它有一个主要问题：内存消耗。例如，如果Z3_push和Z3_pop不使用，则用户创建的所有 AST 将永远不会被删除。