added timeout parameter to auto paramodulation.

diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml
index f063eeafb69ff99d7d49bf6b6810d6768f302e41..b4a3118199d517266147b7712a976a54ce841e08 100644 (file)
--- 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 021afb5abdf0ed36f61450e6119d7fdc2230173c..0ffe64e68e36d50f6ea289edb212235e7ce5c828 100644 (file)
--- 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 d48dfc349ba77d007b9da65e564b618981b68028..d533f88635c3d57bf0b0334c3ca2dcd9449e6521 100644 (file)
--- 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 841ac5f5c930948345c6037f682fd780889dba15..4272ccdc6002b4548be90ae81adbc0b67490d983 100644 (file)
--- 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 7dfa2d3d03314a2b501a0144d069b7b4c9d1a6cc..24ca1004fbce6a0b70355c3da7897fcd8210511b 100644 (file)
--- 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 bf97b47607f144dfc42e27f34b6bfc7468571f40..7270603a9636b7ebcd4be445ce9350b0757dfefb 100644 (file)
--- 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 ced922a231b2644d42ed5fa3dc8d818bf80b9bb4..b4a3119e00f799d1a1f55fbf6b7499f356552347 100644 (file)
--- 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 b3115ec26e6feefff346bfba3ebb9f36b8053035..d085b350c8db1b4d0df21f1d9d9e72596181ed71 100644 (file)
--- 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 6295136b5c6b04df0e7eebc81460702c67b0382d..e0b9cbf0b3d60ed7864024fed86508c34c7b216a 100644 (file)
--- 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