Running z3-solver npm package in browser

[profanat]

Sorry for stupid question, but i tried to import this package into my vue component but it doesn't work
import { init } from 'z3-solver'
export default {
async mounted() {
const { Context } = await init();
}
}
I get error that global is not defined.
If i add window.global = window line i get error:
initZ3 was not imported correctly. Please consult documentation on how to load Z3 in browser
I enabled special headers in vite but it didn't help, can someone help me?

[NikolajBjorner]

Maybe use
https://github.com/microsoft/z3guide/blob/main/website/src/eval-z3/eval-z3.ts
as an example

[profanat]

Added this code and it works now:
var tag = document.createElement("script"); tag.src = "/node_modules/z3-solver/build/z3-built.js"; document.getElementsByTagName("head")[0].appendChild(tag);

[oeb25]

I had the same issue and resorted to copying the files into the public directory.

But I think I figured out a more clean solution, but only works in Chrome!

We can use the Vite ?url in imports to get the paths of the files z3 needs to load at runtime.

import { init } from "z3-solver/build/low-level";
import initZ3 from "z3-solver/build/z3-built";

let z3 = init(async () => {
  const files = {
    "z3-built.js": await import("z3-solver/build/z3-built?url"),
    "z3-built.wasm": await import("z3-solver/build/z3-built.wasm?url"),
    "z3-built.worker.js": await import("z3-solver/build/z3-built.worker?url"),
  };
  return initZ3({
    locateFile: (f) => {
      if (!(f in files)) throw new Error(`unknown z3 file: ${f}`);
      return files[f as keyof typeof files].default;
    },
    mainScriptUrlOrBlob: files["z3-built.js"].default,
  });
});

This works for the low-level API, but I've yet to get it to work with the high-level. One thing still missing, is that browsers might prevent service workers from being loaded over an insecure channel or due to CORS in general, and thus you need to have coi-serviceworker setup as well for localhost.

---

As a side-note for how this could be improved, wasm-pack has a special target for bundlers, where they import their wasm with:

import * as wasm from './wasm_bg.wasm';

To get this to work, you need the vite-plugin-wasm, but overall I think that would be a more sustainable solution.

[MargeKh]

Hello @profanat, could you please provide the required settings for coi-serviceworker? Thanks in advance!