div package:what4

div x1 [x2, ..., xn] with n >= 1 returns x1 div x2 * ... * xn. The terms are expected to have type Int.

Signed bitvector division. The result is truncated to zero. The result of bvSdiv x y is undefined when y is zero, but is equal to floor(x/y) when x and y have the same sign, and equal to ceiling(x/y) when x and y have opposite signs. NOTE! However, that there is a corner case when dividing MIN_INT by -1, in which case an overflow condition occurs, and the result is instead MIN_INT.

Unsigned bitvector division. The result of bvUdiv x y is undefined when y is zero, but is otherwise equal to floor( x / y ).

Divide one number by another. cplxDiv x y is undefined when y is 0.

Divide two floating point numbers.

intDiv x y computes the integer division of x by y. This division is interpreted the same way as the SMT-Lib integer theory, which states that div and mod are the unique Euclidean division operations satisfying the following for all y /= 0:

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

•  0 <= mod x y < abs y

The value of intDiv x y is undefined when y = 0. Integer division requires nonlinear support whenever the divisor is not a constant. Note: div x y is floor (x/y) when y is positive (regardless of sign of x) and ceiling (x/y) when y is negative. This is neither of the more common "round toward zero" nor "round toward -inf" definitions. Some useful theorems that are true of this division/modulus pair:

• mod x y == mod x (- y) == mod x (abs y)

• div x (-y) == -(div x y)

intDivisible x k is true whenever x is an integer divisible by the known natural number k. In other words `divisible x k` holds if there exists an integer z such that `x = k*z`.

natDiv sym x y performs division on naturals. The result is undefined if y equals 0. natDiv and natMod satisfy the property that given

d <- natDiv sym x y
m <- natMod sym x y

and y > 0, we have that y * d + m = x and m < y.

realDiv sym x y returns term equivalent to x/y. The result is undefined when y is zero.

Divide two floating point numbers.

bvsdiv x y returns round_to_zero (to_int x / to_int y) when y != 0. When y = 0, this returns not (from_nat 0). Note. This is in QF_BV, but not the bitvector theory.

bvudiv x y returns floor (to_nat x / to_nat y) when y != 0. When y = 0, this returns not (from_nat 0).

Signed bitvector division. The result is truncated to zero. The result of bvSdiv x y is undefined when y is zero, but is equal to floor(x/y) when x and y have the same sign, and equal to ceiling(x/y) when x and y have opposite signs. NOTE! However, that there is a corner case when dividing MIN_INT by -1, in which case an overflow condition occurs, and the result is instead MIN_INT.