From 13aa772b6820fdc00f84efe14369898ee2fd29b7 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 2 Mar 2020 08:43:06 -0800
Subject: [PATCH] [sledge] Strengthen normalization of equality between Concats

Summary: When equating Concat terms, drop any common prefix or suffix.

Reviewed By: ngorogiannis

Differential Revision: D20120264

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

diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml
index 563e7fbe2..5273319e6 100644
--- a/sledge/src/llair/term.ml
+++ b/sledge/src/llair/term.ml
@@ -838,6 +838,32 @@ let rec simp_eq x y =
     (* e = (c ? t : f) ==> (c ? e = t : e = f) *)
     | e, Ap3 (Conditional, c, t, f) | Ap3 (Conditional, c, t, f), e ->
         simp_cond c (simp_eq e t) (simp_eq e f)
+    (* α^β^δ = α^γ^δ ==> β = γ *)
+    | ApN (Concat, a), ApN (Concat, b) ->
+        let m = Vector.length a in
+        let n = Vector.length b in
+        let length_common_prefix =
+          let rec find_lcp i =
+            if equal (Vector.get a i) (Vector.get b i) then find_lcp (i + 1)
+            else i
+          in
+          find_lcp 0
+        in
+        let length_common_suffix =
+          let rec find_lcs i =
+            if equal (Vector.get a (m - 1 - i)) (Vector.get b (n - 1 - i))
+            then find_lcs (i + 1)
+            else i
+          in
+          find_lcs 0
+        in
+        let length_common = length_common_prefix + length_common_suffix in
+        if length_common = 0 then Ap2 (Eq, x, y)
+        else
+          let pos = length_common_prefix in
+          let a = Vector.sub ~pos ~len:(m - length_common) a in
+          let b = Vector.sub ~pos ~len:(n - length_common) b in
+          simp_eq (simp_concat a) (simp_concat b)
     | ( (Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _))
       , (Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _)) ) ->
         Ap2 (Eq, x, y)