Oh cool. Yeah, I looked around from "Music Composition Constraint Solving/SMT/Z3" stuff and didn't find anything which was surprising. I'll take a look at Rosette too, I've heard of it a couple times but never dug in