simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix: time measurements were wrong

Browse source
This commit is contained in:
Simon Cruanes 2022-08-16 21:45:16 -04:00
parent b61ec35451
commit b23a031519
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/smtlib/Process.ml
View file

@ -146,7 +146,7 @@ let with_file_out (file : string) (f : out_channel -> 'a) : 'a =
(* call the solver to check-sat *) (* call the solver to check-sat *)
let solve ?gc:_ ?restarts:_ ?proof_file ?(pp_model = false) ?(check = false) let solve ?gc:_ ?restarts:_ ?proof_file ?(pp_model = false) ?(check = false)
?time ?memory ?(progress = false) ~assumptions s : Solver.res = ?time ?memory ?(progress = false) ~assumptions s : Solver.res =
let t1 = Sys.time () -. start in let t1 = Sys.time () in
let on_progress = let on_progress =
if progress then if progress then
Some (mk_progress s) Some (mk_progress s)
@ -194,9 +194,9 @@ let solve ?gc:_ ?restarts:_ ?proof_file ?(pp_model = false) ?(check = false)
CCOpt.iter (fun h -> check_smt_model (Solver.solver s) h m) hyps; CCOpt.iter (fun h -> check_smt_model (Solver.solver s) h m) hyps;
); );
*) *)
let t3 = Sys.time () -. t2 in let t3 = Sys.time () in
Fmt.printf "sat@."; Fmt.printf "sat@.";
Fmt.printf "; (%.3f/%.3f/%.3f)@." t1 (t2 -. t1) t3 Fmt.printf "; (%.3f/%.3f/%.3f)@." (t1 -. start) (t2 -. t1) (t3 -. t2)
| Solver.Unsat { unsat_step_id; unsat_core = _ } -> | Solver.Unsat { unsat_step_id; unsat_core = _ } ->
if check then if check then
() ()
@ -227,9 +227,9 @@ let solve ?gc:_ ?restarts:_ ?proof_file ?(pp_model = false) ?(check = false)
flush oc) flush oc)
| _ -> ()); | _ -> ());
let t3 = Sys.time () -. t2 in let t3 = Sys.time () in
Fmt.printf "unsat@."; Fmt.printf "unsat@.";
Fmt.printf "; (%.3f/%.3f/%.3f)@." t1 (t2 -. t1) t3 Fmt.printf "; (%.3f/%.3f/%.3f)@." (t1 -. start) (t2 -. t1) (t3 -. t2)
| Solver.Unknown reas -> | Solver.Unknown reas ->
Fmt.printf "unknown@."; Fmt.printf "unknown@.";
Fmt.printf "; @[<h>:reason %a@]@." Solver.Unknown.pp reas Fmt.printf "; @[<h>:reason %a@]@." Solver.Unknown.pp reas