mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-19 16:53:18 +00:00
Code Activity

Format code with prettier for RCF API implementation

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-01-17 18:50:50 +00:00
parent b1291041e0
commit b5b1af3de7
4 changed files with 57 additions and 56 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/api/js/examples/high-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: 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);

30
src/api/js/src/high-level/high-level.test.ts
View file

@ -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);
});

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

@ -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<Name>[]) => {
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<Name>[] = [];
for (let i = 0; i < numRoots; i++) {
result.push(new RCFNumImpl(rootPtrs[i]));
}
return result;
},
}
) as RCFNumCreation<Name>;
roots: (coefficients: RCFNum<Name>[]) => {
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<Name>[] = [];
for (let i = 0; i < numRoots; i++) {
result.push(new RCFNumImpl(rootPtrs[i]));
}
return result;
},
}) as RCFNumCreation<Name>;
const BitVec = {
sort<Bits extends number>(bits: Bits): BitVecSort<Bits, Name> {
@ -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<Name>, q: Arith<Name>, x: Arith<Name>): Promise<AstVector<Name, Arith<Name>>> {
async function polynomialSubresultants(
p: Arith<Name>,
q: Arith<Name>,
x: Arith<Name>,
): Promise<AstVector<Name, Arith<Name>>> {
const result = await Z3.polynomial_subresultants(contextPtr, p.ast, q.ast, x.ast);
return new AstVectorImpl<ArithImpl>(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({

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

@ -184,12 +184,12 @@ export interface Context<Name extends string = 'main'> {
/**
* 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<Name extends string = 'main'> extends Iterable<FuncDecl<N
export interface StatisticsEntry<Name extends string = 'main'> {
/** @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<Name extends string> {
/**
* 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<Name extends string = 'main'> extends Iterable<StatisticsEntry<Name>> {
@ -1992,26 +1992,26 @@ export interface RatNum<Name extends string = 'main'> extends Arith<Name> {
/**
* 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<Name extends string> {
/**
* 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
*/