From ed82bca4a54eb8a0afa911712c50aba13c8d92da Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 23 Mar 2020 06:19:04 -0700 Subject: [PATCH] [sledge] Document that integer division and remainder use truncation semantics Summary: Integer `div` and `rem` are a pair of functions that satisfy the division rule, where the result of `div` is truncated toward zero: ``` | Div (** Division, for integers result is truncated toward zero *) | Rem (** Remainder of division, satisfies [a = b * div a b + rem a b] and for integers [rem a b] has same sign as [a], and [|rem a b| < |b|] *) ``` Reviewed By: jvillard Differential Revision: D20584626 fbshipit-source-id: fa02a3a98 --- sledge/lib/exp.mli | 6 ++++-- sledge/lib/term.mli | 6 ++++-- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/sledge/lib/exp.mli b/sledge/lib/exp.mli index 4244ac02f..9e387d664 100644 --- a/sledge/lib/exp.mli +++ b/sledge/lib/exp.mli @@ -50,8 +50,10 @@ type op2 = | Add (** Addition *) | Sub (** Subtraction *) | Mul (** Multiplication *) - | Div (** Division *) - | Rem (** Remainder of division *) + | Div (** Division, for integers result is truncated toward zero *) + | Rem + (** Remainder of division, satisfies [a = b * div a b + rem a b] and + for integers [rem a b] has same sign as [a], and [|rem a b| < |b|] *) | Udiv (** Unsigned division *) | Urem (** Remainder of unsigned division *) | And (** Conjunction, boolean or bitwise *) diff --git a/sledge/lib/term.mli b/sledge/lib/term.mli index 69ea56977..ba24c85ae 100644 --- a/sledge/lib/term.mli +++ b/sledge/lib/term.mli @@ -35,8 +35,10 @@ type op2 = | Le (** Less-than-or-equal test *) | Ord (** Ordered test (neither arg is nan) *) | Uno (** Unordered test (some arg is nan) *) - | Div (** Division *) - | Rem (** Remainder of division *) + | Div (** Division, for integers result is truncated toward zero *) + | Rem + (** Remainder of division, satisfies [a = b * div a b + rem a b] and + for integers [rem a b] has same sign as [a], and [|rem a b| < |b|] *) | And (** Conjunction, boolean or bitwise *) | Or (** Disjunction, boolean or bitwise *) | Xor (** Exclusive-or, bitwise *)