From f27b26f3f3d2300b11aa4d68dbe823e15ffbdf1c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 24 Jul 2006 10:32:14 +0000 Subject: [PATCH] added timeout parameter to auto paramodulation. --- components/tactics/autoTactic.ml | 7 ++++++- components/tactics/paramodulation/saturation.ml | 5 +++-- components/tactics/paramodulation/saturation.mli | 1 + components/tptp_grafite/tptp2grafite.ml | 7 +++++-- components/tptp_grafite/tptp2grafite.mli | 1 + matita/matitaGui.ml | 2 +- matita/matitac.ml | 15 ++++++++------- matita/matitaprover.ml | 13 +++++++++---- matita/matitaprover.mli | 2 +- 9 files changed, 35 insertions(+), 18 deletions(-) diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml index f063eeafb..b4a311819 100644 --- a/components/tactics/autoTactic.ml +++ b/components/tactics/autoTactic.ml @@ -325,6 +325,7 @@ let auto_tac ~params ~(dbd:HMysql.dbd) = (* argument parsing *) let depth = int "depth" params in let width = int "width" params in + let timeout = string "timeout" params in let paramodulation = bool "paramodulation" params in let full = bool "full" params in let superposition = bool "superposition" params in @@ -333,6 +334,9 @@ let auto_tac ~params ~(dbd:HMysql.dbd) = let subterms_only = bool "subterms_only" params in let caso_strano = bool "caso_strano" params in let demod_table = string "demod_table" params in + let timeout = + try Some (float_of_string timeout) with Failure _ -> None + in (* the real tactic *) let auto_tac dbd (proof, goal) = let normal_auto () = @@ -364,7 +368,8 @@ let auto_tac ~params ~(dbd:HMysql.dbd) = debug_print (lazy "USO PARAMODULATION..."); (* try *) try - let rc = Saturation.saturate caso_strano dbd ~depth ~width ~full (proof, goal) in + let rc = Saturation.saturate caso_strano dbd ~depth ~width ~full + ?timeout (proof, goal) in prerr_endline (Saturation.get_stats ()); rc with exn -> diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index 021afb5ab..0ffe64e68 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -1211,7 +1211,8 @@ let eq_and_ty_of_goal = function let saturate caso_strano - dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = + dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) + ?(timeout=600.) status = let module C = Cic in reset_refs (); Indexing.init_index (); @@ -1282,7 +1283,7 @@ let saturate *) let goals = make_goal_set goal in let max_iterations = 10000 in - let max_time = Unix.gettimeofday () +. 600. (* minutes *) in + let max_time = Unix.gettimeofday () +. timeout (* minutes *) in given_clause eq_uri env goals theorems passive active max_iterations max_time in diff --git a/components/tactics/paramodulation/saturation.mli b/components/tactics/paramodulation/saturation.mli index d48dfc349..d533f8863 100644 --- a/components/tactics/paramodulation/saturation.mli +++ b/components/tactics/paramodulation/saturation.mli @@ -32,6 +32,7 @@ val saturate : ?full:bool -> ?depth:int -> ?width:int -> + ?timeout:float -> ProofEngineTypes.proof * ProofEngineTypes.goal -> ProofEngineTypes.proof * ProofEngineTypes.goal list diff --git a/components/tptp_grafite/tptp2grafite.ml b/components/tptp_grafite/tptp2grafite.ml index 841ac5f5c..4272ccdc6 100644 --- a/components/tptp_grafite/tptp2grafite.ml +++ b/components/tptp_grafite/tptp2grafite.ml @@ -4,6 +4,8 @@ module PT = CicNotationPt;; module A = Ast;; let floc = HExtlib.dummy_floc;; +let paramod_timeout = ref 600;; + let universe = "Univ" ;; let kw = [ @@ -203,7 +205,7 @@ let convert_ast statements context = function fv)) else [])@ [GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc, - GA.Auto (floc,["paramodulation",""])), + GA.Auto (floc,["paramodulation","";"timeout",string_of_int !paramod_timeout])), Some (GA.Dot(floc)))); GA.Executable(floc,GA.Tactical(floc, GA.Try(floc, GA.Tactic (floc, GA.Assumption floc)), Some (GA.Dot(floc)))) @@ -249,7 +251,8 @@ let resolve ~tptppath s = ;; (* MAIN *) -let tptp2grafite ?raw_preamble ~tptppath ~filename () = +let tptp2grafite ?(timeout=600) ?raw_preamble ~tptppath ~filename () = + paramod_timeout := timeout; let rec aux = function | [] -> [] | ((A.Inclusion (file,_)) as hd) :: tl -> diff --git a/components/tptp_grafite/tptp2grafite.mli b/components/tptp_grafite/tptp2grafite.mli index 7dfa2d3d0..24ca1004f 100644 --- a/components/tptp_grafite/tptp2grafite.mli +++ b/components/tptp_grafite/tptp2grafite.mli @@ -24,6 +24,7 @@ *) val tptp2grafite: + ?timeout:int -> ?raw_preamble:(string -> string) -> tptppath:string -> filename:string -> unit -> string diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index bf97b4760..7270603a9 100644 --- a/matita/matitaGui.ml +++ b/matita/matitaGui.ml @@ -1013,7 +1013,7 @@ class gui () = Helm_registry.get_opt_default Helm_registry.string ~default:"./" "matita.tptppath" in - let data = Matitaprover.p_to_ma ~filename:file ~tptppath in + let data = Matitaprover.p_to_ma ~filename:file ~tptppath () in let filename = Pcre.replace ~pat:"\\.p$" ~templ:".ma" file in script#assignFileName filename; source_view#source_buffer#begin_not_undoable_action (); diff --git a/matita/matitac.ml b/matita/matitac.ml index ced922a23..b4a3119e0 100644 --- a/matita/matitac.ml +++ b/matita/matitac.ml @@ -26,13 +26,14 @@ (* $Id$ *) let main () = - match Filename.basename Sys.argv.(0) with - | "gragrep" | "gragrep.opt" -> Gragrep.main () - | "matitadep" | "matitadep.opt" -> Matitadep.main () - | "matitaclean" | "matitaclean.opt" -> Matitaclean.main () - | "matitamake" | "matitamake.opt" -> Matitamake.main () - | "matitaprover" | "matitaprover.opt" -> Matitaprover.main () - | _ -> + match Filename.basename Sys.argv.(0) with + |"gragrep" |"gragrep.opt" |"gragrep.opt.static" ->Gragrep.main() + |"matitadep" |"matitadep.opt" |"matitadep.opt.static" ->Matitadep.main() + |"matitaclean"|"matitaclean.opt"|"matitaclean.opt.static"->Matitaclean.main() + |"matitamake" |"matitamake.opt" |"matitamake.opt.static" ->Matitamake.main() + |"matitaprover"|"matitaprover.opt" + |"matitaprover.opt.static"->Matitaprover.main() + | _ -> (* let _ = Paramodulation.Saturation.init () in *) (* ALB to link paramodulation *) diff --git a/matita/matitaprover.ml b/matita/matitaprover.ml index b3115ec26..d085b350c 100644 --- a/matita/matitaprover.ml +++ b/matita/matitaprover.ml @@ -74,9 +74,9 @@ for @{ 'exists ${default " ;; -let p_to_ma ~tptppath ~filename = +let p_to_ma ?timeout ~tptppath ~filename () = let data = - Tptp2grafite.tptp2grafite ~filename ~tptppath:tptppath + Tptp2grafite.tptp2grafite ?timeout ~filename ~tptppath:tptppath ~raw_preamble () in data @@ -85,9 +85,12 @@ let p_to_ma ~tptppath ~filename = let main () = MatitaInit.fill_registry (); let tptppath = ref "./" in + let timeout = ref 600 in MatitaInit.add_cmdline_spec ["-tptppath",Arg.String (fun s -> tptppath:= s), - "Where to find the Axioms/ and Problems/ directory"]; + "Where to find the Axioms/ and Problems/ directory"; + "-timeout", Arg.Int (fun x -> timeout := x), + "Timeout in seconds"]; MatitaInit.parse_cmdline (); MatitaInit.load_configuration_file (); Helm_registry.set_bool "db.nodb" true; @@ -99,7 +102,9 @@ let main () = | [file] -> file | _ -> prerr_endline "You must specify exactly one .p file."; exit 1 in - let data = p_to_ma ~filename:inputfile ~tptppath:!tptppath in + let data = + p_to_ma ~timeout:!timeout ~filename:inputfile ~tptppath:!tptppath () + in (* prerr_endline data; *) let is = Ulexing.from_utf8_string data in let gs = GrafiteSync.init () in diff --git a/matita/matitaprover.mli b/matita/matitaprover.mli index 6295136b5..e0b9cbf0b 100644 --- a/matita/matitaprover.mli +++ b/matita/matitaprover.mli @@ -25,5 +25,5 @@ val main: unit -> unit -val p_to_ma: tptppath:string -> filename:string -> string +val p_to_ma: ?timeout:int -> tptppath:string -> filename:string -> unit -> string -- 2.39.2