Transform constraints to z3 constraints which is the final step (#80110)
Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)
We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. Some of the other operations are a 1:1 transformation.
contains tests for alexnet and resnet as well as smaller examples
Pull Request resolved: https://github.com/pytorch/pytorch/pull/80110
Approved by: https://github.com/anijain2305, https://github.com/jamesr66a
