From ffb0f4f9125384d5825bb9c76df7034645cb6307 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 26 Apr 2019 12:03:33 -0700
Subject: [PATCH] [sledge] Relax 'no new subexps' invariant for Xor expressions

Summary:
Boolean Xor expressions are treated directly by the solver, so the 'no
new subexps' invariant for congruence closure is not needed.

Reviewed By: mbouaziz

Differential Revision: D15098817

fbshipit-source-id: d118c5881
---
 sledge/src/llair/exp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index ea8deefda..36cdd0b35 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -1140,7 +1140,7 @@ let app1 ?(partial = false) op arg =
   |> check (fun e ->
          (* every App subexp of output appears in input *)
          match op with
-         | App {op= Eq | Dq} -> ()
+         | App {op= Eq | Dq | Xor} -> ()
          | _ -> (
            match e with
            | App {op= App {op= App {op= Conditional}}} -> ()