From f2dfee296649c8589b1fbf55d0648f6e799a70be Mon Sep 17 00:00:00 2001 From: Jonas Jongejan Date: Sat, 19 Oct 2024 16:10:20 -0400 Subject: [PATCH] js: Adding manual release methods --- src/api/js/src/high-level/high-level.ts | 41 ++++++++++++++++++++++- src/api/js/src/high-level/types.ts | 44 ++++++++++++++++++++++++- 2 files changed, 83 insertions(+), 2 deletions(-) diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 0869dbd7b..b980a5ffe 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -1235,6 +1235,11 @@ export function createApi(Z3: Z3Core): Z3HighLevel { toString() { return this.sexpr(); } + + release() { + Z3.dec_ref(contextPtr, this.ast); + cleanup.unregister(this); + } } class SolverImpl implements Solver { @@ -1327,6 +1332,11 @@ export function createApi(Z3: Z3Core): Z3HighLevel { Z3.solver_from_string(contextPtr, this.ptr, s); throwIfError(); } + + release() { + Z3.solver_dec_ref(contextPtr, this.ptr); + cleanup.unregister(this); + } } class OptimizeImpl implements Optimize { @@ -1422,8 +1432,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel { Z3.optimize_from_string(contextPtr, this.ptr, s); throwIfError(); } - } + release() { + Z3.optimize_dec_ref(contextPtr, this.ptr); + cleanup.unregister(this); + } + } class ModelImpl implements Model { declare readonly __typename: Model['__typename']; @@ -1594,6 +1608,11 @@ export function createApi(Z3: Z3Core): Z3HighLevel { _assertContext(sort); return new AstVectorImpl(check(Z3.model_get_sort_universe(contextPtr, this.ptr, sort.ptr))); } + + release() { + Z3.model_dec_ref(contextPtr, this.ptr); + cleanup.unregister(this); + } } class FuncEntryImpl implements FuncEntry { @@ -1656,6 +1675,11 @@ export function createApi(Z3: Z3Core): Z3HighLevel { assert(this.arity() === argsVec.length(), "Number of arguments in entry doesn't match function arity"); check(Z3.func_interp_add_entry(contextPtr, this.ptr, argsVec.ptr, value.ptr as Z3_ast)); } + + release() { + Z3.func_interp_dec_ref(contextPtr, this.ptr); + cleanup.unregister(this); + } } class SortImpl extends AstImpl implements Sort { @@ -1924,6 +1948,11 @@ export function createApi(Z3: Z3Core): Z3HighLevel { Z3.tactic_inc_ref(contextPtr, myPtr); cleanup.register(this, () => Z3.tactic_dec_ref(contextPtr, myPtr)); } + + release() { + Z3.tactic_dec_ref(contextPtr, this.ptr); + cleanup.unregister(this); + } } class ArithSortImpl extends SortImpl implements ArithSort { @@ -2675,6 +2704,11 @@ export function createApi(Z3: Z3Core): Z3HighLevel { sexpr(): string { return check(Z3.ast_vector_to_string(contextPtr, this.ptr)); } + + release() { + Z3.ast_vector_dec_ref(contextPtr, this.ptr); + cleanup.unregister(this); + } } class AstMapImpl, Value extends AnyAst> implements AstMap { @@ -2734,6 +2768,11 @@ export function createApi(Z3: Z3Core): Z3HighLevel { sexpr(): string { return check(Z3.ast_map_to_string(contextPtr, this.ptr)); } + + release() { + Z3.ast_map_dec_ref(contextPtr, this.ptr); + cleanup.unregister(this); + } } function substitute(t: Expr, ...substitutions: [Expr, Expr][]): Expr { diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index 6f3630a6d..c884126ff 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -663,6 +663,13 @@ export interface Solver { check(...exprs: (Bool | AstVector>)[]): Promise; model(): Model; + + /** + * Manually decrease the reference count of the solver + * This is automatically done when the solver is garbage collected, + * but calling this eagerly can help release memory sooner. + */ + release(): void; } export interface Optimize { @@ -695,8 +702,9 @@ export interface Optimize { check(...exprs: (Bool | AstVector>)[]): Promise; model(): Model; -} + release(): void; +} /** @hidden */ export interface ModelCtor { @@ -746,6 +754,13 @@ export interface Model extends Iterable, defaultValue: CoercibleToMap, Name>, ): FuncInterp; + + /** + * Manually decrease the reference count of the model + * This is automatically done when the model is garbage collected, + * but calling this eagerly can help release memory sooner. + */ + release(): void; } /** @@ -824,6 +839,13 @@ export interface FuncInterp { entry(i: number): FuncEntry; addEntry(args: Expr[], value: Expr): void; + + /** + * Manually decrease the reference count of the func interp + * This is automatically done when the func interp is garbage collected, + * but calling this eagerly can help release memory sooner. + */ + release(): void; } /** @hidden */ @@ -1608,6 +1630,13 @@ export interface Tactic { readonly ctx: Context; readonly ptr: Z3_tactic; + + /** + * Manually decrease the reference count of the tactic + * This is automatically done when the tactic is garbage collected, + * but calling this eagerly can help release memory sooner. + */ + release(): void; } /** @hidden */ @@ -1659,6 +1688,12 @@ export interface AstVector has(v: Item): boolean; sexpr(): string; + /** + * Manually decrease the reference count of the ast vector + * This is automatically done when the ast vector is garbage collected, + * but calling this eagerly can help release memory sooner. + */ + release(): void; } /** @hidden */ @@ -1717,6 +1752,13 @@ export interface AstMap< has(key: Key): boolean; sexpr(): string; + + /** + * Manually decrease the reference count of the ast map + * This is automatically done when the ast map is garbage collected, + * but calling this eagerly can help release memory sooner. + */ + release(): void; } /**