Explore the "zero problem"; cut down on constants

[ninehusky]

I'm referring to the problem of adding constants like zero into the egraph. Once we add zero along with other constants, we derive lots of non-helpful rules like: (a + 1 + 1) ~> (a + 2). Once we reach a large enough size, we need a way of not putting terms into the egraph of that form. This will also cut down on the number of eclasses.

In a way, we want e-classes to be "general"; they should represent the shape of some computation rather than some concrete value. For example, an example like (a + b) is far more valuable than (a + 1 + 1 + 2 + 3 + 4).

[ninehusky]

Now that we have conditions, it might be worth it to remove constants from being generated entirely. You can encode something like (a * 2) ~> (a + a) with if b = 2 then (a * b) ~> (a + a). This cuts down on the number of terms we need to enumerate.