Add a solver module to create solvers with the smtml mappings

[filipeom]

Here's the thing I promised before going on my internship 🙈

In this implementation, we don't use any of the smtml values. We only use the thin parametric layer that allows us to connect to the various solvers. This should be as fast as using the bindings directly.

Currently, it's only expected to work with Z3, as I don't have the mappings to ADTs implemented in Alt-Ergo or CVC5.

There are still a couple of things to do. There are some assert falses in the code, but I think I should be able to do those with the API smtml currently has. This shouldn't be a problem.

I still want to connect it to the cli, which should be easy as smtml has helpers for cmdliner in Smtml.Solver_type and Smtml.Solver_dispatcher.

Also, it's currently pinned to a development version of smtml because I just added mappings to the ADTs. This should be included in our next Monday release.

I won't promise to complete this in the next week, to avoid falling into the trap I did previously, but I'm opening the PR to show you it's almost done and also to gather feedback. I'm not expecting you to adopt smtml just because I really want you to, but I hope that once it's finished and I benchmark it, you'll find some value in it.

We're going to be adding more bindings for other solvers in the future, but this may take some time as we currently don't have anyone working exclusively on smtml.

[giltho]

This is great, I haven't read the code yet but I'm excited!
Thank you Filipe :) We're currently writing the PLDI paper. If the benchmarks are good, I'm very happy to say that we use smt-ml in the paper. And there is no emergency, it can be done for camera ready if the paper gets accepted in many months

One thing we're worried about is having to install z3 through opam as it is famously extra slow but if the benchmarks are improving then that's a net improvement still and we'll merge

[filipeom]

One thing we're worried about is having to install z3 through opam as it is famously extra slow but if the benchmarks are improving then that's a net improvement still and we'll merge

smtml doesn't force you to install any solver when you depend on it, so if you're worried about CI times increasing, you can just avoid using smtml there.

As a side note, I think the Z3 OCaml package maintainers plan to link the bindings to the system-wide installation of Z3. This should avoid building Z3 from scratch (see https://discuss.ocaml.org/t/ask-for-suggestions-for-the-next-z3-package-release/8922/17).

Hopefully, we can do the same for cvc5 in the future to avoid significant overhead when installing solvers.

[giltho]

smtml doesn't force you to install any solver when you depend on it, so if you're worried about CI times increasing, you can just avoid using smtml there.

Yes but I'd like to make smtml default for the C and Rust interpreters if it's faster. But again, this is minor indeed.

Annoying side note, we currently have C_values and BV_values, we're planning on probably removing C_Values and using BV_values in both Rust and C. In addition, we might use something much higher level for Rust (what is currently called Rust_values.t but with an additional Var.t variant). This would require significantly more work to encode it into smt, so maybe we'll keep the simple-smt interface for now in case smt-ml needs modifications.

Finally, actually, when's the CR for TACAS? If we can get it through the finish line before then, you may be able to claim this in your paper :)

[filipeom]

Annoying side note, we currently have C_values and BV_values, we're planning on probably removing C_Values and using BV_values in both Rust and C.

Oh didn't notice there was a BV_values. But if it's just bitv and fpa it should be good. I think we have most of the mappings for it already.

In addition, we might use something much higher level for Rust (what is currently called Rust_values.t but with an additional Var.t variant). This would require significantly more work to encode it into smt, so maybe we'll keep the simple-smt interface for now in case smt-ml needs modifications.

Yeah, my hope would be that you keep simple-smt for that reason. That way, we don't slow you down. I can then look at what SMT features you need, design a semi-decent API, and connect it to all the solvers.

Finally, actually, when's the CR for TACAS? If we can get it through the finish line before then, you may be able to claim this in your paper :)

Hehe, thanks! It's January 22, 2026. So I think I will have time to finish everything by then. Also, after the PLDI deadline, I hope some people on our end will be free to help with smtml, so there's that.