diff options
| -rw-r--r-- | lib/arith.sail | 29 | ||||
| -rw-r--r-- | test/builtins/divmod.sail | 92 |
2 files changed, 87 insertions, 34 deletions
diff --git a/lib/arith.sail b/lib/arith.sail index 6b064433..58f25bbc 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -88,13 +88,38 @@ val tdiv_int = { } : (int, int) -> int /*! Remainder for truncating division (has sign of dividend) */ -val tmod_int = { +val _tmod_int = { ocaml: "tmod_int", interpreter: "tmod_int", lem: "tmod_int", c: "tmod_int", coq: "Z.rem" -} : (int, int) -> nat +} : (int, int) -> int + +/*! If we know the second argument is positive, we know the result is positive */ +val _tmod_int_positive = { + ocaml: "tmod_int", + interpreter: "tmod_int", + lem: "tmod_int", + c: "tmod_int", + coq: "Z.rem" +} : forall 'n, 'n >= 1. (int, int('n)) -> nat + +overload tmod_int = {_tmod_int_positive, _tmod_int} + +function fdiv_int(n: int, m: int) -> int = { + if n < 0 & m > 0 then { + tdiv_int(n + 1, m) - 1 + } else if n > 0 & m < 0 then { + tdiv_int(n - 1, m) - 1 + } else { + tdiv_int(n, m) + } +} + +function fmod_int(n: int, m: int) -> int = { + n - (m * fdiv_int(n, m)) +} val abs_int_plain = { smt : "abs", diff --git a/test/builtins/divmod.sail b/test/builtins/divmod.sail index f9d7e7c5..458d8dfd 100644 --- a/test/builtins/divmod.sail +++ b/test/builtins/divmod.sail @@ -5,39 +5,67 @@ $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(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(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(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(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); }
\ No newline at end of file |