Generating graph with complex structure
I would use a SAT solver.  Use one boolean variable per edge to encode whether that edge is present or not.  Encode the type of a node via a one-hot encoding ($k$ variables per node, where $k$ is the number of possible types).  Then each constraint you mention should translate directly into a simple formula on a few of these boolean variables.

I like Z3 for ease of programming.

I see no reason nor benefit to using bitvectors or SMT; plain SAT should suffice.