Added time/size limits to test utility

tests/run

@@ -4,7 +4,7 @@ solvertest () {
     for f in `find $1 -name *.d -type f`
     do
         echo -ne "\r\033[K Testing $f "
-        tests/main $f | grep $2 > /dev/null 2> /dev/null
+        tests/main -t 5s -s 1G $f | grep $2 > /dev/null 2> /dev/null
         RET=$?
         if [ $RET -ne 0 ];
         then

util/test.ml

@@ -1,19 +1,62 @@
 
 module S = Sat.Make(struct end)
 
+exception Out_of_time
+exception Out_of_space
+
 (* Arguments parsing *)
 let file = ref ""
 let p_assign = ref false
+let time_limit = ref 300.
+let size_limit = ref 1000_000_000.
+;;
+
+let int_arg r arg =
+  let l = String.length arg in
+  let multiplier m =
+    let arg1 = String.sub arg 0 (l-1) in
+    r := m *. (float_of_string arg1)
+  in
+  if l = 0 then raise (Arg.Bad "bad numeric argument")
+  else
+    try
+      match arg.[l-1] with
+      | 'k' -> multiplier 1e3
+      | 'M' -> multiplier 1e6
+      | 'G' -> multiplier 1e9
+      | 'T' -> multiplier 1e12
+      | 's' -> multiplier 1.
+      | 'm' -> multiplier 60.
+      | 'h' -> multiplier 3600.
+      | 'd' -> multiplier 86400.
+      | '0'..'9' -> r := float_of_string arg
+      | _ -> raise (Arg.Bad "bad numeric argument")
+    with Failure "float_of_string" -> raise (Arg.Bad "bad numeric argument")
+;;
 
 let input_file = fun s -> file := s
 let usage = "Usage : main [options] <file>"
 let argspec = Arg.align [
     "-v", Arg.Int (fun i -> Log.set_debug i),
         "<lvl> Sets the debug verbose level";
+    "-t", Arg.String (int_arg time_limit),
+        "<t>[smhd] Sets the time limit for the sat solver";
+    "-s", Arg.String (int_arg size_limit),
+        "<s>[kMGT] Sets the size limit for the sat solver";
     "-model", Arg.Set p_assign,
         " Outputs the boolean model found if sat";
 ]
 
+(* Limits alarm *)
+let check () =
+    let t = Sys.time () in
+    let heap_size = (Gc.quick_stat ()).Gc.heap_words in
+    let s = float heap_size *. float Sys.word_size /. 8. in
+    if t > !time_limit then
+        raise Out_of_time
+    else if s > !size_limit then
+        raise Out_of_space
+
 (* Entry file parsing *)
 let get_cnf () =
     let chan = open_in !file in
@@ -40,11 +83,15 @@ let print_assign fmt () =
     )
 
 let main () =
+  (* Administrative duties *)
   Arg.parse argspec input_file usage;
   if !file = "" then begin
       Arg.usage argspec usage;
       exit 2
   end;
+  let al = Gc.create_alarm check in
+
+  (* Interesting stuff happening *)
   let cnf = get_cnf () in
   S.assume cnf;
   match S.solve () with
@@ -56,4 +103,12 @@ let main () =
           Format.printf "Unsat@."
 ;;
 
-main ()
+try
+    main ()
+with
+| Out_of_time ->
+        Format.printf "Time limit exceeded@.";
+    exit 2
+| Out_of_space ->
+    Format.printf "Size limit exceeded@.";
+    exit 3