# HG changeset patch # User blanchet # Date 1335097006 -7200 # Node ID 24babc4b1925c4dba2eac4a825082ce0160a1ae5 # Parent f3896a53043f9fa3ecffd3976e1730157e2d12ab added timeout argument to TPTP tools diff -r f3896a53043f -r 24babc4b1925 src/HOL/TPTP/ATP_Problem_Import.thy --- a/src/HOL/TPTP/ATP_Problem_Import.thy Sun Apr 22 14:16:46 2012 +0200 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy Sun Apr 22 14:16:46 2012 +0200 @@ -9,6 +9,8 @@ uses ("atp_problem_import.ML") begin +declare [[show_consts]] (* for Refute *) + typedecl iota (* for TPTP *) use "atp_problem_import.ML" diff -r f3896a53043f -r 24babc4b1925 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 **) diff -r f3896a53043f -r 24babc4b1925 src/HOL/TPTP/lib/Tools/tptp_isabelle --- a/src/HOL/TPTP/lib/Tools/tptp_isabelle Sun Apr 22 14:16:46 2012 +0200 +++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle Sun Apr 22 14:16:46 2012 +0200 @@ -9,9 +9,10 @@ function usage() { echo - echo "Usage: isabelle $PRG FILES" + echo "Usage: isabelle $PRG TIMEOUT FILES" echo echo " Runs a combination of Isabelle tactics on TPTP problems." + echo " Each problem is allocated at most TIMEOUT seconds." echo exit 1 } @@ -20,10 +21,13 @@ SCRATCH="Scratch_${PRG}_$$_${RANDOM}" +TIMEOUT=$1 +shift + for FILE in "$@" do echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ -ML {* ATP_Problem_Import.isabelle_tptp_file \"$FILE\" *} end;" \ +ML {* ATP_Problem_Import.isabelle_tptp_file ($TIMEOUT) \"$FILE\" *} end;" \ > /tmp/$SCRATCH.thy "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" done diff -r f3896a53043f -r 24babc4b1925 src/HOL/TPTP/lib/Tools/tptp_nitpick --- a/src/HOL/TPTP/lib/Tools/tptp_nitpick Sun Apr 22 14:16:46 2012 +0200 +++ b/src/HOL/TPTP/lib/Tools/tptp_nitpick Sun Apr 22 14:16:46 2012 +0200 @@ -9,9 +9,10 @@ function usage() { echo - echo "Usage: isabelle $PRG FILES" + echo "Usage: isabelle $PRG TIMEOUT FILES" echo echo " Runs Nitpick on TPTP problems." + echo " Each problem is allocated at most TIMEOUT seconds." echo exit 1 } @@ -20,10 +21,13 @@ SCRATCH="Scratch_${PRG}_$$_${RANDOM}" +TIMEOUT=$1 +shift + for FILE in "$@" do echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ -ML {* ATP_Problem_Import.nitpick_tptp_file \"$FILE\" *} end;" \ +ML {* ATP_Problem_Import.nitpick_tptp_file ($TIMEOUT) \"$FILE\" *} end;" \ > /tmp/$SCRATCH.thy "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" done diff -r f3896a53043f -r 24babc4b1925 src/HOL/TPTP/lib/Tools/tptp_refute --- a/src/HOL/TPTP/lib/Tools/tptp_refute Sun Apr 22 14:16:46 2012 +0200 +++ b/src/HOL/TPTP/lib/Tools/tptp_refute Sun Apr 22 14:16:46 2012 +0200 @@ -9,7 +9,7 @@ function usage() { echo - echo "Usage: isabelle $PRG FILES" + echo "Usage: isabelle $PRG TIMEOUT FILES" echo echo " Runs Refute on TPTP problems." echo @@ -20,10 +20,13 @@ SCRATCH="Scratch_${PRG}_$$_${RANDOM}" +TIMEOUT=$1 +shift + for FILE in "$@" do echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ -ML {* ATP_Problem_Import.refute_tptp_file \"$FILE\" *} end;" \ +ML {* ATP_Problem_Import.refute_tptp_file ($TIMEOUT) \"$FILE\" *} end;" \ > /tmp/$SCRATCH.thy "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" done diff -r f3896a53043f -r 24babc4b1925 src/HOL/TPTP/lib/Tools/tptp_sledgehammer --- a/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Sun Apr 22 14:16:46 2012 +0200 +++ b/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Sun Apr 22 14:16:46 2012 +0200 @@ -9,9 +9,10 @@ function usage() { echo - echo "Usage: isabelle $PRG FILES" + echo "Usage: isabelle $PRG TIMEOUT FILES" echo echo " Runs Sledgehammer on TPTP problems." + echo " Each problem is allocated at most TIMEOUT seconds." echo exit 1 } @@ -20,10 +21,13 @@ SCRATCH="Scratch_${PRG}_$$_${RANDOM}" +TIMEOUT=$1 +shift + for FILE in "$@" do echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ -ML {* ATP_Problem_Import.sledgehammer_tptp_file \"$FILE\" *} end;" \ +ML {* ATP_Problem_Import.sledgehammer_tptp_file ($TIMEOUT) \"$FILE\" *} end;" \ > /tmp/$SCRATCH.thy "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" done diff -r f3896a53043f -r 24babc4b1925 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Sun Apr 22 14:16:46 2012 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Sun Apr 22 14:16:46 2012 +0200 @@ -1048,7 +1048,10 @@ fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) mode i n step subst assm_ts orig_t = - let val print_nt = if is_mode_nt mode then Output.urgent_message else K () in + let + val print_nt = if is_mode_nt mode then Output.urgent_message else K () + val print_t = if mode = TPTP then Output.urgent_message else K () + in if getenv "KODKODI" = "" then (* The "expect" argument is deliberately ignored if Kodkodi is missing so that the "Nitpick_Examples" can be processed on any machine. *) @@ -1064,14 +1067,18 @@ (pick_them_nits_in_term deadline state params mode i n step subst assm_ts) orig_t handle TOO_LARGE (_, details) => - (print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome) + (print_t "% SZS status Unknown"; + print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome) | TOO_SMALL (_, details) => - (print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome) + (print_t "% SZS status Unknown"; + print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome) | Kodkod.SYNTAX (_, details) => - (print_nt ("Malformed Kodkodi output: " ^ details ^ "."); + (print_t "% SZS status Unknown"; + print_nt ("Malformed Kodkodi output: " ^ details ^ "."); unknown_outcome) | TimeLimit.TimeOut => - (print_nt "Nitpick ran out of time."; unknown_outcome) + (print_t "% SZS status TimedOut"; + print_nt "Nitpick ran out of time."; unknown_outcome) in if expect = "" orelse outcome_code = expect then outcome else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")