{"_id":"@cooljapan/oxiz","_rev":"6-05c3c7a614707ed230b0e8e606f31303","name":"@cooljapan/oxiz","dist-tags":{"latest":"0.3.3"},"versions":{"0.2.3":{"name":"@cooljapan/oxiz","version":"0.2.3","keywords":["smt","wasm","webassembly"],"license":"Apache-2.0","_id":"@cooljapan/oxiz@0.2.3","maintainers":[{"name":"kitasan","email":"info@kitasan.io"}],"homepage":"https://github.com/cool-japan/oxiz#readme","bugs":{"url":"https://github.com/cool-japan/oxiz/issues"},"dist":{"shasum":"f23feb82b2896a5175a41312c2db4e410198ecd8","tarball":"https://registry.npmjs.org/@cooljapan/oxiz/-/oxiz-0.2.3.tgz","fileCount":6,"integrity":"sha512-0g8YZ2pnK6cFuqaUKca6l8qnTnu1SVS1jIOK5Hsr3clkJWVJZdG6Khx3SpcMDj9GYiY9azBz+ZU3T+1lnqmOmQ==","signatures":[{"sig":"MEUCIQCVuREcxDF8mntHAo2nKysFJy0MTkwtoDj6BOQb21J8fwIgN1iqzSRBihZjobhWGBk7xnxlERE8+/n0jKyX6+S3TDU=","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":1101249},"main":"oxiz_wasm.js","type":"module","types":"oxiz_wasm.d.ts","_npmUser":{"name":"kitasan","email":"info@kitasan.io"},"repository":{"url":"git+https://github.com/cool-japan/oxiz.git","type":"git"},"_npmVersion":"10.9.8","description":"WebAssembly bindings for OxiZ SMT Solver","directories":{},"sideEffects":["./oxiz_wasm.js","./snippets/*"],"_nodeVersion":"22.22.3","collaborators":["COOLJAPAN OU (Team KitaSan)"],"_hasShrinkwrap":false,"_npmOperationalInternal":{"tmp":"tmp/oxiz_0.2.3_1780979117285_0.2893905209362293","host":"s3://npm-registry-packages-npm-production"}},"0.2.4":{"name":"@cooljapan/oxiz","version":"0.2.4","keywords":["smt","wasm","webassembly"],"license":"Apache-2.0","_id":"@cooljapan/oxiz@0.2.4","maintainers":[{"name":"kitasan","email":"info@kitasan.io"}],"homepage":"https://github.com/cool-japan/oxiz#readme","bugs":{"url":"https://github.com/cool-japan/oxiz/issues"},"dist":{"shasum":"d95b97f0b476dc52dc0a46c590dea695a6d6c2f4","tarball":"https://registry.npmjs.org/@cooljapan/oxiz/-/oxiz-0.2.4.tgz","fileCount":6,"integrity":"sha512-nS/rdrxV99UqnJo0V92FEVAcaYaL0eYQ3mIudDxnUkM1sEzjR6c6bPYfETOzzLUpgZ8aH1S8sLtivk770p+/sQ==","signatures":[{"sig":"MEQCIHEZrtHYX8/wQO6At16/rhbCyr5ZvoN0oXu3LDJTm5K1AiAeIfebbALveXKb+YUEtRo7qYNo7UsBtB0U5An7b3MJGg==","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":1258704},"main":"oxiz_wasm.js","type":"module","types":"oxiz_wasm.d.ts","_npmUser":{"name":"kitasan","email":"info@kitasan.io"},"repository":{"url":"git+https://github.com/cool-japan/oxiz.git","type":"git"},"_npmVersion":"10.9.8","description":"WebAssembly bindings for OxiZ SMT Solver","directories":{},"sideEffects":["./oxiz_wasm.js","./snippets/*"],"_nodeVersion":"22.23.1","collaborators":["COOLJAPAN OU (Team KitaSan)"],"_hasShrinkwrap":false,"_npmOperationalInternal":{"tmp":"tmp/oxiz_0.2.4_1784440090641_0.5156322998815253","host":"s3://npm-registry-packages-npm-production"}},"0.3.0":{"name":"@cooljapan/oxiz","version":"0.3.0","keywords":["smt","wasm","webassembly"],"license":"Apache-2.0","_id":"@cooljapan/oxiz@0.3.0","maintainers":[{"name":"kitasan","email":"info@kitasan.io"}],"homepage":"https://github.com/cool-japan/oxiz#readme","bugs":{"url":"https://github.com/cool-japan/oxiz/issues"},"dist":{"shasum":"7ac63871f3ee6ff6e2af4626484fd86abfc752d4","tarball":"https://registry.npmjs.org/@cooljapan/oxiz/-/oxiz-0.3.0.tgz","fileCount":6,"integrity":"sha512-dDD2z2Kanbs09ypqV/es1NLVtc0kfCdyJlYmmDJ0h/WHwoNsCe8mMnI0H8CghiKYrf1O9lxYr353Ya48+qdXtg==","signatures":[{"sig":"MEUCIDzWcpAw6t0LOZ1E3Wclcj3Y7oEdtfcZEhWfcGJlEiwcAiEA84LJAJt9q+c/lwmdV4A0rRnJST953IDmtMTZukXEtUI=","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":1441236},"main":"oxiz_wasm.js","type":"module","types":"oxiz_wasm.d.ts","_npmUser":{"name":"kitasan","email":"info@kitasan.io"},"repository":{"url":"git+https://github.com/cool-japan/oxiz.git","type":"git"},"_npmVersion":"10.9.8","description":"WebAssembly bindings for OxiZ SMT Solver","directories":{},"sideEffects":["./oxiz_wasm.js","./snippets/*"],"_nodeVersion":"22.23.1","collaborators":["COOLJAPAN OU (Team KitaSan)"],"_hasShrinkwrap":false,"_npmOperationalInternal":{"tmp":"tmp/oxiz_0.3.0_1784721015479_0.27209368632651487","host":"s3://npm-registry-packages-npm-production"}},"0.3.1":{"name":"@cooljapan/oxiz","version":"0.3.1","keywords":["smt","wasm","webassembly"],"license":"Apache-2.0","_id":"@cooljapan/oxiz@0.3.1","maintainers":[{"name":"kitasan","email":"info@kitasan.io"}],"homepage":"https://github.com/cool-japan/oxiz#readme","bugs":{"url":"https://github.com/cool-japan/oxiz/issues"},"dist":{"shasum":"e10ef6c1fc0b46a936bf4d45721b6046e9604433","tarball":"https://registry.npmjs.org/@cooljapan/oxiz/-/oxiz-0.3.1.tgz","fileCount":6,"integrity":"sha512-noAZz5H+GRB0ksiTr/Xy/34IUbM9MBjt5UcNO0pTDUmnmtK+2yjthVOqZKrJFjXZBTtv9MxnUA5hwLarxErL0Q==","signatures":[{"sig":"MEUCIQCmrLoX6pmcq3dwvFIJlxA6rRtsFwbqliqGzYTFUcU2bwIgEdYm17QFSw9B7QEdGQBG9+x+qVQGNTv/1JSeL373vGo=","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":1714217},"main":"oxiz_wasm.js","type":"module","types":"oxiz_wasm.d.ts","_npmUser":{"name":"kitasan","email":"info@kitasan.io"},"repository":{"url":"git+https://github.com/cool-japan/oxiz.git","type":"git"},"_npmVersion":"10.9.8","description":"WebAssembly bindings for OxiZ SMT Solver","directories":{},"sideEffects":["./oxiz_wasm.js","./snippets/*"],"_nodeVersion":"22.23.1","collaborators":["COOLJAPAN OU (Team KitaSan)"],"_hasShrinkwrap":false,"_npmOperationalInternal":{"tmp":"tmp/oxiz_0.3.1_1785482943058_0.4255566981649128","host":"s3://npm-registry-packages-npm-production"}},"0.3.2":{"name":"@cooljapan/oxiz","version":"0.3.2","keywords":["smt","wasm","webassembly"],"license":"Apache-2.0","_id":"@cooljapan/oxiz@0.3.2","maintainers":[{"name":"kitasan","email":"info@kitasan.io"}],"homepage":"https://github.com/cool-japan/oxiz#readme","bugs":{"url":"https://github.com/cool-japan/oxiz/issues"},"dist":{"shasum":"38fc34705a3549e6fbd016e8b6607b1d81eedd70","tarball":"https://registry.npmjs.org/@cooljapan/oxiz/-/oxiz-0.3.2.tgz","fileCount":6,"integrity":"sha512-oBbVtXMGhFof9GJdpp7nr/4uZp5VquVR9a5ZHeWFOaAGYiKKrVWM1fntVzSfDyKbao/Z/q6eIjx+nGUcG8dB9A==","signatures":[{"sig":"MEQCIEXGKmZQnudQrFukoYZvPn3Zh7nr13z0KBHbCXlP7AppAiALbtFS9FCnQT1l+RNWIoVk/wpgd8QfPrwW6TTv8jLafg==","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":1639734},"main":"oxiz_wasm.js","type":"module","types":"oxiz_wasm.d.ts","_npmUser":{"name":"kitasan","email":"info@kitasan.io"},"repository":{"url":"git+https://github.com/cool-japan/oxiz.git","type":"git"},"_npmVersion":"10.9.8","description":"WebAssembly bindings for OxiZ SMT Solver","directories":{},"sideEffects":["./oxiz_wasm.js","./snippets/*"],"_nodeVersion":"22.23.1","collaborators":["COOLJAPAN OU (Team KitaSan)"],"_hasShrinkwrap":false,"_npmOperationalInternal":{"tmp":"tmp/oxiz_0.3.2_1785908216855_0.11297528556375225","host":"s3://npm-registry-packages-npm-production"}},"0.3.3":{"name":"@cooljapan/oxiz","type":"module","collaborators":["COOLJAPAN OU (Team KitaSan)"],"description":"WebAssembly bindings for OxiZ SMT Solver","version":"0.3.3","license":"Apache-2.0","repository":{"type":"git","url":"git+https://github.com/cool-japan/oxiz.git"},"main":"oxiz_wasm.js","types":"oxiz_wasm.d.ts","sideEffects":["./oxiz_wasm.js","./snippets/*"],"keywords":["smt","wasm","webassembly"],"_id":"@cooljapan/oxiz@0.3.3","bugs":{"url":"https://github.com/cool-japan/oxiz/issues"},"homepage":"https://github.com/cool-japan/oxiz#readme","_nodeVersion":"22.23.2","_npmVersion":"10.9.8","dist":{"integrity":"sha512-0kVI6HYJezORXpjsoaAJ8ROLxSxVrh46R7PiYv8J2JLTLRoeinbGZHcd40kthrXXVYuahH2w52Xf0d88kdvHhw==","shasum":"47738178becdb39d1a18b3dd6240f0b46979cc49","tarball":"https://registry.npmjs.org/@cooljapan/oxiz/-/oxiz-0.3.3.tgz","fileCount":6,"unpackedSize":2171120,"signatures":[{"keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U","sig":"MEUCIQCCiF5Q/fQG6PwBmd4V0aD5mZSi+pjJUg3s9gccb2nEPgIgA7l26OezQMmgME+TetTO0hiBlJDbIOLsX6hFKubqLbM="}]},"_npmUser":{"name":"kitasan","email":"info@kitasan.io"},"directories":{},"maintainers":[{"name":"kitasan","email":"info@kitasan.io"}],"_npmOperationalInternal":{"host":"s3://npm-registry-packages-npm-production","tmp":"tmp/oxiz_0.3.3_1787709965683_0.2991539993975523"},"_hasShrinkwrap":false}},"time":{"created":"2026-06-09T04:25:17.003Z","modified":"2026-08-26T02:06:06.065Z","0.2.3":"2026-06-09T04:25:17.453Z","0.2.4":"2026-07-19T05:48:10.843Z","0.3.0":"2026-07-22T11:50:15.644Z","0.3.1":"2026-07-31T07:29:03.233Z","0.3.2":"2026-08-05T05:36:57.042Z","0.3.3":"2026-08-26T02:06:05.884Z"},"bugs":{"url":"https://github.com/cool-japan/oxiz/issues"},"license":"Apache-2.0","homepage":"https://github.com/cool-japan/oxiz#readme","keywords":["smt","wasm","webassembly"],"repository":{"type":"git","url":"git+https://github.com/cool-japan/oxiz.git"},"description":"WebAssembly bindings for OxiZ SMT Solver","maintainers":[{"name":"kitasan","email":"info@kitasan.io"}],"readme":"# OxiZ WASM - WebAssembly Bindings for OxiZ SMT Solver\n\nWebAssembly bindings for the OxiZ SMT solver, enabling high-performance SMT solving directly in web browsers and Node.js.\n\n## Status (v0.3.2)\n\n| Metric | Value |\n|:-------|:------|\n| Version | 0.3.2 |\n| Status | Stable |\n| Tests | 155 passing (`cargo nextest run -p oxiz-wasm --all-features`) |\n| Source files | 30 |\n| Public API items | 471 |\n\n## Overview\n\nThis crate provides comprehensive JavaScript/TypeScript bindings for running OxiZ in web browsers and Node.js environments. It features a complete API with async support, Web Worker compatibility, and structured error handling.\n\n### Key Features\n\n- **Pure Rust**: 100% safe Rust code compiled to WebAssembly (no unsafe, no FFI)\n- **Complete API**: Full SMT-LIB2 operations support (declarations, assertions, models, unsat cores)\n- **Async Support**: Non-blocking operations with `async`/`await`\n- **Web Worker Ready**: Run solver in background threads\n- **Type-Safe Errors**: Structured error objects with detailed messages\n- **Well Documented**: Comprehensive JSDoc comments for all APIs\n- **Examples Included**: Interactive HTML demos and Web Worker examples\n- **TypeScript Support**: Full type definitions and TypeScript examples\n- **Performance Benchmarks**: Comprehensive benchmarking suite included\n- **Build Automation**: Smart build script with optimization support\n\n## Building\n\n### Quick Start\n\n```bash\n# Using the build script (recommended)\n./build.sh dev          # Fast development build\n./build.sh release      # Optimized release build\n./build.sh optimized    # Maximum optimization (requires wasm-opt)\n./build.sh all          # Build for all targets\n```\n\n### Manual Building\n\n```bash\n# Install wasm-pack\ncargo install wasm-pack\n\n# Build for web\nwasm-pack build --target web\n\n# Build for Node.js\nwasm-pack build --target nodejs\n\n# Build for bundlers (webpack, etc.)\nwasm-pack build --target bundler\n```\n\n### Build Script Options\n\nThe `build.sh` script supports multiple build types:\n\n- **dev** - Fast development build with debug info\n- **release** - Standard optimized release build\n- **profiling** - Release build with debug symbols\n- **optimized** - Maximum size optimization using wasm-opt\n- **all** - Build for all targets (web, nodejs, bundler)\n- **clean** - Remove all build artifacts\n\n**Note**: The `optimized` build requires [Binaryen](https://github.com/WebAssembly/binaryen) for wasm-opt:\n```bash\n# macOS\nbrew install binaryen\n\n# Ubuntu/Debian\nsudo apt-get install binaryen\n```\n\n## Usage\n\n### JavaScript (ES Modules)\n\n```javascript\nimport init, { WasmSolver, version } from './pkg/oxiz_wasm.js';\n\nasync function main() {\n    await init();\n\n    console.log(`OxiZ version: ${version()}`);\n\n    const solver = new WasmSolver();\n    solver.setLogic(\"QF_LIA\");\n\n    const result = solver.execute(`\n        (declare-const x Int)\n        (declare-const y Int)\n        (assert (> x 0))\n        (assert (< y 10))\n        (assert (= (+ x y) 15))\n        (check-sat)\n    `);\n\n    console.log(result);  // \"sat\"\n}\n\nmain();\n```\n\n### TypeScript\n\n```typescript\nimport init, { WasmSolver, version, type Model, type SatResult } from './pkg/oxiz_wasm';\n\nasync function solve(): Promise<void> {\n    await init();\n\n    const solver = new WasmSolver();\n    solver.setLogic(\"QF_LIA\");\n\n    // TypeScript provides full type safety\n    solver.declareConst('x', 'Int');  // 'Int' is validated by TypeScript\n    solver.assertFormula('(> x 0)');\n\n    const result: SatResult = solver.checkSat();  // Type: \"sat\" | \"unsat\" | \"unknown\"\n\n    if (result === 'sat') {\n        const model: Model = solver.getModel();\n        console.log(model.x.value);  // Autocomplete works here!\n        console.log(model.x.sort);   // Type: string\n    }\n}\n```\n\nThe package includes comprehensive TypeScript declarations (`oxiz-wasm.d.ts`) providing:\n- Full type safety for all API methods\n- IntelliSense/autocomplete support\n- Type-checked sort names and logic names\n- Structured error types\n- Complete JSDoc documentation\n\n### Node.js (CommonJS)\n\n```javascript\nconst { WasmSolver, version } = require('./pkg/oxiz_wasm');\n\nconst solver = new WasmSolver();\nconsole.log(solver.checkSat());\n```\n\n## API Reference\n\n### `WasmSolver`\n\nMain solver class providing access to all SMT operations.\n\n```typescript\nclass WasmSolver {\n    // Constructor\n    constructor();\n\n    // Script execution\n    execute(script: string): string;\n    executeAsync(script: string): Promise<string>;\n\n    // Logic and options\n    setLogic(logic: string): void;\n    setOption(key: string, value: string): void;\n    getOption(key: string): string | undefined;\n\n    // Variable and function declarations\n    declareConst(name: string, sort: string): void;  // sorts: \"Bool\", \"Int\", \"Real\", \"BitVecN\"\n    declareFun(name: string, argSorts: string[], retSort: string): void;\n\n    // Assertions\n    assertFormula(formula: string): void;\n    getAssertions(): string;\n    resetAssertions(): void;\n\n    // Satisfiability checking\n    checkSat(): string;  // \"sat\" | \"unsat\" | \"unknown\"\n    checkSatAsync(): Promise<string>;\n\n    // Model extraction (after sat result)\n    getModel(): object;  // { varName: { sort: string, value: string } }\n    getModelString(): string;\n    getValue(terms: string[]): string;\n\n    // Unsat core (after unsat result)\n    getUnsatCore(): string;\n\n    // Context management\n    push(): void;\n    pop(): void;\n    reset(): void;\n\n    // Utilities\n    simplify(expr: string): string;\n    cancel(): void;\n    isCancelled(): boolean;\n}\n```\n\n### Global Functions\n\n```typescript\n// Get OxiZ WASM version\nfunction version(): string;\n\n// Initialize WASM module (auto-called on import)\nfunction init(): Promise<void>;\n```\n\n### Error Objects\n\nAll operations that can fail throw structured error objects:\n\n```typescript\ninterface WasmError {\n    kind: \"ParseError\" | \"InvalidSort\" | \"InvalidInput\" |\n          \"NoModel\" | \"NoUnsatCore\" | \"InvalidState\" |\n          \"NotSupported\" | \"Unknown\";\n    message: string;\n}\n```\n\n## Examples\n\nThe [examples](./examples) directory contains complete working examples:\n\n### Browser Examples\n\n- **basic.html**: Interactive browser examples demonstrating:\n  - Boolean satisfiability\n  - Integer linear arithmetic\n  - Unsatisfiable formulas and unsat cores\n  - Async operations\n  - Custom SMT-LIB2 scripts\n\n- **worker.html**: Web Worker demonstration showing:\n  - Running solver in background thread\n  - UI responsiveness during solving\n  - Progress reporting and cancellation\n\n- **benchmark.html**: Performance benchmarking suite with:\n  - Initialization benchmarks\n  - Declaration and assertion benchmarks\n  - SAT solving benchmarks\n  - Model extraction benchmarks\n  - Scalability tests\n\n- **solver-worker.js**: Reusable Web Worker implementation\n\n### TypeScript Examples\n\n- **typescript/basic.ts**: Comprehensive TypeScript examples with:\n  - Full type safety and autocomplete\n  - Error handling with typed errors\n  - Async operations\n  - Incremental solving\n  - Bitvector operations\n\nSee [examples/README.md](./examples/README.md) and [examples/typescript/README.md](./examples/typescript/README.md) for detailed usage patterns and setup instructions.\n\n## Browser Compatibility\n\nRequires modern browser with WebAssembly support:\n- Chrome/Edge 85+\n- Firefox 78+\n- Safari 14+\n- Node.js 14+\n\n## Performance Tips\n\n- Use **release builds** with optimizations for production\n- Use **async methods** (`checkSatAsync()`, `executeAsync()`) for long-running operations\n- Run solver in **Web Worker** for truly non-blocking computation\n- **Reuse solver instances** when solving multiple related problems\n- Use **push/pop** for incremental solving instead of creating new solvers\n\n## Limitations\n\nCurrent limitations (see [TODO.md](./TODO.md) for planned features):\n- Non-nullary functions not yet supported (requires AST changes)\n- Quantifier support is limited\n- Some advanced SMT-LIB2 features not implemented\n\n## Bundle Size\n\nThe WASM binary is approximately 200KB gzipped (may vary based on build options).\n\n## Development\n\n### Running Tests\n\n```bash\n# WASM tests (requires wasm-pack)\nwasm-pack test --headless --firefox\nwasm-pack test --headless --chrome\n```\n\n### Code Structure\n\n- `src/lib.rs` - Main WASM bindings implementation\n- `examples/` - Browser and Web Worker examples\n- `TODO.md` - Planned features and improvements\n- `SCIRS2_POLICY.md` - Dependency policy documentation\n\n## Contributing\n\nContributions welcome! Please ensure:\n- All code is safe Rust (no `unsafe`)\n- Add tests for new features\n- Update documentation\n- Follow existing code style\n- Adhere to the \"no warnings\" policy\n\n## Related Crates\n\n- [oxiz-core](../oxiz-core) - Core SMT solver implementation\n- [oxiz-solver](../oxiz-solver) - High-level solver interface\n- [oxiz-cli](../oxiz-cli) - Command-line interface\n\n## License\n\nLicensed under Apache License 2.0 ([LICENSE](../LICENSE)).\n","readmeFilename":"README.md"}