Add RCFNum high-level API implementation

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/api/js/src/high-level/high-level.ts

@@ -45,6 +45,7 @@ import {
   Z3_goal_prec,
   Z3_param_descrs,
   Z3_simplifier,
+  Z3_rcf_num,
 } from '../low-level';
 import {
   AnyAst,
@@ -93,6 +94,8 @@ import {
   Quantifier,
   BodyT,
   RatNum,
+  RCFNum,
+  RCFNumCreation,
   Seq,
   SeqSort,
   Simplifier,
@@ -526,6 +529,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       return isSort(obj) && obj.kind() === Z3_sort_kind.Z3_REAL_SORT;
     }
 
+    function isRCFNum(obj: unknown): obj is RCFNum<Name> {
+      const r = obj instanceof RCFNumImpl;
+      r && _assertContext(obj);
+      return r;
+    }
+
     function isBitVecSort(obj: unknown): obj is BitVecSort<number, Name> {
       const r = obj instanceof BitVecSortImpl;
       r && _assertContext(obj);
@@ -825,6 +834,29 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return new RatNumImpl(Z3.mk_numeral(contextPtr, value.toString(), Real.sort().ptr));
       },
     };
+
+    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))),
+
+        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>;
+
     const BitVec = {
       sort<Bits extends number>(bits: Bits): BitVecSort<Bits, Name> {
         assert(Number.isSafeInteger(bits), 'number of bits must be an integer');
@@ -3371,6 +3403,112 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       }
     }
 
