[SMT-LIB] Integer division

[John R Harrison]

Hi Cesare,

| Since they are not defined yet, this would be a good time to put
| forward a proposal for their definition, if you have one :)

I don't think there are clear grounds for consensus, so maybe the
clear documentation of the choice is more important than the choice
itself. Or one could define several different operators covering
the variants, as is done in ACL2, following Common LISP. I like the
following survey:

  Raymond Boute:
  "The Euclidean definition of the functions div and mod". 
  ACM TOPLAS vol. 14 (1992), pp127-144

That paper distinguishes three main possibilities, all of which
satisfy the remainder law for all nonzero divisors:

  x = y * (x div y) + x mod y

but otherwise differ as follows:

  T-definition: x div y = trunc(x / y), i.e. rounded towards zero 
  F-definition: x div y = floor(x / y), i.e. rounded towards -infinity
  E-definition: 0 <= x mod y < |y|

My investigations seem to indicate that:

 * Most interactive theorem provers use the F-definition

 * Most programming languages and/or hardware use the T-definition

Nevertheless, I find Boute's arguments for the E-definition quite
sound, and it fits better with the generalization to other Euclidean
rings. I've provisionally decided to use the E-definition for HOL
Light.

John.