feat: progress bar in solver

src/core/Sidekick_core.ml

@@ -626,6 +626,7 @@ module type SOLVER = sig
   val solve :
     ?on_exit:(unit -> unit) list ->
     ?check:bool ->
+    ?on_progress:(t -> unit) ->
     assumptions:Atom.t list ->
     t ->
     res

src/msat-solver/Sidekick_msat_solver.ml

@@ -148,6 +148,7 @@ module Make(A : ARG)
       count_preprocess_clause: int Stat.counter;
       count_conflict: int Stat.counter;
       count_propagate: int Stat.counter;
+      mutable on_progress: unit -> unit;
       simp: Simplify.t;
       mutable preprocess: preprocess_hook list;
       preprocess_cache: T.t T.Tbl.t;
@@ -309,8 +310,8 @@ module Make(A : ARG)
     (* propagation from the bool solver *)
     let check_ ~final (self:t) (acts: msat_acts) =
       let iter = iter_atoms_ acts in
-      (* TODO if Config.progress then print_progress(); *)
       Msat.Log.debugf 5 (fun k->k "(msat-solver.assume :len %d)" (Iter.length iter));
+      self.on_progress();
       assert_lits_ ~final self acts iter
 
     (* propagation from the bool solver *)
@@ -342,6 +343,7 @@ module Make(A : ARG)
         th_states=Ths_nil;
         stat;
         simp=Simplify.create tst;
+        on_progress=(fun () -> ());
         preprocess=[];
         preprocess_cache=T.Tbl.create 32;
         count_axiom = Stat.mk_int stat "solver.th-axioms";
@@ -557,10 +559,12 @@ module Make(A : ARG)
     *)
     ()
 
-  let solve ?(on_exit=[]) ?(check=true) ~assumptions (self:t) : res =
+  let solve ?(on_exit=[]) ?(check=true) ?(on_progress=fun _ -> ())
+      ~assumptions (self:t) : res =
     let do_on_exit () =
       List.iter (fun f->f()) on_exit;
     in
+    self.si.on_progress <- (fun () -> on_progress self);
     let r = Sat_solver.solve ~assumptions (solver self) in
     Stat.incr self.count_solve;
     match r with

src/smtlib/Process.ml

@@ -500,6 +500,21 @@ 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 start = Sys.time() in
+  let n = ref 0 in
+  let syms = "|\\-/" in
+  fun _s ->
+    let diff = Sys.time() -. start in
+    incr n;
+    (* 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;
+      n := 0;
+      flush stdout
+    )
+
 (* call the solver to check-sat *)
 let solve
     ?gc:_
@@ -507,16 +522,19 @@ let solve
     ?dot_proof
     ?(pp_model=false)
     ?(check=false)
-    ?time:_ ?memory:_ ?progress:_
+    ?time:_ ?memory:_ ?(progress=false)
     ?hyps:_
     ~assumptions
     s : unit =
   let t1 = Sys.time() in
+  let on_progress =
+    if progress then Some (mk_progress()) else None in
   let res =
-    Solver.solve ~assumptions s
+    Solver.solve ~assumptions ?on_progress s
     (* ?gc ?restarts ?time ?memory ?progress *)
   in
   let t2 = Sys.time () in
+  Printf.printf "\r"; flush stdout;
   begin match res with
     | Solver.Sat m ->
       if pp_model then (