+    class RCFNumImpl implements RCFNum<Name> {
+      declare readonly __typename: RCFNum['__typename'];
+      readonly ctx: Context<Name>;
+      readonly ptr: Z3_rcf_num;
+
+      constructor(value: string | number);
+      constructor(ptr: Z3_rcf_num);
+      constructor(valueOrPtr: string | number | Z3_rcf_num) {
+        this.ctx = ctx;
+        if (typeof valueOrPtr === 'string') {
+          this.ptr = check(Z3.rcf_mk_rational(contextPtr, valueOrPtr));
+        } else if (typeof valueOrPtr === 'number') {
+          this.ptr = check(Z3.rcf_mk_small_int(contextPtr, valueOrPtr));
+        } else {
+          this.ptr = valueOrPtr;
+        }
+        cleanup.register(this, () => Z3.rcf_del(contextPtr, this.ptr), this);
+      }
+
+      add(other: RCFNum<Name>): RCFNum<Name> {
+        _assertContext(other);
+        return new RCFNumImpl(check(Z3.rcf_add(contextPtr, this.ptr, (other as RCFNumImpl).ptr)));
+      }
+
+      sub(other: RCFNum<Name>): RCFNum<Name> {
+        _assertContext(other);
+        return new RCFNumImpl(check(Z3.rcf_sub(contextPtr, this.ptr, (other as RCFNumImpl).ptr)));
+      }
+
+      mul(other: RCFNum<Name>): RCFNum<Name> {
+        _assertContext(other);
+        return new RCFNumImpl(check(Z3.rcf_mul(contextPtr, this.ptr, (other as RCFNumImpl).ptr)));
+      }
+
+      div(other: RCFNum<Name>): RCFNum<Name> {
+        _assertContext(other);
+        return new RCFNumImpl(check(Z3.rcf_div(contextPtr, this.ptr, (other as RCFNumImpl).ptr)));
+      }
+
+      neg(): RCFNum<Name> {
+        return new RCFNumImpl(check(Z3.rcf_neg(contextPtr, this.ptr)));
+      }
+
+      inv(): RCFNum<Name> {
+        return new RCFNumImpl(check(Z3.rcf_inv(contextPtr, this.ptr)));
+      }
+
+      power(k: number): RCFNum<Name> {
+        return new RCFNumImpl(check(Z3.rcf_power(contextPtr, this.ptr, k)));
+      }
+
+      lt(other: RCFNum<Name>): boolean {
+        _assertContext(other);
+        return check(Z3.rcf_lt(contextPtr, this.ptr, (other as RCFNumImpl).ptr));
+      }
+
+      gt(other: RCFNum<Name>): boolean {
+        _assertContext(other);
+        return check(Z3.rcf_gt(contextPtr, this.ptr, (other as RCFNumImpl).ptr));
+      }
+
+      le(other: RCFNum<Name>): boolean {
+        _assertContext(other);
+        return check(Z3.rcf_le(contextPtr, this.ptr, (other as RCFNumImpl).ptr));
+      }
+
+      ge(other: RCFNum<Name>): boolean {
+        _assertContext(other);
+        return check(Z3.rcf_ge(contextPtr, this.ptr, (other as RCFNumImpl).ptr));
+      }
+
+      eq(other: RCFNum<Name>): boolean {
+        _assertContext(other);
+        return check(Z3.rcf_eq(contextPtr, this.ptr, (other as RCFNumImpl).ptr));
+      }
+
+      neq(other: RCFNum<Name>): boolean {
+        _assertContext(other);
+        return check(Z3.rcf_neq(contextPtr, this.ptr, (other as RCFNumImpl).ptr));
+      }
+
+      isRational(): boolean {
+        return check(Z3.rcf_is_rational(contextPtr, this.ptr));
+      }
+
+      isAlgebraic(): boolean {
+        return check(Z3.rcf_is_algebraic(contextPtr, this.ptr));
+      }
+
+      isInfinitesimal(): boolean {
+        return check(Z3.rcf_is_infinitesimal(contextPtr, this.ptr));
+      }
+
+      isTranscendental(): boolean {
+        return check(Z3.rcf_is_transcendental(contextPtr, this.ptr));
+      }
+
+      toString(compact: boolean = false): string {
+        return check(Z3.rcf_num_to_string(contextPtr, this.ptr, compact, false));
+      }
+
+      toDecimal(precision: number): string {
+        return check(Z3.rcf_num_to_decimal_string(contextPtr, this.ptr, precision));
+      }
+    }
+
     class BitVecSortImpl<Bits extends number> extends SortImpl implements BitVecSort<Bits, Name> {
       declare readonly __typename: BitVecSort['__typename'];
 
@@ -4520,6 +4658,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       isReal,
       isRealVal,
       isRealSort,
+      isRCFNum,
       isBitVecSort,
       isBitVec,
       isBitVecVal, // TODO fix ordering
@@ -4553,6 +4692,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       Bool,
       Int,
       Real,
+      RCFNum,
       BitVec,
       Float,
       FloatRM,

src/api/js/src/high-level/types.ts

@@ -278,6 +278,9 @@ export interface Context<Name extends string = 'main'> {
   /** @category Functions */
   isRealSort(obj: unknown): boolean;
 
+  /** @category Functions */
+  isRCFNum(obj: unknown): obj is RCFNum<Name>;
+
   /** @category Functions */
   isBitVecSort(obj: unknown): obj is BitVecSort<number, Name>;
 
@@ -443,6 +446,8 @@ export interface Context<Name extends string = 'main'> {
   /** @category Expressions */
   readonly Real: RealCreation<Name>;
   /** @category Expressions */
+  readonly RCFNum: RCFNumCreation<Name>;
+  /** @category Expressions */
   readonly BitVec: BitVecCreation<Name>;
   /** @category Expressions */
   readonly Float: FPCreation<Name>;
@@ -1985,6 +1990,212 @@ export interface RatNum<Name extends string = 'main'> extends Arith<Name> {
   asString(): string;
 }
 
+/**
+ * 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
+ * ```
+ * @category Arithmetic
+ */
+export interface RCFNum<Name extends string = 'main'> {
+  /** @hidden */
+  readonly __typename: 'RCFNum';
+
+  /** @hidden */
+  readonly ctx: Context<Name>;
+
+  /**
+   * Add two RCF numerals.
+   * @param other - The RCF numeral to add
+   * @returns this + other
+   */
+  add(other: RCFNum<Name>): RCFNum<Name>;
+
+  /**
+   * Subtract two RCF numerals.
+   * @param other - The RCF numeral to subtract
+   * @returns this - other
+   */
+  sub(other: RCFNum<Name>): RCFNum<Name>;
+
+  /**
+   * Multiply two RCF numerals.
+   * @param other - The RCF numeral to multiply
+   * @returns this * other
+   */
+  mul(other: RCFNum<Name>): RCFNum<Name>;
+
+  /**
+   * Divide two RCF numerals.
+   * @param other - The RCF numeral to divide by
+   * @returns this / other
+   */
+  div(other: RCFNum<Name>): RCFNum<Name>;
+
+  /**
+   * Negate this RCF numeral.
+   * @returns -this
+   */
+  neg(): RCFNum<Name>;
+
+  /**
+   * Compute the multiplicative inverse.
+   * @returns 1/this
+   */
+  inv(): RCFNum<Name>;
+
+  /**
+   * Raise this RCF numeral to a power.
+   * @param k - The exponent
+   * @returns this^k
+   */
+  power(k: number): RCFNum<Name>;
+
+  /**
+   * Check if this RCF numeral is less than another.
+   * @param other - The RCF numeral to compare with
+   * @returns true if this < other
+   */
+  lt(other: RCFNum<Name>): boolean;
+
+  /**
+   * Check if this RCF numeral is greater than another.
+   * @param other - The RCF numeral to compare with
+   * @returns true if this > other
+   */
+  gt(other: RCFNum<Name>): boolean;
+
+  /**
+   * Check if this RCF numeral is less than or equal to another.
+   * @param other - The RCF numeral to compare with
+   * @returns true if this <= other
+   */
+  le(other: RCFNum<Name>): boolean;
+
+  /**
+   * Check if this RCF numeral is greater than or equal to another.
+   * @param other - The RCF numeral to compare with
+   * @returns true if this >= other
+   */
+  ge(other: RCFNum<Name>): boolean;
+
+  /**
+   * Check if this RCF numeral is equal to another.
+   * @param other - The RCF numeral to compare with
+   * @returns true if this == other
+   */
+  eq(other: RCFNum<Name>): boolean;
+
+  /**
+   * Check if this RCF numeral is not equal to another.
+   * @param other - The RCF numeral to compare with
+   * @returns true if this != other
+   */
+  neq(other: RCFNum<Name>): boolean;
+
+  /**
+   * Check if this RCF numeral is a rational number.
+   * @returns true if this is rational
+   */
+  isRational(): boolean;
+
+  /**
+   * Check if this RCF numeral is an algebraic number.
+   * @returns true if this is algebraic
+   */
+  isAlgebraic(): boolean;
+
+  /**
+   * Check if this RCF numeral is an infinitesimal.
+   * @returns true if this is infinitesimal
+   */
+  isInfinitesimal(): boolean;
+
+  /**
+   * Check if this RCF numeral is a transcendental number.
+   * @returns true if this is transcendental
+   */
+  isTranscendental(): boolean;
+
+  /**
+   * Convert this RCF numeral to a string.
+   * @param compact - If true, use compact representation
+   * @returns String representation
+   */
+  toString(compact?: boolean): string;
+
+  /**
+   * Convert this RCF numeral to a decimal string.
+   * @param precision - Number of decimal places
+   * @returns Decimal string representation
+   */
+  toDecimal(precision: number): string;
+}
+
+/**
+ * Creation interface for RCF numerals
+ * @category Arithmetic
+ */
+export interface RCFNumCreation<Name extends string> {
+  /**
+   * Create an RCF numeral from a rational string.
+   * @param value - String representation of a rational number (e.g., "3/2", "0.5", "42")
+   */
+  (value: string): RCFNum<Name>;
+
+  /**
+   * Create an RCF numeral from a small integer.
+   * @param value - Integer value
+   */
+  (value: number): RCFNum<Name>;
+
+  /**
+   * Create an RCF numeral representing pi.
+   */
+  pi(): RCFNum<Name>;
+
+  /**
+   * Create an RCF numeral representing e (Euler's constant).
+   */
+  e(): RCFNum<Name>;
+
+  /**
+   * Create an RCF numeral representing an infinitesimal.
+   */
+  infinitesimal(): RCFNum<Name>;
+
+  /**
+   * 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
+   */
+  roots(coefficients: RCFNum<Name>[]): RCFNum<Name>[];
+}
+
 /**
  * A Sort representing Bit Vector numbers of specified {@link BitVecSort.size size}
  *