mirror of
https://github.com/Z3Prover/z3
synced 2026-01-20 01:03:20 +00:00
Add RCFNum tests and high-level example
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot]
parent
49b8ab623f
commit
9a6735020d
2 changed files with 441 additions and 0 deletions
199
src/api/js/examples/high-level/rcf-example.ts
Normal file
199
src/api/js/examples/high-level/rcf-example.ts
Normal file
|
|
@ -0,0 +1,199 @@
|
|||
/**
|
||||
* 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.
|
||||
*/
|
||||
|
||||
import { init } from 'z3-solver';
|
||||
|
||||
async function rcfBasicExample() {
|
||||
console.log('RCF Basic Example (High-Level API)');
|
||||
console.log('===================================');
|
||||
|
||||
const { Context } = await init();
|
||||
const { RCFNum } = Context('main');
|
||||
|
||||
// Create pi and e
|
||||
const pi = RCFNum.pi();
|
||||
const e = RCFNum.e();
|
||||
|
||||
console.log('pi =', pi.toString());
|
||||
console.log('e =', e.toString());
|
||||
|
||||
// Arithmetic operations
|
||||
const sum = pi.add(e);
|
||||
const prod = pi.mul(e);
|
||||
|
||||
console.log('pi + e =', sum.toString());
|
||||
console.log('pi * e =', prod.toString());
|
||||
|
||||
// Decimal approximations
|
||||
console.log('pi (10 decimals) =', pi.toDecimal(10));
|
||||
console.log('e (10 decimals) =', e.toDecimal(10));
|
||||
|
||||
// Comparisons
|
||||
console.log('pi < e?', pi.lt(e) ? 'yes' : 'no');
|
||||
console.log('pi > e?', pi.gt(e) ? 'yes' : 'no');
|
||||
}
|
||||
|
||||
async function rcfRationalExample() {
|
||||
console.log('\nRCF Rational Example (High-Level API)');
|
||||
console.log('=====================================');
|
||||
|
||||
const { Context } = await init();
|
||||
const { RCFNum } = Context('main');
|
||||
|
||||
// Create rational numbers
|
||||
const half = RCFNum('1/2');
|
||||
const third = RCFNum('1/3');
|
||||
|
||||
console.log('1/2 =', half.toString());
|
||||
console.log('1/3 =', third.toString());
|
||||
|
||||
// Arithmetic
|
||||
const sum = half.add(third);
|
||||
console.log('1/2 + 1/3 =', sum.toString());
|
||||
console.log('1/2 + 1/3 (decimal) =', sum.toDecimal(10));
|
||||
|
||||
// Type queries
|
||||
console.log('Is 1/2 rational?', half.isRational() ? 'yes' : 'no');
|
||||
console.log('Is 1/2 algebraic?', half.isAlgebraic() ? 'yes' : 'no');
|
||||
}
|
||||
|
||||
async function rcfRootsExample() {
|
||||
console.log('\nRCF Roots Example (High-Level API)');
|
||||
console.log('===================================');
|
||||
|
||||
const { Context } = await init();
|
||||
const { RCFNum } = Context('main');
|
||||
|
||||
// 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
|
||||
];
|
||||
|
||||
const roots = RCFNum.roots(coeffs);
|
||||
|
||||
console.log('Roots of x^2 - 2 = 0:');
|
||||
for (let i = 0; i < roots.length; i++) {
|
||||
console.log(` root[${i}] =`, roots[i].toString());
|
||||
console.log(` decimal =`, roots[i].toDecimal(15));
|
||||
console.log(` is_algebraic =`, roots[i].isAlgebraic() ? 'yes' : 'no');
|
||||
}
|
||||
}
|
||||
|
||||
async function rcfInfinitesimalExample() {
|
||||
console.log('\nRCF Infinitesimal Example (High-Level API)');
|
||||
console.log('===========================================');
|
||||
|
||||
const { Context } = await init();
|
||||
const { RCFNum } = Context('main');
|
||||
|
||||
// Create an infinitesimal
|
||||
const eps = RCFNum.infinitesimal();
|
||||
console.log('eps =', eps.toString());
|
||||
console.log('Is eps infinitesimal?', eps.isInfinitesimal() ? 'yes' : 'no');
|
||||
|
||||
// Infinitesimals are smaller than any positive real number
|
||||
const tiny = RCFNum('1/1000000000');
|
||||
console.log('eps < 1/1000000000?', eps.lt(tiny) ? 'yes' : 'no');
|
||||
}
|
||||
|
||||
async function rcfArithmeticExample() {
|
||||
console.log('\nRCF Arithmetic Operations Example');
|
||||
console.log('==================================');
|
||||
|
||||
const { Context } = await init();
|
||||
const { RCFNum } = Context('main');
|
||||
|
||||
const a = RCFNum(5);
|
||||
const b = RCFNum(3);
|
||||
|
||||
console.log('a =', a.toString());
|
||||
console.log('b =', b.toString());
|
||||
console.log('a + b =', a.add(b).toString());
|
||||
console.log('a - b =', a.sub(b).toString());
|
||||
console.log('a * b =', a.mul(b).toString());
|
||||
console.log('a / b =', a.div(b).toString(), '=', a.div(b).toDecimal(5));
|
||||
console.log('-a =', a.neg().toString());
|
||||
console.log('1/a =', a.inv().toString(), '=', a.inv().toDecimal(5));
|
||||
console.log('a^3 =', a.power(3).toString());
|
||||
|
||||
// Comparisons
|
||||
console.log('\nComparisons:');
|
||||
console.log('a < b?', a.lt(b));
|
||||
console.log('a > b?', a.gt(b));
|
||||
console.log('a <= b?', a.le(b));
|
||||
console.log('a >= b?', a.ge(b));
|
||||
console.log('a == b?', a.eq(b));
|
||||
console.log('a != b?', a.neq(b));
|
||||
}
|
||||
|
||||
async function rcfSymbolicMathExample() {
|
||||
console.log('\nRCF Symbolic Mathematics Example');
|
||||
console.log('=================================');
|
||||
|
||||
const { Context } = await init();
|
||||
const { RCFNum } = Context('main');
|
||||
|
||||
// Work with exact symbolic values
|
||||
const pi = RCFNum.pi();
|
||||
const e = RCFNum.e();
|
||||
const sqrt2Coeffs = [RCFNum(-2), RCFNum(0), RCFNum(1)];
|
||||
const sqrt2Roots = RCFNum.roots(sqrt2Coeffs);
|
||||
const sqrt2 = sqrt2Roots.find(r => r.gt(RCFNum(0)))!;
|
||||
|
||||
console.log('π =', pi.toDecimal(15));
|
||||
console.log('e =', e.toDecimal(15));
|
||||
console.log('√2 =', sqrt2.toDecimal(15));
|
||||
|
||||
// Combine them
|
||||
const expr1 = pi.add(e);
|
||||
const expr2 = pi.mul(sqrt2);
|
||||
const expr3 = e.power(2);
|
||||
|
||||
console.log('\nExpressions:');
|
||||
console.log('π + e =', expr1.toDecimal(10));
|
||||
console.log('π × √2 =', expr2.toDecimal(10));
|
||||
console.log('e² =', expr3.toDecimal(10));
|
||||
|
||||
// Check properties
|
||||
console.log('\nProperties:');
|
||||
console.log('π is transcendental:', pi.isTranscendental());
|
||||
console.log('e is transcendental:', e.isTranscendental());
|
||||
console.log('√2 is algebraic:', sqrt2.isAlgebraic());
|
||||
console.log('√2 is rational:', sqrt2.isRational());
|
||||
}
|
||||
|
||||
async function main() {
|
||||
try {
|
||||
await rcfBasicExample();
|
||||
await rcfRationalExample();
|
||||
await rcfRootsExample();
|
||||
await rcfInfinitesimalExample();
|
||||
await rcfArithmeticExample();
|
||||
await rcfSymbolicMathExample();
|
||||
|
||||
console.log('\n✓ All RCF examples completed successfully!');
|
||||
console.log('\nThe RCF API in TypeScript now provides:');
|
||||
console.log(' • 38 functions for exact real arithmetic');
|
||||
console.log(' • Support for π, e, algebraic numbers, and infinitesimals');
|
||||
console.log(' • Full arithmetic and comparison operations');
|
||||
console.log(' • Polynomial root finding');
|
||||
console.log(' • Type predicates and conversions');
|
||||
} catch (error) {
|
||||
console.error('Error:', error);
|
||||
throw error;
|
||||
}
|
||||
}
|
||||
|
||||
main();
|
||||
|
|
@ -1984,4 +1984,246 @@ describe('high-level', () => {
|
|||
}
|
||||
});
|
||||
});
|
||||
|
||||
describe('RCFNum', () => {
|
||||
let RCFNum: Z3HighLevel['RCFNum'];
|
||||
|
||||
beforeEach(() => {
|
||||
({ RCFNum } = api.Context('rcf'));
|
||||
});
|
||||
|
||||
it('should create RCF from string', () => {
|
||||
const half = RCFNum('1/2');
|
||||
expect(half.toString()).toContain('1');
|
||||
expect(half.toString()).toContain('2');
|
||||
expect(half.isRational()).toBe(true);
|
||||
});
|
||||
|
||||
it('should create RCF from integer', () => {
|
||||
const five = RCFNum(5);
|
||||
expect(five.toString()).toContain('5');
|
||||
expect(five.isRational()).toBe(true);
|
||||
});
|
||||
|
||||
it('should create pi', () => {
|
||||
const pi = RCFNum.pi();
|
||||
expect(pi.isTranscendental()).toBe(true);
|
||||
expect(pi.isRational()).toBe(false);
|
||||
const piStr = pi.toDecimal(10);
|
||||
expect(piStr).toContain('3.14');
|
||||
});
|
||||
|
||||
it('should create e', () => {
|
||||
const e = RCFNum.e();
|
||||
expect(e.isTranscendental()).toBe(true);
|
||||
expect(e.isRational()).toBe(false);
|
||||
const eStr = e.toDecimal(10);
|
||||
expect(eStr).toContain('2.71');
|
||||
});
|
||||
|
||||
it('should create infinitesimal', () => {
|
||||
const eps = RCFNum.infinitesimal();
|
||||
expect(eps.isInfinitesimal()).toBe(true);
|
||||
expect(eps.isRational()).toBe(false);
|
||||
});
|
||||
|
||||
it('should perform addition', () => {
|
||||
const a = RCFNum('1/2');
|
||||
const b = RCFNum('1/3');
|
||||
const sum = a.add(b);
|
||||
expect(sum.isRational()).toBe(true);
|
||||
// 1/2 + 1/3 = 5/6
|
||||
const decimal = sum.toDecimal(5);
|
||||
expect(decimal).toContain('0.833');
|
||||
});
|
||||
|
||||
it('should perform subtraction', () => {
|
||||
const a = RCFNum(1);
|
||||
const b = RCFNum('1/2');
|
||||
const diff = a.sub(b);
|
||||
expect(diff.isRational()).toBe(true);
|
||||
// 1 - 1/2 = 1/2
|
||||
const decimal = diff.toDecimal(5);
|
||||
expect(decimal).toContain('0.5');
|
||||
});
|
||||
|
||||
it('should perform multiplication', () => {
|
||||
const a = RCFNum(2);
|
||||
const b = RCFNum(3);
|
||||
const prod = a.mul(b);
|
||||
expect(prod.isRational()).toBe(true);
|
||||
expect(prod.toString()).toContain('6');
|
||||
});
|
||||
|
||||
it('should perform division', () => {
|
||||
const a = RCFNum(1);
|
||||
const b = RCFNum(2);
|
||||
const quot = a.div(b);
|
||||
expect(quot.isRational()).toBe(true);
|
||||
const decimal = quot.toDecimal(5);
|
||||
expect(decimal).toContain('0.5');
|
||||
});
|
||||
|
||||
it('should perform negation', () => {
|
||||
const a = RCFNum(5);
|
||||
const negA = a.neg();
|
||||
expect(negA.toString()).toContain('-');
|
||||
});
|
||||
|
||||
it('should perform inversion', () => {
|
||||
const a = RCFNum(2);
|
||||
const inv = a.inv();
|
||||
expect(inv.isRational()).toBe(true);
|
||||
const decimal = inv.toDecimal(5);
|
||||
expect(decimal).toContain('0.5');
|
||||
});
|
||||
|
||||
it('should perform power', () => {
|
||||
const a = RCFNum(2);
|
||||
const squared = a.power(2);
|
||||
expect(squared.toString()).toContain('4');
|
||||
});
|
||||
|
||||
it('should compare with lt', () => {
|
||||
const a = RCFNum(1);
|
||||
const b = RCFNum(2);
|
||||
expect(a.lt(b)).toBe(true);
|
||||
expect(b.lt(a)).toBe(false);
|
||||
});
|
||||
|
||||
it('should compare with gt', () => {
|
||||
const a = RCFNum(2);
|
||||
const b = RCFNum(1);
|
||||
expect(a.gt(b)).toBe(true);
|
||||
expect(b.gt(a)).toBe(false);
|
||||
});
|
||||
|
||||
it('should compare with le', () => {
|
||||
const a = RCFNum(1);
|
||||
const b = RCFNum(2);
|
||||
const c = RCFNum(1);
|
||||
expect(a.le(b)).toBe(true);
|
||||
expect(a.le(c)).toBe(true);
|
||||
expect(b.le(a)).toBe(false);
|
||||
});
|
||||
|
||||
it('should compare with ge', () => {
|
||||
const a = RCFNum(2);
|
||||
const b = RCFNum(1);
|
||||
const c = RCFNum(2);
|
||||
expect(a.ge(b)).toBe(true);
|
||||
expect(a.ge(c)).toBe(true);
|
||||
expect(b.ge(a)).toBe(false);
|
||||
});
|
||||
|
||||
it('should compare with eq', () => {
|
||||
const a = RCFNum(5);
|
||||
const b = RCFNum(5);
|
||||
const c = RCFNum(6);
|
||||
expect(a.eq(b)).toBe(true);
|
||||
expect(a.eq(c)).toBe(false);
|
||||
});
|
||||
|
||||
it('should compare with neq', () => {
|
||||
const a = RCFNum(5);
|
||||
const b = RCFNum(6);
|
||||
const c = RCFNum(5);
|
||||
expect(a.neq(b)).toBe(true);
|
||||
expect(a.neq(c)).toBe(false);
|
||||
});
|
||||
|
||||
it('should find polynomial roots', () => {
|
||||
// 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
|
||||
];
|
||||
|
||||
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');
|
||||
expect(decimals[1]).toContain('1.4');
|
||||
});
|
||||
|
||||
it('should check isRational predicate', () => {
|
||||
const rational = RCFNum('3/4');
|
||||
const pi = RCFNum.pi();
|
||||
|
||||
expect(rational.isRational()).toBe(true);
|
||||
expect(pi.isRational()).toBe(false);
|
||||
});
|
||||
|
||||
it('should check isAlgebraic predicate', () => {
|
||||
// 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);
|
||||
});
|
||||
|
||||
it('should check isTranscendental predicate', () => {
|
||||
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);
|
||||
});
|
||||
|
||||
it('should check isInfinitesimal predicate', () => {
|
||||
const eps = RCFNum.infinitesimal();
|
||||
const rational = RCFNum(5);
|
||||
|
||||
expect(eps.isInfinitesimal()).toBe(true);
|
||||
expect(rational.isInfinitesimal()).toBe(false);
|
||||
});
|
||||
|
||||
it('should convert to string with compact mode', () => {
|
||||
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);
|
||||
});
|
||||
|
||||
it('should convert to decimal with precision', () => {
|
||||
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');
|
||||
expect(decimal10).toContain('3.141592');
|
||||
});
|
||||
|
||||
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);
|
||||
});
|
||||
});
|
||||
});
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue