From f699c9b9a84fb212ee10af07e791eeb7281d5fa8 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 10 Oct 2019 06:16:54 -0700
Subject: [PATCH] =?UTF-8?q?[sledge]=20Simplify=20=C2=AC=C2=ACe=20to=20e?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Reviewed By: bennostein

Differential Revision: D17725617

fbshipit-source-id: 7467fad3e
---
 sledge/src/llair/term.ml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml
index 910aaa8e1..8a4b8bd5d 100644
--- a/sledge/src/llair/term.ml
+++ b/sledge/src/llair/term.ml
@@ -770,6 +770,9 @@ and simp_not term =
   | Ap2 (And, x, y) -> simp_or (simp_not x) (simp_not y)
   (* ¬(a ∨ b) ==> ¬a ∧ ¬b *)
   | Ap2 (Or, x, y) -> simp_and (simp_not x) (simp_not y)
+  (* ¬¬e ==> e *)
+  | Ap2 (Xor, Integer {data}, e) when Z.is_true data -> e
+  | Ap2 (Xor, e, Integer {data}) when Z.is_true data -> e
   (* ¬(c ? t : e) ==> c ? ¬t : ¬e *)
   | Ap3 (Conditional, cnd, thn, els) ->
       simp_cond cnd (simp_not thn) (simp_not els)