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

test program: -gc option to print GC stats

Browse source
This commit is contained in:
Simon Cruanes 2014-11-04 20:37:00 +01:00
parent 30e372d302
commit 3107fc4755
1 changed files with 22 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
util/test.ml
View file

@ -9,7 +9,6 @@ let file = ref ""
let p_assign = ref false let p_assign = ref false
let time_limit = ref 300. let time_limit = ref 300.
let size_limit = ref 1000_000_000. let size_limit = ref 1000_000_000.
;;
let int_arg r arg = let int_arg r arg =
let l = String.length arg in let l = String.length arg in
@ -32,19 +31,25 @@ let int_arg r arg =
| '0'..'9' -> r := float_of_string arg | '0'..'9' -> r := float_of_string arg
| _ -> raise (Arg.Bad "bad numeric argument") | _ -> raise (Arg.Bad "bad numeric argument")
with Failure "float_of_string" -> raise (Arg.Bad "bad numeric argument") with Failure "float_of_string" -> raise (Arg.Bad "bad numeric argument")
;;
let setup_gc_stat () =
at_exit (fun () ->
Gc.print_stat stdout;
)
let input_file = fun s -> file := s let input_file = fun s -> file := s
let usage = "Usage : main [options] <file>" let usage = "Usage : main [options] <file>"
let argspec = Arg.align [ let argspec = Arg.align [
"-v", Arg.Int (fun i -> Log.set_debug i), "-v", Arg.Int (fun i -> Log.set_debug i),
"<lvl> Sets the debug verbose level"; "<lvl> Sets the debug verbose level";
"-t", Arg.String (int_arg time_limit), "-t", Arg.String (int_arg time_limit),
"<t>[smhd] Sets the time limit for the sat solver"; "<t>[smhd] Sets the time limit for the sat solver";
"-s", Arg.String (int_arg size_limit), "-s", Arg.String (int_arg size_limit),
"<s>[kMGT] Sets the size limit for the sat solver"; "<s>[kMGT] Sets the size limit for the sat solver";
"-model", Arg.Set p_assign, "-model", Arg.Set p_assign,
" Outputs the boolean model found if sat"; "Outputs the boolean model found if sat";
"-gc", Arg.Unit setup_gc_stat,
"Outputs statistics about the GC";
] ]
(* Limits alarm *) (* Limits alarm *)
@ -86,7 +91,7 @@ let main () =
Arg.usage argspec usage; Arg.usage argspec usage;
exit 2 exit 2
end; end;
let al = Gc.create_alarm check in ignore(Gc.create_alarm check);
(* Interesting stuff happening *) (* Interesting stuff happening *)
let cnf = get_cnf () in let cnf = get_cnf () in
@ -98,14 +103,14 @@ let main () =
print_assign Format.std_formatter () print_assign Format.std_formatter ()
| S.Unsat -> | S.Unsat ->
Format.printf "Unsat@." Format.printf "Unsat@."
;;
try let () =
main () try
with main ()
| Out_of_time -> with
Format.printf "Time limit exceeded@."; | Out_of_time ->
exit 2 Format.printf "Time limit exceeded@.";
| Out_of_space -> exit 2
Format.printf "Size limit exceeded@."; | Out_of_space ->
exit 3 Format.printf "Size limit exceeded@.";
exit 3