In non-linear logics, rewrite DIVISION, INTS_DIVISION, and INTS_MODULUS into ITEs...

In non-linear logics, rewrite DIVISION, INTS_DIVISION, and INTS_MODULUS into ITEs of the form:

  IF (denom = 0) THEN divByZero(num) ELSE (DIVISION_TOTAL num denom) ENDIF

where divByZero is an uninterpreted function symbol (there's one for each of the partial operators).

In linear logics, don't do any of this.

Bitvector partial functions to come, if this is successful for Tim.

(this commit was certified error- and warning-free by the test-and-commit script.)