From d7579706e23b125ba8ba60c97f13553030610c95 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Sat, 10 Jan 2026 12:55:08 -0800
Subject: [PATCH] Add Floating-Point and String/Sequence APIs to TypeScript
 bindings (#8135)

* Initial plan

* Add FP and String/Seq type definitions to TypeScript bindings

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

* Implement FP and String/Seq in TypeScript high-level bindings

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

* Add comprehensive tests for FP and String/Seq APIs

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

* Fix build errors: Add isFP to test scope and use eqIdentity for Sort comparison

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

* Fix code formatting with Prettier for WASM build

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

* Fix FPNum.value() to use Z3_get_numeral_double instead of parsing string

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

* Simplify length check for empty sequence

Refactor length check for empty sequence in tests.

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/js/src/high-level/high-level.test.ts | 322 ++++++++++++-
 src/api/js/src/high-level/high-level.ts      | 454 +++++++++++++++++++
 src/api/js/src/high-level/types.ts           | 415 ++++++++++++++++-
 3 files changed, 1187 insertions(+), 4 deletions(-)

diff --git a/src/api/js/src/high-level/high-level.test.ts b/src/api/js/src/high-level/high-level.test.ts
index 934669505..dba731156 100644
--- a/src/api/js/src/high-level/high-level.test.ts
+++ b/src/api/js/src/high-level/high-level.test.ts
@@ -1051,7 +1051,6 @@ describe('high-level', () => {
       expect(nonUnits).toBeDefined();
       expect(nonUnits.length()).toBeGreaterThanOrEqual(0);
     });
-
   });
 
   describe('solver congruence closure APIs', () => {
@@ -1196,4 +1195,325 @@ describe('high-level', () => {
       expect(typeof solver.fromFile).toBe('function');
     });
   });
