diff --git a/src/api/js/examples/high-level/rcf-example.ts b/src/api/js/examples/high-level/rcf-example.ts index a5f021e28..6b26d5da5 100644 --- a/src/api/js/examples/high-level/rcf-example.ts +++ b/src/api/js/examples/high-level/rcf-example.ts @@ -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: This example uses the high-level API for a cleaner interface. */ @@ -76,9 +76,9 @@ async function rcfRootsExample() { // Find roots of x^2 - 2 = 0 // Polynomial: -2 + 0*x + 1*x^2 const coeffs = [ - RCFNum(-2), // constant term - RCFNum(0), // x coefficient - RCFNum(1) // x^2 coefficient + RCFNum(-2), // constant term + RCFNum(0), // x coefficient + RCFNum(1), // x^2 coefficient ]; const roots = RCFNum.roots(coeffs); diff --git a/src/api/js/src/high-level/high-level.test.ts b/src/api/js/src/high-level/high-level.test.ts index cc449ad11..413fcce30 100644 --- a/src/api/js/src/high-level/high-level.test.ts +++ b/src/api/js/src/high-level/high-level.test.ts @@ -2136,23 +2136,23 @@ describe('high-level', () => { // x^2 - 2 = 0 has roots ±√2 // Polynomial: -2 + 0*x + 1*x^2 const coeffs = [ - RCFNum(-2), // constant term - RCFNum(0), // x coefficient - RCFNum(1) // x^2 coefficient + RCFNum(-2), // constant term + RCFNum(0), // x coefficient + RCFNum(1), // x^2 coefficient ]; - + const roots = RCFNum.roots(coeffs); expect(roots.length).toBe(2); - + // All roots should be algebraic roots.forEach(root => { expect(root.isAlgebraic()).toBe(true); }); - + // Check that roots are approximately ±√2 const root1Decimal = roots[0].toDecimal(5); const root2Decimal = roots[1].toDecimal(5); - + // One should be approximately 1.414 and the other -1.414 const decimals = [root1Decimal, root2Decimal].sort(); expect(decimals[0]).toContain('-1.4'); @@ -2162,7 +2162,7 @@ describe('high-level', () => { it('should check isRational predicate', () => { const rational = RCFNum('3/4'); const pi = RCFNum.pi(); - + expect(rational.isRational()).toBe(true); expect(pi.isRational()).toBe(false); }); @@ -2171,9 +2171,9 @@ describe('high-level', () => { // x^2 - 2 = 0 const coeffs = [RCFNum(-2), RCFNum(0), RCFNum(1)]; const roots = RCFNum.roots(coeffs); - + expect(roots[0].isAlgebraic()).toBe(true); - + // Pi is not algebraic const pi = RCFNum.pi(); expect(pi.isAlgebraic()).toBe(false); @@ -2183,7 +2183,7 @@ describe('high-level', () => { const pi = RCFNum.pi(); const e = RCFNum.e(); const rational = RCFNum(5); - + expect(pi.isTranscendental()).toBe(true); expect(e.isTranscendental()).toBe(true); expect(rational.isTranscendental()).toBe(false); @@ -2192,7 +2192,7 @@ describe('high-level', () => { it('should check isInfinitesimal predicate', () => { const eps = RCFNum.infinitesimal(); const rational = RCFNum(5); - + expect(eps.isInfinitesimal()).toBe(true); expect(rational.isInfinitesimal()).toBe(false); }); @@ -2201,7 +2201,7 @@ describe('high-level', () => { const pi = RCFNum.pi(); const compact = pi.toString(true); const nonCompact = pi.toString(false); - + // Both should contain 'pi' or similar representation expect(compact.length).toBeGreaterThan(0); expect(nonCompact.length).toBeGreaterThan(0); @@ -2211,7 +2211,7 @@ describe('high-level', () => { const pi = RCFNum.pi(); const decimal5 = pi.toDecimal(5); const decimal10 = pi.toDecimal(10); - + // 10 decimal places should be longer than 5 expect(decimal10.length).toBeGreaterThanOrEqual(decimal5.length); expect(decimal5).toContain('3.14'); @@ -2221,7 +2221,7 @@ describe('high-level', () => { it('should work with infinitesimal comparisons', () => { const eps = RCFNum.infinitesimal(); const tiny = RCFNum('1/1000000'); - + // Infinitesimal should be smaller than any positive real expect(eps.lt(tiny)).toBe(true); }); diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 8a2bc9fe7..22d2a98ba 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -835,27 +835,24 @@ export function createApi(Z3: Z3Core): Z3HighLevel { }, }; - const RCFNum = Object.assign( - (value: string | number) => new RCFNumImpl(value), - { - pi: () => new RCFNumImpl(check(Z3.rcf_mk_pi(contextPtr))), + const RCFNum = Object.assign((value: string | number) => new RCFNumImpl(value), { + pi: () => new RCFNumImpl(check(Z3.rcf_mk_pi(contextPtr))), - e: () => new RCFNumImpl(check(Z3.rcf_mk_e(contextPtr))), + e: () => new RCFNumImpl(check(Z3.rcf_mk_e(contextPtr))), - infinitesimal: () => new RCFNumImpl(check(Z3.rcf_mk_infinitesimal(contextPtr))), + infinitesimal: () => new RCFNumImpl(check(Z3.rcf_mk_infinitesimal(contextPtr))), - roots: (coefficients: RCFNum[]) => { - assert(coefficients.length > 0, 'Polynomial coefficients cannot be empty'); - const coeffPtrs = coefficients.map(c => (c as RCFNumImpl).ptr); - const { rv: numRoots, roots: rootPtrs } = Z3.rcf_mk_roots(contextPtr, coeffPtrs); - const result: RCFNum[] = []; - for (let i = 0; i < numRoots; i++) { - result.push(new RCFNumImpl(rootPtrs[i])); - } - return result; - }, - } - ) as RCFNumCreation; + roots: (coefficients: RCFNum[]) => { + assert(coefficients.length > 0, 'Polynomial coefficients cannot be empty'); + const coeffPtrs = coefficients.map(c => (c as RCFNumImpl).ptr); + const { rv: numRoots, roots: rootPtrs } = Z3.rcf_mk_roots(contextPtr, coeffPtrs); + const result: RCFNum[] = []; + for (let i = 0; i < numRoots; i++) { + result.push(new RCFNumImpl(rootPtrs[i])); + } + return result; + }, + }) as RCFNumCreation; const BitVec = { sort(bits: Bits): BitVecSort { @@ -1776,7 +1773,11 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return new FuncDeclImpl(check(Z3.mk_transitive_closure(contextPtr, f.ptr))); } - async function polynomialSubresultants(p: Arith, q: Arith, x: Arith): Promise>> { + async function polynomialSubresultants( + p: Arith, + q: Arith, + x: Arith, + ): Promise>> { const result = await Z3.polynomial_subresultants(contextPtr, p.ast, q.ast, x.ast); return new AstVectorImpl(check(result)); } @@ -2492,7 +2493,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { const key = Z3.stats_get_key(contextPtr, this.ptr, i); const isUint = Z3.stats_is_uint(contextPtr, this.ptr, i); const isDouble = Z3.stats_is_double(contextPtr, this.ptr, i); - const value = isUint + const value = isUint ? Z3.stats_get_uint_value(contextPtr, this.ptr, i) : Z3.stats_get_double_value(contextPtr, this.ptr, i); result.push({ diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index 6c3c0aae2..539b287f3 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -184,12 +184,12 @@ export interface Context { /** * Set the pretty printing mode for ASTs. - * + * * @param mode - The print mode to use: * - Z3_PRINT_SMTLIB_FULL (0): Print AST nodes in SMTLIB verbose format. * - Z3_PRINT_LOW_LEVEL (1): Print AST nodes using a low-level format. * - Z3_PRINT_SMTLIB2_COMPLIANT (2): Print AST nodes in SMTLIB 2.x compliant format. - * + * * @category Functions */ setPrintMode(mode: Z3_ast_print_mode): void; @@ -1523,16 +1523,16 @@ export interface Model extends Iterable { /** @hidden */ readonly __typename: 'StatisticsEntry'; - + /** The key/name of this statistic */ readonly key: string; - + /** The numeric value of this statistic */ readonly value: number; - + /** True if this statistic is stored as an unsigned integer */ readonly isUint: boolean; - + /** True if this statistic is stored as a double */ readonly isDouble: boolean; } @@ -1543,8 +1543,8 @@ export interface StatisticsCtor { /** * Statistics for solver operations - * - * Provides access to performance metrics, memory usage, decision counts, + * + * Provides access to performance metrics, memory usage, decision counts, * and other diagnostic information from solver operations. */ export interface Statistics extends Iterable> { @@ -1992,26 +1992,26 @@ export interface RatNum extends Arith { /** * A Real Closed Field (RCF) numeral. - * + * * RCF numerals can represent: * - Rational numbers * - Algebraic numbers (roots of polynomials) * - Transcendental extensions (e.g., pi, e) * - Infinitesimal extensions - * + * * ```typescript * const { RCFNum } = Context('main'); - * + * * // Create pi * const pi = RCFNum.pi(); * console.log(pi.toDecimal(10)); // "3.1415926536" - * + * * // Create a rational * const half = new RCFNum('1/2'); - * + * * // Arithmetic * const sum = pi.add(half); - * + * * // Check properties * console.log(pi.isTranscendental()); // true * console.log(half.isRational()); // true @@ -2187,9 +2187,9 @@ export interface RCFNumCreation { /** * Find roots of a polynomial. - * + * * The polynomial is a[n-1]*x^(n-1) + ... + a[1]*x + a[0]. - * + * * @param coefficients - Polynomial coefficients (constant term first) * @returns Array of RCF numerals representing the roots */