Что такое определение опустошения в Z3 терминологии

Question

Играя с Z3_mk_bvadd_no_underflow() и Z3_mk_bvadd_no_overflow() у меня было ощущение, что определение сгущенного продукта не соответствует тому, что я нашел в другом месте в литературе (Wikipedia, INTEL руководство по программированию, StackOverflow, ...):

• Я понимаю, что переполнение, когда результат сложения больше, чем наибольшее число, которое может быть представлено, учитывая количество битов, на которых закодированных операнды. Это обычно.

• Для underflow я понимаю, что (в терминологии Z3) это когда результат меньше наименьшего целого числа, которое может быть представлено с учетом количества бит, на котором закодированы операнды. Это нормально, но необычно в литературе из того, что я видел (например, wikipedia), поскольку это понятие применимо только к числам с плавающей запятой.

В Intel программирующий вручную, переполнение/сгущенного рассматриваются несут и переполнения флаги:

флаг переноса - Устанавливается, если арифметическая операция генерирует перенос или заимствовать из самой значимой части результата; очищено в противном случае. Этот флаг указывает условие переполнения для арифметики без знака. Он также используется в арифметике с множественной точностью .

Переполнение флаг - Устанавливается, если целочисленный результат слишком велик положительный число или слишком мал, отрицательное число (без знака-бит), чтобы соответствовать в адресате; очищается в противном случае. Этот флаг указывает на условие переполнения для арифметики со знаком целого числа (двух дополнений).

Не могли бы вы подтвердить точное определение нижнего уровня в терминологии Z3?

Я предлагаю добавить это в документацию, а также предполагаемый способ вычитания (первый операнд вычитается из второго операнда и второго операнда, вычитаемого из первого операнда), который выполняется из многих других API Z3.

Answer 1

Лучшим определением предикатов underflow является сам код, см., Например, Z3_mk_bvadd_no_underflow; которая выполняет следующие действия (минус подсчет ссылок):

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; 
} 

Обратите внимание, что для нижнего предикаты предположат аргументы, подписанные битовые векторы, для Z3_mk_bvsub_no_underflow, который имеет флаг, чтобы включить неподписанную семантику кроме.

Для окончательного комментария: Z3_mk_bvsub (c, t1, t2) всегда вычисляет t1-t2.