--- a/src/HOL/TPTP/atp_problem_import.ML Wed Jun 06 10:35:05 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Wed Jun 06 10:35:05 2012 +0200
@@ -21,8 +21,8 @@
val freeze_problem_consts : theory -> term -> term
val make_conj : term list * term list -> term list -> term
val sledgehammer_tptp_file : theory -> int -> string -> unit
- val isabelle_demo_tptp_file : theory -> int -> string -> unit
- val isabelle_comp_tptp_file : theory -> int -> string -> unit
+ val isabelle_tptp_file : theory -> int -> string -> unit
+ val isabelle_hot_tptp_file : theory -> int -> string -> unit
val translate_tptp_file : string -> string -> string -> unit
end;
@@ -285,7 +285,7 @@
|> print_szs_from_success conjs
end
-fun isabelle_tptp_file demo thy timeout file_name =
+fun generic_isabelle_tptp_file demo thy timeout file_name =
let
val (conjs, assms, ctxt) =
read_tptp_file thy (freeze_problem_consts thy) file_name
@@ -300,8 +300,8 @@
|> print_szs_from_success conjs
end
-val isabelle_demo_tptp_file = isabelle_tptp_file true
-val isabelle_comp_tptp_file = isabelle_tptp_file false
+val isabelle_tptp_file = generic_isabelle_tptp_file false
+val isabelle_hot_tptp_file = generic_isabelle_tptp_file true
(** Translator between TPTP(-like) file formats **)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle Wed Jun 06 10:35:05 2012 +0200
@@ -0,0 +1,33 @@
+#!/usr/bin/env bash
+#
+# Author: Jasmin Blanchette
+#
+# DESCRIPTION: Isabelle tactics for TPTP competitive division
+
+
+PRG="$(basename "$0")"
+
+function usage() {
+ echo
+ 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
+}
+
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
+
+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 @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
+ > /tmp/$SCRATCH.thy
+ "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
+done
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle_comp Wed Jun 06 10:35:05 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Jasmin Blanchette
-#
-# DESCRIPTION: Isabelle tactics for TPTP competitive division
-
-
-PRG="$(basename "$0")"
-
-function usage() {
- echo
- 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
-}
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-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_comp_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
- > /tmp/$SCRATCH.thy
- "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
-done
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle_demo Wed Jun 06 10:35:05 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Jasmin Blanchette
-#
-# DESCRIPTION: Isabelle tactics for TPTP demo division
-
-
-PRG="$(basename "$0")"
-
-function usage() {
- echo
- 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
-}
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-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_demo_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
- > /tmp/$SCRATCH.thy
- "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
-done
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot Wed Jun 06 10:35:05 2012 +0200
@@ -0,0 +1,33 @@
+#!/usr/bin/env bash
+#
+# Author: Jasmin Blanchette
+#
+# DESCRIPTION: Isabelle tactics for TPTP demo division
+
+
+PRG="$(basename "$0")"
+
+function usage() {
+ echo
+ 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
+}
+
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
+
+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_hot_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
+ > /tmp/$SCRATCH.thy
+ "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
+done