Thanks for the discussion! I agree in most cases SMT solving are light-weight, given the majority of operators have simple constraints (e.g., element-wise or injective). Such optimization should only be considered in very rare cases. Taking the example of reshape again, solving one single reshape operator could bring up to 8 second solving time subjective to the number of symbols and prior constraints, which is why sometimes it is meanful to do some optimization.
But it could be specific to z3. There are other alternative solvers such as cvc5 and mip which might solve those constraints faster. BTW, we can talk more about the prior work elsewhere and let’s keep this thread more focused on RFC’s content. 