Function init

The main entry point to the Z3 API

import { init } from 'z3-solver';

const { Context } = await init();
const { Solver, Int } = new Context('main');

const x = Int.const('x');
const y = Int.const('y');

const solver = new Solver();
solver.add(x.add(2).le(y.sub(10))); // x + 2 <= y - 10

if (await solver.check() !== 'sat') {
  throw new Error("couldn't find a solution")
}
const model = solver.model();

console.log(`x=${model.get(x)}, y=${model.get(y)}`);
// x=0, y=12

// Deno users can provide an Emscripten locateFile hook to load the wasm
// through npm's asset resolution instead of filesystem reads.
// const api = await init({
//   locateFile: (file, _prefix): string =>
//     import.meta.resolve(`npm:z3-solver/build/${file}`), // _prefix is unused here
// });
Copy