Expr simplifier: implement prove::isPositive, prove::isNonNegative, prove::isNonZero

[zasdfgbnm]

This PR implements prove::isPositive, prove::isNonNegative and improve prove::isNonZero. This PR also added a new pass eliminateTrivialPredicate to simplify compare with zero. I don't the eliminateTrivialPredicate will be super important to simplify predicates that we generate, but it is super helpful for me to write unit tests to check if these proves works as expected.

The proves prove::isPositive, prove::isNonNegative, and prove::isNonZero are very important for expression simplification because many rules require sign compatibility check:

// J) Distributivity of % over +:
//    If compatible_sign(a, b), then (a + b) % c = (a % c + b % c) % c
// K) Distributivity of % over *:
//    If compatible_sign(a, b), then (a * b) % c = (a % c * b % c) % c
// Q) If compatible_sign(a, b) and -|c| < a % c + b % c < |c|, then
//    (a+b)/c = a/c + b/c

[naoyam]

This would be fine, but why don't we add static methods to create tensor size and stride named scalars and explicitly tag them as such? That seems more robust than the string-based pattern match.

[zasdfgbnm]

I generally agree, but I prefer to keep NamedScalar string only. We could have new subclasses of Val for values that has special meaning, for example class TensorAttribute : public Val. And I believe a good place to do this refactor is at #2282, where I need to access the .data of a global tensor.

[naoyam]

Yeah, that would be better, and it should have a dependency connection to the tensor itself. I just don't like the string matching-based approach as it seems backward.

[naoyam]

Why are only these ops considered here? Why not, e.g., BinaryOpType::Add?

[zasdfgbnm]

Because Add and Mul are already flattened as FlattenedAssocCommOp, so we will not see BinaryOp with Add and Mul here.

[naoyam]

Where is the fattening done? Does this function assume the value parameter is flattened?

[zasdfgbnm]

Flatten is done before running any other passes:

pytorch/third_party/nvfuser/csrc/expr_simplifier.cpp

Line 1183 in 2ca39e3

auto simplified = assoc_comm::flatten(value);

So all other passes assumes the input value already flattened.

[naoyam]

OK, thanks. Could you mention that as a comment? Probably obvious to you, but it would have been definitely a helpful comment for me.

[zasdfgbnm]

OK, thanks. Could you mention that as a comment? Probably obvious to you, but it would have been definitely a helpful comment for me.

Oh, sorry, missed this comment. Will add to #2275

[zasdfgbnm]

Added in dbe16cd

[naoyam]

nit: Looks like the block below is mostly a duplicate of the above block. Would be great if refactored.

[zasdfgbnm]

I can not think of a more readable way to refactor this. This is like implementing a table lookup using if statements. Different branches will look similar, but each with some small modifications. To me, the most straightforward way to implement this is to just list them all.

[naoyam]

LGTM. Thanks for answering the questions.