1.1 --- a/src/HOL/TPTP/atp_problem_import.ML Sun Apr 29 11:44:33 2012 +0200
1.2 +++ b/src/HOL/TPTP/atp_problem_import.ML Sun Apr 29 11:44:33 2012 +0200
1.3 @@ -10,7 +10,8 @@
1.4 val nitpick_tptp_file : theory -> int -> string -> unit
1.5 val refute_tptp_file : theory -> int -> string -> unit
1.6 val sledgehammer_tptp_file : theory -> int -> string -> unit
1.7 - val isabelle_tptp_file : theory -> int -> string -> unit
1.8 + val isabelle_demo_tptp_file : theory -> int -> string -> unit
1.9 + val isabelle_comp_tptp_file : theory -> int -> string -> unit
1.10 val translate_tptp_file : string -> string -> string -> unit
1.11 end;
1.12
1.13 @@ -175,33 +176,44 @@
1.14 {add = [(Facts.named (Thm.derivation_name ext), [])],
1.15 del = [], only = true}
1.16
1.17 -fun sledgehammer_tac ctxt timeout i =
1.18 +fun sledgehammer_tac demo ctxt timeout i =
1.19 let
1.20 - fun slice overload_params fraq prover =
1.21 - SOLVE_TIMEOUT (timeout div fraq) prover
1.22 - (atp_tac ctxt overload_params (timeout div fraq) prover i)
1.23 + val frac = if demo then 6 else 4
1.24 + fun slice prover =
1.25 + SOLVE_TIMEOUT (timeout div frac) prover
1.26 + (atp_tac ctxt [] (timeout div frac) prover i)
1.27 in
1.28 - slice [] 5 ATP_Systems.satallaxN
1.29 - ORELSE slice [] 5 ATP_Systems.leo2N
1.30 - ORELSE slice [] 5 ATP_Systems.spassN
1.31 - ORELSE slice [] 5 ATP_Systems.vampireN
1.32 - ORELSE slice [] 5 ATP_Systems.eN
1.33 + (if demo then
1.34 + slice ATP_Systems.satallaxN
1.35 + ORELSE slice ATP_Systems.leo2N
1.36 + else
1.37 + no_tac)
1.38 + ORELSE slice ATP_Systems.spassN
1.39 + ORELSE slice ATP_Systems.vampireN
1.40 + ORELSE slice ATP_Systems.eN
1.41 + ORELSE slice ATP_Systems.z3_tptpN
1.42 end
1.43
1.44 +fun smt_solver_tac solver ctxt =
1.45 + let
1.46 + val ctxt = ctxt |> Context.proof_map (SMT_Config.select_solver solver)
1.47 + in SMT_Solver.smt_tac ctxt [] end
1.48 +
1.49 fun auto_etc_tac ctxt timeout i =
1.50 SOLVE_TIMEOUT (timeout div 20) "nitpick"
1.51 (nitpick_finite_oracle_tac ctxt (timeout div 20) i)
1.52 - ORELSE SOLVE_TIMEOUT (timeout div 10) "simp"
1.53 + ORELSE SOLVE_TIMEOUT (timeout div 20) "simp"
1.54 (asm_full_simp_tac (simpset_of ctxt) i)
1.55 ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i)
1.56 ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
1.57 (auto_tac ctxt
1.58 THEN ALLGOALS (atp_tac ctxt [] (timeout div 5) ATP_Systems.spassN))
1.59 - ORELSE SOLVE_TIMEOUT (timeout div 5) "smt" (SMT_Solver.smt_tac ctxt [] i)
1.60 + ORELSE SOLVE_TIMEOUT (timeout div 10) "z3" (smt_solver_tac "z3" ctxt i)
1.61 + ORELSE SOLVE_TIMEOUT (timeout div 10) "cvc3" (smt_solver_tac "cvc3" ctxt i)
1.62 ORELSE SOLVE_TIMEOUT (timeout div 20) "fast" (fast_tac ctxt i)
1.63 ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac ctxt i)
1.64 ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac ctxt i)
1.65 - ORELSE SOLVE_TIMEOUT (timeout div 20) "arith" (Arith_Data.arith_tac ctxt i)
1.66 + ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac ctxt [] i)
1.67 ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac ctxt i)
1.68
1.69 fun problem_const_prefix thy = Context.theory_name thy ^ Long_Name.separator
1.70 @@ -233,22 +245,27 @@
1.71 read_tptp_file thy (freeze_problem_consts thy) file_name
1.72 val conj = make_conj assms conjs
1.73 in
1.74 - can_tac ctxt (sledgehammer_tac ctxt timeout 1) conj
1.75 + can_tac ctxt (sledgehammer_tac true ctxt timeout 1) conj
1.76 |> print_szs_from_success conjs
1.77 end
1.78
1.79 -fun isabelle_tptp_file thy timeout file_name =
1.80 +fun isabelle_tptp_file demo thy timeout file_name =
1.81 let
1.82 val (conjs, assms, ctxt) =
1.83 read_tptp_file thy (freeze_problem_consts thy) file_name
1.84 val conj = make_conj assms conjs
1.85 + val last_hope = if demo then ATP_Systems.satallaxN else ATP_Systems.spassN
1.86 in
1.87 (can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
1.88 - can_tac ctxt (sledgehammer_tac ctxt (timeout div 2) 1) conj orelse
1.89 - can_tac ctxt (atp_tac ctxt [] timeout ATP_Systems.satallaxN 1) conj)
1.90 + can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) 1) conj orelse
1.91 + can_tac ctxt (atp_tac ctxt [] timeout last_hope 1) conj)
1.92 |> print_szs_from_success conjs
1.93 end
1.94
1.95 +val isabelle_demo_tptp_file = isabelle_tptp_file true
1.96 +val isabelle_comp_tptp_file = isabelle_tptp_file false
1.97 +
1.98 +
1.99 (** Translator between TPTP(-like) file formats **)
1.100
1.101 fun translate_tptp_file format in_file_name out_file_name = ()
2.1 --- a/src/HOL/TPTP/lib/Tools/tptp_isabelle Sun Apr 29 11:44:33 2012 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,33 +0,0 @@
2.4 -#!/usr/bin/env bash
2.5 -#
2.6 -# Author: Jasmin Blanchette
2.7 -#
2.8 -# DESCRIPTION: Isabelle tactics for TPTP
2.9 -
2.10 -
2.11 -PRG="$(basename "$0")"
2.12 -
2.13 -function usage() {
2.14 - echo
2.15 - echo "Usage: isabelle $PRG TIMEOUT FILES"
2.16 - echo
2.17 - echo " Runs a combination of Isabelle tactics on TPTP problems."
2.18 - echo " Each problem is allocated at most TIMEOUT seconds."
2.19 - echo
2.20 - exit 1
2.21 -}
2.22 -
2.23 -[ "$#" -eq 0 -o "$1" = "-?" ] && usage
2.24 -
2.25 -SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
2.26 -
2.27 -TIMEOUT=$1
2.28 -shift
2.29 -
2.30 -for FILE in "$@"
2.31 -do
2.32 - echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
2.33 -ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
2.34 - > /tmp/$SCRATCH.thy
2.35 - "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
2.36 -done
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_comp Sun Apr 29 11:44:33 2012 +0200
3.3 @@ -0,0 +1,33 @@
3.4 +#!/usr/bin/env bash
3.5 +#
3.6 +# Author: Jasmin Blanchette
3.7 +#
3.8 +# DESCRIPTION: Isabelle tactics for TPTP competitive division
3.9 +
3.10 +
3.11 +PRG="$(basename "$0")"
3.12 +
3.13 +function usage() {
3.14 + echo
3.15 + echo "Usage: isabelle $PRG TIMEOUT FILES"
3.16 + echo
3.17 + echo " Runs a combination of Isabelle tactics on TPTP problems."
3.18 + echo " Each problem is allocated at most TIMEOUT seconds."
3.19 + echo
3.20 + exit 1
3.21 +}
3.22 +
3.23 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
3.24 +
3.25 +SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
3.26 +
3.27 +TIMEOUT=$1
3.28 +shift
3.29 +
3.30 +for FILE in "$@"
3.31 +do
3.32 + echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
3.33 +ML {* ATP_Problem_Import.isabelle_comp_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
3.34 + > /tmp/$SCRATCH.thy
3.35 + "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
3.36 +done
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_demo Sun Apr 29 11:44:33 2012 +0200
4.3 @@ -0,0 +1,33 @@
4.4 +#!/usr/bin/env bash
4.5 +#
4.6 +# Author: Jasmin Blanchette
4.7 +#
4.8 +# DESCRIPTION: Isabelle tactics for TPTP demo division
4.9 +
4.10 +
4.11 +PRG="$(basename "$0")"
4.12 +
4.13 +function usage() {
4.14 + echo
4.15 + echo "Usage: isabelle $PRG TIMEOUT FILES"
4.16 + echo
4.17 + echo " Runs a combination of Isabelle tactics on TPTP problems."
4.18 + echo " Each problem is allocated at most TIMEOUT seconds."
4.19 + echo
4.20 + exit 1
4.21 +}
4.22 +
4.23 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
4.24 +
4.25 +SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
4.26 +
4.27 +TIMEOUT=$1
4.28 +shift
4.29 +
4.30 +for FILE in "$@"
4.31 +do
4.32 + echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
4.33 +ML {* ATP_Problem_Import.isabelle_demo_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
4.34 + > /tmp/$SCRATCH.thy
4.35 + "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
4.36 +done