Don't bother including bad rules

[ninehusky]

There are some bad rules, such as:

if a > 0 then a > 0 ~> a - a

We shouldn't include them. One pattern I've noticed with these rules is that in the case where the condition holds, the lhs evaluates to exactly one value (because they essentially rewrite false ~> false or true ~> true). Pruning rules that fall under this category would get rid of a lot of these bad conditional rules. However, they'd also get rid of rules like if a != 0 then a / a ~> 1, so I'm unsure of how to handle it.

Chandra said that we could start by just getting rid of rules whose conditions are syntactically equal with their lhs. This won't get rid of rules like if a > 0 then a <= 1 ~> 1, but it's a start.

[ninehusky]

Chandra said that we could start by just getting rid of rules whose conditions are syntactically equal with their lhs. This won't get rid of rules like if a > 0 then a <= 1 ~> 1, but it's a start.

Chandra said that this was my idea? I don't think I'm that smart. Anyways, this is implemented in #68 .

Chandra mentioned we could also do something were we check the extracted term during cvec_match: (assuming that Egglog automatically extracts using size), we can see if the term corresponding to an eclass is a constant -- if it is, let's just skip it. This works in the total case, but for the conditional case we'll still need to iterate through.

To elaborate: under our current implementation, if we're considering if c then a ~> b, then forall i . pvec[i] -> cvec(a) = cvec(b). What I'm proposing is that we throw away all cases where: forall i, j. pvec[i] -> cvec(a)[i] = cvec(a)[j] or cvec(b)[i] = cvec(b)[j]. More intuitively, this means that if it's the case that whenever the predicate holds, we're rewriting const ~> const, we should just not consider it as a candidate rule.