timeouts are passed as arguments, so that tptpprover can

[helm.git] / helm / software / components / binaries / matitaprover / matitaprover.ml

diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml
index b80091e810701b15ad5cb0b0b300e8772e3143a3..2a5f9fdb069da24746b75e370b4e3aeaea0de5d0 100644 (file)
--- a/helm/software/components/binaries/matitaprover/matitaprover.ml
+++ b/helm/software/components/binaries/matitaprover/matitaprover.ml
@@ -1,3 +1,16 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.      
+     \ /   This software is distributed as is, NO WARRANTY.     
+      V_______________________________________________________________ *)
+
+(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
+
 module OT = struct type t = string  let compare = Pervasives.compare end 
 module HC = Map.Make(OT)
 
@@ -17,11 +30,26 @@ let hash s =
 hash "==";;
 hash "_";;
 
+let problem_file = ref "no-file-given";;
+let tptppath = ref "./";;
+let seconds = ref 300;;
+
+let fail_msg () =
+      print_endline ("% SZS status Timeout for " ^ 
+        Filename.basename !problem_file)
+;;
+
 let main () =
-  let problem_file = ref "no-file-given" in
-  let tptppath = ref "./" in
+  let _ =
+    Sys.signal 24 (Sys.Signal_handle (fun _ -> fail_msg (); exit 1)) in
+  let _ =
+    Sys.signal Sys.sigalrm 
+      (Sys.Signal_handle (fun _ -> fail_msg (); exit 1)) in
   Arg.parse [
-   "--tptppath", Arg.String (fun p -> tptppath := p), "[path]  TPTP lib root"
+   "--tptppath", Arg.String (fun p -> tptppath := p), 
+     ("[path]  TPTP lib root, default " ^ !tptppath);
+   "--timeout", Arg.Int (fun p -> seconds := p), 
+     ("[seconds]  timeout, default " ^ string_of_int !seconds);
    ] (fun x -> problem_file := x) "matitaprover [problemfile]";
   let hypotheses, goals = Tptp_cnf.parse ~tptppath:!tptppath !problem_file in
   let goal = match goals with [x] -> x | _ -> assert false in
@@ -64,13 +92,26 @@ let main () =
     HExtlib.list_mapi_acc (fun x _ b -> P.mk_passive b x) bag hypotheses 
   in
   prerr_endline "Order";
-  HC.iter (fun _ (w,x) -> prerr_endline (" " ^ x ^ " is " ^ string_of_int w)) !cache;
+  HC.iter 
+    (fun _ (w,x) -> prerr_endline (" " ^ x ^ " is " ^ string_of_int w)) !cache;
   prerr_endline "Facts";
   List.iter (fun x -> prerr_endline (" " ^ Pp.pp_unit_clause x)) passives;
   prerr_endline "Goal";
   prerr_endline (" " ^ Pp.pp_unit_clause g_passives);
-  ignore(P.paramod bag ~g_passives:[g_passives] ~passives);
-  ()
+  let _ = Unix.alarm !seconds in
+  match P.paramod ~max_steps:max_int bag ~g_passives:[g_passives] ~passives with
+  | [] -> fail_msg ()
+  | (bag,_,l)::_ ->
+      print_endline ("% SZS status Unsatisfiable for " ^ 
+        Filename.basename !problem_file);
+      print_endline ("% SZS output start CNFRefutation for " ^ 
+        Filename.basename !problem_file);
+      flush stdout;
+      List.iter (fun x ->
+        print_endline (Pp.pp_unit_clause ~margin:max_int 
+          (fst(Terms.M.find x bag)))) l;
+      print_endline ("% SZS output end CNFRefutation for " ^ 
+        Filename.basename !problem_file);
 ;;
 
 main ()