(SMT/verification geek here)
Can you give a bit more context about this?
Are these SMT files created by Sympy or is this an alternative code path in PyTorch that bypasses Sympy entirely?
The goal of the symbolic shapes code, I think, is two fold:
- Do type/shape checking. This is a simple satisfiability check to ensure the program is type-safe
- Compute symbolic shapes for each operator, with a simplified expression (whatever that means). This is not easily solvable with SMT solvers.
Also, could you give an example of a complex shape computation that requires such heavy machinery?
Happy to help with this stuff if needed, but I need a bit more context.
I’ve started to play with symbolic stuff today, with partial success. I still see some crashes, especially when mixing with torch.compile. I’m probably doing something that is not supported…
Thanks,
Nuno