z3js

A tiny utility library for building z3-powered JavaScript.

The main features are:

• A transpiler for converting a tiny subset of JavaScript programs to smt2 to use z3 solver.
• A tiny s-expression parser for reading z3 outputs in smt2 to JavaScript objects.

Examples

Create a file demo.js and add:

const { jsParser, toSMT2, declareDatatypes } = require("z3js"); // or "path/to/z3js/src"

const JS_CODE = `
var x;

function f(args) {
  return args.one * args.two;
}

assert(f(x) === 2);
check_sat();
get_model();
`;

const typeDefs = {
  x: "(Arg)",
  y: "(Arg)",
  f: {
    args: "(Arg)",
    return: "Int"
  }
};

console.log(`
${declareDatatypes("Arg", { one: "Int", two: "Int" })}
${toSMT2(jsParser.parse(JS_CODE), typeDefs)}
`);

and run node demo.js | z3 -in. You'll need z3, which you can install by running brew install z3 or sudo apt install z3 on Mac or Ubuntu, respectively.

Reading Z3 outputs

Try

node examples/synth.js | z3 -in | node examples/parseSynthZ3Output.js

and check out ./examples/parseSynthZ3Output.js.

Program Synthesis demo

Check out ./examples/synth.js! The demo code is loosely based on Adrian Sampson's program synthesis blog post.

Inspired by

• @stanford-oval's node-smtlib
• @levjj's esverify
• @cpitclaudel's z3.wasm
• @emina's rosette
• "Program Synthesis is Possible" by Adrian Sampson