as a note, I've tried MiniZinc for modeling a problem in the past, and the language/ecosystem simply wasn't up to my task. iirc, function calls in MiniZinc are expanded/unrolled when the model is generated, rather than the function definition and its callers being symbolically translated into the model.

this is no fault of MiniZinc, I simply thought that an SMT solver would be sufficient and it wasn't. I need a mixed-integer or non-linear program solver, and ended up approaching it with a computer algebra system to generate my models and passing it to Gurobi or HiGHS.

tl;dr there's different types of hard, and SMT solvers are only good at some types of hard.

One interesting development in the latter years is the mix of Constraint programming and SAT solvers. For example Google OR-tools (https://developers.google.com/optimization/ ) which mixes CP, SAT and MIP. It has won most of the MiniZinc Challenge categories (https://www.minizinc.org/challenge.html ) several years now. The Chuffed solver is another solver mixing CP and SAT.

isn't or-tools just a wrapper library for a bunch of solvers? I must be missing something.

""" CP-SAT is a discrete optimization solver built on top of a SAT engine. It is available within the OR-Tools open-source repository (website: https://developers.google.com/optimization, github repository: https://github.com/google/or-tools). It has won multiple gold medals at the MiniZinc challenge (https://www.minizinc.org/challenge.html) since its debut in 2017.

The CP-SAT solver is architectured around five components: The base layer is a clause learning SAT solver. Above the SAT layer sits a Constraint Programming (CP) module with Boolean, integer and interval variables, and standard integer, scheduling and routing constraints. Alongside the CP solver, a simplex provides a global linear relaxation. Its integration with the CP and SAT layers enable the CP-SAT solver to solve MIP problems with the same techniques as (commercial) MIP solvers: relaxation, cuts, heuristics and duality based techniques. Both the CP and MIP modules rely on a unified protobuf representation of the model that can serve as a file format, as well as an intermediate representation of the model during all phases of the solve (input format, presolved model, LNS fragment). On top, the search layer implements a robust information-sharing portfolio of specialized workers that offers both good and fast solutions, and superior optimality proving capabilities.

This work was presented at the CPAIOR 2020 masterclass. The recording is available on youtube (https://www.youtube.com/watch?v=lmy1ddn4cyw). """