[sledge] Minor exception optimizations

Summary:
When exceptions are used due to the lack of goto, use `raise_notrace`
instead of `raise` to avoid the overhead of populating the backtrace.

Reviewed By: ngorogiannis

Differential Revision: D24630525

fbshipit-source-id: c5051d9c4

sledge/nonstdlib/map.ml

@@ -76,13 +76,15 @@ end) : S with type key = Key.t = struct
   let is_empty = M.is_empty
 
   let root_key m =
+    if M.is_empty m then None
+    else
       let exception Found in
       let found = ref None in
       try
         M.find_first
           (fun key ->
             found := Some key ;
-          raise Found )
+            raise_notrace Found )
           m
         |> ignore ;
         None
@@ -97,7 +99,7 @@ end) : S with type key = Key.t = struct
       M.for_all
         (fun key data ->
           found := Some (key, data) ;
-          raise Found )
+          raise_notrace Found )
         m
       |> ignore ;
       None

sledge/nonstdlib/set.ml

@@ -53,7 +53,7 @@ end) : S with type elt = Elt.t = struct
       S.for_all
         (fun elt ->
           found := Some elt ;
-          raise Found )
+          raise_notrace Found )
         s
       |> ignore ;
       None

sledge/src/fol/trm.ml

@@ -182,7 +182,7 @@ end = struct
             String.init (Array.length elts) ~f:(fun i ->
                 match elts.(i) with
                 | Z c -> Char.of_int_exn (Z.to_int c)
-                | _ -> raise Not_a_string )
+                | _ -> raise_notrace Not_a_string )
           with
           | s -> Format.fprintf fs "%S" s
           | exception (Not_a_string | Z.Overflow | Failure _) ->

sledge/src/llair/exp.ml

@@ -154,7 +154,7 @@ and pp_record fs elts =
           String.init (IArray.length elts) ~f:(fun i ->
               match IArray.get elts i with
               | Integer {data} -> Char.of_int_exn (Z.to_int data)
-              | _ -> raise (Invalid_argument "not a string") )
+              | _ -> raise_notrace (Invalid_argument "not a string") )
         with
         | s -> Format.fprintf fs "@[<h>%s@]" (String.escaped s)
         | exception _ ->