src/HOL/TPTP/atp_problem_import.ML

--- a/src/HOL/TPTP/atp_problem_import.ML	Sun Apr 22 14:16:46 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Sun Apr 22 14:16:46 2012 +0200
@@ -7,10 +7,10 @@
 
 signature ATP_PROBLEM_IMPORT =
 sig
-  val isabelle_tptp_file : string -> unit
-  val nitpick_tptp_file : string -> unit
-  val refute_tptp_file : string -> unit
-  val sledgehammer_tptp_file : string -> unit
+  val isabelle_tptp_file : int -> string -> unit
+  val nitpick_tptp_file : int -> string -> unit
+  val refute_tptp_file : int -> string -> unit
+  val sledgehammer_tptp_file : int -> string -> unit
   val translate_tptp_file : string -> string -> string -> unit
 end;
 
@@ -150,12 +150,12 @@
 
 (** Isabelle (combination of provers) **)
 
-fun isabelle_tptp_file file_name = ()
+fun isabelle_tptp_file timeout file_name = ()
 
 
 (** Nitpick (alias Nitrox) **)
 
-fun nitpick_tptp_file file_name =
+fun nitpick_tptp_file timeout file_name =
   let
     val (falsify, ts) = read_tptp_file @{theory} file_name
     val state = Proof.init @{context}
@@ -172,8 +172,7 @@
        ("show_consts", "true"),
        ("format", "1000"),
        ("max_potential", "0"),
-       ("timeout", "none"),
-       ("expect", Nitpick.genuineN)]
+       ("timeout", string_of_int timeout)]
       |> Nitpick_Isar.default_params @{theory}
     val i = 1
     val n = 1
@@ -195,13 +194,11 @@
      "Unknown")
   |> writeln
 
-fun refute_tptp_file file_name =
+fun refute_tptp_file timeout file_name =
   let
     val (falsify, ts) = read_tptp_file @{theory} file_name
     val params =
-      [("maxtime", "10000"),
-       ("assms", "true"),
-       ("expect", Nitpick.genuineN)]
+      [("maxtime", string_of_int timeout)]
   in
     Refute.refute_term @{context} params ts @{prop False}
     |> print_szs_from_outcome falsify
@@ -210,7 +207,7 @@
 
 (** Sledgehammer **)
 
-fun sledgehammer_tptp_file file_name = ()
+fun sledgehammer_tptp_file timeout file_name = ()
 
 
 (** Translator between TPTP(-like) file formats **)