mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-20 17:14:43 +00:00
Code Activity

Fix RCFNum cleanup callback to avoid capturing 'this'

Browse source 
The cleanup callback was capturing 'this.ptr' which could cause issues
with the FinalizationRegistry. Changed to use a local variable 'myPtr'
instead, following the pattern used by other implementations in the
codebase (e.g., SolverImpl, ModelImpl).

Also format low-level rcf-example.ts for consistency.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-01-17 20:29:46 +00:00
parent 08a8b1cc71
commit 79bc59b792
2 changed files with 11 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/api/js/examples/low-level/rcf-example.ts
View file

@ -1,12 +1,12 @@
/**
* Example demonstrating the RCF (Real Closed Field) API in TypeScript.
*
*
* This example shows how to use RCF numerals to work with:
* - Transcendental numbers (pi, e)
* - Algebraic numbers (roots of polynomials)
* - Infinitesimals
* - Exact real arithmetic
*
*
* Note: The RCF API is exposed at the low-level API layer.
* Import from 'z3-solver' for low-level access.
*/
@ -96,9 +96,9 @@ async function rcfRootsExample() {
// Find roots of x^2 - 2 = 0
// Polynomial: -2 + 0*x + 1*x^2
const coeffs = [
Z3.rcf_mk_small_int(ctx, -2), // constant term
Z3.rcf_mk_small_int(ctx, 0), // x coefficient
Z3.rcf_mk_small_int(ctx, 1) // x^2 coefficient
Z3.rcf_mk_small_int(ctx, -2), // constant term
Z3.rcf_mk_small_int(ctx, 0), // x coefficient
Z3.rcf_mk_small_int(ctx, 1), // x^2 coefficient
];
const roots = new Array(coeffs.length);

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

@ -3413,14 +3413,16 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
constructor(ptr: Z3_rcf_num);
constructor(valueOrPtr: string | number | Z3_rcf_num) {
this.ctx = ctx;
let myPtr: Z3_rcf_num;
if (typeof valueOrPtr === 'string') {
this.ptr = check(Z3.rcf_mk_rational(contextPtr, valueOrPtr));
myPtr = check(Z3.rcf_mk_rational(contextPtr, valueOrPtr));
} else if (typeof valueOrPtr === 'number') {
this.ptr = check(Z3.rcf_mk_small_int(contextPtr, valueOrPtr));
myPtr = check(Z3.rcf_mk_small_int(contextPtr, valueOrPtr));
} else {
this.ptr = valueOrPtr;
myPtr = valueOrPtr;
}
cleanup.register(this, () => Z3.rcf_del(contextPtr, this.ptr), this);
this.ptr = myPtr;
cleanup.register(this, () => Z3.rcf_del(contextPtr, myPtr), this);
}
add(other: RCFNum<Name>): RCFNum<Name> {