Library for smt-solvers

Learn
#1

Hello there,

So I’m working on an implementation to one of my research projects. Naturally, my first thought was to use Haskell, :slight_smile:

I need to use smt solvers, one candidate is Z3. I was able to use the z3 library and it worked well.
But for benchmarks that’s a too hard of a dependency I want to be able to test solving instances of my problem with others smt solvers as well.

After some googling I found the smtlib library.
Yay! There is when my nightmares began, though.

Using stack to compile my project I can’t possible compile this library (added it as external dependency). So the library seems to be very old too, and I can’t figure out how to ‘fix’ it, I tried to do it and do a PR there.

So, finally my general question: Is there any other options to use smt solvers in Haskell?
Should I try to build my own FFI (it seems all of them work that way) to use them? That seems to be a lot of work!

I’m almost switching to ocaml due to not being able to solve this… I really want to use Haskell in this project.
Can anyone give me help in this matter?

Thank you,
Deivid.

1 Like
#3

The best SMT library is SBV hands down. It supports all SMT-Lib compatible solvers. It is in all recent stackage snapshots, so it should be very easy to use with stack.

5 Likes
#4

Hi I built my PhD thesis project using Haskell + SBV, and contributed to SBV in the process!

SBV is definitely the most fully featured, but it provides those features by piping the SMTLIB program to the solver process through stdout. That serialization comes at quite a cost, so if you know you will be building up one big SAT/SMT problem and the solver time will dominate then SBV is a good choice. But if you are going to be doing a lot of incremental SAT/SMT solving then you might be better off using the z3 library since the FFI will have much faster (a few orders of magnitude) inter-process communication.

So I would recommend starting with SBV, write your research project on it, and then when you need to optimize you can branch and swap for Z3 if you really need to. As long as you stick close to the SMTLIB2 standard (I would recommend reading the standard if you are doing SAT/SMT stuff too) you’ll be fine. You can also wrap the solver provider in a type class to make most of your code polymorphic over the solver since the APIs are almost identical. You might lose some performance due to the abstraction but you could always use a specialize pragma to regain what you might have lost, and since you’ll only have two cases: SBV and Z3, it won’t be too much pain.

Also also, if you go with Z3 you can fork and disable some of its internal checks to get ~100x speedup again! I’d have to dig through some old code for an example, but I just wanted to point it out.

You might also check out picosat by Steven Deihl, although I am unsure if it is still maintained.

5 Likes
#5

Also also also, if you go with sbv you should be aware that its hash-consing cache has a memory leak. This is also very easy to fix but I never finished my PR on it. You can read the discussion and fix here. Another plus with sbv is that Levent Erkok (the library author/maintainer) is great to work with and very responsive, so don’t hesitate to open an issue if you need some help.

2 Likes
#6

Thanks for your response, @doyougnu

I’ll check it out for sure and go with sbv.

:slight_smile: