From 9488a404ff464ffad8d1523e9416eef38ad509e0 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 4 Mar 2020 06:21:30 -0800 Subject: [PATCH] [sledge] Compare logical variables by id only Summary: Program (and global) variables are only distinct when considering their string names, but logical variables need only their ids. Reviewed By: jvillard Differential Revision: D20214528 fbshipit-source-id: f7892c3ad --- sledge/src/llair/term.ml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml index b1a7ee038..166403ab6 100644 --- a/sledge/src/llair/term.ml +++ b/sledge/src/llair/term.ml @@ -104,6 +104,12 @@ end = struct | Float of {data: string} | Integer of {data: Z.t} [@@deriving compare, equal, hash, sexp] + + 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 end (* suppress spurious "Warning 60: unused module T0." *)