These types of constraint solving approaches have been done before. Despite claims otherwise, it is not actually practical. The number of models solved well in

These types of constraint solving approaches have been done before. Despite claims otherwise, it is not actually practical. The number of models solved well in 100-200ms is basically zero. They seem to believe 10-20 seconds per function is reasonable, and it's not. They probably otherwise take < 1 second to compile (if not a small number of milliseconds). It's already pretty well-known that you can get some significant gain from optimal instruction scheduling and selection (and other things). The models are even super nice to work with. So it would be awesome if it could be used. But unfortunately even this paper does not make it practical to do even for those who want it, as the class of users willing to spend days to compile things is very small.