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

improve progress bar and printingof stat after timeout

Browse source
This commit is contained in:
Simon Cruanes 2022-02-17 18:27:20 -05:00
parent 20791a551f
commit 52cae96ee2
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 34 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
src/main/main.ml
View file

@ -33,6 +33,8 @@ let proof_file = ref ""
let proof_store_memory = ref false
let proof_store_file = ref ""
let reset_line = "\x1b[2K\r"
(* Arguments parsing *)
let int_arg r arg =
let l = String.length arg in
@ -149,6 +151,13 @@ let main_smt () : _ result =
Process.Solver.create ~proof ~theories tst () ()
in
let finally() =
if !p_stat then (
Format.printf "%s%a@." reset_line Solver.pp_stats solver;
);
in
CCFun.protect ~finally @@ fun () ->
(* FIXME: emit an actual proof *)
let proof_file = if !proof_file ="" then None else Some !proof_file in
if !check then (
@ -174,9 +183,6 @@ let main_smt () : _ result =
with Exit ->
E.return()
in
if !p_stat then (
Format.printf "%a@." Solver.pp_stats solver;
);
res
let main_cnf () : _ result =
@ -195,18 +201,21 @@ let main_cnf () : _ result =
in
let stat = Stat.create () in
let finally() =
if !p_stat then (
Fmt.printf "%a@." Stat.pp_all (Stat.all stat);
);
Proof.close proof;
in
CCFun.protect ~finally @@ fun () ->
let solver = S.SAT.create ~size:`Big ~proof ~stat () in
S.Dimacs.parse_file solver !file >>= fun () ->
let r = S.solve ~check:!check ?in_memory_proof solver in
(* FIXME: if in memory proof and !proof_file<>"",
then dump proof into file now *)
Proof.close proof;
if !p_stat then (
Fmt.printf "%a@." Stat.pp_all (Stat.all stat);
);
r
let main () =
@ -225,6 +234,14 @@ let main () =
let al = Gc.create_alarm check_limits in
Util.setup_gc();
let is_cnf = Filename.check_suffix !file ".cnf" in
let finally() =
if !p_gc_stat then (
Printf.printf "(gc_stats\n%t)\n" Gc.print_stat;
)
in
CCFun.protect ~finally @@ fun () ->
let res =
if is_cnf then (
main_cnf ()
@ -232,9 +249,6 @@ let main () =
main_smt ()
)
in
if !p_gc_stat then (
Printf.printf "(gc_stats\n%t)\n" Gc.print_stat;
);
Gc.delete_alarm al;
res

10
src/smtlib/Process.ml
View file

@ -111,6 +111,8 @@ let check_smt_model (solver:Solver.Sat_solver.t) (hyps:_ Vec.t) (m:Model.t) : un
Vec.iter check_c hyps
*)
let reset_line = "\x1b[2K\r"
let mk_progress (_s:Solver.t) : _ -> unit =
let start = Sys.time() in
let n = ref 0 in
@ -124,7 +126,7 @@ let mk_progress (_s:Solver.t) : _ -> unit =
(* limit frequency *)
if float !n > 6. *. diff then (
let sym = String.get syms (!n mod String.length syms) in
Printf.printf "\r[%.2fs %c]" diff sym;
Printf.printf "%s[%.2fs %c]" reset_line diff sym;
n := 0;
flush stdout
)
@ -219,7 +221,11 @@ let solve
Format.printf "Unsat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
| Solver.Unknown reas ->
Format.printf "Unknown (:reason %a)" Solver.Unknown.pp reas
Format.printf "Unknown (:reason %a)@." Solver.Unknown.pp reas
| exception exn ->
Printf.printf "%s%!" reset_line;
raise exn
end;
res