Z3 には、自動参照カウントと手動の 2 つのモードがあります。
手動参照カウントの仕組みを理解しています。例に感謝します。
しかし、自動参照カウントの場合、Z3 はどのようにして AST ノードを削除するかを知るのでしょうか? Z3_ast は C 言語の構造体であるため => Z3_ast が作成された後、Z3 の外部で Z3_ast のすべての割り当てと使用法を追跡することは不可能です。
または、Z3 は Z3 内のみの参照を追跡しますか? たとえば、ast1 = ast2 の場合、ref カウンターの更新は行われません。
自動モードでは、非常に単純なポリシーが使用されます。AST がユーザーに返されるたびに、Z3 はそれをスタックに格納し、Sその参照カウンターをインクリメントします。Z3_push関数が実行されると、Z3 はスタックのサイズを保存しますS。マッチングZ3_popが実行されると、スタックのサイズSが復元され、スタックからポップされた AST の参照カウンターが減分されます。このモードは非常に使いやすいですが、主な問題があります: メモリ消費です。たとえば、Z3_pushとZ3_popを使用しない場合、ユーザーが作成したすべての AST は削除されません。