Generating graph with complex structure I want to generate a bunch of graphs of about 100 nodes, where each node is a categorial variable.  I want the graphs to satisfy complex properties, like, "if a node of type A is connected to a node of type B, that node of type B should also be either connected to both a node of type C and a node of type D, or should be connected to a node of type E" and "no nodes of type F and G can be connected to the same node."  How do I go about generating such structures?  I was thinking of using an SMT solver, but even then I'm not exactly sure how to proceed.  For instance, is there a way to do it using only BitVectors?
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.