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.