From 138af8ad1b6a6382606e367cc906f4232fa626ff Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 25 Jun 2009 20:54:52 +0000 Subject: [PATCH] timeouts are passed as arguments, so that tptpprover can accept --timeout argument. Moreover it prints the proof according to the SZS ontology --- .../binaries/matitaprover/matitaprover.ml | 53 ++++++++++++++-- .../ng_paramodulation/nCicParamod.ml | 5 +- .../components/ng_paramodulation/paramod.ml | 60 +++++++++++-------- .../components/ng_paramodulation/paramod.mli | 5 +- .../components/ng_paramodulation/pp.ml | 7 ++- .../components/ng_paramodulation/pp.mli | 2 +- 6 files changed, 94 insertions(+), 38 deletions(-) diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml index b80091e81..2a5f9fdb0 100644 --- 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 () diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml index dc346d7c4..2536f6443 100644 --- a/helm/software/components/ng_paramodulation/nCicParamod.ml +++ b/helm/software/components/ng_paramodulation/nCicParamod.ml @@ -31,7 +31,10 @@ let nparamod rdb metasenv subst context t table = let (bag,maxvar), goals = HExtlib.list_mapi_acc (fun x _ a -> P.mk_goal a x) (bag,maxvar) [t] in - let solutions = P.paramod (bag,maxvar) ~g_passives:goals ~passives in + let solutions = + P.paramod ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0) + ~g_passives:goals ~passives (bag,maxvar) + in List.map (fun (bag,i,l) -> let stamp = Unix.gettimeofday () in diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index d63d1449a..d85c5627a 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -11,12 +11,9 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) - (*let debug s = prerr_endline s ;;*) - let debug _ = ();; +let debug s = prerr_endline s ;; +let debug _ = ();; -let max_nb_iter = max_int ;; -let amount_of_time = 300.0 ;; - module Paramod (B : Terms.Blob) = struct exception Failure of string * B.t Terms.bag * int * int type bag = B.t Terms.bag * int @@ -159,18 +156,21 @@ module Paramod (B : Terms.Blob) = struct add_passive_clauses g_passives new_goals ;; - let rec given_clause bag maxvar nb_iter timeout actives passives g_actives g_passives = - (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag); - prerr_endline "Active table :"; - (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x)) - (fst actives)); *) - let nb_iter = nb_iter + 1 in - if nb_iter = max_nb_iter then - raise (Failure ("No iterations left !",bag,maxvar,nb_iter)); - if Unix.gettimeofday () > timeout then - raise (Failure ("Timeout !",bag,maxvar,nb_iter)); + let rec given_clause + bag maxvar iterno max_steps timeout + actives passives g_actives g_passives + = + let iterno = iterno + 1 in + if iterno = max_steps then + raise (Failure ("No iterations left !",bag,maxvar,iterno)); + (* timeout check: gettimeofday called only if timeout set *) + (match timeout with + | None -> () + | Some timeout -> + if Unix.gettimeofday () > timeout then + raise (Failure ("Timeout !",bag,maxvar,iterno))); - let use_age = nb_iter mod 10 = 0 in + let use_age = iterno mod 10 = 0 in let rec aux_select passives g_passives = let backward,current,passives,g_passives = @@ -191,6 +191,11 @@ module Paramod (B : Terms.Blob) = struct forward_infer_step bag maxvar actives passives g_actives g_passives current in + + (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag); + prerr_endline "Active table :"; + (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x)) + (fst actives)); *) let bag,maxvar,actives,passives,g_actives,g_passives = aux_select passives g_passives @@ -207,18 +212,19 @@ module Paramod (B : Terms.Blob) = struct (Printf.sprintf "Number of passives : %d" (passive_set_cardinal passives)); given_clause - bag maxvar nb_iter timeout actives passives g_actives g_passives + bag maxvar iterno max_steps timeout + actives passives g_actives g_passives ;; - let paramod (bag,maxvar) ~g_passives ~passives = - let timeout = Unix.gettimeofday () +. amount_of_time in + let paramod ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives = + let initial_timestamp = Unix.gettimeofday () in let passives = add_passive_clauses passive_empty_set passives in let g_passives = add_passive_clauses passive_empty_set g_passives in let g_actives = [] in let actives = [], IDX.DT.empty in try given_clause - bag maxvar 0 timeout actives passives g_actives g_passives + bag maxvar 0 max_steps timeout actives passives g_actives g_passives with | Sup.Success (bag, _, (i,_,_,_)) -> let l = @@ -240,14 +246,16 @@ module Paramod (B : Terms.Blob) = struct in prerr_endline (Printf.sprintf "Found proof, %fs" - (Unix.gettimeofday() -. timeout +. amount_of_time)); - (* prerr_endline "Proof:"; - List.iter (fun x -> prerr_endline (string_of_int x); - prerr_endline (Pp.pp_unit_clause (fst (Terms.M.find x bag)))) l;*) + (Unix.gettimeofday() -. initial_timestamp)); + (* + prerr_endline "Proof:"; + List.iter (fun x -> + prerr_endline (Pp.pp_unit_clause (fst(Terms.M.find x bag)))) l; + *) [ bag, i, l ] - | Failure (msg,_bag,_maxvar,nb_iter) -> + | Failure (msg,_bag,_maxvar,iterno) -> prerr_endline msg; - prerr_endline (Printf.sprintf "FAILURE in %d iterations" nb_iter); + prerr_endline (Printf.sprintf "FAILURE in %d iterations" iterno); [] ;; diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli index 9a2d397ca..c8ba6cad9 100644 --- a/helm/software/components/ng_paramodulation/paramod.mli +++ b/helm/software/components/ng_paramodulation/paramod.mli @@ -17,7 +17,10 @@ module Paramod ( B : Terms.Blob ) : val mk_passive : bag -> B.input * B.input -> bag * B.t Terms.unit_clause val mk_goal : bag -> B.input * B.input -> bag * B.t Terms.unit_clause val paramod : - bag -> g_passives:B.t Terms.unit_clause list -> + max_steps:int -> + ?timeout:float -> + bag -> + g_passives:B.t Terms.unit_clause list -> passives:B.t Terms.unit_clause list -> (B.t Terms.bag * int * int list) list end diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml index e9628220d..e8035da65 100644 --- a/helm/software/components/ng_paramodulation/pp.ml +++ b/helm/software/components/ng_paramodulation/pp.ml @@ -128,9 +128,10 @@ let pp_bag ~formatter:f bag = ;; (* String buffer implementation *) -let on_buffer f t = +let on_buffer ?(margin=80) f t = let buff = Buffer.create 100 in let formatter = Format.formatter_of_buffer buff in + Format.pp_set_margin formatter margin; f ~formatter:formatter t; Format.fprintf formatter "@?"; Buffer.contents buff @@ -152,8 +153,8 @@ let pp_proof bag = on_buffer (pp_proof bag) ;; -let pp_unit_clause = - on_buffer pp_unit_clause +let pp_unit_clause ?margin x= + on_buffer ?margin pp_unit_clause x ;; end diff --git a/helm/software/components/ng_paramodulation/pp.mli b/helm/software/components/ng_paramodulation/pp.mli index 9cdc7a7c1..767c87e0b 100644 --- a/helm/software/components/ng_paramodulation/pp.mli +++ b/helm/software/components/ng_paramodulation/pp.mli @@ -17,7 +17,7 @@ module Pp (B : Terms.Blob) : val pp_foterm: B.t Terms.foterm -> string val pp_proof: B.t Terms.bag -> B.t Terms.proof -> string val pp_substitution: B.t Terms.substitution -> string - val pp_unit_clause: B.t Terms.unit_clause -> string + val pp_unit_clause: ?margin:int -> B.t Terms.unit_clause -> string val pp_bag: B.t Terms.bag -> string end -- 2.39.2