simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 12:24:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

wip: better progress bar

Browse source
This commit is contained in:
Simon Cruanes 2020-10-11 23:30:22 -04:00
parent f556fe58ab
commit 534fc45783
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/smtlib/Process.ml
View file

@ -123,17 +123,20 @@ let check_smt_model (solver:Solver.Sat_solver.t) (hyps:_ Vec.t) (m:Model.t) : un
Vec.iter check_c hyps Vec.iter check_c hyps
*) *)
let mk_progress () : _ -> unit = let mk_progress (_s:Solver.t) : _ -> unit =
let start = Sys.time() in let start = Sys.time() in
let n = ref 0 in let n = ref 0 in
let syms = "|\\-/" in let syms = "|\\-/" in
fun _s -> fun _s ->
let diff = Sys.time() -. start in let diff = Sys.time() -. start in
incr n; incr n;
(* TODO: print some core stats in the progress bar
let n_cl = Solver.pp_stats
*)
(* limit frequency *) (* limit frequency *)
if float !n > 6. *. diff then ( if float !n > 6. *. diff then (
let sym = String.get syms (!n mod String.length syms) in let sym = String.get syms (!n mod String.length syms) in
Printf.printf "\r [%.2fs %c]" diff sym; Printf.printf "\r[%.2fs %c]" diff sym;
n := 0; n := 0;
flush stdout flush stdout
) )
@ -151,7 +154,7 @@ let solve
s : unit = s : unit =
let t1 = Sys.time() in let t1 = Sys.time() in
let on_progress = let on_progress =
if progress then Some (mk_progress()) else None in if progress then Some (mk_progress s) else None in
let res = let res =
Solver.solve ~assumptions ?on_progress s Solver.solve ~assumptions ?on_progress s
(* ?gc ?restarts ?time ?memory ?progress *) (* ?gc ?restarts ?time ?memory ?progress *)