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将不会被删除。