1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71
|
default Order dec
$include <exception_basic.sail>
$include <arith.sail>
$include <smt.sail>
function main (() : unit) -> unit = {
assert(ediv_int(7, 5) == 1);
assert(ediv_int(7, -5) == -1);
assert(ediv_int(-7, 5) == -2);
assert(ediv_int(-7, -5) == 2);
assert(ediv_int(12, 3) == 4);
assert(ediv_int(12, -3) == -4);
assert(ediv_int(-12, 3) == -4);
assert(ediv_int(-12, -3) == 4);
assert(emod_int(7, 5) == 2);
assert(emod_int(7, -5) == 2);
assert(emod_int(-7, 5) == 3);
assert(emod_int(-7, -5) == 3);
assert(emod_int(12, 3) == 0);
assert(emod_int(12, -3) == 0);
assert(emod_int(-12, 3) == 0);
assert(emod_int(-12, -3) == 0);
assert(tdiv_int(7, 5) == 1);
assert(tdiv_int(7, -5) == -1);
assert(tdiv_int(-7, 5) == -1);
assert(tdiv_int(-7, -5) == 1);
assert(tdiv_int(12, 3) == 4);
assert(tdiv_int(12, -3) == -4);
assert(tdiv_int(-12, 3) == -4);
assert(tdiv_int(-12, -3) == 4);
assert(tmod_int(7, 5) == 2);
assert(tmod_int(7, -5) == 2);
assert(tmod_int(-7, 5) == -2);
assert(tmod_int(-7, -5) == -2);
assert(tmod_int(12, 3) == 0);
assert(tmod_int(12, -3) == 0);
assert(tmod_int(-12, 3) == 0);
assert(tmod_int(-12, -3) == 0);
assert(fdiv_int(7, 5) == 1);
assert(fdiv_int(7, -5) == -2);
assert(fdiv_int(-7, 5) == -2);
assert(fdiv_int(-7, -5) == 1);
assert(fdiv_int(12, 3) == 4);
assert(fdiv_int(12, -3) == -4);
assert(fdiv_int(-12, 3) == -4);
assert(fdiv_int(-12, -3) == 4);
assert(fmod_int(7, 5) == 2);
assert(fmod_int(7, -5) == -3);
assert(fmod_int(-7, 5) == 3);
assert(fmod_int(-7, -5) == -2);
assert(fmod_int(12, 3) == 0);
assert(fmod_int(12, -3) == 0);
assert(fmod_int(-12, 3) == 0);
assert(fmod_int(-12, -3) == 0);
assert(fdiv_int(5, 2) == 2);
assert(fdiv_int(-5, -2) == 2);
assert(fdiv_int(5, -2) == -3);
assert(fdiv_int(-5, 2) == -3);
assert(tdiv_int(5, 2) == 2);
assert(tdiv_int(-5, -2) == 2);
assert(tdiv_int(5, -2) == -2);
assert(tdiv_int(-5, 2) == -2);
}
|