I'm attempting to use Z3Py to start off with a boolean formula then abstract it so that the boolean functions are unknown then convert it to smt-constraints such that each model of these constraints corresponds to a different formula similar to my original one. I would like to enumerate all models. I am wondering if this is possible using z3?
It appears you're looking for uninterpreted functions. You can define functions without any definition (just their type-signature), and SMT-solvers can reason with them quite effectively. Things get tricky if you need to use quantifiers to restrict the behavior of these functions, but if they're over boolean domains (and assuming you don't have a gazillion inputs), there might be effective ways to model these without any blow-up issues.
See here for a description of uninterpeted functions in z3py: Uninterpreted Sorts (Search in that page for the section named "Uninterpreted Sorts").