From 60f5a76516d599f5aaeb0ea41d7994e3c62eff12 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 20 Feb 2026 04:28:10 +0000 Subject: [PATCH] Add tests and documentation for addAndTrack in TypeScript bindings (fix discussion #8705) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/api/js/package-lock.json | 8 ++- src/api/js/src/high-level/high-level.test.ts | 51 ++++++++++++++++++++ src/api/js/src/high-level/types.ts | 44 +++++++++++++++++ 3 files changed, 102 insertions(+), 1 deletion(-) diff --git a/src/api/js/package-lock.json b/src/api/js/package-lock.json index a93b8c8a8..acfa8eb8b 100644 --- a/src/api/js/package-lock.json +++ b/src/api/js/package-lock.json @@ -74,6 +74,7 @@ "resolved": "https://registry.npmjs.org/@babel/core/-/core-7.19.3.tgz", "integrity": "sha512-WneDJxdsjEvyKtXKsaBGbDeiyOjR5vYq4HcShxnIbG0qixpoHjI3MqeZM9NDvsojNCEBItQE4juOo/bU6e72gQ==", "dev": true, + "peer": true, "dependencies": { "@ampproject/remapping": "^2.1.0", "@babel/code-frame": "^7.18.6", @@ -1552,7 +1553,8 @@ "version": "17.0.45", "resolved": "https://registry.npmjs.org/@types/node/-/node-17.0.45.tgz", "integrity": "sha512-w+tIMs3rq2afQdsPJlODhoUEKzFP1ayaoyl1CcnwtIlsVe7K7bA1NGm4s3PraqTLlXnbIN84zuBlxBWo1u9BLw==", - "dev": true + "dev": true, + "peer": true }, "node_modules/@types/prettier": { "version": "2.7.1", @@ -1926,6 +1928,7 @@ "url": "https://tidelift.com/funding/github/npm/browserslist" } ], + "peer": true, "dependencies": { "caniuse-lite": "^1.0.30001400", "electron-to-chromium": "^1.4.251", @@ -3312,6 +3315,7 @@ "resolved": "https://registry.npmjs.org/jest/-/jest-28.1.3.tgz", "integrity": "sha512-N4GT5on8UkZgH0O5LUavMRV1EDEhNTL0KEfRmDIeZHSV7p2XgLoY9t9VDUgL6o+yfdgYHVxuz81G8oB9VG5uyA==", "dev": true, + "peer": true, "dependencies": { "@jest/core": "^28.1.3", "@jest/types": "^28.1.3", @@ -6540,6 +6544,7 @@ "resolved": "https://registry.npmjs.org/ts-node/-/ts-node-10.9.1.tgz", "integrity": "sha512-NtVysVPkxxrwFGUUxGYhfux8k78pQB3JqYBXlLRZgdGUqTO5wU/UyHop5p70iEbGhB7q5KmiZiU0Y3KlJrScEw==", "dev": true, + "peer": true, "dependencies": { "@cspotcode/source-map-support": "^0.8.0", "@tsconfig/node10": "^1.0.7", @@ -6659,6 +6664,7 @@ "integrity": "sha512-i5t66RHxDvVN40HfDd1PsEThGNnlMCMT3jMUuoh9/0TaqWevNontacunWyN02LA9/fIbEWlcHZcgTKb9QoaLfg==", "dev": true, "license": "Apache-2.0", + "peer": true, "bin": { "tsc": "bin/tsc", "tsserver": "bin/tsserver" 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 c908a480f..0eb897ba3 100644 --- a/src/api/js/src/high-level/high-level.test.ts +++ b/src/api/js/src/high-level/high-level.test.ts @@ -824,6 +824,41 @@ describe('high-level', () => { expect(core.length()).toBeGreaterThan(0); expect(core.length()).toBeLessThanOrEqual(3); }); + + it('can use addAndTrack to extract unsat core', async () => { + const { Solver, Int, Bool } = api.Context('main'); + const solver = new Solver(); + const x = Int.const('x'); + const p1 = Bool.const('p1'); + const p2 = Bool.const('p2'); + + // Track conflicting constraints using addAndTrack + solver.addAndTrack(x.gt(0), p1); + solver.addAndTrack(x.lt(0), p2); + + const result = await solver.check(); + expect(result).toStrictEqual('unsat'); + + // The unsat core should contain the tracking literals + const core = solver.unsatCore(); + expect(core.length()).toBeGreaterThan(0); + }); + + it('can use addAndTrack with string constant name', async () => { + const { Solver, Int } = api.Context('main'); + const solver = new Solver(); + const x = Int.const('x'); + + // addAndTrack accepts a string as the tracking constant name + solver.addAndTrack(x.gt(0), 'p1'); + solver.addAndTrack(x.lt(0), 'p2'); + + const result = await solver.check(); + expect(result).toStrictEqual('unsat'); + + const core = solver.unsatCore(); + expect(core.length()).toBeGreaterThan(0); + }); }); describe('AstVector', () => { @@ -943,6 +978,22 @@ describe('high-level', () => { expect(model.eval(y).eqIdentity(Int.val(0))).toBeTruthy(); expect(model.eval(z).eqIdentity(Int.val(5))).toBeTruthy(); }); + + it('can use addAndTrack with Optimize', async () => { + const { Int, Bool, Optimize } = api.Context('main'); + + const opt = new Optimize(); + const x = Int.const('x'); + const p1 = Bool.const('p1'); + const p2 = Bool.const('p2'); + + // Track conflicting constraints using addAndTrack + opt.addAndTrack(x.gt(0), p1); + opt.addAndTrack(x.lt(0), p2); + + const result = await opt.check(); + expect(result).toStrictEqual('unsat'); + }); }); describe('datatypes', () => { diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index 2db0da591..40ce49863 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -987,6 +987,29 @@ export interface Solver { add(...exprs: (Bool | AstVector>)[]): void; + /** + * Assert a constraint and associate it with a tracking literal (Boolean constant). + * This is the TypeScript equivalent of `assertAndTrack` in other Z3 language bindings. + * + * When the solver returns `unsat`, the tracked literals that contributed to + * unsatisfiability can be retrieved via {@link unsatCore}. + * + * @param expr - The Boolean expression to assert + * @param constant - A Boolean constant (or its name as a string) used as the tracking literal + * + * @example + * ```typescript + * const solver = new Solver(); + * const x = Int.const('x'); + * const p1 = Bool.const('p1'); + * const p2 = Bool.const('p2'); + * solver.addAndTrack(x.gt(0), p1); + * solver.addAndTrack(x.lt(0), p2); + * if (await solver.check() === 'unsat') { + * const core = solver.unsatCore(); // contains p1 and p2 + * } + * ``` + */ addAndTrack(expr: Bool, constant: Bool | string): void; /** @@ -1288,6 +1311,27 @@ export interface Optimize { addSoft(expr: Bool, weight: number | bigint | string | CoercibleRational, id?: number | string): void; + /** + * Assert a constraint and associate it with a tracking literal (Boolean constant). + * This is the TypeScript equivalent of `assertAndTrack` in other Z3 language bindings. + * + * When the optimizer returns `unsat`, the tracked literals that contributed to + * unsatisfiability can be used to identify which constraints caused the conflict. + * + * @param expr - The Boolean expression to assert + * @param constant - A Boolean constant (or its name as a string) used as the tracking literal + * + * @example + * ```typescript + * const opt = new Optimize(); + * const x = Int.const('x'); + * const p1 = Bool.const('p1'); + * const p2 = Bool.const('p2'); + * opt.addAndTrack(x.gt(0), p1); + * opt.addAndTrack(x.lt(0), p2); + * const result = await opt.check(); // 'unsat' + * ``` + */ addAndTrack(expr: Bool, constant: Bool | string): void; assertions(): AstVector>;