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

more stats for main

Browse source
This commit is contained in:
Simon Cruanes 2021-07-21 20:24:27 -04:00
parent 77c61b536e
commit a174e5958a
2 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/main/main.ml
View file

@ -152,9 +152,10 @@ let main_cnf () : _ result =
S.Dimacs.parse_file solver !file >>= fun () ->
let r = S.solve solver in
if !p_stat then (
Fmt.printf "; n-conflicts: %d n-decisions: %d n-propagations: %d n-atoms: %d@."
Fmt.printf "; n-conflicts: %d n-decisions: %d n-propagations: %d@. \
; n-restarts: %d n-atoms: %d@."
(S.SAT.n_conflicts solver) (S.SAT.n_decisions solver)
(S.SAT.n_propagations solver) !n_atoms;
(S.SAT.n_propagations solver) (S.SAT.n_restarts solver) !n_atoms;
);
r

3
src/sat/Solver_intf.ml
View file

@ -379,6 +379,8 @@ module type S = sig
?on_conflict:(atom array -> unit) ->
?on_decision:(atom -> unit) ->
?on_new_atom:(atom -> unit) ->
?on_learnt:(atom array -> unit) ->
?on_gc:(atom array -> unit) ->
?store_proof:bool ->
?size:[`Tiny|`Small|`Big] ->
theory ->
@ -444,5 +446,6 @@ module type S = sig
val n_propagations : t -> int
val n_decisions : t -> int
val n_conflicts : t -> int
val n_restarts : t -> int
end