Hello all, looking for guidance! I want to "simplify Boolean expression" to create a minimal description of a boolean vector using pre-defined expressions, e.g. convert [0,0,1,1,0,1,1,1,0,0,0,0,0] into `fromEurope || (hasCar && likesMusic)` (made up example).

I've been looking into Z3 solver and `simplify` and patterns, but I'm not sure it can "go backwards", and I'm lost in the nomenclature and high-level math. E.g. would "weakest precondition"[1] apply to my case?

[1] https://en.wikipedia.org/wiki/Predicate_transformer_semantics