From 534fc45783613700bc8b44b2c46b49a0ed0fd45e Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sun, 11 Oct 2020 23:30:22 -0400
Subject: [PATCH] wip: better progress bar

---
 src/smtlib/Process.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml
index 3ae64420..f8e049d9 100644
--- a/src/smtlib/Process.ml
+++ b/src/smtlib/Process.ml
@@ -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
    *)
 
-let mk_progress () : _ -> unit =
+let mk_progress (_s:Solver.t) : _ -> unit =
   let start = Sys.time() in
   let n = ref 0 in
   let syms = "|\\-/" in
   fun _s ->
     let diff = Sys.time() -. start in
     incr n;
+    (* TODO: print some core stats in the progress bar
+    let n_cl = Solver.pp_stats
+       *)
     (* 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 "\r[%.2fs %c]" diff sym;
       n := 0;
       flush stdout
     )
@@ -151,7 +154,7 @@ let solve
     s : unit =
   let t1 = Sys.time() in
   let on_progress =
-    if progress then Some (mk_progress()) else None in
+    if progress then Some (mk_progress s) else None in
   let res =
     Solver.solve ~assumptions ?on_progress s
     (* ?gc ?restarts ?time ?memory ?progress *)