From c31e7f2ee719b0f7ddf41290353cab4f66b002e5 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 13 Nov 2020 07:32:38 -0800
Subject: [PATCH] [sledge] Treat Splat as interpreted

Summary:
In practice this has not been observed to matter so far, since
treating `Splat N` as interpreted or uninterpreted does not matter
when `N` is a literal constant, and code seen so far only uses `Splat`
for zero initializers or memset with literal constant bytes.

Reviewed By: jvillard

Differential Revision: D24934118

fbshipit-source-id: 213e9724e
---
 sledge/src/fol/context.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml
index 02a70f0e4..afd5d824d 100644
--- a/sledge/src/fol/context.ml
+++ b/sledge/src/fol/context.ml
@@ -22,9 +22,9 @@ let rec classify e =
     | Const _ -> Atomic
     | Interpreted -> Interpreted
     | Uninterpreted -> Uninterpreted )
-  | Sized _ | Extract _ | Concat _ -> Interpreted
+  | Splat _ | Sized _ | Extract _ | Concat _ -> Interpreted
   | Var _ | Z _ | Q _ -> Atomic
-  | Splat _ | Apply _ -> Uninterpreted
+  | Apply _ -> Uninterpreted
 
 let interpreted e = equal_kind (classify e) Interpreted
 let non_interpreted e = not (interpreted e)
@@ -348,6 +348,11 @@ and solve_ ?f d e s =
       | None -> Some s
       | Some m -> solve_ ?f n m s )
       >>= solve_ ?f a b
+  (*
+   * Splat
+   *)
+  (* a^ = b^ ==> a = b *)
+  | Some (Splat a, Splat b) -> s |> solve_ ?f a b
   (*
    * Arithmetic
    *)