Associate all lemmas in non-linear arithmetic with an inference identifier (#4712)

Associate all lemmas in non-linear arithmetic with an inference identifier (#4712)

This marks all lemmas in non-linear arithmetic with an identifier, which indicates informally the kind of justification that was used for them. The main motivation for this is for debugging the behavior of the non-linear solver.

The number of inferences can then be seen with --stats:

nl::inferences, [(SPLIT_ZERO : 19), (SIGN : 4), (COMPARISON : 29)]
The same design was used in strings and has been quite helpful.

This also adds a few high level stats to the new statistics class for non-linear.