From: Enrico Tassi Date: Tue, 30 Jun 2009 14:33:37 +0000 (+0000) Subject: parallel X-Git-Tag: make_still_working~3763 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=68a557b997805b4a96fb2851cb4d2ab2076bba36;p=helm.git parallel --- diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml index d615d18ca..3bec2c9c1 100644 --- a/helm/software/components/binaries/matitaprover/matitaprover.ml +++ b/helm/software/components/binaries/matitaprover/matitaprover.ml @@ -38,39 +38,18 @@ let fail_msg () = print_endline ("% SZS status Timeout for " ^ Filename.basename !problem_file) ;; + +module type LeafComparer = + sig + val cmp : leaf -> leaf -> int + end +;; -let main () = - 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, default " ^ !tptppath); - "--timeout", Arg.Int (fun p -> seconds := p), - ("[seconds] timeout, default " ^ string_of_int !seconds); - ] (fun x -> problem_file := x) " -Matitaprover is the first order automatic prover that equips the -Matita interactive theorem prover (http://matita.cs.unibo.it). - -Developed by A.Asperti, M.Denes and E.Tassi, released under GPL-2.1 - -If --tptppath is given, instead of the problem file you can just give the -problem name with the .p suffix (e.g. BOO001-1.p) - -If --tptppath is not given, included files (i.e. axiom sets) are searched -in the current directory only. - -usage: matitaprover [options] problemfile"; - let hypotheses, goals = Tptp_cnf.parse ~tptppath:!tptppath !problem_file in - let goal = match goals with [x] -> x | _ -> assert false in - let leaf_compare = ref (fun ((a,_) : leaf) ((b,_) : leaf) -> Pervasives.compare a b) in - let module B : Terms.Blob +module MakeBlob(C:LeafComparer) : Terms.Blob with type t = leaf and type input = Ast.term = struct type t = leaf let eq a b = a == b - let compare a b = !leaf_compare a b + let compare a b = C.cmp a b let eqP = hash "==" let pp (_,a) = a type input = Ast.term @@ -97,49 +76,103 @@ usage: matitaprover [options] problemfile"; let embed t = snd(embed [] t);; end - in - let module Pp = Pp.Pp(B) in - let module P = Paramod.Paramod(B) in - let success_msg bag l (pp : ?margin:int -> B.t Terms.unit_clause -> string)= - 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 ~margin:max_int - (fst(Terms.M.find x bag)))) l; - print_endline ("% SZS output end CNFRefutation for " ^ - Filename.basename !problem_file) - in - let bag = Terms.M.empty, 0 in - let bag, g_passives = P.mk_goal bag goal in - let bag, passives = - 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; +;; + +let success_msg bag l (pp : ?margin:int -> leaf Terms.unit_clause -> string) = + 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 ~margin:max_int + (fst(Terms.M.find x bag)))) l; + print_endline ("% SZS output end CNFRefutation for " ^ + Filename.basename !problem_file) +;; + +let start_msg passives g_passives (pp : leaf Terms.unit_clause -> string) = + prerr_endline (string_of_int (Unix.getpid ())); +(* prerr_endline "Facts"; - List.iter (fun x -> prerr_endline (" " ^ Pp.pp_unit_clause x)) passives; + List.iter (fun x -> prerr_endline (" " ^ pp x)) passives; prerr_endline "Goal"; - prerr_endline (" " ^ Pp.pp_unit_clause g_passives); + prerr_endline (" " ^ pp g_passives) +*) +;; + +module Main(C:LeafComparer) = struct + let main goal hypotheses = + let module B = MakeBlob(C) in + let module Pp = Pp.Pp(B) in + let module P = Paramod.Paramod(B) in + let bag = Terms.M.empty, 0 in + let bag, g_passives = P.mk_goal bag goal in + let bag, passives = + HExtlib.list_mapi_acc (fun x _ b -> P.mk_passive b x) bag hypotheses + in + start_msg passives g_passives Pp.pp_unit_clause; + match + P.paramod + ~max_steps:max_int bag ~g_passives:[g_passives] ~passives + with + | [] -> () + | (bag,_,l)::_ -> success_msg bag l Pp.pp_unit_clause + ;; +end + +let killall l = + List.iter (fun pid -> try Unix.kill pid 9 with _ -> ()) l +;; + +let main () = + let childs = ref [] in + let _ = + Sys.signal 24 (Sys.Signal_handle + (fun _ -> fail_msg (); killall !childs; exit 1)) + in + let _ = + Sys.signal Sys.sigalrm + (Sys.Signal_handle (fun _ -> fail_msg (); killall !childs; exit 1)) + in + Arg.parse [ + "--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 is the first order automatic prover that equips the +Matita interactive theorem prover (http://matita.cs.unibo.it). + +Developed by A.Asperti, M.Denes and E.Tassi, released under GPL-2.1 + +If --tptppath is given, instead of the problem file you can just give the +problem name with the .p suffix (e.g. BOO001-1.p) + +If --tptppath is not given, included files (i.e. axiom sets) are searched +in the current directory only. + +usage: matitaprover [options] problemfile"; + let hypotheses, goals = Tptp_cnf.parse ~tptppath:!tptppath !problem_file in + let goal = match goals with [x] -> x | _ -> assert false in let _ = Unix.alarm !seconds in - match - P.paramod - ~timeout:(Unix.gettimeofday () +. float_of_int (!seconds / 2) ) - ~max_steps:max_int bag ~g_passives:[g_passives] ~passives - with - | [] -> - leaf_compare := (fun (_,a) (_,b) -> Pervasives.compare a b); - (match - P.paramod - ~timeout:(Unix.gettimeofday () +. float_of_int (!seconds / 2) ) - ~max_steps:max_int bag ~g_passives:[g_passives] ~passives - with - | [] -> fail_msg () - | (bag,_,l)::_ -> success_msg bag l Pp.pp_unit_clause) - | (bag,_,l)::_ -> success_msg bag l Pp.pp_unit_clause + childs := + List.map + (fun f -> + let pid = Unix.fork () in + if pid = 0 then (f ();exit 0) else pid) + [ + (fun () -> + let module M = Main(struct let cmp (a,_) (b,_) = compare a b end) in + M.main goal hypotheses) + ; + (fun () -> + let module M = Main(struct let cmp (a,_) (b,_) = compare b a end) in + M.main goal hypotheses) + ]; + let _ = Unix.wait () in + killall !childs; + exit 0; ;; main ()