--- a/src/HOL/TPTP/atp_problem_import.ML Sun Apr 29 11:44:33 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Sun Apr 29 11:44:33 2012 +0200
@@ -10,7 +10,8 @@
val nitpick_tptp_file : theory -> int -> string -> unit
val refute_tptp_file : theory -> int -> string -> unit
val sledgehammer_tptp_file : theory -> int -> string -> unit
- val isabelle_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 translate_tptp_file : string -> string -> string -> unit
end;
@@ -175,33 +176,44 @@
{add = [(Facts.named (Thm.derivation_name ext), [])],
del = [], only = true}
-fun sledgehammer_tac ctxt timeout i =
+fun sledgehammer_tac demo ctxt timeout i =
let
- fun slice overload_params fraq prover =
- SOLVE_TIMEOUT (timeout div fraq) prover
- (atp_tac ctxt overload_params (timeout div fraq) prover i)
+ val frac = if demo then 6 else 4
+ fun slice prover =
+ SOLVE_TIMEOUT (timeout div frac) prover
+ (atp_tac ctxt [] (timeout div frac) prover i)
in
- slice [] 5 ATP_Systems.satallaxN
- ORELSE slice [] 5 ATP_Systems.leo2N
- ORELSE slice [] 5 ATP_Systems.spassN
- ORELSE slice [] 5 ATP_Systems.vampireN
- ORELSE slice [] 5 ATP_Systems.eN
+ (if demo then
+ slice ATP_Systems.satallaxN
+ ORELSE slice ATP_Systems.leo2N
+ else
+ no_tac)
+ ORELSE slice ATP_Systems.spassN
+ ORELSE slice ATP_Systems.vampireN
+ ORELSE slice ATP_Systems.eN
+ ORELSE slice ATP_Systems.z3_tptpN
end
+fun smt_solver_tac solver ctxt =
+ let
+ val ctxt = ctxt |> Context.proof_map (SMT_Config.select_solver solver)
+ in SMT_Solver.smt_tac ctxt [] end
+
fun auto_etc_tac ctxt timeout i =
SOLVE_TIMEOUT (timeout div 20) "nitpick"
(nitpick_finite_oracle_tac ctxt (timeout div 20) i)
- ORELSE SOLVE_TIMEOUT (timeout div 10) "simp"
+ ORELSE SOLVE_TIMEOUT (timeout div 20) "simp"
(asm_full_simp_tac (simpset_of ctxt) i)
ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
(auto_tac ctxt
THEN ALLGOALS (atp_tac ctxt [] (timeout div 5) ATP_Systems.spassN))
- ORELSE SOLVE_TIMEOUT (timeout div 5) "smt" (SMT_Solver.smt_tac ctxt [] i)
+ ORELSE SOLVE_TIMEOUT (timeout div 10) "z3" (smt_solver_tac "z3" ctxt i)
+ ORELSE SOLVE_TIMEOUT (timeout div 10) "cvc3" (smt_solver_tac "cvc3" ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 20) "fast" (fast_tac ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac ctxt i)
- ORELSE SOLVE_TIMEOUT (timeout div 20) "arith" (Arith_Data.arith_tac ctxt i)
+ ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac ctxt [] i)
ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac ctxt i)
fun problem_const_prefix thy = Context.theory_name thy ^ Long_Name.separator
@@ -233,22 +245,27 @@
read_tptp_file thy (freeze_problem_consts thy) file_name
val conj = make_conj assms conjs
in
- can_tac ctxt (sledgehammer_tac ctxt timeout 1) conj
+ can_tac ctxt (sledgehammer_tac true ctxt timeout 1) conj
|> print_szs_from_success conjs
end
-fun isabelle_tptp_file thy timeout file_name =
+fun isabelle_tptp_file demo thy timeout file_name =
let
val (conjs, assms, ctxt) =
read_tptp_file thy (freeze_problem_consts thy) file_name
val conj = make_conj assms conjs
+ val last_hope = if demo then ATP_Systems.satallaxN else ATP_Systems.spassN
in
(can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
- can_tac ctxt (sledgehammer_tac ctxt (timeout div 2) 1) conj orelse
- can_tac ctxt (atp_tac ctxt [] timeout ATP_Systems.satallaxN 1) conj)
+ can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) 1) conj orelse
+ can_tac ctxt (atp_tac ctxt [] timeout last_hope 1) conj)
|> print_szs_from_success conjs
end
+val isabelle_demo_tptp_file = isabelle_tptp_file true
+val isabelle_comp_tptp_file = isabelle_tptp_file false
+
+
(** Translator between TPTP(-like) file formats **)
fun translate_tptp_file format in_file_name out_file_name = ()
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle Sun Apr 29 11:44:33 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
-
-
-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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_comp Sun Apr 29 11:44:33 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_comp_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_demo Sun Apr 29 11:44:33 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_demo_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
+ > /tmp/$SCRATCH.thy
+ "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
+done