Instanciar z3 solver

[samuelbarbosazup]

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

[sim642]

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]

Thanks a lot, very helpful.