Add class size based scheduler

[remysucre]

This is similar to the Backoff Scheduler, but bans rewrites based on the class size. Specifically, when a class grows past a limit, we stop applying rewrites to it for a few iterations.

This is more fine-grained than the Backoff Scheduler, which bans a rule for all classes when that rule explodes some class. Scheduling based on class size is also closer to how we do prove by hand: if we have rewritten a certain subterm too many times, we'll move on to some other subterms. For example, if we've applied AC to a certain class too many times, we'll still apply AC, but to other classes.

[mwillsey]

I think we'll close this for now, as it's implementable as an external library (as demonstrated by this PR).