Avoid installing Z3 as default solver

[filipeom]

Ship the encoding with another solver that is quicker to install (Bitwuzla?). Is it possible to retain the z3_mappings implementation? Perhaps, utilize a stub z3 library that fails at runtime if z3 is not installed?

[redianthus]

There's a way to mark a dependency as optional. If we do this for Z3, it's possible to tell the users: install Z3 if you want better performances. Opam will then recompile the encoding package when Z3 gets installed (this requires some dune magic ofc).

I don't know which solver could be used instead (I would suggest alt-ergo but I'm biased :-)).

[filipeom]

That's great! I'll look into it.

Also, can we flag that certain modules require optional dependencies so that they don't get compiled?

[filipeom]

Heheh, as for the sovler I really like bitwuzla's bindings for ocaml. But I can try alt-ergo first 😃

[redianthus]

Also, can we flag that certain modules require optional dependencies so that they don't get compiled?

Yes kinda. I already did it, we can discuss it in details together when you'll be implementing it if you want.

Heheh, as for the sovler I really like bitwuzla's bindings for ocaml. But I can try alt-ergo first 😃

I don't know bitwuzla at all. But alt-ergo is written in OCaml so I'm quite interested (for the web interface of Owi it would be much simpler thanks to js_of_ocaml). Maybe @hra687261, @Halbaroth or @bclement-ocp could help writing the alt-ergo part.

Also, @hra687261 already wrote the colibri2 interface a few months ago, would you accept a PR ?

[filipeom]

Yes kinda. I already did it, we can discuss it in details together when you'll be implementing it if you want.

Cool thanks! 😃

Also, @hra687261 already wrote the colibri2 interface a few months ago, would you accept a PR ?

Yes, of course! I was planning on it 😃 I also think Hichem mentioned the interface to alt-ergo is similar to colibri's one? So it might be easy to adapt his

[hra687261]

Yes, I can rebase the Colibri2 branch. To use Alt-Ergo, it shouldn't be too hard since it supports the same front-end as Colibri2 (Dolmen), also there's an example on using Alt-Ergo as a library in https://github.com/hra687261/alt-ergo-fuzz, on the other hand its FPA theory is different from the standard SMT-LIB one, but I'm not sure that it will be an issue.

Bitwuzla could in fact be a good idea, it's known to be pretty good with BVs and FPA, dunno about it's installation/compilation time tho.

[filipeom]

Yes, I can rebase the Colibri2 branch.

Thanks, if you can do this and create PR it would be fantastic! 😄

its FPA theory is different from the standaI also don't think this will be an issue, and Z3's rd SMT-LIB one, but I'm not sure that it will be an issue.

From what I understand, does Alt-Ergo not support NaNs? We would need to find a way to encode this in Owi for bug-finding purposes. However, if this speeds up the analysis, it would probably be better for Test-Comp since it's time limited.

Bitwuzla could in fact be a good idea, it's known to be pretty good with BVs and FPA, dunno about it's installation/compilation time tho.

I tried installing it through OPAM, and it's considerably faster than Z3. We will probably be trying it out in the future; there's no rush at the moment.

[hra687261]

Thanks, if you can do this and create PR it would be fantastic! 😄

Done #57 :)

From what I understand, does Alt-Ergo not support NaNs? We would need to find a way to encode this in Owi for bug-finding purposes. However, if this speeds up the analysis, it would probably be better for Test-Comp since it's time limited.

Yes, if there's a way around it then it should be ok. When it comes to performance, it's hard to guess without testing. If my memory serves me right, Alt-Ergo's FPA theory is particularly efficient for specific problems in which you use both reals and floats.

[filipeom]

Thanks for the PR! 🎉

Yeah, and I guess it will also depend on the type of program we'd be analyzing with Owi. We will see 😃

[redianthus]

I think this can be closed @filipeom :)