+
+  describe('floating-point', () => {
+    it('can create FP sorts', () => {
+      const { Float } = api.Context('main');
+
+      const fp16 = Float.sort16();
+      expect(fp16.ebits()).toBe(5);
+      expect(fp16.sbits()).toBe(11);
+
+      const fp32 = Float.sort32();
+      expect(fp32.ebits()).toBe(8);
+      expect(fp32.sbits()).toBe(24);
+
+      const fp64 = Float.sort64();
+      expect(fp64.ebits()).toBe(11);
+      expect(fp64.sbits()).toBe(53);
+
+      const fp128 = Float.sort128();
+      expect(fp128.ebits()).toBe(15);
+      expect(fp128.sbits()).toBe(113);
+
+      const custom = Float.sort(5, 10);
+      expect(custom.ebits()).toBe(5);
+      expect(custom.sbits()).toBe(10);
+    });
+
+    it('can create FP rounding modes', () => {
+      const { FloatRM } = api.Context('main');
+
+      const rne = FloatRM.RNE();
+      const rna = FloatRM.RNA();
+      const rtp = FloatRM.RTP();
+      const rtn = FloatRM.RTN();
+      const rtz = FloatRM.RTZ();
+
+      expect(rne.toString()).toContain('roundNearestTiesToEven');
+    });
+
+    it('can create FP constants and values', () => {
+      const { Float, FloatRM } = api.Context('main');
+      const fp32 = Float.sort32();
+
+      const x = Float.const('x', fp32);
+      expect(x.sort.ebits()).toBe(8);
+      expect(x.sort.sbits()).toBe(24);
+
+      const val = Float.val(3.14, fp32);
+      expect(val.value()).toBeCloseTo(3.14, 2);
+
+      const nan = Float.NaN(fp32);
+      const inf = Float.inf(fp32);
+      const negInf = Float.inf(fp32, true);
+      const zero = Float.zero(fp32);
+      const negZero = Float.zero(fp32, true);
+
+      expect(typeof nan.value()).toBe('number');
+      expect(typeof inf.value()).toBe('number');
+    });
+
+    it('can perform FP arithmetic', async () => {
+      const { Float, FloatRM, Solver } = api.Context('main');
+      const fp32 = Float.sort32();
+      const rm = FloatRM.RNE();
+
+      const x = Float.const('x', fp32);
+      const y = Float.const('y', fp32);
+
+      const sum = x.add(rm, y);
+      const diff = x.sub(rm, y);
+      const prod = x.mul(rm, y);
+      const quot = x.div(rm, y);
+
+      const solver = new Solver();
+      solver.add(x.eq(Float.val(2.0, fp32)));
+      solver.add(y.eq(Float.val(3.0, fp32)));
+      solver.add(sum.eq(Float.val(5.0, fp32)));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+    });
+
+    it('can perform FP comparisons', async () => {
+      const { Float, FloatRM, Solver, isFP } = api.Context('main');
+      const fp32 = Float.sort32();
+
+      const x = Float.const('x', fp32);
+      const two = Float.val(2.0, fp32);
+      const three = Float.val(3.0, fp32);
+
+      const solver = new Solver();
+      solver.add(x.gt(two));
+      solver.add(x.lt(three));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+
+      const model = solver.model();
+      const xVal = model.eval(x);
+      expect(isFP(xVal)).toBe(true);
+    });
+
+    it('can use FP predicates', async () => {
+      const { Float, Solver, isFP } = api.Context('main');
+      const fp32 = Float.sort32();
+
+      const x = Float.const('x', fp32);
+      const nan = Float.NaN(fp32);
+      const inf = Float.inf(fp32);
+      const zero = Float.zero(fp32);
+
+      // Test NaN predicate
+      {
+        const solver = new Solver();
+        solver.add(x.eq(nan));
+        solver.add(x.isNaN());
+        expect(await solver.check()).toBe('sat');
+      }
+
+      // Test infinity predicate
+      {
+        const solver = new Solver();
+        solver.add(x.eq(inf));
+        solver.add(x.isInf());
+        expect(await solver.check()).toBe('sat');
+      }
+
+      // Test zero predicate
+      {
+        const solver = new Solver();
+        solver.add(x.eq(zero));
+        solver.add(x.isZero());
+        expect(await solver.check()).toBe('sat');
+      }
+    });
+
+    it('supports FP type checking', () => {
+      const { Float, FloatRM, isFPSort, isFP, isFPVal, isFPRMSort, isFPRM } = api.Context('main');
+      const fp32 = Float.sort32();
+      const rmSort = FloatRM.sort();
+
+      expect(isFPSort(fp32)).toBe(true);
+      expect(isFPRMSort(rmSort)).toBe(true);
+
+      const x = Float.const('x', fp32);
+      const val = Float.val(1.0, fp32);
+      const rm = FloatRM.RNE();
+
+      expect(isFP(x)).toBe(true);
+      expect(isFPVal(val)).toBe(true);
+      expect(isFPRM(rm)).toBe(true);
+    });
+  });
+
+  describe('strings and sequences', () => {
+    it('can create string sort and values', () => {
+      const { String: Str } = api.Context('main');
+
+      const strSort = Str.sort();
+      expect(strSort.isString()).toBe(true);
+
+      const hello = Str.val('hello');
+      expect(hello.isString()).toBe(true);
+      expect(hello.asString()).toBe('hello');
+
+      const x = Str.const('x');
+      expect(x.isString()).toBe(true);
+    });
+
+    it('can create sequence sorts', () => {
+      const { Seq, Int, eqIdentity } = api.Context('main');
+
+      const intSeq = Seq.sort(Int.sort());
+      expect(eqIdentity(intSeq.basis(), Int.sort())).toBe(true);
+
+      const empty = Seq.empty(Int.sort());
+      const len_empty = empty.length();
+      // TOOD: simplify len_empty const len_empty_simplified = 
+//      expect(len_empty_simplified.toString()).toContain('0');
+    });
+
+    it('can concatenate strings', async () => {
+      const { String: Str, Solver } = api.Context('main');
+
+      const x = Str.const('x');
+      const y = Str.const('y');
+
+      const hello = Str.val('hello');
+      const world = Str.val('world');
+
+      const solver = new Solver();
+      solver.add(x.eq(hello));
+      solver.add(y.eq(world));
+      solver.add(x.concat(y).eq(Str.val('helloworld')));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+    });
+
+    it('can compute string length', async () => {
+      const { String: Str, Solver, Int } = api.Context('main');
+
+      const x = Str.const('x');
+      const hello = Str.val('hello');
+
+      const solver = new Solver();
+      solver.add(x.eq(hello));
+      solver.add(x.length().eq(Int.val(5)));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+    });
+
+    it('can extract substrings', async () => {
+      const { String: Str, Solver } = api.Context('main');
+
+      const x = Str.const('x');
+      const hello = Str.val('hello');
+
+      const solver = new Solver();
+      solver.add(x.eq(hello));
+      solver.add(x.extract(0, 2).eq(Str.val('he')));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+    });
+
+    it('can check string containment', async () => {
+      const { String: Str, Solver } = api.Context('main');
+
+      const x = Str.const('x');
+      const hello = Str.val('hello');
+
+      const solver = new Solver();
+      solver.add(x.eq(hello));
+      solver.add(x.contains('ell'));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+    });
+
+    it('can find substring index', async () => {
+      const { String: Str, Solver, Int } = api.Context('main');
+
+      const x = Str.const('x');
+      const hello = Str.val('hello');
+
+      const solver = new Solver();
+      solver.add(x.eq(hello));
+      solver.add(x.indexOf('ell').eq(Int.val(1)));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+    });
+
+    it('can check string prefix and suffix', async () => {
+      const { String: Str, Solver } = api.Context('main');
+
+      const x = Str.const('x');
+      const hello = Str.val('hello');
+
+      const solver = new Solver();
+      solver.add(x.eq(hello));
+      solver.add(x.prefixOf('helloworld'));
+      solver.add(Str.val('lo').suffixOf(x));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+    });
+
+    it('can replace substrings', async () => {
+      const { String: Str, Solver } = api.Context('main');
+
+      const x = Str.const('x');
+      const hello = Str.val('hello');
+
+      const solver = new Solver();
+      solver.add(x.eq(hello));
+      solver.add(x.replace('l', 'L').eq(Str.val('heLlo'))); // First occurrence
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+    });
+
+    it('supports string type checking', () => {
+      const { String: Str, Seq, Int, isSeqSort, isSeq, isStringSort, isString } = api.Context('main');
+
+      const strSort = Str.sort();
+      const intSeqSort = Seq.sort(Int.sort());
+
+      expect(isSeqSort(strSort)).toBe(true);
+      expect(isStringSort(strSort)).toBe(true);
+      expect(isSeqSort(intSeqSort)).toBe(true);
+      expect(isStringSort(intSeqSort)).toBe(false);
+
+      const hello = Str.val('hello');
+      const x = Str.const('x');
+
+      expect(isSeq(hello)).toBe(true);
+      expect(isString(hello)).toBe(true);
+      expect(isSeq(x)).toBe(true);
+      expect(isString(x)).toBe(true);
+    });
+
+    it('can work with sequences of integers', async () => {
+      const { Seq, Int, Solver } = api.Context('main');
+
+      const one = Int.val(1);
+      const seq1 = Seq.unit(one);
+
+      const two = Int.val(2);
+      const seq2 = Seq.unit(two);
+
+      const concat = seq1.concat(seq2);
+
+      const solver = new Solver();
+      solver.add(concat.length().eq(Int.val(2)));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+    });
+  });
 });
diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts
index f8d2ef12c..2eab4f28f 100644
--- a/src/api/js/src/high-level/high-level.ts
+++ b/src/api/js/src/high-level/high-level.ts
@@ -64,9 +64,15 @@ import {
   CoercibleToBitVec,
   CoercibleToExpr,
   CoercibleFromMap,
+  CoercibleToFP,
   Context,
   ContextCtor,
   Expr,
+  FP,
+  FPNum,
+  FPSort,
+  FPRM,
+  FPRMSort,
   Fixedpoint,
   FuncDecl,
   FuncDeclSignature,
@@ -79,6 +85,8 @@ import {
   Quantifier,
   BodyT,
   RatNum,
+  Seq,
+  SeqSort,
   SMTArray,
   SMTArraySort,
   Solver,
@@ -267,6 +275,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
           return new ArithSortImpl(ast);
         case Z3_sort_kind.Z3_BV_SORT:
           return new BitVecSortImpl(ast);
+        case Z3_sort_kind.Z3_FLOATING_POINT_SORT:
+          return new FPSortImpl(ast);
+        case Z3_sort_kind.Z3_ROUNDING_MODE_SORT:
+          return new FPRMSortImpl(ast);
+        case Z3_sort_kind.Z3_SEQ_SORT:
+          return new SeqSortImpl(ast);
         case Z3_sort_kind.Z3_ARRAY_SORT:
           return new ArraySortImpl(ast);
         default:
@@ -301,6 +315,15 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
             return new BitVecNumImpl(ast);
           }
           return new BitVecImpl(ast);
+        case Z3_sort_kind.Z3_FLOATING_POINT_SORT:
+          if (kind === Z3_ast_kind.Z3_NUMERAL_AST || kind === Z3_ast_kind.Z3_APP_AST) {
+            return new FPNumImpl(ast);
+          }
+          return new FPImpl(ast);
+        case Z3_sort_kind.Z3_ROUNDING_MODE_SORT:
+          return new FPRMImpl(ast);
+        case Z3_sort_kind.Z3_SEQ_SORT:
+          return new SeqImpl(ast);
         case Z3_sort_kind.Z3_ARRAY_SORT:
           return new ArrayImpl(ast);
         default:
@@ -520,6 +543,56 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       return isAppOf(obj, Z3_decl_kind.Z3_OP_CONST_ARRAY);
     }
 
+    function isFPRMSort(obj: unknown): obj is FPRMSort<Name> {
+      const r = obj instanceof FPRMSortImpl;
+      r && _assertContext(obj);
+      return r;
+    }
+
+    function isFPRM(obj: unknown): obj is FPRM<Name> {
+      const r = obj instanceof FPRMImpl;
+      r && _assertContext(obj);
+      return r;
+    }
+
+    function isFPSort(obj: unknown): obj is FPSort<Name> {
+      const r = obj instanceof FPSortImpl;
+      r && _assertContext(obj);
+      return r;
+    }
+
+    function isFP(obj: unknown): obj is FP<Name> {
+      const r = obj instanceof FPImpl;
+      r && _assertContext(obj);
+      return r;
+    }
+
+    function isFPVal(obj: unknown): obj is FPNum<Name> {
+      const r = obj instanceof FPNumImpl;
+      r && _assertContext(obj);
+      return r;
+    }
+
+    function isSeqSort(obj: unknown): obj is SeqSort<Name> {
+      const r = obj instanceof SeqSortImpl;
+      r && _assertContext(obj);
+      return r;
+    }
+
+    function isSeq(obj: unknown): obj is Seq<Name> {
+      const r = obj instanceof SeqImpl;
+      r && _assertContext(obj);
+      return r;
+    }
+
+    function isStringSort(obj: unknown): obj is SeqSort<Name> {
+      return isSeqSort(obj) && obj.isString();
+    }
+
+    function isString(obj: unknown): obj is Seq<Name> {
+      return isSeq(obj) && obj.isString();
+    }
+
     function isProbe(obj: unknown): obj is Probe<Name> {
       const r = obj instanceof ProbeImpl;
       r && _assertContext(obj);
@@ -762,6 +835,119 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         );
       },
     };
+
+    const Float = {
+      sort(ebits: number, sbits: number): FPSort<Name> {
+        assert(Number.isSafeInteger(ebits) && ebits > 0, 'ebits must be a positive integer');
+        assert(Number.isSafeInteger(sbits) && sbits > 0, 'sbits must be a positive integer');
+        return new FPSortImpl(Z3.mk_fpa_sort(contextPtr, ebits, sbits));
+      },
+
+      sort16(): FPSort<Name> {
+        return new FPSortImpl(Z3.mk_fpa_sort_16(contextPtr));
+      },
+
+      sort32(): FPSort<Name> {
+        return new FPSortImpl(Z3.mk_fpa_sort_32(contextPtr));
+      },
+
+      sort64(): FPSort<Name> {
+        return new FPSortImpl(Z3.mk_fpa_sort_64(contextPtr));
+      },
+
+      sort128(): FPSort<Name> {
+        return new FPSortImpl(Z3.mk_fpa_sort_128(contextPtr));
+      },
+
+      const(name: string, sort: FPSort<Name>): FP<Name> {
+        return new FPImpl(check(Z3.mk_const(contextPtr, _toSymbol(name), sort.ptr)));
+      },
+
+      consts(names: string | string[], sort: FPSort<Name>): FP<Name>[] {
+        if (typeof names === 'string') {
+          names = names.split(' ');
+        }
+        return names.map(name => Float.const(name, sort));
+      },
+
+      val(value: number, sort: FPSort<Name>): FPNum<Name> {
+        return new FPNumImpl(check(Z3.mk_fpa_numeral_double(contextPtr, value, sort.ptr)));
+      },
+
+      NaN(sort: FPSort<Name>): FPNum<Name> {
+        return new FPNumImpl(check(Z3.mk_fpa_nan(contextPtr, sort.ptr)));
+      },
+
+      inf(sort: FPSort<Name>, negative: boolean = false): FPNum<Name> {
+        return new FPNumImpl(check(Z3.mk_fpa_inf(contextPtr, sort.ptr, negative)));
+      },
+
+      zero(sort: FPSort<Name>, negative: boolean = false): FPNum<Name> {
+        return new FPNumImpl(check(Z3.mk_fpa_zero(contextPtr, sort.ptr, negative)));
+      },
+    };
+
+    const FloatRM = {
+      sort(): FPRMSort<Name> {
+        return new FPRMSortImpl(Z3.mk_fpa_rounding_mode_sort(contextPtr));
+      },
+
+      RNE(): FPRM<Name> {
+        return new FPRMImpl(check(Z3.mk_fpa_rne(contextPtr)));
+      },
+
+      RNA(): FPRM<Name> {
+        return new FPRMImpl(check(Z3.mk_fpa_rna(contextPtr)));
+      },
+
+      RTP(): FPRM<Name> {
+        return new FPRMImpl(check(Z3.mk_fpa_rtp(contextPtr)));
+      },
+
+      RTN(): FPRM<Name> {
+        return new FPRMImpl(check(Z3.mk_fpa_rtn(contextPtr)));
+      },
+
+      RTZ(): FPRM<Name> {
+        return new FPRMImpl(check(Z3.mk_fpa_rtz(contextPtr)));
+      },
+    };
+
+    const String = {
+      sort(): SeqSort<Name> {
+        return new SeqSortImpl(Z3.mk_string_sort(contextPtr));
+      },
+
+      const(name: string): Seq<Name> {
+        return new SeqImpl(check(Z3.mk_const(contextPtr, _toSymbol(name), String.sort().ptr)));
+      },
+
+      consts(names: string | string[]): Seq<Name>[] {
+        if (typeof names === 'string') {
+          names = names.split(' ');
+        }
+        return names.map(name => String.const(name));
+      },
+
+      val(value: string): Seq<Name> {
+        return new SeqImpl(check(Z3.mk_string(contextPtr, value)));
+      },
+    };
+
+    const Seq = {
+      sort<ElemSort extends Sort<Name>>(elemSort: ElemSort): SeqSort<Name, ElemSort> {
+        return new SeqSortImpl<ElemSort>(Z3.mk_seq_sort(contextPtr, elemSort.ptr));
+      },
+
+      empty<ElemSort extends Sort<Name>>(elemSort: ElemSort): Seq<Name, ElemSort> {
+        return new SeqImpl<ElemSort>(check(Z3.mk_seq_empty(contextPtr, Seq.sort(elemSort).ptr)));
+      },
+
+      unit<ElemSort extends Sort<Name>>(elem: Expr<Name>): Seq<Name, ElemSort> {
+        return new SeqImpl<ElemSort>(check(Z3.mk_seq_unit(contextPtr, elem.ast)));
+      },
+    };
+
     const Array = {
       sort<DomainSort extends NonEmptySortArray<Name>, RangeSort extends AnySort<Name>>(
         ...sig: [...DomainSort, RangeSort]
@@ -2860,6 +3046,261 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       }
     }
 
