{"id":26680,"library":"z3js","title":"z3js","description":"z3js is a tiny utility library (v0.0.0) for transpiling a small subset of JavaScript expressions to SMT2 format for use with the Z3 solver. It includes a JavaScript parser, a SMT2 code generator, and a minimal S-expression parser for reading Z3 outputs. The library is experimental and limited to simple variable declarations, function definitions, and assertions. It requires an external Z3 solver binary and is intended for prototyping program synthesis and formal verification tools. No releases or update cadence is established; the project appears to be in early development. Key differentiators: focuses on a tight JS→SMT2 bridge, unlike full verification frameworks.","status":"active","version":"0.0.0","language":"javascript","source_language":"en","source_url":"https://github.com/mjyc/z3js","tags":["javascript"],"install":[{"cmd":"npm install z3js","lang":"bash","label":"npm"},{"cmd":"yarn add z3js","lang":"bash","label":"yarn"},{"cmd":"pnpm add z3js","lang":"bash","label":"pnpm"}],"dependencies":[{"reason":"External solver binary required for SMT solving (not an npm package). Typically installed via brew/apt.","package":"z3","optional":true}],"imports":[{"note":"No ESM module published; only CommonJS supported.","wrong":"const jsParser = require('z3js').jsParser","symbol":"jsParser","correct":"import { jsParser } from 'z3js'"},{"note":"Default export not available; always use named import.","wrong":null,"symbol":"toSMT2","correct":"const { toSMT2 } = require('z3js')"},{"note":"No default export; only named exports.","wrong":"import declareDatatypes from 'z3js'","symbol":"declareDatatypes","correct":"const { declareDatatypes } = require('z3js')"}],"quickstart":{"code":"const { jsParser, toSMT2, declareDatatypes } = require('z3js');\n\nconst JS_CODE = `\nvar x;\nfunction f(args) {\n  return args.one * args.two;\n}\nassert(f(x) === 2);\ncheck_sat();\nget_model();\n`;\n\nconst typeDefs = {\n  x: '(Arg)',\n  y: '(Arg)',\n  f: {\n    args: '(Arg)',\n    return: 'Int'\n  }\n};\n\nconsole.log(declareDatatypes('Arg', { one: 'Int', two: 'Int' }));\nconsole.log(toSMT2(jsParser.parse(JS_CODE), typeDefs));","lang":"javascript","description":"Transpile a small JS program with function and assertion to SMT2 and pipe to Z3 solver."},"warnings":[{"fix":"Pin to exact version and expect future breaking changes.","message":"The library is version 0.0.0 and API is unstable. No semVer guarantees.","severity":"breaking","affected_versions":"0.0.0"},{"fix":"Install Z3 via 'brew install z3' or 'apt install z3' and ensure it's in PATH.","message":"Requires external Z3 binary. Does not bundle or install Z3 automatically.","severity":"gotcha","affected_versions":"*"},{"fix":"Refer to project examples for the supported syntax.","message":"Only a tiny subset of JavaScript is supported. For loops, arrays, objects, and closures are not supported.","severity":"gotcha","affected_versions":"*"},{"fix":"Use JSDoc or manually declare types if using TypeScript.","message":"No TypeScript type definitions are provided. All types are lost when using this library.","severity":"gotcha","affected_versions":"*"}],"env_vars":null,"last_verified":"2026-05-01T00:00:00.000Z","next_check":"2026-07-30T00:00:00.000Z","problems":[{"fix":"Run `npm install z3js` or use a local path like 'require('./path/to/z3js/src')'.","cause":"Package not installed or not installed correctly.","error":"Error: Cannot find module 'z3js'"},{"fix":"Rewrite using only 'var', function declarations, and simple expressions.","cause":"JavaScript code contains unsupported syntax (e.g., arrow functions, let/const, templates).","error":"parse error: unexpected token"},{"fix":"Install Z3 via 'brew install z3' (macOS) or 'sudo apt install z3' (Ubuntu) or download from GitHub.","cause":"Z3 solver binary is not installed or not in PATH.","error":"z3: command not found"}],"ecosystem":"npm","meta_description":null,"install_score":null,"install_tag":null,"quickstart_score":null,"quickstart_tag":null}