Claire Xen  🏳️‍⚧️ 🏳️‍🌈 🧙🏻‍♀️ BLM  🏴 🚩

a nice API boundary that allows different solvers to be swapped in. Note that I'm not outputting SMTLIB2, instead using libraries' native interface. Maybe a mistake, but I am nervous about introducing a text parse to my performance pathway when I have gazillions of quick solves.

So far my experience is Yices >> Z3 as far as QF_BV is concerned, although my Z3 prototype used a lot of stuff I didn't really need (integers and arrays). I'll give Z3 a shot in the new framework, but I really built it to use Boolector, which sounds like the bee's knees.

In my experience Yices >> Z3 and Boolector >> Z3. Yices vs Boolector is a bit more difficult. I'd say Boolector has the better SAT engine but Yices has better theories. For most pure QF_BV my expectation would be that Boolector performs slightly better.

Crossing my fingers for more than slightly... Maybe SMTCOMP19 isn't the Final Word on things but it looks a good deal like Boolector did considerably better on QF_BV - and the most competitive Yices results seem to have had a bit of tweaking in terms of what SAT was used.

Also, I don't really know how to understand SMTCOMP results outside of a crude 'league table'. I am using the solvers in incremental mode and do know what my theory is - QF_BV with a very light usage of UF in a earlier, less CPU-hogging phase of my code.

In the end you always have to try the solvers yourself on your specific problem.. So outputting SMTLIB2 code is the way to go IMO. When your algorithm does 1000s of fast small queries then going through SMTLIB2 can be a huge overhead, but for a few hard queries it's best imo.

Well, I've taken the stupid route, I guess, but after a uninspiring day of filling in a Really Big Pile of Pure Virtual Functions (yes, today I truly am the boolector_saddo) I'll be able to find out. My problem with the few hard queries approach is that my overheads are ...

very much a combination of "hey, the top 200 problems you gave me were kinda hard" and "whoa, really, 800,000 different CEGIS runs, are you fucking kidding me?". So a solver that absolutely slays on the hard stuff would be nice but I also need to be sure the easy stuff is fast.