More programming content for TS/JS

[rlisahuang]

I expect the build to fail for some examples because the way I constructed them does not work with Kevin's solution for TS inputs. Main problems:

• We cannot write top-level functions such as solve() and prove() in the unit test without bypassing type checking the function parameters
• setParam doesn't quite work
• We also would have to bypass type checking variable declarations if the types are within the Z3 namespace.

@NikolajBjorner I should leave it to your judgement in terms of how to utilize/modify these examples so that everything works, or modify the eval-z3.js code as needed.

[bakkot]

We cannot write top-level functions such as solve() and prove() in the unit test without bypassing type checking the function parameters

What goes wrong? I can probably suggest a solution.

setParam doesn't quite work

That's because it exists on the global namespace, not on a specific context, which is where you're trying to invoke it. That is, you'll need to pull it off of the result of the init call, not off the Context('main') call. You can tweak these lines as follows if you want to use it:

  let wrapped = `
(function (Z3, setParam) { // note additional param
  'use strict';
  let module = {};
  ${result.result}
  return module.exports;
})
  `;
  return await (0, eval)(wrapped)(Z3.Context('main'), Z3.setParam); // note additional argument

and then invoke setParam directly (not as Z3.setParam).

We also would have to bypass type checking variable declarations if the types are within the Z3 namespace.

You can add more type imports to the scope used for type checking by adding them to this line. TypeScript is pretty good about type inference, though, so you should only rarely need to explicitly refer to a type (other than in function parameters, which it doesn't infer); you still get the benefits of type checking. Though you might want to explicitly refer to types just for documentation purposes.

---

Feel free to ping me about issues like this; I'm not necessarily going to be able to help but I'm happy to take a look.

[NikolajBjorner]

console.log doesn't seem to work

[NikolajBjorner]

cast?

[rlisahuang]

Thanks for joining the conversation.

We cannot write top-level functions such as solve() and prove() in the unit test without bypassing type checking the function parameters

What goes wrong? I can probably suggest a solution.

The issue here is that type annotations are enforced unless you do @ts-ignore, and those types are not imported to the scope. I believe the issue can be addressed by your suggestion of type imports, though.

That is, you'll need to pull it off of the result of the init call, not off the Context('main') call. You can tweak these lines as follows if you want to use it:

  let wrapped = `
(function (Z3, setParam) { // note additional param
  'use strict';
  let module = {};
  ${result.result}
  return module.exports;
})
  `;
  return await (0, eval)(wrapped)(Z3.Context('main'), Z3.setParam); // note additional argument

and then invoke setParam directly (not as Z3.setParam).

The build would fail at compileZ3JS, so we don't even reach the evaluation. The complaint is that setParam does not exist on type Context<'main'>. I'm looking into the issue now, see if we can get around it without explicitly specifying the type of Z3.

[rlisahuang]

@bakkot I'm not sure I'm on the right track, so definitely would appreciate your help here. The example failed to be compiled is

// non-linear arithmetic

Z3.setParam('pp.decimal', true);
Z3.setParam('pp.decimal_precision', 20);

const x = Z3.Real.const('x');
const y = Z3.Real.const('y');
const z = Z3.Real.const('z');

const solver = new Z3.Solver();
solver.add(x.mul(x).add(y.mul(y)).eq(1)); // x^2 + y^2 == 1
solver.add(x.mul(x).mul(x).add(z.mul(z).mul(z)).lt('1/2')); // x^3 + z^3 < 1/2

await solver.check(); // sat

[bakkot]

Yeah, adding declare let { Context, setParam } = Z3 should make the typechecker happy, and then including the change I suggested above should make the actual runtime behavior work. (Except it will be called as setParam, not Z3.setParam.)

[bakkot]

Oh, sorry, that's not legal syntax. Needs to be what it currently is, just with setParam also: declare let { Context, setParam }: Awaited<ReturnType<typeof init>>;

[rlisahuang]

I messed up with the types in this commit. After further understanding the high-level API the issue is now fixed. The imports should be

  declare let { Context, setParam }: Awaited<ReturnType<typeof init>>;
  declare let Z3: ReturnType<typeof Context<'main'>>;

simply add setParam to the destructure of init()

[bakkot]

Also, if you want to make the Z3.Model style of type names work, instead of explicitly importing all the types you need and referring to them with bare names like Model, I believe you can do that by adding

// @ts-ignore
import type * as Z3 from 'z3-solver';

to the imports. (The ts-ignore is an unfortunate necessity due to microsoft/TypeScript#48764 (comment), but it doesn't actually disable the type checking in this instance.)

You'll need to also increment the index (currently 4) in this line so the rewriting still works.

[rlisahuang]

Also, if you want to make the Z3.Model style of type names work, instead of explicitly importing all the types you need and referring to them with bare names like Model, I believe you can do that by adding

// @ts-ignore
import type * as Z3 from 'z3-solver';

I'll let @NikolajBjorner decide which style of type names is desired in the examples.

[rlisahuang]

All problems in the extra examples fixed, ready to merge.

[github-actions]

🎉 This PR is included in version 1.0.0 🎉

The release is available on GitHub release

Your semantic-release bot 📦🚀

[github-actions]

🎉 This PR is included in version 1.0.0 🎉

The release is available on GitHub release

Your semantic-release bot 📦🚀