From 6c03d88cf723ae120ee1cf50b1161b24d1ce0085 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 16 Apr 2020 03:38:34 -0700 Subject: [PATCH] [sledge] Move Term.agg_size Reviewed By: jvillard Differential Revision: D20863530 fbshipit-source-id: 8d0e0f938 --- sledge/lib/term.ml | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml index 00f41fe6a..6b3988344 100644 --- a/sledge/lib/term.ml +++ b/sledge/lib/term.ml @@ -595,17 +595,6 @@ let simp_cond cnd thn els = | Integer {data} when Z.is_false data -> els | _ -> Ap3 (Conditional, cnd, thn, els) -(* aggregate sizes *) - -let rec agg_size_exn = function - | Ap2 (Memory, n, _) | Ap3 (Extract, _, _, n) -> n - | ApN (Concat, a0U) -> - IArray.fold a0U ~init:zero ~f:(fun a0I aJ -> - simp_add2 a0I (agg_size_exn aJ) ) - | _ -> invalid_arg "agg_size_exn" - -let agg_size e = try Some (agg_size_exn e) with Invalid_argument _ -> None - (* boolean / bitwise *) let rec is_boolean = function @@ -651,6 +640,17 @@ let rec simp_or x y = | _ when equal x y -> x | _ -> Ap2 (Or, x, y) +(* aggregate sizes *) + +let rec agg_size_exn = function + | Ap2 (Memory, n, _) | Ap3 (Extract, _, _, n) -> n + | ApN (Concat, a0U) -> + IArray.fold a0U ~init:zero ~f:(fun a0I aJ -> + simp_add2 a0I (agg_size_exn aJ) ) + | _ -> invalid_arg "agg_size_exn" + +let agg_size e = try Some (agg_size_exn e) with Invalid_argument _ -> None + (* memory *) let empty_agg = ApN (Concat, IArray.of_array [||])