mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-18 16:28:56 +00:00
Code Activity

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

Browse source 
* 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>
This commit is contained in:
Copilot 2026-01-08 19:53:08 -08:00 • committed by GitHub
parent bc4f587acc
commit f690afa6b1
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 300 additions and 88 deletions
Download patch file Download diff file Expand all files Collapse all files

75
src/api/js/src/high-level/high-level.test.ts
View file

@ -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');

128
src/api/js/src/high-level/high-level.ts
View file

@ -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>> {
return new AstVectorImpl(check(Z3.solver_get_unsat_core(contextPtr, this.ptr)));
reasonUnknown(): string {
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>,
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>
{
@ -3243,6 +3307,8 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
PbEq,
PbGe,
PbLe,
AtMost,
AtLeast,
ForAll,
Exists,
Lambda,

185
src/api/js/src/high-level/types.ts
View file

@ -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>
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'
@ -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'>
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'];
@ -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 */