+    class FPRMSortImpl extends SortImpl implements FPRMSort<Name> {
+      declare readonly __typename: FPRMSort['__typename'];
+
+      cast(other: FPRM<Name>): FPRM<Name>;
+      cast(other: CoercibleToExpr<Name>): never;
+      cast(other: any): any {
+        if (isFPRM(other)) {
+          _assertContext(other);
+          return other;
+        }
+        throw new Error("Can't cast to FPRMSort");
+      }
+    }
+
+    class FPRMImpl extends ExprImpl<Z3_ast, FPRMSortImpl> implements FPRM<Name> {
+      declare readonly __typename: FPRM['__typename'];
+    }
+
+    class FPSortImpl extends SortImpl implements FPSort<Name> {
+      declare readonly __typename: FPSort['__typename'];
+
+      ebits() {
+        return Z3.fpa_get_ebits(contextPtr, this.ptr);
+      }
+
+      sbits() {
+        return Z3.fpa_get_sbits(contextPtr, this.ptr);
+      }
+
+      cast(other: CoercibleToFP<Name>): FP<Name>;
+      cast(other: CoercibleToExpr<Name>): Expr<Name>;
+      cast(other: CoercibleToExpr<Name>): Expr<Name> {
+        if (isExpr(other)) {
+          _assertContext(other);
+          return other;
+        }
+        if (typeof other === 'number') {
+          return Float.val(other, this);
+        }
+        throw new Error("Can't cast to FPSort");
+      }
+    }
+
+    class FPImpl extends ExprImpl<Z3_ast, FPSortImpl> implements FP<Name> {
+      declare readonly __typename: FP['__typename'];
+
+      add(rm: FPRM<Name>, other: CoercibleToFP<Name>): FP<Name> {
+        const otherFP = isFP(other) ? other : Float.val(other, this.sort);
+        return new FPImpl(check(Z3.mk_fpa_add(contextPtr, rm.ast, this.ast, otherFP.ast)));
+      }
+
+      sub(rm: FPRM<Name>, other: CoercibleToFP<Name>): FP<Name> {
+        const otherFP = isFP(other) ? other : Float.val(other, this.sort);
+        return new FPImpl(check(Z3.mk_fpa_sub(contextPtr, rm.ast, this.ast, otherFP.ast)));
+      }
+
+      mul(rm: FPRM<Name>, other: CoercibleToFP<Name>): FP<Name> {
+        const otherFP = isFP(other) ? other : Float.val(other, this.sort);
+        return new FPImpl(check(Z3.mk_fpa_mul(contextPtr, rm.ast, this.ast, otherFP.ast)));
+      }
+
+      div(rm: FPRM<Name>, other: CoercibleToFP<Name>): FP<Name> {
+        const otherFP = isFP(other) ? other : Float.val(other, this.sort);
+        return new FPImpl(check(Z3.mk_fpa_div(contextPtr, rm.ast, this.ast, otherFP.ast)));
+      }
+
+      neg(): FP<Name> {
+        return new FPImpl(check(Z3.mk_fpa_neg(contextPtr, this.ast)));
+      }
+
+      abs(): FP<Name> {
+        return new FPImpl(check(Z3.mk_fpa_abs(contextPtr, this.ast)));
+      }
+
+      sqrt(rm: FPRM<Name>): FP<Name> {
+        return new FPImpl(check(Z3.mk_fpa_sqrt(contextPtr, rm.ast, this.ast)));
+      }
+
+      rem(other: CoercibleToFP<Name>): FP<Name> {
+        const otherFP = isFP(other) ? other : Float.val(other, this.sort);
+        return new FPImpl(check(Z3.mk_fpa_rem(contextPtr, this.ast, otherFP.ast)));
+      }
+
+      fma(rm: FPRM<Name>, y: CoercibleToFP<Name>, z: CoercibleToFP<Name>): FP<Name> {
+        const yFP = isFP(y) ? y : Float.val(y, this.sort);
+        const zFP = isFP(z) ? z : Float.val(z, this.sort);
+        return new FPImpl(check(Z3.mk_fpa_fma(contextPtr, rm.ast, this.ast, yFP.ast, zFP.ast)));
+      }
+
+      lt(other: CoercibleToFP<Name>): Bool<Name> {
+        const otherFP = isFP(other) ? other : Float.val(other, this.sort);
+        return new BoolImpl(check(Z3.mk_fpa_lt(contextPtr, this.ast, otherFP.ast)));
+      }
+
+      gt(other: CoercibleToFP<Name>): Bool<Name> {
+        const otherFP = isFP(other) ? other : Float.val(other, this.sort);
+        return new BoolImpl(check(Z3.mk_fpa_gt(contextPtr, this.ast, otherFP.ast)));
+      }
+
+      le(other: CoercibleToFP<Name>): Bool<Name> {
+        const otherFP = isFP(other) ? other : Float.val(other, this.sort);
+        return new BoolImpl(check(Z3.mk_fpa_leq(contextPtr, this.ast, otherFP.ast)));
+      }
+
+      ge(other: CoercibleToFP<Name>): Bool<Name> {
+        const otherFP = isFP(other) ? other : Float.val(other, this.sort);
+        return new BoolImpl(check(Z3.mk_fpa_geq(contextPtr, this.ast, otherFP.ast)));
+      }
+
+      isNaN(): Bool<Name> {
+        return new BoolImpl(check(Z3.mk_fpa_is_nan(contextPtr, this.ast)));
+      }
+
+      isInf(): Bool<Name> {
+        return new BoolImpl(check(Z3.mk_fpa_is_infinite(contextPtr, this.ast)));
+      }
+
+      isZero(): Bool<Name> {
+        return new BoolImpl(check(Z3.mk_fpa_is_zero(contextPtr, this.ast)));
+      }
+
+      isNormal(): Bool<Name> {
+        return new BoolImpl(check(Z3.mk_fpa_is_normal(contextPtr, this.ast)));
+      }
+
+      isSubnormal(): Bool<Name> {
+        return new BoolImpl(check(Z3.mk_fpa_is_subnormal(contextPtr, this.ast)));
+      }
+
+      isNegative(): Bool<Name> {
+        return new BoolImpl(check(Z3.mk_fpa_is_negative(contextPtr, this.ast)));
+      }
+
+      isPositive(): Bool<Name> {
+        return new BoolImpl(check(Z3.mk_fpa_is_positive(contextPtr, this.ast)));
+      }
+    }
+
+    class FPNumImpl extends FPImpl implements FPNum<Name> {
+      declare readonly __typename: FPNum['__typename'];
+
+      value(): number {
+        // Get the floating-point numeral as a JavaScript number
+        // Note: This may lose precision for values outside JavaScript number range
+        return Z3.get_numeral_double(contextPtr, this.ast);
+      }
+    }
+
+    class SeqSortImpl<ElemSort extends Sort<Name> = Sort<Name>> extends SortImpl implements SeqSort<Name, ElemSort> {
+      declare readonly __typename: SeqSort['__typename'];
+
+      isString(): boolean {
+        return Z3.is_string_sort(contextPtr, this.ptr);
+      }
+
+      basis(): Sort<Name> {
+        return _toSort(check(Z3.get_seq_sort_basis(contextPtr, this.ptr)));
+      }
+
+      cast(other: Seq<Name>): Seq<Name>;
+      cast(other: string): Seq<Name>;
+      cast(other: CoercibleToExpr<Name>): Expr<Name>;
+      cast(other: any): any {
+        if (isSeq(other)) {
+          _assertContext(other);
+          return other;
+        }
+        if (typeof other === 'string') {
+          return String.val(other);
+        }
+        throw new Error("Can't cast to SeqSort");
+      }
+    }
+
+    class SeqImpl<ElemSort extends Sort<Name> = Sort<Name>>
+      extends ExprImpl<Z3_ast, SeqSortImpl<ElemSort>>
+      implements Seq<Name, ElemSort>
+    {
+      declare readonly __typename: Seq['__typename'];
+
+      isString(): boolean {
+        return Z3.is_string_sort(contextPtr, Z3.get_sort(contextPtr, this.ast));
+      }
+
+      asString(): string {
+        if (!Z3.is_string(contextPtr, this.ast)) {
+          throw new Error('Not a string value');
+        }
+        return Z3.get_string(contextPtr, this.ast);
+      }
+
+      concat(other: Seq<Name, ElemSort> | string): Seq<Name, ElemSort> {
+        const otherSeq = isSeq(other) ? other : String.val(other);
+        return new SeqImpl<ElemSort>(check(Z3.mk_seq_concat(contextPtr, [this.ast, otherSeq.ast])));
+      }
+
+      length(): Arith<Name> {
+        return new ArithImpl(check(Z3.mk_seq_length(contextPtr, this.ast)));
+      }
+
+      at(index: Arith<Name> | number | bigint): Seq<Name, ElemSort> {
+        const indexExpr = isArith(index) ? index : Int.val(index);
+        return new SeqImpl<ElemSort>(check(Z3.mk_seq_at(contextPtr, this.ast, indexExpr.ast)));
+      }
+
+      nth(index: Arith<Name> | number | bigint): Expr<Name> {
+        const indexExpr = isArith(index) ? index : Int.val(index);
+        return _toExpr(check(Z3.mk_seq_nth(contextPtr, this.ast, indexExpr.ast)));
+      }
+
+      extract(offset: Arith<Name> | number | bigint, length: Arith<Name> | number | bigint): Seq<Name, ElemSort> {
+        const offsetExpr = isArith(offset) ? offset : Int.val(offset);
+        const lengthExpr = isArith(length) ? length : Int.val(length);
+        return new SeqImpl<ElemSort>(check(Z3.mk_seq_extract(contextPtr, this.ast, offsetExpr.ast, lengthExpr.ast)));
+      }
+
+      indexOf(substr: Seq<Name, ElemSort> | string, offset?: Arith<Name> | number | bigint): Arith<Name> {
+        const substrSeq = isSeq(substr) ? substr : String.val(substr);
+        const offsetExpr = offset !== undefined ? (isArith(offset) ? offset : Int.val(offset)) : Int.val(0);
+        return new ArithImpl(check(Z3.mk_seq_index(contextPtr, this.ast, substrSeq.ast, offsetExpr.ast)));
+      }
+
+      lastIndexOf(substr: Seq<Name, ElemSort> | string): Arith<Name> {
+        const substrSeq = isSeq(substr) ? substr : String.val(substr);
+        return new ArithImpl(check(Z3.mk_seq_last_index(contextPtr, this.ast, substrSeq.ast)));
+      }
+
+      contains(substr: Seq<Name, ElemSort> | string): Bool<Name> {
+        const substrSeq = isSeq(substr) ? substr : String.val(substr);
+        return new BoolImpl(check(Z3.mk_seq_contains(contextPtr, this.ast, substrSeq.ast)));
+      }
+
+      prefixOf(s: Seq<Name, ElemSort> | string): Bool<Name> {
+        const sSeq = isSeq(s) ? s : String.val(s);
+        return new BoolImpl(check(Z3.mk_seq_prefix(contextPtr, this.ast, sSeq.ast)));
+      }
+
+      suffixOf(s: Seq<Name, ElemSort> | string): Bool<Name> {
+        const sSeq = isSeq(s) ? s : String.val(s);
+        return new BoolImpl(check(Z3.mk_seq_suffix(contextPtr, this.ast, sSeq.ast)));
+      }
+
+      replace(src: Seq<Name, ElemSort> | string, dst: Seq<Name, ElemSort> | string): Seq<Name, ElemSort> {
+        const srcSeq = isSeq(src) ? src : String.val(src);
+        const dstSeq = isSeq(dst) ? dst : String.val(dst);
+        return new SeqImpl<ElemSort>(check(Z3.mk_seq_replace(contextPtr, this.ast, srcSeq.ast, dstSeq.ast)));
+      }
+
+      replaceAll(src: Seq<Name, ElemSort> | string, dst: Seq<Name, ElemSort> | string): Seq<Name, ElemSort> {
+        const srcSeq = isSeq(src) ? src : String.val(src);
+        const dstSeq = isSeq(dst) ? dst : String.val(dst);
+        return new SeqImpl<ElemSort>(check(Z3.mk_seq_replace_all(contextPtr, this.ast, srcSeq.ast, dstSeq.ast)));
+      }
+    }
+
     class ArraySortImpl<DomainSort extends NonEmptySortArray<Name>, RangeSort extends Sort<Name>>
       extends SortImpl
       implements SMTArraySort<Name, DomainSort, RangeSort>
