--- 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"
--- 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 **)
--- 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
--- 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
--- 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
--- 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
--- 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 ^ ".")