From a8feaa42621a8bc98a31aeb61301ea085987a7db Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 12 Nov 2020 16:39:08 -0800
Subject: [PATCH] [sledge] Add missing case to sequence theory solver
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Summary: Solving equations such as `eⁿ = a⌢b` was missing.

Reviewed By: jvillard

Differential Revision: D24920761

fbshipit-source-id: 09ba30c8c
---
 sledge/src/fol/context.ml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml
index 44d99c6ec..ae8fe5a93 100644
--- a/sledge/src/fol/context.ml
+++ b/sledge/src/fol/context.ml
@@ -305,6 +305,9 @@ and solve_ ?f d e s =
   (* ⟨n,a⟩ = ⟨m,b⟩ ==> n = m ∧ a = β *)
   | Some (Sized {siz= n; seq= a}, Sized {siz= m; seq= b}) ->
       s |> solve_ ?f n m >>= solve_ ?f a b
+  (* ⟨n,e^⟩ = α₀^…^αᵥ ==> *)
+  | Some ((Sized {siz= n; seq= Splat _} as b), Concat a0V) ->
+      solve_concat ?f a0V b n s
   (* ⟨n,a⟩ = β ==> n = |β| ∧ a = β *)
   | Some (Sized {siz= n; seq= a}, b) ->
       ( match Trm.seq_size b with