diff options
| author | Alasdair | 2019-02-15 03:04:37 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-02-15 17:52:36 +0000 |
| commit | 65599f14b3ecac193529caafbee7672b38ed367e (patch) | |
| tree | e64a51bdbecead9fb57e06d94203dbfedca9b1d9 /src/profile.ml | |
| parent | 96f0df85a129666e3b960d6d17df165de13b3024 (diff) | |
Use multiple solvers
Useful to see what constraints we are generating that are particularly
hard, and which of our specs work with different solvers.
Refactor code to use smt in names rather than specifically z3
Diffstat (limited to 'src/profile.ml')
| -rw-r--r-- | src/profile.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/profile.ml b/src/profile.ml index 1a8bd30b..f64bdfe0 100644 --- a/src/profile.ml +++ b/src/profile.ml @@ -51,13 +51,13 @@ let opt_profile = ref false type profile = { - z3_calls : int; - z3_time : float + smt_calls : int; + smt_time : float } let new_profile = { - z3_calls = 0; - z3_time = 0.0 + smt_calls = 0; + smt_time = 0.0 } let profile_stack = ref [] @@ -68,12 +68,12 @@ let update_profile f = | (p :: ps) -> profile_stack := f p :: ps -let start_z3 () = - update_profile (fun p -> { p with z3_calls = p.z3_calls + 1 }); +let start_smt () = + update_profile (fun p -> { p with smt_calls = p.smt_calls + 1 }); Sys.time () -let finish_z3 t = - update_profile (fun p -> { p with z3_time = p.z3_time +. (Sys.time () -. t) }) +let finish_smt t = + update_profile (fun p -> { p with smt_time = p.smt_time +. (Sys.time () -. t) }) let start () = profile_stack := new_profile :: !profile_stack; @@ -84,7 +84,7 @@ let finish msg t = begin match !profile_stack with | p :: ps -> prerr_endline (Printf.sprintf "%s %s: %fs" Util.("Profiled" |> magenta |> clear) msg (Sys.time () -. t)); - prerr_endline (Printf.sprintf " Z3 calls: %d, Z3 time: %fs" p.z3_calls p.z3_time); + prerr_endline (Printf.sprintf " SMT calls: %d, SMT time: %fs" p.smt_calls p.smt_time); profile_stack := ps | [] -> () end |