Add AtMost, AtLeast, unsatCore, and reasonUnknown to JS/TS API (#8118)

* Initial plan

* Add AtMost, AtLeast, checkAssumptions, and unsatCore methods to JS/TS API

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

* Format code with prettier

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

* Add comprehensive documentation for Solver.check, checkAssumptions, and unsatCore methods

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

* Remove redundant checkAssumptions method, use check() for assumptions

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

* Enable unsat_core tracking in test to fix 'unknown' result

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

* Add reasonUnknown() method and use it in test to debug unknown results

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

---------

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

@@ -559,7 +559,10 @@ describe('high-level', () => {
       const set = Z3.Set.const('set', Z3.Int.sort());
       const [a, b] = Z3.Int.consts('a b');
 
-      const conjecture = set.contains(a).and(set.contains(b)).implies(Z3.Set.val([a, b], Z3.Int.sort()).subsetOf(set));
+      const conjecture = set
+        .contains(a)
+        .and(set.contains(b))
+        .implies(Z3.Set.val([a, b], Z3.Int.sort()).subsetOf(set));
       await prove(conjecture);
     });
 
@@ -569,7 +572,10 @@ describe('high-level', () => {
       const set = Z3.Set.const('set', Z3.Int.sort());
       const [a, b] = Z3.Int.consts('a b');
 
-      const conjecture = set.contains(a).and(set.contains(b)).and(Z3.Set.val([a, b], Z3.Int.sort()).eq(set));
+      const conjecture = set
+        .contains(a)
+        .and(set.contains(b))
+        .and(Z3.Set.val([a, b], Z3.Int.sort()).eq(set));
       await solve(conjecture);
     });
 
@@ -583,7 +589,7 @@ describe('high-level', () => {
       const conjecture = set.intersect(abset).subsetOf(abset);
       await prove(conjecture);
     });
-    
+
     it('Intersection 2', async () => {
       const Z3 = api.Context('main');
 
@@ -605,7 +611,7 @@ describe('high-level', () => {
       const conjecture = set.subsetOf(set.union(abset));
       await prove(conjecture);
     });
-    
+
     it('Union 2', async () => {
       const Z3 = api.Context('main');
 
@@ -616,14 +622,14 @@ describe('high-level', () => {
       const conjecture = set.union(abset).subsetOf(abset);
       await solve(conjecture);
     });
-    
+
     it('Complement 1', async () => {
       const Z3 = api.Context('main');
 
       const set = Z3.Set.const('set', Z3.Int.sort());
       const a = Z3.Int.const('a');
 
-      const conjecture = set.complement().complement().eq(set)
+      const conjecture = set.complement().complement().eq(set);
       await prove(conjecture);
     });
     it('Complement 2', async () => {
@@ -632,28 +638,28 @@ describe('high-level', () => {
       const set = Z3.Set.const('set', Z3.Int.sort());
       const a = Z3.Int.const('a');
 
-      const conjecture = set.contains(a).implies(Z3.Not(set.complement().contains(a)))
+      const conjecture = set.contains(a).implies(Z3.Not(set.complement().contains(a)));
       await prove(conjecture);
     });
-    
+
     it('Difference', async () => {
       const Z3 = api.Context('main');
 
       const [set1, set2] = Z3.Set.consts('set1 set2', Z3.Int.sort());
       const a = Z3.Int.const('a');
 
-      const conjecture = set1.contains(a).implies(Z3.Not(set2.diff(set1).contains(a)))
+      const conjecture = set1.contains(a).implies(Z3.Not(set2.diff(set1).contains(a)));
-      
+
       await prove(conjecture);
     });
-    
+
     it('FullSet', async () => {
       const Z3 = api.Context('main');
 
       const set = Z3.Set.const('set', Z3.Int.sort());
 
       const conjecture = set.complement().eq(Z3.FullSet(Z3.Int.sort()).diff(set));
-      
+
       await prove(conjecture);
     });
 
@@ -664,7 +670,7 @@ describe('high-level', () => {
       const [a, b] = Z3.Int.consts('a b');
 
       const conjecture = empty.add(a).add(b).del(a).del(b).eq(empty);
-      
+
       await prove(conjecture);
     });
   });
@@ -793,6 +799,31 @@ describe('high-level', () => {
         });
       expect(results).toStrictEqual([1n, 2n, 3n, 4n, 5n]);
     });
+
+    it('can use check with assumptions and unsatCore', async () => {
+      const { Solver, Bool } = 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');
+
+      // Add conflicting assertions
+      solver.add(x.or(y));
+      solver.add(x.or(z));
+
+      // Check with assumptions that create a conflict
+      const result = await solver.check(x.not(), y.not(), z.not());
+      if (result === 'unknown') {
+        console.log('Solver returned unknown. Reason:', solver.reasonUnknown());
+      }
+      expect(result).toStrictEqual('unsat');
+
+      // Get the unsat core
+      const core = solver.unsatCore();
+      expect(core.length()).toBeGreaterThan(0);
+      expect(core.length()).toBeLessThanOrEqual(3);
+    });
   });
 
   describe('AstVector', () => {
@@ -923,14 +954,14 @@ describe('high-level', () => {
       Color.declare('red');
       Color.declare('green');
       Color.declare('blue');
-      
+
       const ColorSort = Color.create();
-      
+
       // Test that we can access the constructors
       expect(typeof (ColorSort as any).red).not.toBe('undefined');
       expect(typeof (ColorSort as any).green).not.toBe('undefined');
       expect(typeof (ColorSort as any).blue).not.toBe('undefined');
-      
+
       // Test that we can access the recognizers
       expect(typeof (ColorSort as any).is_red).not.toBe('undefined');
       expect(typeof (ColorSort as any).is_green).not.toBe('undefined');
@@ -944,9 +975,9 @@ describe('high-level', () => {
       const List = Datatype('List');
       List.declare('cons', ['car', Int.sort()], ['cdr', List]);
       List.declare('nil');
-      
+
       const ListSort = List.create();
-      
+
       // Test that constructors and accessors exist
       expect(typeof (ListSort as any).cons).not.toBe('undefined');
       expect(typeof (ListSort as any).nil).not.toBe('undefined');
@@ -962,20 +993,20 @@ describe('high-level', () => {
       // Create mutually recursive Tree and TreeList datatypes
       const Tree = Datatype('Tree');
       const TreeList = Datatype('TreeList');
-      
+
       Tree.declare('leaf', ['value', Int.sort()]);
       Tree.declare('node', ['children', TreeList]);
       TreeList.declare('nil');
       TreeList.declare('cons', ['car', Tree], ['cdr', TreeList]);
-      
+
       const [TreeSort, TreeListSort] = Datatype.createDatatypes(Tree, TreeList);
-      
+
       // Test that both datatypes have their constructors
       expect(typeof (TreeSort as any).leaf).not.toBe('undefined');
       expect(typeof (TreeSort as any).node).not.toBe('undefined');
       expect(typeof (TreeListSort as any).nil).not.toBe('undefined');
       expect(typeof (TreeListSort as any).cons).not.toBe('undefined');
-      
+
       // Test accessors exist
       expect(typeof (TreeSort as any).value).not.toBe('undefined');
       expect(typeof (TreeSort as any).children).not.toBe('undefined');

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

@@ -808,12 +808,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       sort<ElemSort extends AnySort<Name>>(sort: ElemSort): SMTSetSort<Name, ElemSort> {
         return Array.sort(sort, Bool.sort());
       },
-      const<ElemSort extends AnySort<Name>>(name: string, sort: ElemSort) : SMTSet<Name, ElemSort> {
+      const<ElemSort extends AnySort<Name>>(name: string, sort: ElemSort): SMTSet<Name, ElemSort> {
         return new SetImpl<ElemSort>(
           check(Z3.mk_const(contextPtr, _toSymbol(name), Array.sort(sort, Bool.sort()).ptr)),
         );
       },
-      consts<ElemSort extends AnySort<Name>>(names: string | string[], sort: ElemSort) : SMTSet<Name, ElemSort>[] {
+      consts<ElemSort extends AnySort<Name>>(names: string | string[], sort: ElemSort): SMTSet<Name, ElemSort>[] {
         if (typeof names === 'string') {
           names = names.split(' ');
         }
@@ -822,14 +822,17 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       empty<ElemSort extends AnySort<Name>>(sort: ElemSort): SMTSet<Name, ElemSort> {
         return EmptySet(sort);
       },
-      val<ElemSort extends AnySort<Name>>(values: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>[], sort: ElemSort): SMTSet<Name, ElemSort> {
+      val<ElemSort extends AnySort<Name>>(
+        values: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>[],
+        sort: ElemSort,
+      ): SMTSet<Name, ElemSort> {
         var result = EmptySet(sort);
         for (const value of values) {
           result = SetAdd(result, value);
         }
         return result;
-      }
+      },
-    }
+    };
 
     const Datatype = Object.assign(
       (name: string): DatatypeImpl => {
@@ -838,8 +841,8 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       {
         createDatatypes(...datatypes: DatatypeImpl[]): DatatypeSortImpl[] {
           return createDatatypes(...datatypes);
-        }
+        },
-      }
+      },
     );
 
     ////////////////
@@ -1058,6 +1061,32 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       );
     }
 
+    function AtMost(args: [Bool<Name>, ...Bool<Name>[]], k: number): Bool<Name> {
+      _assertContext(...args);
+      return new BoolImpl(
+        check(
+          Z3.mk_atmost(
+            contextPtr,
+            args.map(arg => arg.ast),
+            k,
+          ),
+        ),
+      );
+    }
+
+    function AtLeast(args: [Bool<Name>, ...Bool<Name>[]], k: number): Bool<Name> {
+      _assertContext(...args);
+      return new BoolImpl(
+        check(
+          Z3.mk_atleast(
+            contextPtr,
+            args.map(arg => arg.ast),
+            k,
+          ),
+        ),
+      );
+    }
+
     function ForAll<QVarSorts extends NonEmptySortArray<Name>>(
       quantifiers: ArrayIndexType<Name, QVarSorts>,
       body: Bool<Name>,
@@ -1296,41 +1325,69 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
     }
 
     function SetUnion<ElemSort extends AnySort<Name>>(...args: SMTSet<Name, ElemSort>[]): SMTSet<Name, ElemSort> {
-      return new SetImpl<ElemSort>(check(Z3.mk_set_union(contextPtr, args.map(arg => arg.ast))));
+      return new SetImpl<ElemSort>(
+        check(
+          Z3.mk_set_union(
+            contextPtr,
+            args.map(arg => arg.ast),
+          ),
+        ),
+      );
     }
-    
+
     function SetIntersect<ElemSort extends AnySort<Name>>(...args: SMTSet<Name, ElemSort>[]): SMTSet<Name, ElemSort> {
-      return new SetImpl<ElemSort>(check(Z3.mk_set_intersect(contextPtr, args.map(arg => arg.ast))));
+      return new SetImpl<ElemSort>(
+        check(
+          Z3.mk_set_intersect(
+            contextPtr,
+            args.map(arg => arg.ast),
+          ),
+        ),
+      );
     }
-    
+
-    function SetDifference<ElemSort extends AnySort<Name>>(a: SMTSet<Name, ElemSort>, b: SMTSet<Name, ElemSort>): SMTSet<Name, ElemSort> {
+    function SetDifference<ElemSort extends AnySort<Name>>(
+      a: SMTSet<Name, ElemSort>,
+      b: SMTSet<Name, ElemSort>,
+    ): SMTSet<Name, ElemSort> {
       return new SetImpl<ElemSort>(check(Z3.mk_set_difference(contextPtr, a.ast, b.ast)));
     }
-    
 
-    function SetAdd<ElemSort extends AnySort<Name>>(set: SMTSet<Name, ElemSort>, elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>): SMTSet<Name, ElemSort> {
+    function SetAdd<ElemSort extends AnySort<Name>>(
+      set: SMTSet<Name, ElemSort>,
+      elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>,
+    ): SMTSet<Name, ElemSort> {
       const arg = set.elemSort().cast(elem as any);
       return new SetImpl<ElemSort>(check(Z3.mk_set_add(contextPtr, set.ast, arg.ast)));
     }
-    function SetDel<ElemSort extends AnySort<Name>>(set: SMTSet<Name, ElemSort>, elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>): SMTSet<Name, ElemSort> {
+    function SetDel<ElemSort extends AnySort<Name>>(
+      set: SMTSet<Name, ElemSort>,
+      elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>,
+    ): SMTSet<Name, ElemSort> {
       const arg = set.elemSort().cast(elem as any);
       return new SetImpl<ElemSort>(check(Z3.mk_set_del(contextPtr, set.ast, arg.ast)));
     }
     function SetComplement<ElemSort extends AnySort<Name>>(set: SMTSet<Name, ElemSort>): SMTSet<Name, ElemSort> {
       return new SetImpl<ElemSort>(check(Z3.mk_set_complement(contextPtr, set.ast)));
     }
-    
+
     function EmptySet<ElemSort extends AnySort<Name>>(sort: ElemSort): SMTSet<Name, ElemSort> {
       return new SetImpl<ElemSort>(check(Z3.mk_empty_set(contextPtr, sort.ptr)));
     }
     function FullSet<ElemSort extends AnySort<Name>>(sort: ElemSort): SMTSet<Name, ElemSort> {
       return new SetImpl<ElemSort>(check(Z3.mk_full_set(contextPtr, sort.ptr)));
     }
-    function isMember<ElemSort extends AnySort<Name>>(elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>, set: SMTSet<Name, ElemSort>): Bool<Name> {
+    function isMember<ElemSort extends AnySort<Name>>(
+      elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>,
+      set: SMTSet<Name, ElemSort>,
+    ): Bool<Name> {
       const arg = set.elemSort().cast(elem as any);
       return new BoolImpl(check(Z3.mk_set_member(contextPtr, arg.ast, set.ast)));
     }
-    function isSubset<ElemSort extends AnySort<Name>>(a: SMTSet<Name, ElemSort>, b: SMTSet<Name, ElemSort>): Bool<Name> {
+    function isSubset<ElemSort extends AnySort<Name>>(
+      a: SMTSet<Name, ElemSort>,
+      b: SMTSet<Name, ElemSort>,
+    ): Bool<Name> {
       return new BoolImpl(check(Z3.mk_set_subset(contextPtr, a.ast, b.ast)));
     }
 
@@ -1459,12 +1516,16 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         }
       }
 
+      unsatCore(): AstVector<Name, Bool<Name>> {
+        return new AstVectorImpl(check(Z3.solver_get_unsat_core(contextPtr, this.ptr)));
+      }
+
       model() {
         return new ModelImpl(check(Z3.solver_get_model(contextPtr, this.ptr)));
       }
 
-      unsatCore(): AstVector<Name, Bool<Name>> {
+      reasonUnknown(): string {
-        return new AstVectorImpl(check(Z3.solver_get_unsat_core(contextPtr, this.ptr)));
+        return check(Z3.solver_get_reason_unknown(contextPtr, this.ptr));
       }
 
       toString() {
@@ -2629,7 +2690,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       }
     }
 
-    class SetImpl<ElemSort extends Sort<Name>> extends ExprImpl<Z3_ast, ArraySortImpl<[ElemSort], BoolSort<Name>>> implements SMTSet<Name, ElemSort> {
+    class SetImpl<ElemSort extends Sort<Name>>
+      extends ExprImpl<Z3_ast, ArraySortImpl<[ElemSort], BoolSort<Name>>>
+      implements SMTSet<Name, ElemSort>
+    {
       declare readonly __typename: 'Array';
 
       elemSort(): ElemSort {
@@ -2757,7 +2821,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
 
             for (const [fieldName, fieldSort] of fields) {
               fieldNames.push(fieldName);
-              
+
               if (fieldSort instanceof DatatypeImpl) {
                 // Reference to another datatype being defined
                 const refIndex = datatypes.indexOf(fieldSort);
@@ -2780,7 +2844,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
               Z3.mk_string_symbol(contextPtr, `is_${constructorName}`),
               fieldNames.map(name => Z3.mk_string_symbol(contextPtr, name)),
               fieldSorts,
-              fieldRefs
+              fieldRefs,
             );
             constructors.push(constructor);
             scopedConstructors.push(constructor);
@@ -2798,14 +2862,14 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         const results: DatatypeSortImpl[] = [];
         for (let i = 0; i < resultSorts.length; i++) {
           const sortImpl = new DatatypeSortImpl(resultSorts[i]);
-          
+
           // Attach constructor, recognizer, and accessor functions dynamically
           const numConstructors = sortImpl.numConstructors();
           for (let j = 0; j < numConstructors; j++) {
             const constructor = sortImpl.constructorDecl(j);
             const recognizer = sortImpl.recognizer(j);
             const constructorName = constructor.name().toString();
-            
+
             // Attach constructor function
             if (constructor.arity() === 0) {
               // Nullary constructor (constant)
@@ -2813,10 +2877,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
             } else {
               (sortImpl as any)[constructorName] = constructor;
             }
-            
+
             // Attach recognizer function
             (sortImpl as any)[`is_${constructorName}`] = recognizer;
-            
+
             // Attach accessor functions
             for (let k = 0; k < constructor.arity(); k++) {
               const accessor = sortImpl.accessor(j, k);
@@ -2824,7 +2888,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
               (sortImpl as any)[accessorName] = accessor;
             }
           }
-          
+
           results.push(sortImpl);
         }
 
@@ -2841,9 +2905,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
     }
 
     class QuantifierImpl<
-        QVarSorts extends NonEmptySortArray<Name>,
+      QVarSorts extends NonEmptySortArray<Name>,
-        QSort extends BoolSort<Name> | SMTArraySort<Name, QVarSorts>,
+      QSort extends BoolSort<Name> | SMTArraySort<Name, QVarSorts>,
-      >
+    >
       extends ExprImpl<Z3_ast, QSort>
       implements Quantifier<Name, QVarSorts, QSort>
     {
@@ -3243,6 +3307,8 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       PbEq,
       PbGe,
       PbLe,
+      AtMost,
+      AtLeast,
       ForAll,
       Exists,
       Lambda,

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

@@ -73,7 +73,13 @@ export type CoercibleToBitVec<Bits extends number = number, Name extends string
 export type CoercibleRational = { numerator: bigint | number; denominator: bigint | number };
 
 /** @hidden */
-export type CoercibleToExpr<Name extends string = 'main'> = number | string | bigint | boolean | CoercibleRational | Expr<Name>;
+export type CoercibleToExpr<Name extends string = 'main'> =
+  | number
+  | string
+  | bigint
+  | boolean
+  | CoercibleRational
+  | Expr<Name>;
 
 /** @hidden */
 export type CoercibleToArith<Name extends string = 'main'> = number | string | bigint | CoercibleRational | Arith<Name>;
@@ -448,6 +454,12 @@ export interface Context<Name extends string = 'main'> {
   /** @category Operations */
   PbLe(args: [Bool<Name>, ...Bool<Name>[]], coeffs: [number, ...number[]], k: number): Bool<Name>;
 
+  /** @category Operations */
+  AtMost(args: [Bool<Name>, ...Bool<Name>[]], k: number): Bool<Name>;
+
+  /** @category Operations */
+  AtLeast(args: [Bool<Name>, ...Bool<Name>[]], k: number): Bool<Name>;
+
   // Quantifiers
 
   /** @category Operations */
@@ -621,33 +633,45 @@ export interface Context<Name extends string = 'main'> {
   substitute(t: Expr<Name>, ...substitutions: [Expr<Name>, Expr<Name>][]): Expr<Name>;
 
   simplify(expr: Expr<Name>): Promise<Expr<Name>>;
-  
+
   /** @category Operations */
   SetUnion<ElemSort extends AnySort<Name>>(...args: SMTSet<Name, ElemSort>[]): SMTSet<Name, ElemSort>;
-  
+
   /** @category Operations */
   SetIntersect<ElemSort extends AnySort<Name>>(...args: SMTSet<Name, ElemSort>[]): SMTSet<Name, ElemSort>;
-  
-  /** @category Operations */
-  SetDifference<ElemSort extends AnySort<Name>>(a: SMTSet<Name, ElemSort>, b: SMTSet<Name, ElemSort>): SMTSet<Name, ElemSort>;
 
   /** @category Operations */
-  SetAdd<ElemSort extends AnySort<Name>>(set: SMTSet<Name, ElemSort>, elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>): SMTSet<Name, ElemSort>;
+  SetDifference<ElemSort extends AnySort<Name>>(
+    a: SMTSet<Name, ElemSort>,
+    b: SMTSet<Name, ElemSort>,
+  ): SMTSet<Name, ElemSort>;
 
   /** @category Operations */
-  SetDel<ElemSort extends AnySort<Name>>(set: SMTSet<Name, ElemSort>, elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>): SMTSet<Name, ElemSort>;
+  SetAdd<ElemSort extends AnySort<Name>>(
+    set: SMTSet<Name, ElemSort>,
+    elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>,
+  ): SMTSet<Name, ElemSort>;
+
+  /** @category Operations */
+  SetDel<ElemSort extends AnySort<Name>>(
+    set: SMTSet<Name, ElemSort>,
+    elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>,
+  ): SMTSet<Name, ElemSort>;
 
   /** @category Operations */
   SetComplement<ElemSort extends AnySort<Name>>(set: SMTSet<Name, ElemSort>): SMTSet<Name, ElemSort>;
-  
+
   /** @category Operations */
   EmptySet<ElemSort extends AnySort<Name>>(sort: ElemSort): SMTSet<Name, ElemSort>;
 
   /** @category Operations */
   FullSet<ElemSort extends AnySort<Name>>(sort: ElemSort): SMTSet<Name, ElemSort>;
-  
+
   /** @category Operations */
-  isMember<ElemSort extends AnySort<Name>>(elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>, set: SMTSet<Name, ElemSort>): Bool<Name>;
+  isMember<ElemSort extends AnySort<Name>>(
+    elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>,
+    set: SMTSet<Name, ElemSort>,
+  ): Bool<Name>;
 
   /** @category Operations */
   isSubset<ElemSort extends AnySort<Name>>(a: SMTSet<Name, ElemSort>, b: SMTSet<Name, ElemSort>): Bool<Name>;
@@ -709,12 +733,90 @@ export interface Solver<Name extends string = 'main'> {
 
   fromString(s: string): void;
 
+  /**
+   * Check whether the assertions in the solver are consistent or not.
+   *
+   * Optionally, you can provide additional boolean expressions as assumptions.
+   * These assumptions are temporary and only used for this check - they are not
+   * permanently added to the solver.
+   *
+   * @param exprs - Optional assumptions to check in addition to the solver's assertions.
+   *                These are temporary and do not modify the solver state.
+   * @returns A promise resolving to:
+   *          - `'sat'` if the assertions (plus assumptions) are satisfiable
+   *          - `'unsat'` if they are unsatisfiable
+   *          - `'unknown'` if Z3 cannot determine satisfiability
+   *
+   * @example
+   * ```typescript
+   * const solver = new Solver();
+   * const x = Int.const('x');
+   * solver.add(x.gt(0));
+   *
+   * // Check without assumptions
+   * await solver.check(); // 'sat'
+   *
+   * // Check with temporary assumption (doesn't modify solver)
+   * await solver.check(x.lt(0)); // 'unsat'
+   * await solver.check(); // still 'sat' - assumption was temporary
+   * ```
+   *
+   * @see {@link unsatCore} - Retrieve unsat core after checking with assumptions
+   */
   check(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): Promise<CheckSatResult>;
 
+  /**
+   * Retrieve the unsat core after a check that returned `'unsat'`.
+   *
+   * The unsat core is a (typically small) subset of the assumptions that were
+   * sufficient to determine unsatisfiability. This is useful for understanding
+   * which assumptions are conflicting.
+   *
+   * Note: To use unsat cores effectively, you should call {@link check} with
+   * assumptions (not just assertions added via {@link add}).
+   *
+   * @returns An AstVector containing the subset of assumptions that caused UNSAT
+   *
+   * @example
+   * ```typescript
+   * const solver = new Solver();
+   * const x = Bool.const('x');
+   * const y = Bool.const('y');
+   * const z = Bool.const('z');
+   * solver.add(x.or(y));
+   * solver.add(x.or(z));
+   *
+   * const result = await solver.check(x.not(), y.not(), z.not());
+   * if (result === 'unsat') {
+   *   const core = solver.unsatCore();
+   *   // core will contain a minimal set of conflicting assumptions
+   *   console.log('UNSAT core size:', core.length());
+   * }
+   * ```
+   *
+   * @see {@link check} - Check with assumptions to use with unsat core
+   */
+  unsatCore(): AstVector<Name, Bool<Name>>;
+
   model(): Model<Name>;
 
   unsatCore(): AstVector<Name, Bool<Name>>;
 
+  /**
+   * Return a string describing why the last call to {@link check} returned `'unknown'`.
+   *
+   * @returns A string explaining the reason, or an empty string if the last check didn't return unknown
+   *
+   * @example
+   * ```typescript
+   * const result = await solver.check();
+   * if (result === 'unknown') {
+   *   console.log('Reason:', solver.reasonUnknown());
+   * }
+   * ```
+   */
+  reasonUnknown(): string;
+
   /**
    * Manually decrease the reference count of the solver
    * This is automatically done when the solver is garbage collected,
@@ -963,8 +1065,10 @@ 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>
+export interface Expr<Name extends string = 'main', S extends Sort<Name> = AnySort<Name>, Ptr = unknown> extends Ast<
-  extends Ast<Name, Ptr> {
+  Name,
+  Ptr
+> {
   /** @hidden */
   readonly __typename:
     | 'Expr'
@@ -1263,8 +1367,11 @@ export interface BitVecCreation<Name extends string> {
  * Represents Bit Vector expression
  * @category Bit Vectors
  */
-export interface BitVec<Bits extends number = number, Name extends string = 'main'>
+export interface BitVec<Bits extends number = number, Name extends string = 'main'> extends Expr<
-  extends Expr<Name, BitVecSort<Bits, Name>, Z3_ast> {
+  Name,
+  BitVecSort<Bits, Name>,
+  Z3_ast
+> {
   /** @hidden */
   readonly __typename: 'BitVec' | BitVecNum['__typename'];
 
@@ -1614,12 +1721,15 @@ export interface SMTArray<
 
 /**
  * Set Implemented using Arrays
- * 
+ *
  * @typeParam ElemSort The sort of the element of the set
  * @category Sets
  */
-export type SMTSetSort<Name extends string = 'main', ElemSort extends AnySort<Name> = Sort<Name>> = SMTArraySort<Name, [ElemSort], BoolSort<Name>>;
+export type SMTSetSort<Name extends string = 'main', ElemSort extends AnySort<Name> = Sort<Name>> = SMTArraySort<
-
+  Name,
+  [ElemSort],
+  BoolSort<Name>
+>;
 
 /** @category Sets*/
 export interface SMTSetCreation<Name extends string> {
@@ -1628,10 +1738,13 @@ export interface SMTSetCreation<Name extends string> {
   const<ElemSort extends AnySort<Name>>(name: string, elemSort: ElemSort): SMTSet<Name, ElemSort>;
 
   consts<ElemSort extends AnySort<Name>>(names: string | string[], elemSort: ElemSort): SMTSet<Name, ElemSort>[];
-  
+
   empty<ElemSort extends AnySort<Name>>(sort: ElemSort): SMTSet<Name, ElemSort>;
-  
+
-  val<ElemSort extends AnySort<Name>>(values: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>[], sort: ElemSort): SMTSet<Name, ElemSort>;
+  val<ElemSort extends AnySort<Name>>(
+    values: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>[],
+    sort: ElemSort,
+  ): SMTSet<Name, ElemSort>;
 }
 
 /**
@@ -1640,23 +1753,25 @@ 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;
 
   union(...args: SMTSet<Name, ElemSort>[]): SMTSet<Name, ElemSort>;
   intersect(...args: SMTSet<Name, ElemSort>[]): SMTSet<Name, ElemSort>;
   diff(b: SMTSet<Name, ElemSort>): SMTSet<Name, ElemSort>;
-  
 
   add(elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>): SMTSet<Name, ElemSort>;
   del(elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>): SMTSet<Name, ElemSort>;
   complement(): SMTSet<Name, ElemSort>;
-  
+
   contains(elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>): Bool<Name>;
   subsetOf(b: SMTSet<Name, ElemSort>): Bool<Name>;
-
 }
 //////////////////////////////////////////
 //
@@ -1666,10 +1781,10 @@ export interface SMTSet<Name extends string = 'main', ElemSort extends AnySort<N
 
 /**
  * Helper class for declaring Z3 datatypes.
- * 
+ *
  * Follows the same pattern as Python Z3 API for declaring constructors
  * before creating the actual datatype sort.
- * 
+ *
  * @example
  * ```typescript
  * const List = new ctx.Datatype('List');
@@ -1677,7 +1792,7 @@ export interface SMTSet<Name extends string = 'main', ElemSort extends AnySort<N
  * List.declare('nil');
  * const ListSort = List.create();
  * ```
- * 
+ *
  * @category Datatypes
  */
 export interface Datatype<Name extends string = 'main'> {
@@ -1686,7 +1801,7 @@ export interface Datatype<Name extends string = 'main'> {
 
   /**
    * Declare a constructor for this datatype.
-   * 
+   *
    * @param name Constructor name
    * @param fields Array of [field_name, field_sort] pairs
    */
@@ -1710,7 +1825,7 @@ export interface DatatypeCreation<Name extends string> {
 
   /**
    * Create mutually recursive datatypes.
-   * 
+   *
    * @param datatypes Array of Datatype declarations
    * @returns Array of created DatatypeSort instances
    */
@@ -1719,10 +1834,10 @@ export interface DatatypeCreation<Name extends string> {
 
 /**
  * A Sort representing an algebraic datatype.
- * 
+ *
  * After creation, this sort will have constructor, recognizer, and accessor
  * functions dynamically attached based on the declared constructors.
- * 
+ *
  * @category Datatypes
  */
 export interface DatatypeSort<Name extends string = 'main'> extends Sort<Name> {
@@ -1756,8 +1871,8 @@ export interface DatatypeSort<Name extends string = 'main'> extends Sort<Name> {
 
 /**
  * Represents expressions of datatype sorts.
- * 
+ *
- * @category Datatypes  
+ * @category Datatypes
  */
 export interface DatatypeExpr<Name extends string = 'main'> extends Expr<Name, DatatypeSort<Name>, Z3_ast> {
   /** @hidden */