3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00

Update README with info about Smalltalk bindings ()

This commit is contained in:
Jan Vraný 2022-03-09 20:31:12 +00:00 committed by GitHub
parent 43f7636826
commit 8e18a94558
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -199,6 +199,11 @@ The Julia package [Z3.jl](https://github.com/ahumenberger/Z3.jl) wraps the C++ A
A WebAssembly build with associated TypeScript typings is published on npm as [z3-solver](https://www.npmjs.com/package/z3-solver). Information about building these bindings can be found in [src/api/js](src/api/js).
### Smalltalk (``Pharo`` / ``Smalltalk/X``)
Project [MachineArithmetic](https://github.com/shingarov/MachineArithmetic) provides Smalltalk interface
to Z3's C API. For more information, see [MachineArithmetic/README.md](https://github.com/shingarov/MachineArithmetic/blob/pure-z3/MachineArithmetic/README.md)
## System Overview
![System Diagram](https://github.com/Z3Prover/doc/blob/master/programmingz3/images/Z3Overall.jpg)
@ -215,5 +220,6 @@ A WebAssembly build with associated TypeScript typings is published on npm as [z
* C
* OCaml
* [Julia](https://github.com/ahumenberger/Z3.jl)
* [Smalltalk](https://github.com/shingarov/MachineArithmetic/blob/pure-z3/MachineArithmetic/README.md) (supports Pharo and Smalltalk/X)