From 65f8a61913d8769281023c66121f781925c6d67b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 21 Aug 2022 13:52:33 -0400 Subject: [PATCH] feat(pure-sat): correct timing printing --- src/main/pure_sat_solver.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/main/pure_sat_solver.ml b/src/main/pure_sat_solver.ml index a0f96058..4eff561b 100644 --- a/src/main/pure_sat_solver.ml +++ b/src/main/pure_sat_solver.ml @@ -231,6 +231,8 @@ end !ok *) +let start = Sys.time () + let solve ?(check = false) ?in_memory_proof (solver : SAT.t) : (unit, string) result = let res = Profile.with_ "solve" (fun () -> SAT.solve solver) in @@ -239,18 +241,18 @@ let solve ?(check = false) ?in_memory_proof (solver : SAT.t) : flush stdout; (match res with | SAT.Sat _ -> - let t3 = Sys.time () -. t2 in - Format.printf "Sat (%.3f/%.3f)@." t2 t3 + let t3 = Sys.time () in + Format.printf "Sat (%.3f/%.3f)@." (t2 -. start) (t3 -. t2) | SAT.Unsat _ -> if check then ( match in_memory_proof with | None -> Error.errorf "Cannot validate proof, no in-memory proof provided" - | Some proof -> + | Some _proof -> let ok = true (* FIXME check_proof proof *) in if not ok then Error.errorf "Proof validation failed" ); - let t3 = Sys.time () -. t2 in - Format.printf "Unsat (%.3f/%.3f)@." t2 t3); + let t3 = Sys.time () in + Format.printf "Unsat (%.3f/%.3f)@." (t2 -. start) (t3 -. t2)); Ok ()