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

@@ -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"

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', () => {

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

@@ -987,6 +987,29 @@ export interface Solver<Name extends string = 'main'> {
 
   add(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): 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<Name>, constant: Bool<Name> | string): void;
 
   /**
@@ -1288,6 +1311,27 @@ export interface Optimize<Name extends string = 'main'> {
 
   addSoft(expr: Bool<Name>, 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<Name>, constant: Bool<Name> | string): void;
 
   assertions(): AstVector<Name, Bool<Name>>;