From fcd0e41ee6e2e76a1a43736bdc07f96786514e8c Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 16 Apr 2020 03:40:05 -0700 Subject: [PATCH] [sledge] Return early for == args in Term compare and equal Reviewed By: jvillard Differential Revision: D21048931 fbshipit-source-id: 30e76278f --- sledge/lib/term.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml index 9eaae1f4f..18fa0bd76 100644 --- a/sledge/lib/term.ml +++ b/sledge/lib/term.ml @@ -114,12 +114,16 @@ end = struct non-coefficient, so Integer and Rational terms must compare higher than any valid monomial *) let compare x y = - match (x, y) with - | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 -> - Int.compare i j - | _ -> compare x y + if x == y then 0 + else + match (x, y) with + | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 -> + Int.compare i j + | _ -> compare x y let equal x y = + x == y + || match (x, y) with | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 -> Int.equal i j