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

Delete src/api/js/RCF_API_IMPLEMENTATION.md

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-01-18 13:06:59 -08:00 • committed by GitHub
parent 50722fc9b4
commit 2cc08ffe6b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 306 deletions
Download patch file Download diff file Expand all files Collapse all files

306
src/api/js/RCF_API_IMPLEMENTATION.md
View file

@ -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<Name>` interface
- Added `RCFNumCreation<Name>` 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).