From 57ff90a11e51723e5473d8de9f55373999706819 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 9 Apr 2021 08:14:07 -0700
Subject: [PATCH] [sledge] Fix construction of equalities between Concat

Summary:
The computation of common prefixes and suffixes was wrong. In
particular, the computation of the common suffix did not correctly
consider the common prefix. This manifested in case one entire
sequence is a suffix of the other.

Reviewed By: ngorogiannis

Differential Revision: D27564874

fbshipit-source-id: 267a75102
---
 sledge/src/fol/fml.ml | 41 +++++++++++++++++++++++++----------------
 1 file changed, 25 insertions(+), 16 deletions(-)

diff --git a/sledge/src/fol/fml.ml b/sledge/src/fol/fml.ml
index 960024390..76c9b8c6e 100644
--- a/sledge/src/fol/fml.ml
+++ b/sledge/src/fol/fml.ml
@@ -102,30 +102,39 @@ let _Eq x y =
         _Eq0 (Trm.sub x y)
     (* α^β^δ = α^γ^δ ==> β = γ *)
     | Concat a, Concat b ->
-        let m = Array.length a in
-        let n = Array.length b in
-        let l = min m n in
+        let length_a = Array.length a in
+        let length_b = Array.length b in
+        let min_length = min length_a length_b in
         let length_common_prefix =
           let rec find_lcp i =
-            if i < l && Trm.equal a.(i) b.(i) then find_lcp (i + 1) else i
+            if i < min_length && Trm.equal a.(i) b.(i) then find_lcp (i + 1)
+            else i
           in
           find_lcp 0
         in
-        if length_common_prefix = l then tt
-        else
-          let length_common_suffix =
-            let rec find_lcs i =
-              if Trm.equal a.(m - 1 - i) b.(n - 1 - i) then find_lcs (i + 1)
-              else i
-            in
-            find_lcs 0
+        let min_length_without_common_prefix =
+          min_length - length_common_prefix
+        in
+        let length_common_suffix =
+          let rec find_lcs i =
+            if
+              i < min_length_without_common_prefix
+              && Trm.equal a.(length_a - 1 - i) b.(length_b - 1 - i)
+            then find_lcs (i + 1)
+            else i
           in
-          let length_common = length_common_prefix + length_common_suffix in
-          if length_common = 0 then sort_eq x y
+          find_lcs 0
+        in
+        let length_common = length_common_prefix + length_common_suffix in
+        if length_common = 0 then sort_eq x y
+        else
+          let len_a = length_a - length_common in
+          let len_b = length_b - length_common in
+          if len_a = 0 && len_b = 0 then tt
           else
             let pos = length_common_prefix in
-            let a = Array.sub ~pos ~len:(m - length_common) a in
-            let b = Array.sub ~pos ~len:(n - length_common) b in
+            let a = Array.sub ~pos ~len:len_a a in
+            let b = Array.sub ~pos ~len:len_b b in
             _Eq (Trm.concat a) (Trm.concat b)
     | (Sized _ | Extract _ | Concat _), (Sized _ | Extract _ | Concat _) ->
         sort_eq x y