high-level JavaScript API

[bakkot]

As a followup to #5762, I've started work on high-level JS bindings, which you can see on this branch. There's an example of how they're used here, and some important notes about the implementation here. It is very far from being complete, having basically only enough to make a sudoku or n-queens solver, but it has all of the foundational work - GC, correct TypeScript types, etc. I'm not entirely happy with the structure yet, but it's functional.

I didn't PR this because I got stuck on a design question, and then forgot about it. The design question is:

How should contexts work? There's a few possible designs I see.

1. As in the Python design, make every single API take a context parameter which defaults to a shared global context. So, e.g.,

let context = new Context();
let x = Int('x', context);

// or, use the global context
let y = Int('y');

2. Put the primary API behind a function which you invoke to create a context and bind the rest of the API to that context. So, e.g.,

let c = context();
let { Int, Solver } = c;
let x = new Int('x');
let y = new Int('y');
let solver = new Solver();
// all implicitly using `c`
// there is no global `Int`, you have to get it by calling `context`

let c2 = context();
let z = new c2.Int('z'); // different context than above

3. A hybrid approach: have a global context and global versions of all the API functions like Int which implicitly use the global context, but also have a context function which gives you new versions of all the API functions which are bound to the new context.

4. Only ever have one, global context.

There's some tradeoffs in the usability of option 1 vs 2. In option 1, if you only ever have one context, then you never have to think about it: you just import the global Int class and use it and everything works. On the other hand, if you do have multiple contexts, you now have to remember to pass it to everything.

I can't really evaluate these tradeoffs because I don't know how often you actually want to work with contexts explicitly, rather than just having everything use a shared global context.

Currently it's implemented as option 1, because I was just copying python. I think option 2 is theoretically cleaner, but maybe a little more annoying to use since you can't just import things you need. Option 3 might be a best-of-both-worlds approach.

With any of these approaches I might be able to make the type system help out some, by preventing you from mixing values from different contexts, but I would have to think about how to do that more.

[ritave]

By a coincidence, I've also started work on high level bindings for JS this week. I've posted a not-working draft PR here #6048.

Since you've been the main developer of js bindings, how should we proceed?

[bakkot]

If you're feeling motivated, go for it. I wasn't going to get back to mine for a while anyway. I'll offer some comments on your PR regarding things I did differently and why.

Feel free to borrow from my branch, which does work.

[NikolajBjorner]

I can't really evaluate these tradeoffs because I don't know how often you actually want to work with contexts explicitly, rather than just having everything use a shared global context.

It might be that option 2, 3 are better, but I can't say for sure outright.
What I can say is that multiple contexts are required when using multi-threading from the Python API.
Many users don't know this, so they use the same context from different threads and it crashes. They file github issues.
The implicit context argument can also easily be forgotten. In one call to "Int('x', myctx)", then the next call to "Bool('y')" forgets the context argument.

[ritave]

I'm thinking about also generating native node-gyp C wrapper, which would be multithreaded. Creating an API that would support such functionality as well as WASM one would be best.

[bakkot]

The library itself can be multithreaded, but that isn't the same as the JS portion of it being multithreaded. In node, as in browsers, the only way to run JS code in a separate thread is with a worker, and while it is possible to clone a JS object to a worker with postMessage, that's not the same as actually sharing the object. (And doing so here would mess up all the GC, so that would be a bad idea.)

That is, in JS, unlike in Python, if you have let context = new Context();, then context is only ever going to exist on a single thread at a time. So the specific problem of using the same context on multiple threads can't come up.

But maybe there's some other scenario I'm missing where it would matter. In any case, it seems like design 2 above would not add too much overhead and would be defensive against some case arising where multiple contexts are necessary. You have to do a function call to initialize the library anyway, so a second function call to initialize the high-level API isn't that bad.

If we are going to support multiple contexts, I think we should require them to be named, and to have both a type-level and a runtime check which prevents you from mixing values from different contexts. It shouldn't be too hard to enforce, I think. I'll update my branch in a bit.

[ritave]

I'm working forward with my branch as well. If you find a way to separate Contexts in the type system that would be great, in the meantime I'll add runtime checks

[bakkot]

If you find a way to separate Contexts in the type system that would be great

You can do let makeContext<ContextName extends string> = (name: ContextName) => ({ name }) or whatever, and then let x = makeContext('a'); and let y = makeContext('b'); end up as different types. I'll do it on my branch and push it up.

[bakkot]

Well, that took more work than I was expecting, but I've updated the branch.

You use it as

let { createContext, em } = await init();
let Z3 = createContext('main');

and then as normal. If you make a different context and give it a different name, then you will be prevented at a type level from mixing values across contexts.

(I added runtime checks too, since they're quite cheap.)

[ritave]

@bakkot I'm trying to understand some design decisions and trade-off that were made.

• Why an error handler can't be provided to Z3?
• Is there a technical reason Z3 is build to be single-threaded?

[bakkot]

Why an error handler can't be provided to Z3?

Basically because it's quite hard to add a function to a WASM program at runtime. It's possible but complicated (there's a couple different approaches possible, from what I can tell: either you actually do add the function at runtime, or you build in a single "wrapper" function which just dispatches to a JS function stored in some list, where that list can be updated dynamically) and I didn't have the energy for it.

Is there a technical reason Z3 is build to be single-threaded?

I guess not, now that you mention it. I think that decision was made before anyone trying this had realized threads were required even in the "single threaded" build. If you can make it work multi-threaded, seems like that would be an improvement.