mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

js: Adding manual release methods

Browse source
This commit is contained in:
Jonas Jongejan 2024-10-19 16:10:20 -04:00
parent a23a8cdfc5
commit f2dfee2966
2 changed files with 83 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

41
src/api/js/src/high-level/high-level.ts
View file

@ -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<Name> {
@ -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<Name> {
@ -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<Name> {
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<Name> {
@ -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<Z3_sort> implements Sort<Name> {
@ -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<Name> {
@ -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<Key extends AnyAst<Name>, Value extends AnyAst<Name>> implements AstMap<Name, Key, Value> {
@ -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<Name>, ...substitutions: [Expr<Name>, Expr<Name>][]): Expr<Name> {

44
src/api/js/src/high-level/types.ts
View file

@ -663,6 +663,13 @@ export interface Solver<Name extends string = 'main'> {
check(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): Promise<CheckSatResult>;
model(): Model<Name>;
/**
* 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<Name extends string = 'main'> {
@ -695,8 +702,9 @@ export interface Optimize<Name extends string = 'main'> {
check(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): Promise<CheckSatResult>;
model(): Model<Name>;
}
release(): void;
}
/** @hidden */
export interface ModelCtor<Name extends string> {
@ -746,6 +754,13 @@ export interface Model<Name extends string = 'main'> extends Iterable<FuncDecl<N
decl: FuncDecl<Name, DomainSort, RangeSort>,
defaultValue: CoercibleToMap<SortToExprMap<RangeSort, Name>, Name>,
): FuncInterp<Name>;
/**
* 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<Name extends string = 'main'> {
entry(i: number): FuncEntry<Name>;
addEntry(args: Expr<Name>[], value: Expr<Name>): 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<Name extends string = 'main'> {
readonly ctx: Context<Name>;
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<Name extends string = 'main', Item extends Ast<Name>
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;
}
/**