From 9cb74ac9ac1eb8062e59482d2d1f8ae454236698 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 9 Jul 2020 07:43:57 -0700 Subject: [PATCH] [sledge] Refactor: Move Equality replay debugging to Fol Reviewed By: ngorogiannis Differential Revision: D22170524 fbshipit-source-id: 9f1b8fcdd --- sledge/src/fol.ml | 80 ++++++++++++++++++++++++++++ sledge/src/fol.mli | 4 ++ sledge/src/ses/equality.ml | 93 --------------------------------- sledge/src/ses/equality.mli | 4 -- sledge/src/ses/equality_test.ml | 7 --- 5 files changed, 84 insertions(+), 104 deletions(-) diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml index 679f90de3..2e2d05f1d 100644 --- a/sledge/src/fol.ml +++ b/sledge/src/fol.ml @@ -35,4 +35,84 @@ module Context = struct let substf = subst end + + (* Replay debugging *) + + type call = + | Normalize of t * Term.t + | And_formula of Var.Set.t * Formula.t * t + | And_ 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 + | Normalize (r, e) -> normalize r e |> ignore + | And_formula (us, e, r) -> and_formula us e r |> ignore + | And_ (us, r, s) -> and_ 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 report ~name ~elapsed ~aggregate ~count = + Format.eprintf "%15s time: %12.3f ms %12.3f ms %12d calls@." name + elapsed aggregate count + + let dump_threshold = ref 1000. + + let wrap tmr f call = + let f () = + Timer.start tmr ; + let r = f () in + Timer.stop_report tmr (fun ~name ~elapsed ~aggregate ~count -> + report ~name ~elapsed ~aggregate ~count ; + if Float.(elapsed > !dump_threshold) then ( + dump_threshold := 2. *. !dump_threshold ; + Format.eprintf "@\n%a@\n@." Sexp.pp_hum (sexp_of_call (call ())) + ) ) ; + r + in + if not [%debug] then f () + else + try f () with exn -> raise_s ([%sexp_of: exn * call] (exn, call ())) + + let normalize_tmr = Timer.create "normalize" ~at_exit:report + let and_formula_tmr = Timer.create "and_formula" ~at_exit:report + let and_tmr = Timer.create "and_" ~at_exit:report + let orN_tmr = Timer.create "orN" ~at_exit:report + let rename_tmr = Timer.create "rename" ~at_exit:report + let apply_subst_tmr = Timer.create "apply_subst" ~at_exit:report + let solve_for_vars_tmr = Timer.create "solve_for_vars" ~at_exit:report + + let normalize r e = + wrap normalize_tmr (fun () -> normalize r e) (fun () -> Normalize (r, e)) + + let and_formula us e r = + wrap and_formula_tmr + (fun () -> and_formula us e r) + (fun () -> And_formula (us, e, r)) + + let and_ us r s = + wrap and_tmr (fun () -> and_ us r s) (fun () -> And_ (us, r, s)) + + let orN us rs = wrap orN_tmr (fun () -> orN us rs) (fun () -> OrN (us, rs)) + + let rename r s = + wrap rename_tmr (fun () -> rename r s) (fun () -> Rename (r, s)) + + let apply_subst us s r = + wrap apply_subst_tmr + (fun () -> apply_subst us s r) + (fun () -> Apply_subst (us, s, r)) + + let solve_for_vars vss r = + wrap solve_for_vars_tmr + (fun () -> solve_for_vars vss r) + (fun () -> Solve_for_vars (vss, r)) end diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli index 1d61add91..7717acbdc 100644 --- a/sledge/src/fol.mli +++ b/sledge/src/fol.mli @@ -261,4 +261,8 @@ module Context : sig val elim : Var.Set.t -> t -> t (** Weaken relation by removing oriented equations [k ↦ _] for [k] in [ks]. *) + + (* Replay debugging *) + + val replay : string -> unit end diff --git a/sledge/src/ses/equality.ml b/sledge/src/ses/equality.ml index 9f37c877f..d47cfe2a1 100644 --- a/sledge/src/ses/equality.ml +++ b/sledge/src/ses/equality.ml @@ -1068,96 +1068,3 @@ let solve_for_vars vss r = ~finish:(fun _ -> false) ) )] let elim xs r = {r with rep= Subst.remove xs r.rep} - -(* Replay debugging *) - -type call = - | Normalize of t * Term.t - | 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 - | Normalize (r, e) -> normalize r e |> ignore - | 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 report ~name ~elapsed ~aggregate ~count = - Format.eprintf "%15s time: %12.3f ms %12.3f ms %12d calls@." name - elapsed aggregate count - -let dump_threshold = ref 1000. - -let wrap tmr f call = - let f () = - Timer.start tmr ; - let r = f () in - Timer.stop_report tmr (fun ~name ~elapsed ~aggregate ~count -> - report ~name ~elapsed ~aggregate ~count ; - if Float.(elapsed > !dump_threshold) then ( - dump_threshold := 2. *. !dump_threshold ; - Format.eprintf "@\n%a@\n@." Sexp.pp_hum (sexp_of_call (call ())) ) ) ; - r - in - if not [%debug] then f () - else - try f () with exn -> raise_s ([%sexp_of: exn * call] (exn, call ())) - -let normalize_tmr = Timer.create "normalize" ~at_exit:report -let and_eq_tmr = Timer.create "and_eq" ~at_exit:report -let and_term_tmr = Timer.create "and_term" ~at_exit:report -let and_tmr = Timer.create "and_" ~at_exit:report -let or_tmr = Timer.create "or_" ~at_exit:report -let orN_tmr = Timer.create "orN" ~at_exit:report -let rename_tmr = Timer.create "rename" ~at_exit:report -let apply_subst_tmr = Timer.create "apply_subst" ~at_exit:report -let solve_for_vars_tmr = Timer.create "solve_for_vars" ~at_exit:report - -let normalize r e = - wrap normalize_tmr (fun () -> normalize r e) (fun () -> Normalize (r, e)) - -let and_eq us a b r = - wrap and_eq_tmr - (fun () -> and_eq us a b r) - (fun () -> And_eq (us, a, b, r)) - -let and_term us e r = - wrap and_term_tmr - (fun () -> and_term us e r) - (fun () -> And_term (us, e, r)) - -let and_ us r s = - wrap and_tmr (fun () -> and_ us r s) (fun () -> And_ (us, r, s)) - -let or_ us r s = - wrap or_tmr (fun () -> or_ us r s) (fun () -> Or_ (us, r, s)) - -let orN us rs = wrap orN_tmr (fun () -> orN us rs) (fun () -> OrN (us, rs)) - -let rename r s = - wrap rename_tmr (fun () -> rename r s) (fun () -> Rename (r, s)) - -let apply_subst us s r = - wrap apply_subst_tmr - (fun () -> apply_subst us s r) - (fun () -> Apply_subst (us, s, r)) - -let solve_for_vars vss r = - wrap solve_for_vars_tmr - (fun () -> solve_for_vars vss r) - (fun () -> Solve_for_vars (vss, r)) diff --git a/sledge/src/ses/equality.mli b/sledge/src/ses/equality.mli index a536606fc..16ca6415e 100644 --- a/sledge/src/ses/equality.mli +++ b/sledge/src/ses/equality.mli @@ -110,7 +110,3 @@ val solve_for_vars : Var.Set.t list -> t -> Subst.t val elim : Var.Set.t -> t -> t (** Weaken relation by removing oriented equations [k ↦ _] for [k] in [ks]. *) - -(* Replay debugging *) - -val replay : string -> unit diff --git a/sledge/src/ses/equality_test.ml b/sledge/src/ses/equality_test.ml index 65209842b..86409e1e9 100644 --- a/sledge/src/ses/equality_test.ml +++ b/sledge/src/ses/equality_test.ml @@ -498,11 +498,4 @@ let%test_module _ = rep= [[%x_5 ↦ 0]; [%y_6 ↦ 0]; [%z_7 ↦ 0]; [-1 ↦ ]; [0 ↦ ]]} |}] let%test _ = entails_eq r19 z !0 - - let%expect_test _ = - Equality.replay - {|(And_eq () (Var (id 10) (name v)) - (Mul (((Var (id 8) (name v)) 1) ((Var (id 9) (name v)) 1))) - ((xs ()) (sat true) (rep ())))|} ; - [%expect {| |}] end )