Since then, played around with its optimizer a bit and found the API UX pretty lackluster: You can put in problems it doesn't support and rather than blow up, it will often just return non-optimal results.
As a makeshift CP solver, it does seem excellent though!
@fuglede Cool! I stopped playing AoC way too early in 2018, but that puzzle looks fun. Have you used other similar libraries?
@ahf Probably not per se. As in, can't say SMT is something I've encountered regularly.
But as I'm sure you know, there's a huge market for optimization libraries in general, which Z3 ends up being a competitor in with its functionality (the AoC puzzle could also be solved with one of a billion LP solvers, but Z3 was way better; my own AoC solution used scipy.optimize and took 6 hours to run).
In the direction of theorem proving, I get the feel that Lean (also MS) is picking up a lot of speed.
Server run by the main developers of the project It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!