From 7bb1ec073aa73724328630fa0033b8934ee4a303 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 27 Jan 2020 08:19:45 -0800
Subject: [PATCH] [sledge] Strengthen Term.invariant on aggregates

Summary:
Aggregate args of Extract and Concat must be aggregate terms, in
particular, not variables. This maintains the property that the size
of any aggregate can be computed.

Reviewed By: ngorogiannis

Differential Revision: D19286625

fbshipit-source-id: 1af1e4183
---
 sledge/src/llair/term.ml | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml
index 3f3874328..294c8a3ca 100644
--- a/sledge/src/llair/term.ml
+++ b/sledge/src/llair/term.ml
@@ -280,13 +280,24 @@ let assert_polynomial poly =
       Qset.iter args ~f:(fun m c -> assert_poly_term m c |> Fn.id)
   | _ -> assert false
 
+(* aggregate args of Extract and Concat must be aggregate terms, in
+   particular, not variables *)
+let rec assert_aggregate = function
+  | Ap2 (Memory, _, _) -> ()
+  | Ap3 (Extract, a, _, _) -> assert_aggregate a
+  | ApN (Concat, a0N) ->
+      assert (Vector.length a0N <> 1) ;
+      Vector.iter ~f:assert_aggregate a0N
+  | _ -> assert false
+
 let invariant e =
   Invariant.invariant [%here] e [%sexp_of: t]
   @@ fun () ->
   match e with
   | Add _ -> assert_polynomial e |> Fn.id
   | Mul _ -> assert_monomial e |> Fn.id
-  | ApN (Concat, mems) -> assert (Vector.length mems <> 1)
+  | Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _) ->
+      assert_aggregate e
   | ApN (Record, elts) | RecN (Record, elts) ->
       assert (not (Vector.is_empty elts))
   | Ap1 (Convert {src= Integer _; dst= Integer _}, _) -> assert false