diff --git a/src/api/js/RCF_API_IMPLEMENTATION.md b/src/api/js/RCF_API_IMPLEMENTATION.md deleted file mode 100644 index bd278f206..000000000 --- a/src/api/js/RCF_API_IMPLEMENTATION.md +++ /dev/null @@ -1,306 +0,0 @@ -# RCF API Implementation for TypeScript - -This document describes the newly implemented Real Closed Field (RCF) API for the TypeScript bindings of Z3. - -## Overview - -The RCF API provides support for exact real arithmetic with: -- **Rational numbers** - Exact representation of fractions -- **Algebraic numbers** - Roots of polynomials with rational coefficients -- **Transcendental numbers** - π, e, and other transcendental constants -- **Infinitesimals** - Numbers smaller than any positive real number - -## Status - -✅ **COMPLETE** - All 38 RCF functions are now available in TypeScript - -The TypeScript bindings now have **100% feature parity** with Python, Java, C#, and C++ for RCF operations. - -## API Reference - -### Creation Functions (6 functions) - -#### Constructor -```typescript -const { RCFNum } = Context('main'); - -// From string (rational) -const half = RCFNum('1/2'); -const pi_over_two = RCFNum('3.14159'); - -// From integer -const five = RCFNum(5); -``` - -#### Static Creation Methods -```typescript -// Transcendental constants -const pi = RCFNum.pi(); -const e = RCFNum.e(); - -// Infinitesimal -const epsilon = RCFNum.infinitesimal(); - -// Polynomial roots -// Find roots of x^2 - 2 = 0 (yields ±√2) -const coeffs = [RCFNum(-2), RCFNum(0), RCFNum(1)]; -const roots = RCFNum.roots(coeffs); -``` - -### Arithmetic Operations (7 functions) - -```typescript -const a = RCFNum(5); -const b = RCFNum(3); - -const sum = a.add(b); // 5 + 3 = 8 -const diff = a.sub(b); // 5 - 3 = 2 -const product = a.mul(b); // 5 * 3 = 15 -const quotient = a.div(b); // 5 / 3 -const negation = a.neg(); // -5 -const inverse = a.inv(); // 1/5 -const power = a.power(3); // 5^3 = 125 -``` - -### Comparison Operations (6 functions) - -```typescript -const x = RCFNum(5); -const y = RCFNum(3); - -x.lt(y); // false (5 < 3) -x.gt(y); // true (5 > 3) -x.le(y); // false (5 <= 3) -x.ge(y); // true (5 >= 3) -x.eq(y); // false (5 == 3) -x.neq(y); // true (5 != 3) -``` - -### Type Predicates (4 functions) - -```typescript -const rational = RCFNum('3/4'); -const pi = RCFNum.pi(); -const sqrt2 = RCFNum.roots([RCFNum(-2), RCFNum(0), RCFNum(1)])[1]; -const eps = RCFNum.infinitesimal(); - -rational.isRational(); // true -pi.isRational(); // false - -sqrt2.isAlgebraic(); // true -pi.isAlgebraic(); // false - -pi.isTranscendental(); // true -rational.isTranscendental(); // false - -eps.isInfinitesimal(); // true -rational.isInfinitesimal(); // false -``` - -### Conversion Functions (2 functions) - -```typescript -const pi = RCFNum.pi(); - -// String representation -pi.toString(); // Symbolic representation -pi.toString(true); // Compact representation - -// Decimal approximation -pi.toDecimal(5); // "3.14159" -pi.toDecimal(10); // "3.1415926536" -``` - -### Type Guard (1 function) - -```typescript -const { isRCFNum } = Context('main'); - -const x = RCFNum(5); -if (isRCFNum(x)) { - // TypeScript knows x is RCFNum<'main'> - console.log(x.toDecimal(5)); -} -``` - -## Usage Examples - -### Example 1: Basic Arithmetic with Transcendentals - -```typescript -import { init } from 'z3-solver'; - -const { Context } = await init(); -const { RCFNum } = Context('main'); - -const pi = RCFNum.pi(); -const e = RCFNum.e(); - -// Exact symbolic computation -const sum = pi.add(e); -const product = pi.mul(e); - -console.log('π + e ≈', sum.toDecimal(10)); -console.log('π × e ≈', product.toDecimal(10)); -``` - -### Example 2: Finding Polynomial Roots - -```typescript -const { Context } = await init(); -const { RCFNum } = Context('main'); - -// Find roots of x^2 - 2 = 0 -const coeffs = [ - RCFNum(-2), // constant term - RCFNum(0), // x coefficient - RCFNum(1) // x^2 coefficient -]; - -const roots = RCFNum.roots(coeffs); -console.log('Roots of x² - 2 = 0:'); -roots.forEach((root, i) => { - console.log(` root[${i}] = ${root.toDecimal(15)}`); - console.log(` is algebraic: ${root.isAlgebraic()}`); -}); -``` - -### Example 3: Exact Rational Arithmetic - -```typescript -const { Context } = await init(); -const { RCFNum } = Context('main'); - -const half = RCFNum('1/2'); -const third = RCFNum('1/3'); - -const sum = half.add(third); -console.log('1/2 + 1/3 =', sum.toString()); // Exact: 5/6 -console.log('decimal =', sum.toDecimal(10)); // Approx: 0.8333333333 -``` - -### Example 4: Working with Infinitesimals - -```typescript -const { Context } = await init(); -const { RCFNum } = Context('main'); - -const eps = RCFNum.infinitesimal(); -const tiny = RCFNum('1/1000000000'); - -// Infinitesimals are smaller than any positive real -console.log('ε < 1/1000000000:', eps.lt(tiny)); // true -console.log('ε is infinitesimal:', eps.isInfinitesimal()); // true -``` - -## Implementation Details - -### Files Modified - -1. **src/api/js/src/high-level/types.ts** - - Added `RCFNum` interface - - Added `RCFNumCreation` interface - - Added `isRCFNum` type guard to Context - -2. **src/api/js/src/high-level/high-level.ts** - - Imported `Z3_rcf_num` from low-level API - - Implemented `RCFNumImpl` class - - Added `RCFNum` creation object with callable interface - - Implemented `isRCFNum` type guard function - -3. **src/api/js/src/high-level/high-level.test.ts** - - Added comprehensive test suite for RCFNum - - Tests cover all operations: creation, arithmetic, comparison, predicates, roots - -4. **src/api/js/examples/high-level/rcf-example.ts** - - Created comprehensive example demonstrating all RCF features - -### Design Decisions - -1. **Callable Interface**: `RCFNum` uses a callable interface (not `new RCFNum()`) to match the style of other creation interfaces like `Int.val()` and `Real.val()`. - -2. **Type Safety**: All RCF operations are strongly typed with TypeScript generics for context tracking. - -3. **Memory Management**: RCF numerals use automatic cleanup through `FinalizationRegistry` with `Z3.rcf_del()`. - -4. **Consistency**: The API design matches the patterns established by other numeric types (IntNum, RatNum) while exposing RCF-specific functionality. - -## Comparison with Other Languages - -The TypeScript RCF API now provides equivalent functionality to: - -### Python -```python -from z3 import * - -pi = RCFVal.pi() -e = RCFVal.e() -sum = pi + e -``` - -### Java -```java -RCFNum pi = RCFNum.mkPi(ctx); -RCFNum e = RCFNum.mkE(ctx); -RCFNum sum = pi.add(e); -``` - -### C# -```csharp -var pi = RCFNum.Pi(ctx); -var e = RCFNum.E(ctx); -var sum = pi.Add(e); -``` - -### C++ -```cpp -rcf_num pi = rcf_mk_pi(ctx); -rcf_num e = rcf_mk_e(ctx); -rcf_num sum = rcf_add(ctx, pi, e); -``` - -### TypeScript (NEW) -```typescript -const pi = RCFNum.pi(); -const e = RCFNum.e(); -const sum = pi.add(e); -``` - -## Testing - -The implementation includes a comprehensive test suite covering: - -- ✅ Creation from strings and integers -- ✅ Transcendental constants (π, e) -- ✅ Infinitesimals -- ✅ All arithmetic operations -- ✅ All comparison operations -- ✅ All type predicates -- ✅ Polynomial root finding -- ✅ String and decimal conversion - -To run tests (requires WASM build): -```bash -cd src/api/js -npm test -``` - -## Use Cases - -The RCF API enables: - -1. **Symbolic Mathematics**: Work with exact representations of π, e, and algebraic numbers -2. **Computer Algebra**: Perform exact rational and algebraic arithmetic -3. **Numerical Analysis**: Use infinitesimals for non-standard analysis -4. **Polynomial Solving**: Find exact roots of polynomials -5. **Scientific Computing**: Maintain precision in complex calculations - -## References - -- [Z3 C API Documentation - RCF](https://z3prover.github.io/api/html/group__capi.html) -- [Java RCF Implementation](../../java/RCFNum.java) -- [Low-Level RCF Example](../examples/low-level/rcf-example.ts) - -## Credits - -Implementation completed as part of TypeScript API enhancement initiative (2026-01-17).