From 1b5302b4d2617f8210068aedc5c070a088ccbce0 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 16 Apr 2020 03:40:18 -0700
Subject: [PATCH] [sledge] Simplify remainder of a rational by an integer

Summary:
Treat the remainder of dividing a rational by an integer as if the
rational was an integer division.

Reviewed By: jvillard

Differential Revision: D21042515

fbshipit-source-id: b5d42ddec
---
 sledge/lib/term.ml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml
index 18fa0bd76..3317a2223 100644
--- a/sledge/lib/term.ml
+++ b/sledge/lib/term.ml
@@ -634,6 +634,9 @@ let simp_rem x y =
   (* i % j *)
   | Integer {data= i}, Integer {data= j} when not (Z.equal Z.zero j) ->
       integer (Z.rem i j)
+  (* (n/d) % i ==> (n / d) % i *)
+  | Rational {data= q}, Integer {data= i} when not (Z.equal Z.zero i) ->
+      integer (Z.rem (Z.div q.num q.den) i)
   (* e % 1 ==> 0 *)
   | _, Integer {data} when Z.equal Z.one data -> zero
   | _ -> Ap2 (Rem, x, y)