search

sim642 / z3em

Z3 via emscripten
https://www.npmjs.com/package/z3em
MIT License
8 stars 1 forks source link

Instanciar z3 solver #4

Open samuelbarbosazup opened 4 years ago

samuelbarbosazup commented 4 years ago

How can I instantiate the z3 solver and if possible how to pass a formula for testing?

sim642 commented 4 years ago

Since I created this for just my own use in another project, it really lacks documentation or comprehensive features (and is massively outdated Z3 now).

I don't have a simple example script either, but it exposes the Z3Em object, which is an emscripten object with all of its standard features. Some example of initialization: https://github.com/sim642/einstein-js/blob/d1fd63549cad60e2485b768f8a475fab425e9bcf/src/z3/Z3.ts#L15-L22. To use the initialized emscripten object, you can wrap the few C functions that are exported like this: https://github.com/sim642/einstein-js/blob/d1fd63549cad60e2485b768f8a475fab425e9bcf/src/z3/Z3.ts#L72-L82. Basic usage can be seen here (creating config, context and evaluating smtlib2 formulae): https://github.com/sim642/einstein-js/blob/d1fd63549cad60e2485b768f8a475fab425e9bcf/src/puzzle/generate/Z3HintsGenerator.ts#L25-L54.

samuelbarbosazup commented 4 years ago

Thanks a lot, very helpful.