Add TypeScript API parity: Solver introspection, congruence closure, and Model sort universe methods (#8129)

* Initial plan

* Add TypeScript API parity: Solver and Model introspection methods

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

* Format code and add API parity demo example

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

* Add comprehensive API parity documentation

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

* Fix Context usage in tests and demo - use api.Context('main')

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

* Delete src/api/js/API_PARITY.md

* Delete src/api/js/examples/high-level/api-parity-demo.ts

---------

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/scripts/make-cc-wrapper.ts

@@ -12,26 +12,28 @@ export function makeCCWrapper() {
     if (fn == null) {
       throw new Error(`could not find definition for ${fnName}`);
     }
-    
+
     // Check if function has array parameters
     const arrayParams = fn.params.filter(p => p.isArray && p.kind === 'in_array');
     const hasArrayParams = arrayParams.length > 0;
-    
+
     if (hasArrayParams) {
       // Generate custom wrapper for functions with array parameters
-      const paramList = fn.params.map(p => `${p.isConst ? 'const ' : ''}${p.cType}${p.isPtr ? '*' : ''} ${p.name}${p.isArray ? '[]' : ''}`).join(', ');
-      
+      const paramList = fn.params
+        .map(p => `${p.isConst ? 'const ' : ''}${p.cType}${p.isPtr ? '*' : ''} ${p.name}${p.isArray ? '[]' : ''}`)
+        .join(', ');
+
       // Find the size parameter for each array and build copy/free code
       const arrayCopies: string[] = [];
       const arrayFrees: string[] = [];
       const arrayCopyNames: string[] = [];
-      
+
       for (let p of arrayParams) {
         const sizeParam = fn.params[p.sizeIndex!];
         const ptrType = p.cType.endsWith('*') ? p.cType : `${p.cType}*`;
         const copyName = `${p.name}_copy`;
         arrayCopyNames.push(copyName);
-        
+
         // Allocate and copy with null check
         arrayCopies.push(`${ptrType} ${copyName} = (${ptrType})malloc(sizeof(${p.cType}) * ${sizeParam.name});`);
         arrayCopies.push(`if (!${copyName}) {`);
@@ -39,25 +41,27 @@ export function makeCCWrapper() {
         arrayCopies.push(`  return;`);
         arrayCopies.push(`}`);
         arrayCopies.push(`memcpy(${copyName}, ${p.name}, sizeof(${p.cType}) * ${sizeParam.name});`);
-        
+
         arrayFrees.push(`free(${copyName});`);
       }
-      
+
       // Build lambda capture list
       const nonArrayParams = fn.params.filter(p => !p.isArray || p.kind !== 'in_array');
       const captureList = [...arrayCopyNames, ...nonArrayParams.map(p => p.name)].join(', ');
-      
+
       // Build argument list for the actual function call, using copied arrays
-      const callArgs = fn.params.map(p => {
-        if (p.isArray && p.kind === 'in_array') {
-          return `${p.name}_copy`;
-        }
-        return p.name;
-      }).join(', ');
-      
+      const callArgs = fn.params
+        .map(p => {
+          if (p.isArray && p.kind === 'in_array') {
+            return `${p.name}_copy`;
+          }
+          return p.name;
+        })
+        .join(', ');
+
       const isString = fn.cRet === 'Z3_string';
       const returnType = isString ? 'auto' : fn.cRet;
-      
+
       wrappers.push(
         `
 extern "C" void async_${fn.name}(${paramList}) {
@@ -65,15 +69,19 @@ extern "C" void async_${fn.name}(${paramList}) {
   std::thread t([${captureList}] {
     try {
       ${returnType} result = ${fn.name}(${callArgs});
-      ${isString ? `
+      ${
+        isString
+          ? `
       MAIN_THREAD_ASYNC_EM_ASM({
         resolve_async(UTF8ToString($0));
       }, result);
-      ` : `
+      `
+          : `
       MAIN_THREAD_ASYNC_EM_ASM({
         resolve_async($0);
       }, result);
-      `}
+      `
+      }
     } catch (std::exception& e) {
       MAIN_THREAD_ASYNC_EM_ASM({
         reject_async(new Error(UTF8ToString($0)));

src/api/js/scripts/make-ts-wrapper.ts

@@ -150,7 +150,7 @@ async function makeTsWrapper() {
 
     let arrayLengthParams = new Map();
     let allocatedArrays: string[] = []; // Track allocated arrays for cleanup
-    
+
     for (let p of inParams) {
       if (p.nullable && !p.isArray) {
         // this would be easy to implement - just map null to 0 - but nothing actually uses nullable non-array input parameters, so we can't ensure we've done it right
@@ -181,7 +181,7 @@ async function makeTsWrapper() {
       }
       args[sizeIndex] = `${p.name}.length`;
       params[sizeIndex] = null;
-      
+
       // For async functions, we need to manually manage array memory
       // because ccall frees it before the async thread uses it
       if (isAsync && p.kind === 'in_array') {
@@ -197,13 +197,14 @@ async function makeTsWrapper() {
         ctypes[paramIdx] = 'number'; // Pass as pointer, not array
       }
     }
-    
+
     // Add try-finally for async functions with allocated arrays
     if (isAsync && allocatedArrays.length > 0) {
       prefix += `
       try {
       `.trim();
-      suffix = `
+      suffix =
+        `
       } finally {
         ${allocatedArrays.map(arr => `Mod._free(${arr});`).join('\n        ')}
       }

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

@@ -178,7 +178,7 @@ describe('high-level', () => {
       const { Bool, Solver } = api.Context('main');
       const solver = new Solver();
       solver.set('unsat_core', true);
-      
+
       const x = Bool.const('x');
       const y = Bool.const('y');
       const z = Bool.const('z');
@@ -191,7 +191,7 @@ describe('high-level', () => {
       // This tests the async array parameter fix
       const result = await solver.check(x.not(), y.not(), z.not());
       expect(result).toStrictEqual('unsat');
-      
+
       // Verify we can get the unsat core
       const core = solver.unsatCore();
       expect(core.length()).toBeGreaterThan(0);
@@ -1014,4 +1014,204 @@ describe('high-level', () => {
       expect(typeof (TreeListSort as any).cdr).not.toBe('undefined');
     });
   });
+
+  describe('solver introspection APIs', () => {
+    it('can retrieve unit literals', async () => {
+      const { Solver, Bool } = api.Context('main');
+
+      const solver = new Solver();
+      const x = Bool.const('x');
+
+      // Add a constraint that makes x true
+      solver.add(x);
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+
+      // Get unit literals
+      const units = solver.units();
+      expect(units).toBeDefined();
+      expect(units.length()).toBeGreaterThanOrEqual(0);
+    });
+
+    it('can retrieve non-unit literals', async () => {
+      const { Solver, Bool } = api.Context('main');
+
+      const solver = new Solver();
+      const x = Bool.const('x');
+      const y = Bool.const('y');
+
+      solver.add(x.or(y));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+
+      // Get non-unit literals
+      const nonUnits = solver.nonUnits();
+      expect(nonUnits).toBeDefined();
+      expect(nonUnits.length()).toBeGreaterThanOrEqual(0);
+    });
+
+    it('can retrieve solver trail', async () => {
+      const { Solver, Bool } = api.Context('main');
+
+      const solver = new Solver();
+      const x = Bool.const('x');
+      const y = Bool.const('y');
+
+      solver.add(x.implies(y));
+      solver.add(x);
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+
+      // Get trail
+      const trail = solver.trail();
+      expect(trail).toBeDefined();
+      expect(trail.length()).toBeGreaterThanOrEqual(0);
+    });
+  });
+
+  describe('solver congruence closure APIs', () => {
+    it('can get congruence root', async () => {
+      const { Solver, Int } = api.Context('main');
+
+      const solver = new Solver();
+      const x = Int.const('x');
+      const y = Int.const('y');
+
+      solver.add(x.eq(y));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+
+      // Get congruence root
+      const root = solver.congruenceRoot(x);
+      expect(root).toBeDefined();
+    });
+
+    it('can get congruence next', async () => {
+      const { Solver, Int } = api.Context('main');
+
+      const solver = new Solver();
+      const x = Int.const('x');
+      const y = Int.const('y');
+      const z = Int.const('z');
+
+      solver.add(x.eq(y));
+      solver.add(y.eq(z));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+
+      // Get next element in congruence class
+      const next = solver.congruenceNext(x);
+      expect(next).toBeDefined();
+    });
+
+    it('can explain congruence', async () => {
+      const { Solver, Int } = api.Context('main');
+
+      const solver = new Solver();
+      const x = Int.const('x');
+      const y = Int.const('y');
+
+      solver.add(x.eq(y));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+
+      // Get explanation for why x and y are congruent
+      const explanation = solver.congruenceExplain(x, y);
+      expect(explanation).toBeDefined();
+    });
+  });
+
+  describe('model sort universe APIs', () => {
+    it('can get number of sorts', async () => {
+      const { Solver, Sort, Const } = api.Context('main');
+
+      const solver = new Solver();
+      const A = Sort.declare('A');
+      const x = Const('x', A);
+
+      solver.add(x.eq(x));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+
+      const model = solver.model();
+      const numSorts = model.numSorts();
+      expect(numSorts).toBeGreaterThanOrEqual(0);
+    });
+
+    it('can get individual sort by index', async () => {
+      const { Solver, Sort, Const } = api.Context('main');
+
+      const solver = new Solver();
+      const A = Sort.declare('A');
+      const x = Const('x', A);
+
+      solver.add(x.eq(x));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+
+      const model = solver.model();
+      const numSorts = model.numSorts();
+
+      if (numSorts > 0) {
+        const sort = model.getSort(0);
+        expect(sort).toBeDefined();
+      }
+    });
+
+    it('can get all sorts', async () => {
+      const { Solver, Sort, Const } = api.Context('main');
+
+      const solver = new Solver();
+      const A = Sort.declare('A');
+      const x = Const('x', A);
+
+      solver.add(x.eq(x));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+
+      const model = solver.model();
+      const sorts = model.getSorts();
+      expect(Array.isArray(sorts)).toBe(true);
+      expect(sorts.length).toBe(model.numSorts());
+    });
+
+    it('can get sort universe', async () => {
+      const { Solver, Sort, Const } = api.Context('main');
+
+      const solver = new Solver();
+      const A = Sort.declare('A');
+      const x = Const('x', A);
+      const y = Const('y', A);
+
+      solver.add(x.neq(y));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+
+      const model = solver.model();
+      const universe = model.sortUniverse(A);
+      expect(universe).toBeDefined();
+      expect(universe.length()).toBeGreaterThanOrEqual(2); // At least x and y
+    });
+  });
+
+  describe('solver file loading API', () => {
+    it('has fromFile method', () => {
+      const { Solver } = api.Context('main');
+      const solver = new Solver();
+
+      // Just verify the method exists - we don't test actual file loading
+      // as that would require creating test files
+      expect(typeof solver.fromFile).toBe('function');
+    });
+  });
 });

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

@@ -1537,6 +1537,39 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         throwIfError();
       }
 
+      units(): AstVector<Name, Bool<Name>> {
+        return new AstVectorImpl(check(Z3.solver_get_units(contextPtr, this.ptr)));
+      }
+
+      nonUnits(): AstVector<Name, Bool<Name>> {
+        return new AstVectorImpl(check(Z3.solver_get_non_units(contextPtr, this.ptr)));
+      }
+
+      trail(): AstVector<Name, Bool<Name>> {
+        return new AstVectorImpl(check(Z3.solver_get_trail(contextPtr, this.ptr)));
+      }
+
+      congruenceRoot(expr: Expr<Name>): Expr<Name> {
+        _assertContext(expr);
+        return _toExpr(check(Z3.solver_congruence_root(contextPtr, this.ptr, expr.ast)));
+      }
+
+      congruenceNext(expr: Expr<Name>): Expr<Name> {
+        _assertContext(expr);
+        return _toExpr(check(Z3.solver_congruence_next(contextPtr, this.ptr, expr.ast)));
+      }
+
+      congruenceExplain(a: Expr<Name>, b: Expr<Name>): Expr<Name> {
+        _assertContext(a);
+        _assertContext(b);
+        return _toExpr(check(Z3.solver_congruence_explain(contextPtr, this.ptr, a.ast, b.ast)));
+      }
+
+      fromFile(filename: string) {
+        Z3.solver_from_file(contextPtr, this.ptr, filename);
+        throwIfError();
+      }
+
       release() {
         Z3.solver_dec_ref(contextPtr, this.ptr);
         // Mark the ptr as null to prevent double free
@@ -1824,6 +1857,27 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return new AstVectorImpl(check(Z3.model_get_sort_universe(contextPtr, this.ptr, sort.ptr)));
       }
 
+      numSorts(): number {
+        return check(Z3.model_get_num_sorts(contextPtr, this.ptr));
+      }
+
+      getSort(i: number): Sort<Name> {
+        return _toSort(check(Z3.model_get_sort(contextPtr, this.ptr, i)));
+      }
+
+      getSorts(): Sort<Name>[] {
+        const n = this.numSorts();
+        const result: Sort<Name>[] = [];
+        for (let i = 0; i < n; i++) {
+          result.push(this.getSort(i));
+        }
+        return result;
+      }
+
+      sortUniverse(sort: Sort<Name>): AstVector<Name, AnyExpr<Name>> {
+        return this.getUniverse(sort) as AstVector<Name, AnyExpr<Name>>;
+      }
+
       release() {
         Z3.model_dec_ref(contextPtr, this.ptr);
         this._ptr = null;
@@ -2905,9 +2959,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
     }
 
     class QuantifierImpl<
-      QVarSorts extends NonEmptySortArray<Name>,
-      QSort extends BoolSort<Name> | SMTArraySort<Name, QVarSorts>,
-    >
+        QVarSorts extends NonEmptySortArray<Name>,
+        QSort extends BoolSort<Name> | SMTArraySort<Name, QVarSorts>,
+      >
       extends ExprImpl<Z3_ast, QSort>
       implements Quantifier<Name, QVarSorts, QSort>
     {

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

@@ -815,6 +815,144 @@ export interface Solver<Name extends string = 'main'> {
    */
   reasonUnknown(): string;
 
+  /**
+   * Retrieve the set of literals that were inferred by the solver as unit literals.
+   * These are boolean literals that the solver has determined must be true in all models.
+   *
+   * @returns An AstVector containing the unit literals
+   *
+   * @example
+   * ```typescript
+   * const solver = new Solver();
+   * const x = Bool.const('x');
+   * solver.add(x.or(x)); // simplifies to x
+   * await solver.check();
+   * const units = solver.units();
+   * console.log('Unit literals:', units.length());
+   * ```
+   */
+  units(): AstVector<Name, Bool<Name>>;
+
+  /**
+   * Retrieve the set of tracked boolean literals that are not unit literals.
+   *
+   * @returns An AstVector containing the non-unit literals
+   *
+   * @example
+   * ```typescript
+   * const solver = new Solver();
+   * const x = Bool.const('x');
+   * const y = Bool.const('y');
+   * solver.add(x.or(y));
+   * await solver.check();
+   * const nonUnits = solver.nonUnits();
+   * ```
+   */
+  nonUnits(): AstVector<Name, Bool<Name>>;
+
+  /**
+   * Retrieve the trail of boolean literals assigned by the solver during solving.
+   * The trail represents the sequence of decisions and propagations made by the solver.
+   *
+   * @returns An AstVector containing the trail of assigned literals
+   *
+   * @example
+   * ```typescript
+   * const solver = new Solver();
+   * const x = Bool.const('x');
+   * const y = Bool.const('y');
+   * solver.add(x.implies(y));
+   * solver.add(x);
+   * await solver.check();
+   * const trail = solver.trail();
+   * console.log('Trail length:', trail.length());
+   * ```
+   */
+  trail(): AstVector<Name, Bool<Name>>;
+
+  /**
+   * Retrieve the root of the congruence class containing the given expression.
+   * This is useful for understanding equality reasoning in the solver.
+   *
+   * Note: This works primarily with SimpleSolver and may not work with terms
+   * eliminated during preprocessing.
+   *
+   * @param expr - The expression to find the congruence root for
+   * @returns The root expression of the congruence class
+   *
+   * @example
+   * ```typescript
+   * const solver = new Solver();
+   * const x = Int.const('x');
+   * const y = Int.const('y');
+   * solver.add(x.eq(y));
+   * await solver.check();
+   * const root = solver.congruenceRoot(x);
+   * ```
+   */
+  congruenceRoot(expr: Expr<Name>): Expr<Name>;
+
+  /**
+   * Retrieve the next expression in the congruence class containing the given expression.
+   * The congruence class forms a circular linked list.
+   *
+   * Note: This works primarily with SimpleSolver and may not work with terms
+   * eliminated during preprocessing.
+   *
+   * @param expr - The expression to find the next congruent expression for
+   * @returns The next expression in the congruence class
+   *
+   * @example
+   * ```typescript
+   * const solver = new Solver();
+   * const x = Int.const('x');
+   * const y = Int.const('y');
+   * const z = Int.const('z');
+   * solver.add(x.eq(y));
+   * solver.add(y.eq(z));
+   * await solver.check();
+   * const next = solver.congruenceNext(x);
+   * ```
+   */
+  congruenceNext(expr: Expr<Name>): Expr<Name>;
+
+  /**
+   * Explain why two expressions are congruent according to the solver's reasoning.
+   * Returns a proof term explaining the congruence.
+   *
+   * Note: This works primarily with SimpleSolver and may not work with terms
+   * eliminated during preprocessing.
+   *
+   * @param a - First expression
+   * @param b - Second expression
+   * @returns An expression representing the proof of congruence
+   *
+   * @example
+   * ```typescript
+   * const solver = new Solver();
+   * const x = Int.const('x');
+   * const y = Int.const('y');
+   * solver.add(x.eq(y));
+   * await solver.check();
+   * const explanation = solver.congruenceExplain(x, y);
+   * ```
+   */
+  congruenceExplain(a: Expr<Name>, b: Expr<Name>): Expr<Name>;
+
+  /**
+   * Load SMT-LIB2 format assertions from a file into the solver.
+   *
+   * @param filename - Path to the file containing SMT-LIB2 format assertions
+   *
+   * @example
+   * ```typescript
+   * const solver = new Solver();
+   * solver.fromFile('problem.smt2');
+   * const result = await solver.check();
+   * ```
+   */
+  fromFile(filename: string): void;
+
   /**
    * Manually decrease the reference count of the solver
    * This is automatically done when the solver is garbage collected,
@@ -911,6 +1049,86 @@ export interface Model<Name extends string = 'main'> extends Iterable<FuncDecl<N
     defaultValue: CoercibleToMap<SortToExprMap<RangeSort, Name>, Name>,
   ): FuncInterp<Name>;
 
+  /**
+   * Return the number of uninterpreted sorts that have an interpretation in the model.
+   *
+   * @returns The number of uninterpreted sorts
+   *
+   * @example
+   * ```typescript
+   * const { Solver, Sort } = await init();
+   * const solver = new Solver();
+   * const A = Sort.declare('A');
+   * const x = Const('x', A);
+   * solver.add(x.eq(x));
+   * await solver.check();
+   * const model = solver.model();
+   * console.log('Number of sorts:', model.numSorts());
+   * ```
+   */
+  numSorts(): number;
+
+  /**
+   * Return the uninterpreted sort at the given index.
+   *
+   * @param i - Index of the sort (must be less than numSorts())
+   * @returns The sort at the given index
+   *
+   * @example
+   * ```typescript
+   * const model = solver.model();
+   * for (let i = 0; i < model.numSorts(); i++) {
+   *   const sort = model.getSort(i);
+   *   console.log('Sort:', sort.toString());
+   * }
+   * ```
+   */
+  getSort(i: number): Sort<Name>;
+
+  /**
+   * Return all uninterpreted sorts that have an interpretation in the model.
+   *
+   * @returns An array of all uninterpreted sorts
+   *
+   * @example
+   * ```typescript
+   * const model = solver.model();
+   * const sorts = model.getSorts();
+   * for (const sort of sorts) {
+   *   console.log('Sort:', sort.toString());
+   *   const universe = model.sortUniverse(sort);
+   *   console.log('Universe size:', universe.length());
+   * }
+   * ```
+   */
+  getSorts(): Sort<Name>[];
+
+  /**
+   * Return the finite set of elements that represent the interpretation for the given sort.
+   * This is only applicable to uninterpreted sorts with finite interpretations.
+   *
+   * @param sort - The sort to get the universe for
+   * @returns An AstVector containing all elements in the sort's universe
+   *
+   * @example
+   * ```typescript
+   * const { Solver, Sort, Const } = await init();
+   * const solver = new Solver();
+   * const A = Sort.declare('A');
+   * const x = Const('x', A);
+   * const y = Const('y', A);
+   * solver.add(x.neq(y));
+   * await solver.check();
+   * const model = solver.model();
+   * const universe = model.sortUniverse(A);
+   * console.log('Universe has', universe.length(), 'elements');
+   * for (let i = 0; i < universe.length(); i++) {
+   *   console.log('Element:', universe.get(i).toString());
+   * }
+   * ```
+   */
+  sortUniverse(sort: Sort<Name>): AstVector<Name, AnyExpr<Name>>;
+
   /**
    * Manually decrease the reference count of the model
    * This is automatically done when the model is garbage collected,
@@ -1063,10 +1281,8 @@ export interface FuncDecl<
   call(...args: CoercibleToArrayIndexType<Name, DomainSort>): SortToExprMap<RangeSort, Name>;
 }
 
-export interface Expr<Name extends string = 'main', S extends Sort<Name> = AnySort<Name>, Ptr = unknown> extends Ast<
-  Name,
-  Ptr
-> {
+export interface Expr<Name extends string = 'main', S extends Sort<Name> = AnySort<Name>, Ptr = unknown>
+  extends Ast<Name, Ptr> {
   /** @hidden */
   readonly __typename:
     | 'Expr'
@@ -1365,11 +1581,8 @@ export interface BitVecCreation<Name extends string> {
  * Represents Bit Vector expression
  * @category Bit Vectors
  */
-export interface BitVec<Bits extends number = number, Name extends string = 'main'> extends Expr<
-  Name,
-  BitVecSort<Bits, Name>,
-  Z3_ast
-> {
+export interface BitVec<Bits extends number = number, Name extends string = 'main'>
+  extends Expr<Name, BitVecSort<Bits, Name>, Z3_ast> {
   /** @hidden */
   readonly __typename: 'BitVec' | BitVecNum['__typename'];
 
@@ -1751,11 +1964,8 @@ export interface SMTSetCreation<Name extends string> {
  * @typeParam ElemSort The sort of the element of the set
  * @category Arrays
  */
-export interface SMTSet<Name extends string = 'main', ElemSort extends AnySort<Name> = Sort<Name>> extends Expr<
-  Name,
-  SMTSetSort<Name, ElemSort>,
-  Z3_ast
-> {
+export interface SMTSet<Name extends string = 'main', ElemSort extends AnySort<Name> = Sort<Name>>
+  extends Expr<Name, SMTSetSort<Name, ElemSort>, Z3_ast> {
   readonly __typename: 'Array';
 
   elemSort(): ElemSort;