Happy to! The SMT files here bypass sympy entirely; they contain exactly the shape computations that the original user program / operators had. The asserts correspond to places where people (usually operators) did control flow
The goal of the reasoning code is a little difficult to express exactly. The smt2 instances test one particular thing that is easy to formulate for SMT solvers: given a sequence of shape computations and asserts, find a satisfying assignment of input shapes that satisfies all the asserts. This could be used to, for example, take a model and regenerate a small version of it (with small parameters and inputs) for easy testing. But this is actually not really the most pressing problem for dynamic shapes in PyTorch as is, IMO. The PyTorch reasoning code tends to do two other things: find simple canonical forms for size expressions, so that we can eventually simplify the loop bound / indexing computation we generate in inductor, and determine if guards are redundant or not (since we spend a lot of time testing conditionals, which naively must be retested before we can reuse compiled code.) And we would like to do this all in a simple Python implementation, which precludes more typical approaches like throwing LLVM’s optimizer at the problem. “Simple” canonical forms is not so easy to express in smt-lib2 nomenclature; redundant guards is technically expressible but awkward (and better suited as a compiler benchmark.)
We currently have a baseline sympy+unification implementation (which I have provided a crappy hookup for) which also takes some extra simplifications I haven’t encoded in the problem instance yet (duck sizing, 0/1 specialization) and while, if you treat sympy as a black box it’s pretty simple, empirically our biggest problem is that it is slow. I’ll post some measurements I took but in some pathological cases we can spend minutes just crunching sympy simplifications. And as a team we have a bit of a disagreement about how to proceed. I kind of want to chuck sympy entirely and roll our own domain specific algebra system, but @Chillee thinks this is too much and we should be able to patch over the specific sympy badness more quickly than having to rewrite everything from scratch. We also kind of need an entailment system, which an SMT solver would provide, but we don’t have a good sense for how to do this integration. Should Z3 really be a mandatory dependency for dynamic shapes?
Re crashes, post up what you are doing. Inductor still doesn’t work on master but you should be able to play around with aot_eager