@@ -3529,6 +3970,15 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       isBitVecSort,
       isBitVec,
       isBitVecVal, // TODO fix ordering
+      isFPRMSort,
+      isFPRM,
+      isFPSort,
+      isFP,
+      isFPVal,
+      isSeqSort,
+      isSeq,
+      isStringSort,
+      isString,
       isArraySort,
       isArray,
       isConstArray,
@@ -3550,6 +4000,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       Int,
       Real,
       BitVec,
+      Float,
+      FloatRM,
+      String,
+      Seq,
       Array,
       Set,
       Datatype,
diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts
index ffc7aecc3..fa14ebfd6 100644
--- a/src/api/js/src/high-level/types.ts
+++ b/src/api/js/src/high-level/types.ts
@@ -25,7 +25,10 @@ export type AnySort<Name extends string = 'main'> =
   | BoolSort<Name>
   | ArithSort<Name>
   | BitVecSort<number, Name>
-  | SMTArraySort<Name>;
+  | SMTArraySort<Name>
+  | FPSort<Name>
+  | FPRMSort<Name>
+  | SeqSort<Name>;
 /** @hidden */
 export type AnyExpr<Name extends string = 'main'> =
   | Expr<Name>
@@ -35,7 +38,11 @@ export type AnyExpr<Name extends string = 'main'> =
   | RatNum<Name>
   | BitVec<number, Name>
   | BitVecNum<number, Name>
