A rule set that never settles over a whole tree is caught too (#825)

[Rafael-SOWNet]

The cycle check merged in #1165 rewrites at the root, which is what makes its "a term came back"
criterion mean something — and it is also what it cannot see past. A full pass can move its rewrite
to a different node each time and never repeat a term while still never settling.

UntilStable already answers that question, and says so in its own remarks:

Hitting the bound is reported as no answer rather than as the last value reached. An unbounded
rewrite loop is the failure mode this layer is supposed to make visible, and handing back a value
from the middle of one would hide exactly the case worth seeing.

This is a caller taking it up on that, over every registered set and the same seeds.

It finds one, and it is not a cycle

NumericNeat has no fixed point on -x / (-y). It grows by four nodes a pass, indefinitely:

  0    7  -x / (-y)
  1    9  -1 * x / (-y)
  2   15  -1 * 1 * x / (1 * y) * 1 * (-1)
  3   19  -1 * 1 * 1 * x / (1 * y) * 1 * 1 * (-1)
  ...

No term ever repeats, so the root check was right to pass — this needed the whole-tree form.

a-negative-factor-in-a-numerator-comes-out and its denominator twin each take a negative factor out
and write the magnitude back in its place. When the factor is -1 the magnitude is 1, and it
goes back as a literal 1 * rather than folding away; the two rules then undo each other around the
factors that accumulate.

That is #1056 one file over. #1056 was fixed by having the collecting rule decline c = -1, with
a comment giving the reason — "that is not a numeric factor to collect but the sign, which the
language spells as a product." The same reasoning applies here.

Latent, not live — checked rather than assumed

Simplify is unaffected: "-x / (-y)".Simplify() answers x / y in 68 ms, because the pipeline
is bounded and selects by size rather than running this set alone to a fixed point. Nothing a user
does today reaches it.

It still matters. A caller may reasonably use Transformation.Rewriting(set).UntilStable(n) — that
is what the layer is for — and equality saturation runs sets against a budget, which a set with no
fixed point spends.

Not fixed here

Declining at a magnitude of 1 is the obvious move and matches #1056's precedent, but it narrows two
rules that are otherwise doing useful work. #1167
records what a fix would need to establish first: which expressions currently reach a better form
through the 1 * step, and whether Simplify's answer moves for any of them.

Pinned as the one known pair rather than counted, so a new one fails the test — and so does this
one disappearing. A fix should delete the entry rather than leave a name behind that no longer means
anything.

Verification

Full suite 9555 passed, 0 failed, 14 skipped.

Part of #825.