pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[sledge] Refactor: Move Equality replay debugging to Fol

Browse Source 
Reviewed By: ngorogiannis

Differential Revision: D22170524

fbshipit-source-id: 9f1b8fcdd
master
Josh Berdine 5 years ago committed by Facebook GitHub Bot
parent 0568f2ee2d
commit 9cb74ac9ac
5 changed files with 84 additions and 104 deletions
Show Stats Download Patch File Download Diff File

80
sledge/src/fol.ml
Unescape View File

@ -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

4
sledge/src/fol.mli
Unescape View File

@ -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

93
sledge/src/ses/equality.ml
Unescape View File

@ -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))

4
sledge/src/ses/equality.mli
Unescape View File

@ -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

7
sledge/src/ses/equality_test.ml
Unescape View File

@ -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 )

Write Preview
Loading…
Cancel
Save