-  | SMTArray<Name>;
+  | SMTArray<Name>
+  | FP<Name>
+  | FPNum<Name>
+  | FPRM<Name>
+  | Seq<Name>;
 /** @hidden */
 export type AnyAst<Name extends string = 'main'> = AnyExpr<Name> | AnySort<Name> | FuncDecl<Name>;
 
@@ -49,6 +56,12 @@ export type SortToExprMap<S extends AnySort<Name>, Name extends string = 'main'>
   ? BitVec<Size, Name>
   : S extends SMTArraySort<Name, infer DomainSort, infer RangeSort>
   ? SMTArray<Name, DomainSort, RangeSort>
+  : S extends FPSort<Name>
+  ? FP<Name>
+  : S extends FPRMSort<Name>
+  ? FPRM<Name>
+  : S extends SeqSort<Name>
+  ? Seq<Name>
   : S extends Sort<Name>
   ? Expr<Name, S, Z3_ast>
   : never;
@@ -71,6 +84,9 @@ export type CoercibleToBitVec<Bits extends number = number, Name extends string
   | number
   | BitVec<Bits, Name>;
 
+/** @hidden */
+export type CoercibleToFP<Name extends string = 'main'> = number | FP<Name>;
+
 export type CoercibleRational = { numerator: bigint | number; denominator: bigint | number };
 
 /** @hidden */
@@ -97,6 +113,8 @@ export type CoercibleToMap<T extends AnyExpr<Name>, Name extends string = 'main'
   ? CoercibleToArith<Name>
   : T extends BitVec<infer Size, Name>
   ? CoercibleToBitVec<Size, Name>
+  : T extends FP<Name>
+  ? CoercibleToFP<Name>
   : T extends SMTArray<Name, infer DomainSort, infer RangeSort>
   ? SMTArray<Name, DomainSort, RangeSort>
   : T extends Expr<Name>
