[sledge] Add replay debugging for Equality

Summary:
This diff adds wrappers for Equality entry points that augment
exceptions escaping out of Equality with an sexp that can be given
back to Equality.replay in order to reexecute the function call that
failed.

A (bogus) example could be raising:
```
((Failure "domains intersect: ((u8) %x_5)")
 (And_eq () (Ap1 (Unsigned (bits 8)) (Var (id 5) (name x)))
   (Var (id 6) (name y))
   ((xs ()) (sat true)
     (rep (((Var (id 6) (name y)) (Var (id 5) (name x))))))))
```
and then calling `Equality.replay {|(And_eq ...)|}`.

Reviewed By: jvillard

Differential Revision: D20583753

fbshipit-source-id: 80d855950

sledge/lib/equality.ml

@@ -1015,3 +1015,51 @@ let solve_for_vars vss r =
               then Stop true
               else Continue us_xs )
             ~finish:(fun _ -> false) ) )]
+
+(* Replay debugging *)
+
+type call =
+  | And_eq of Var.Set.t * Term.t * Term.t * t
+  | And_term of Var.Set.t * Term.t * t
+  | And_ of Var.Set.t * t * t
+  | Or_ of Var.Set.t * t * t
+  | OrN of Var.Set.t * t list
+  | Rename of t * Var.Subst.t
+  | Apply_subst of Var.Set.t * Subst.t * t
+  | Solve_for_vars of Var.Set.t list * t
+[@@deriving sexp]
+
+let replay c =
+  match call_of_sexp (Sexp.of_string c) with
+  | And_eq (us, a, b, r) -> and_eq us a b r |> ignore
+  | And_term (us, e, r) -> and_term us e r |> ignore
+  | And_ (us, r, s) -> and_ us r s |> ignore
+  | Or_ (us, r, s) -> or_ us r s |> ignore
+  | OrN (us, rs) -> orN us rs |> ignore
+  | Rename (r, s) -> rename r s |> ignore
+  | Apply_subst (us, s, r) -> apply_subst us s r |> ignore
+  | Solve_for_vars (vss, r) -> solve_for_vars vss r |> ignore
+
+(* Debug wrappers *)
+
+let wrap f call =
+  if not [%debug] then f ()
+  else
+    try f () with exn -> raise_s ([%sexp_of: exn * call] (exn, call ()))
+
+let and_eq us a b r =
+  wrap (fun () -> and_eq us a b r) (fun () -> And_eq (us, a, b, r))
+
+let and_term us e r =
+  wrap (fun () -> and_term us e r) (fun () -> And_term (us, e, r))
+
+let and_ us r s = wrap (fun () -> and_ us r s) (fun () -> And_ (us, r, s))
+let or_ us r s = wrap (fun () -> or_ us r s) (fun () -> Or_ (us, r, s))
+let orN us rs = wrap (fun () -> orN us rs) (fun () -> OrN (us, rs))
+let rename r s = wrap (fun () -> rename r s) (fun () -> Rename (r, s))
+
+let apply_subst us s r =
+  wrap (fun () -> apply_subst us s r) (fun () -> Apply_subst (us, s, r))
+
+let solve_for_vars vss r =
+  wrap (fun () -> solve_for_vars vss r) (fun () -> Solve_for_vars (vss, r))

sledge/lib/equality.mli

@@ -96,3 +96,7 @@ val solve_for_vars : Var.Set.t list -> t -> Subst.t
     with free variables contained in (the union of) a prefix [uss] of [vss]
     to terms [e] with free variables contained in as short a prefix of [uss]
     as possible. *)
+
+(* Replay debugging *)
+
+val replay : string -> unit

sledge/lib/equality_test.ml

@@ -5,8 +5,6 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-(* [@@@warning "-32"] *)
-
 let%test_module _ =
   ( module struct
     open Equality
@@ -16,7 +14,9 @@ let%test_module _ =
     (* let () =
      *   Trace.init ~margin:160
      *     ~config:(Result.ok_exn (Trace.parse "+Equality"))
-     *     () *)
+     *     ()
+     * 
+     * [@@@warning "-32"] *)
 
     let printf pp = Format.printf "@\n%a@." pp
     let pp = printf pp
@@ -410,4 +410,10 @@ let%test_module _ =
         {| {sat= true; rep= [[%x_5 ↦ 0]; [%y_6 ↦ 0]; [%z_7 ↦ 0]]} |}]
 
     let%test _ = entails_eq r19 z !0
+
+    let%expect_test _ =
+      Equality.replay
+        {|(Solve_for_vars (() () ((Var (id 8) (name m)) (Var (id 9) (name n))))
+           ((xs ()) (sat true) (rep (((Var (id 9) (name n)) (Var (id 8) (name m)))))))|} ;
+      [%expect {||}]
   end )