在Z3中有2种模式:自动参考计数和手动.
我理解手动引用计数的工作原理.谢谢你的例子.
但Z3如何知道何时在自动引用计数中删除AST节点？ 由于Z3_ast是来自C语言=>的结构,因此在创建Z3_ast之后,无法跟踪Z3_ast之外的所有赋值和用法.
或Z3仅在Z3内跟踪参考？例如,如果您执行以下操作,则不会对ref计数器进行更新:ast1 = ast2.
自动模式使用非常简单的策略.每当AST返回给用户时,Z3将其存储在堆栈上S并递增其引用计数器.Z3_push执行该功能时,Z3会保存堆栈的大小S.Z3_pop执行匹配时,将S恢复堆栈的大小,并且从堆栈弹出的AST的引用计数器递减.这种模式非常容易使用,但它有一个主要问题:内存消耗.例如,如果Z3_push和Z3_pop未使用,则永远不会删除用户创建的所有AST.
| 归档时间： |
|
| 查看次数： |
183 次 |
| 最近记录： |