Constrain edge and node symbolics during smt encoding

[DKLoehr]

Right now edges and nodes are encoded into smt as integers, and can take any value (even those not in the program). Some of our experiments suggested we could get speedups by constraining edge values to be only those which appear in the network, so we should look into doing that. The most likely way to do this is by adding a requires clause during the UnboxEdges transformation.