@@ -258,6 +276,33 @@ export interface Context<Name extends string = 'main'> {
   /** @category Functions */
   isConstArray(obj: unknown): boolean;
 
+  /** @category Functions */
+  isFPSort(obj: unknown): obj is FPSort<Name>;
+
+  /** @category Functions */
+  isFP(obj: unknown): obj is FP<Name>;
+
+  /** @category Functions */
+  isFPVal(obj: unknown): obj is FPNum<Name>;
+
+  /** @category Functions */
+  isFPRMSort(obj: unknown): obj is FPRMSort<Name>;
+
+  /** @category Functions */
+  isFPRM(obj: unknown): obj is FPRM<Name>;
+
+  /** @category Functions */
+  isSeqSort(obj: unknown): obj is SeqSort<Name>;
+
+  /** @category Functions */
+  isSeq(obj: unknown): obj is Seq<Name>;
+
+  /** @category Functions */
+  isStringSort(obj: unknown): obj is SeqSort<Name>;
+
+  /** @category Functions */
+  isString(obj: unknown): obj is Seq<Name>;
+
   /** @category Functions */
   isProbe(obj: unknown): obj is Probe<Name>;
 
@@ -371,6 +416,14 @@ export interface Context<Name extends string = 'main'> {
   /** @category Expressions */
   readonly BitVec: BitVecCreation<Name>;
   /** @category Expressions */
+  readonly Float: FPCreation<Name>;
+  /** @category Expressions */
+  readonly FloatRM: FPRMCreation<Name>;
+  /** @category Expressions */
+  readonly String: StringCreation<Name>;
+  /** @category Expressions */
+  readonly Seq: SeqCreation<Name>;
+  /** @category Expressions */
   readonly Array: SMTArrayCreation<Name>;
   /** @category Expressions */
   readonly Set: SMTSetCreation<Name>;
@@ -1327,7 +1380,10 @@ export interface Sort<Name extends string = 'main'> extends Ast<Name, Z3_sort> {
     | ArithSort['__typename']
     | BitVecSort['__typename']
     | SMTArraySort['__typename']
-    | DatatypeSort['__typename'];
+    | DatatypeSort['__typename']
+    | FPSort['__typename']
+    | FPRMSort['__typename']
+    | SeqSort['__typename'];
 
   kind(): Z3_sort_kind;
 
@@ -1451,6 +1507,9 @@ export interface Expr<Name extends string = 'main', S extends Sort<Name> = AnySo
     | Bool['__typename']
     | Arith['__typename']
     | BitVec['__typename']
+    | FP['__typename']
+    | FPRM['__typename']
+    | Seq['__typename']
     | SMTArray['__typename']
     | DatatypeExpr['__typename'];
 
@@ -2256,6 +2315,356 @@ export interface DatatypeExpr<Name extends string = 'main'> extends Expr<Name, D
   readonly __typename: 'DatatypeExpr';
 }
 
+///////////////////////
+// Floating-Point API //
+///////////////////////
+
+/**
+ * Floating-point rounding mode sort
+ * @category Floating-Point
+ */
+export interface FPRMSort<Name extends string = 'main'> extends Sort<Name> {
+  /** @hidden */
+  readonly __typename: 'FPRMSort';
+
+  cast(other: FPRM<Name>): FPRM<Name>;
+  cast(other: CoercibleToExpr<Name>): never;
+}
+
+/**
+ * Floating-point sort (IEEE 754)
+ * @category Floating-Point
+ */
+export interface FPSort<Name extends string = 'main'> extends Sort<Name> {
+  /** @hidden */
+  readonly __typename: 'FPSort';
+
+  /**
+   * Number of exponent bits
+   */
+  ebits(): number;
+
+  /**
+   * Number of significand bits (including hidden bit)
+   */
+  sbits(): number;
+
+  cast(other: CoercibleToFP<Name>): FP<Name>;
+  cast(other: CoercibleToExpr<Name>): Expr<Name>;
+}
+
+/** @category Floating-Point */
+export interface FPCreation<Name extends string> {
+  /**
+   * Create a floating-point sort with custom exponent and significand bit sizes
+   * @param ebits Number of exponent bits
+   * @param sbits Number of significand bits (including hidden bit)
+   */
+  sort(ebits: number, sbits: number): FPSort<Name>;
+
+  /**
+   * IEEE 754 16-bit floating-point sort (half precision)
+   */
+  sort16(): FPSort<Name>;
+
+  /**
+   * IEEE 754 32-bit floating-point sort (single precision)
+   */
+  sort32(): FPSort<Name>;
+
+  /**
+   * IEEE 754 64-bit floating-point sort (double precision)
+   */
+  sort64(): FPSort<Name>;
+
+  /**
+   * IEEE 754 128-bit floating-point sort (quadruple precision)
+   */
+  sort128(): FPSort<Name>;
+
+  /**
+   * Create a floating-point constant
+   */
+  const(name: string, sort: FPSort<Name>): FP<Name>;
+
+  /**
+   * Create multiple floating-point constants
+   */
+  consts(names: string | string[], sort: FPSort<Name>): FP<Name>[];
+
+  /**
+   * Create a floating-point value from a number
+   */
+  val(value: number, sort: FPSort<Name>): FPNum<Name>;
+
+  /**
+   * Create floating-point NaN
+   */
+  NaN(sort: FPSort<Name>): FPNum<Name>;
+
+  /**
+   * Create floating-point infinity
+   * @param negative If true, creates negative infinity
+   */
+  inf(sort: FPSort<Name>, negative?: boolean): FPNum<Name>;
+
+  /**
+   * Create floating-point zero
+   * @param negative If true, creates negative zero
+   */
+  zero(sort: FPSort<Name>, negative?: boolean): FPNum<Name>;
+}
+
+/** @category Floating-Point */
+export interface FPRMCreation<Name extends string> {
+  /**
+   * Get the floating-point rounding mode sort
+   */
+  sort(): FPRMSort<Name>;
+
+  /**
+   * Round nearest, ties to even (default rounding mode)
+   */
+  RNE(): FPRM<Name>;
+
+  /**
+   * Round nearest, ties to away
+   */
+  RNA(): FPRM<Name>;
+
+  /**
+   * Round toward positive infinity
+   */
+  RTP(): FPRM<Name>;
+
+  /**
+   * Round toward negative infinity
+   */
+  RTN(): FPRM<Name>;
+
+  /**
+   * Round toward zero
+   */
+  RTZ(): FPRM<Name>;
+}
+
+/**
+ * Floating-point rounding mode expression
+ * @category Floating-Point
+ */
+export interface FPRM<Name extends string = 'main'> extends Expr<Name, FPRMSort<Name>, Z3_ast> {
+  /** @hidden */
+  readonly __typename: 'FPRM';
+}
+
+/**
+ * Floating-point expression (IEEE 754)
+ * @category Floating-Point
+ */
+export interface FP<Name extends string = 'main'> extends Expr<Name, FPSort<Name>, Z3_ast> {
+  /** @hidden */
+  readonly __typename: 'FP' | FPNum['__typename'];
+
+  /** @category Arithmetic */
+  add(rm: FPRM<Name>, other: CoercibleToFP<Name>): FP<Name>;
+
+  /** @category Arithmetic */
+  sub(rm: FPRM<Name>, other: CoercibleToFP<Name>): FP<Name>;
+
+  /** @category Arithmetic */
+  mul(rm: FPRM<Name>, other: CoercibleToFP<Name>): FP<Name>;
+
+  /** @category Arithmetic */
+  div(rm: FPRM<Name>, other: CoercibleToFP<Name>): FP<Name>;
+
+  /** @category Arithmetic */
+  neg(): FP<Name>;
+
+  /** @category Arithmetic */
+  abs(): FP<Name>;
+
+  /** @category Arithmetic */
+  sqrt(rm: FPRM<Name>): FP<Name>;
+
+  /** @category Arithmetic */
+  rem(other: CoercibleToFP<Name>): FP<Name>;
+
+  /** @category Arithmetic */
+  fma(rm: FPRM<Name>, y: CoercibleToFP<Name>, z: CoercibleToFP<Name>): FP<Name>;
+
+  /** @category Comparison */
+  lt(other: CoercibleToFP<Name>): Bool<Name>;
+
+  /** @category Comparison */
+  gt(other: CoercibleToFP<Name>): Bool<Name>;
+
+  /** @category Comparison */
+  le(other: CoercibleToFP<Name>): Bool<Name>;
+
+  /** @category Comparison */
+  ge(other: CoercibleToFP<Name>): Bool<Name>;
+
+  /** @category Predicates */
+  isNaN(): Bool<Name>;
+
+  /** @category Predicates */
+  isInf(): Bool<Name>;
+
+  /** @category Predicates */
+  isZero(): Bool<Name>;
+
+  /** @category Predicates */
+  isNormal(): Bool<Name>;
+
+  /** @category Predicates */
+  isSubnormal(): Bool<Name>;
+
+  /** @category Predicates */
+  isNegative(): Bool<Name>;
+
+  /** @category Predicates */
+  isPositive(): Bool<Name>;
+}
+
+/**
+ * Floating-point numeral value
+ * @category Floating-Point
+ */
+export interface FPNum<Name extends string = 'main'> extends FP<Name> {
+  /** @hidden */
+  readonly __typename: 'FPNum';
+
+  /**
+   * Get the floating-point value as a JavaScript number
+   * Note: May lose precision for values outside JavaScript number range
+   */
+  value(): number;
+}
+
+///////////////////////
+// String/Sequence API //
+///////////////////////
+
+/**
+ * Sequence sort (can be string or sequence of any element type)
+ * @category String/Sequence
+ */
+export interface SeqSort<Name extends string = 'main', ElemSort extends Sort<Name> = Sort<Name>> extends Sort<Name> {
+  /** @hidden */
+  readonly __typename: 'SeqSort';
+
+  /**
+   * Check if this is a string sort
+   */
+  isString(): boolean;
+
+  /**
+   * Get the element sort of this sequence
+   */
+  basis(): Sort<Name>;
+
+  cast(other: Seq<Name>): Seq<Name>;
+  cast(other: string): Seq<Name>;
+  cast(other: CoercibleToExpr<Name>): Expr<Name>;
+}
+
+/** @category String/Sequence */
+export interface StringCreation<Name extends string> {
+  /**
+   * Create a string sort
+   */
+  sort(): SeqSort<Name>;
+
+  /**
+   * Create a string constant
+   */
+  const(name: string): Seq<Name>;
+
+  /**
+   * Create multiple string constants
+   */
+  consts(names: string | string[]): Seq<Name>[];
+
+  /**
+   * Create a string value
+   */
+  val(value: string): Seq<Name>;
+}
+
+/** @category String/Sequence */
+export interface SeqCreation<Name extends string> {
+  /**
+   * Create a sequence sort over the given element sort
+   */
+  sort<ElemSort extends Sort<Name>>(elemSort: ElemSort): SeqSort<Name, ElemSort>;
+
+  /**
+   * Create an empty sequence
+   */
+  empty<ElemSort extends Sort<Name>>(elemSort: ElemSort): Seq<Name, ElemSort>;
+
+  /**
+   * Create a unit sequence (sequence with single element)
+   */
+  unit<ElemSort extends Sort<Name>>(elem: Expr<Name>): Seq<Name, ElemSort>;
+}
+
+/**
+ * Sequence expression (includes strings)
+ * @category String/Sequence
+ */
+export interface Seq<Name extends string = 'main', ElemSort extends Sort<Name> = Sort<Name>>
+  extends Expr<Name, SeqSort<Name, ElemSort>, Z3_ast> {
+  /** @hidden */
+  readonly __typename: 'Seq';
+
+  /**
+   * Check if this is a string value
+   */
+  isString(): boolean;
+
+  /**
+   * Get string value if this is a concrete string
+   */
+  asString(): string;
+
+  /** @category Operations */
+  concat(other: Seq<Name, ElemSort> | string): Seq<Name, ElemSort>;
+
+  /** @category Operations */
+  length(): Arith<Name>;
+
+  /** @category Operations */
+  at(index: Arith<Name> | number | bigint): Seq<Name, ElemSort>;
+
+  /** @category Operations */
+  nth(index: Arith<Name> | number | bigint): Expr<Name>;
+
+  /** @category Operations */
+  extract(offset: Arith<Name> | number | bigint, length: Arith<Name> | number | bigint): Seq<Name, ElemSort>;
+
+  /** @category Operations */
+  indexOf(substr: Seq<Name, ElemSort> | string, offset?: Arith<Name> | number | bigint): Arith<Name>;
+
+  /** @category Operations */
+  lastIndexOf(substr: Seq<Name, ElemSort> | string): Arith<Name>;
+
+  /** @category Operations */
+  contains(substr: Seq<Name, ElemSort> | string): Bool<Name>;
+
+  /** @category Operations */
+  prefixOf(s: Seq<Name, ElemSort> | string): Bool<Name>;
+
+  /** @category Operations */
+  suffixOf(s: Seq<Name, ElemSort> | string): Bool<Name>;
+
+  /** @category Operations */
+  replace(src: Seq<Name, ElemSort> | string, dst: Seq<Name, ElemSort> | string): Seq<Name, ElemSort>;
+
+  /** @category Operations */
+  replaceAll(src: Seq<Name, ElemSort> | string, dst: Seq<Name, ElemSort> | string): Seq<Name, ElemSort>;
+}
+
 /**
  * Defines the expression type of the body of a quantifier expression
  *