From 06f2863dd8629f1030a7b2166035dd392f0d4add Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 10 Oct 2019 06:16:50 -0700 Subject: [PATCH] [sledge] Simplify `e xor e` to `0` Reviewed By: bennostein Differential Revision: D17665226 fbshipit-source-id: 655ddf6a8 --- sledge/src/llair/term.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml index cdd339519..910aaa8e1 100644 --- a/sledge/src/llair/term.ml +++ b/sledge/src/llair/term.ml @@ -787,6 +787,8 @@ let simp_xor x y = (* true xor b ==> ¬b *) | Integer {data}, b when Z.is_true data && is_boolean b -> simp_not b | b, Integer {data} when Z.is_true data && is_boolean b -> simp_not b + (* e xor e ==> 0 *) + | _ when equal x y -> zero | _ -> Ap2 (Xor, x, y) let simp_shl x y =