What is the definition of underflow in Z3 terminology

Question

Playing with Z3_mk_bvadd_no_underflow() and Z3_mk_bvadd_no_overflow() I had the feeling that the definition of underflow does not match what I found elsewhere in the literature (Wikipedia, INTEL programming manual,stackoverflow,...):

I understand that an overflow is when the result of the addition is greater than the greatest number that can be represented given the number of bits on which the operands are coded. This is usual.
For underflow, I understand that (in Z3 terminology) it is when the result is smaller than the smallest integer that can be represented given the number of bits on which the operands are coded. This is ok, but unusual in the literature from what I have seen (e.g. wikipedia) as this notion only applies to floating point numbers.

In the intel programing manual, overflow/underflow are dealt with carry and overflow flags:

Carry flag — Set if an arithmetic operation generates a carry or a borrow out of the most significant bit of the result; cleared otherwise. This flag indicates an overflow condition for unsigned-integer arithmetic. It is also used in multiple-precision arithmetic.

Overflow flag — Set if the integer result is too large a positive number or too small a negative number (excluding the sign-bit) to fit in the destination operand; cleared otherwise. This flag indicates an overflow condition for signed-integer (two’s complement) arithmetic.

Can you please confirm the exact definition of an underflow in Z3 terminology ?

I suggest to add that to the documentation, as well as the assumed way of the subtraction (first operand subtracted from second operand versus second operand subtracted from first operand), which holds from many other API of Z3.

score 1 · Accepted Answer · answered Sep 14 '15 at 09:31

The best definition for the underflow predicates is the code itself, see e.g., Z3_mk_bvadd_no_underflow; which does the following (minus reference counting):

Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2) {
    Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1));
    Z3_ast r = Z3_mk_bvadd(c, t1, t2);
    Z3_ast l1 = Z3_mk_bvslt(c, t1, zero);
    Z3_ast l2 = Z3_mk_bvslt(c, t2, zero);
    Z3_ast args[2] = { l1, l2 };
    Z3_ast args_neg = Z3_mk_and(c, 2, args);
    Z3_ast lt = Z3_mk_bvslt(c, r, zero);
    Z3_ast result = Z3_mk_implies(c, args_neg, lt);
    return result;
}

Note that the underflow predicates assume the the arguments are signed bit-vectors, except for Z3_mk_bvsub_no_underflow which has a flag to enable unsigned semantics.

For the final comment: Z3_mk_bvsub(c, t1, t2) always computes t1-t2.

What is the definition of underflow in Z3 terminology

1 Answers1