From 435c3de5bb47ada23597ded9088421e65a448f0c Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sun, 21 Feb 2021 13:18:18 -0800 Subject: [PATCH] [sledge] Optimize Trm.compare Reviewed By: jvillard Differential Revision: D26338019 fbshipit-source-id: 886604c2b --- sledge/src/fol/trm.ml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/sledge/src/fol/trm.ml b/sledge/src/fol/trm.ml index 79ba468c6..c73c385ad 100644 --- a/sledge/src/fol/trm.ml +++ b/sledge/src/fol/trm.ml @@ -29,6 +29,13 @@ module Trm1 = struct (* uninterpreted *) | Apply of Funsym.t * t array [@@deriving compare, equal, sexp] + + let compare a b = + if a == b then 0 + else + match (a, b) with + | Var x, Var y -> Int.compare x.id y.id + | _ -> compare a b end (* Add comparer, needed to instantiate arithmetic and containers *)