--- a/Admin/contributed_components Wed Mar 23 08:50:42 2011 +0100
+++ b/Admin/contributed_components Thu Mar 24 10:39:47 2011 +0100
@@ -5,4 +5,5 @@
contrib/spass-3.7
contrib/scala-2.8.1.final
contrib/vampire-1.0
-contrib/z3-2.15
+contrib/yices-1.0.28
+contrib/z3-2.19
--- a/bin/isabelle Wed Mar 23 08:50:42 2011 +0100
+++ b/bin/isabelle Thu Mar 24 10:39:47 2011 +0100
@@ -17,8 +17,6 @@
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
-splitarray ":" "$ISABELLE_TOOLS"; TOOLS=("${SPLITARRAY[@]}")
-
## diagnostics
@@ -30,19 +28,7 @@
echo " Start Isabelle tool NAME with ARGS; pass \"-?\" for tool specific help."
echo
echo " Available tools are:"
- for DIR in "${TOOLS[@]}"
- do
- if [ -d "$DIR" ]; then
- for TOOL in "$DIR"/*
- do
- if [ -f "$TOOL" -a -x "$TOOL" ]; then
- NAME="$(basename "$TOOL")"
- DESCRLINE="$(fgrep DESCRIPTION: "$TOOL" | sed -e 's/^.*DESCRIPTION: *//')"
- echo " $NAME - $DESCRLINE"
- fi
- done
- fi
- done
+ perl -w "$ISABELLE_HOME/lib/scripts/tools.pl"
exit 1
}
@@ -63,10 +49,15 @@
## main
+splitarray ":" "$ISABELLE_TOOLS"; TOOLS=("${SPLITARRAY[@]}")
+
for DIR in "${TOOLS[@]}"
do
TOOL="$DIR/$TOOLNAME"
- [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
+ case "$TOOL" in
+ *~) ;;
+ *) [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@" ;;
+ esac
done
fail "Unknown Isabelle tool: $TOOLNAME"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/tools.pl Thu Mar 24 10:39:47 2011 +0100
@@ -0,0 +1,37 @@
+#
+# Author: Makarius
+#
+# tools.pl - list Isabelle tools with description
+#
+
+use strict;
+use warnings;
+
+my @tools = ();
+
+for my $dir (split(":", $ENV{"ISABELLE_TOOLS"})) {
+ if (-d $dir) {
+ if (opendir DIR, $dir) {
+ for my $name (readdir DIR) {
+ my $file = "$dir/$name";
+ if (-f $file and -x $file and !($file =~ /~$/)) {
+ if (open FILE, $file) {
+ my $description;
+ while (<FILE>) {
+ if (!defined($description) and m/DESCRIPTION: *(.*)$/) {
+ $description = $1;
+ }
+ }
+ close FILE;
+ if (defined($description)) {
+ push(@tools, " $name - $description\n");
+ }
+ }
+ }
+ }
+ closedir DIR;
+ }
+ }
+}
+
+for (sort @tools) { print };
--- a/src/HOL/IsaMakefile Wed Mar 23 08:50:42 2011 +0100
+++ b/src/HOL/IsaMakefile Thu Mar 24 10:39:47 2011 +0100
@@ -467,8 +467,8 @@
Library/Sublist_Order.thy Library/Sum_of_Squares.thy \
Library/Sum_of_Squares/sos_wrapper.ML \
Library/Sum_of_Squares/sum_of_squares.ML \
- Library/TPTP.thy Library/Transitive_Closure_Table.thy \
- Library/Univ_Poly.thy Library/While_Combinator.thy Library/Zorn.thy \
+ Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy \
+ Library/While_Combinator.thy Library/Zorn.thy \
$(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \
Library/reflection.ML Library/reify_data.ML \
Library/Quickcheck_Narrowing.thy \
@@ -1048,9 +1048,10 @@
ex/Quickcheck_Narrowing_Examples.thy \
ex/Quicksort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy \
- ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy ex/Sqrt.thy \
+ ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy \
+ ex/sledgehammer_tactics.ML ex/Sqrt.thy \
ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy \
- ex/Transfer_Ex.thy ex/Tree23.thy ex/Unification.thy \
+ ex/TPTP.thy ex/Transfer_Ex.thy ex/Tree23.thy ex/Unification.thy \
ex/While_Combinator_Example.thy ex/document/root.bib \
ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \
../Tools/interpretation_with_defs.ML
@@ -1316,9 +1317,9 @@
Mirabelle/Tools/mirabelle_refute.ML \
Mirabelle/Tools/mirabelle_sledgehammer.ML \
Mirabelle/Tools/mirabelle_sledgehammer_filter.ML \
- Mirabelle/Tools/sledgehammer_tactics.ML \
- Mirabelle/lib/Tools/mirabelle Mirabelle/lib/scripts/mirabelle.pl \
- Library/FrechetDeriv.thy Library/Inner_Product.thy
+ ex/sledgehammer_tactics.ML Mirabelle/lib/Tools/mirabelle \
+ Mirabelle/lib/scripts/mirabelle.pl Library/FrechetDeriv.thy \
+ Library/Inner_Product.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
@cd Library; $(ISABELLE_TOOL) mirabelle -q arith Inner_Product.thy # some arbitrary small test case
--- a/src/HOL/Library/TPTP.thy Wed Mar 23 08:50:42 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
-theory TPTP
-imports Main
-uses "~~/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML"
-begin
-
-declare mem_def [simp add]
-
-declare [[smt_oracle]]
-
-ML {* proofs := 0 *}
-
-ML {*
-fun SOLVE_TIMEOUT seconds name tac st =
- let
- val result =
- TimeLimit.timeLimit (Time.fromSeconds seconds)
- (fn () => SINGLE (SOLVE tac) st) ()
- handle TimeLimit.TimeOut => NONE
- | ERROR _ => NONE
- in
- (case result of
- NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
- | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st'))
- end
-*}
-
-ML {*
-fun isabellep_tac max_secs =
- SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
- (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
- ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac @{simpset}))
- ORELSE
- SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac @{claset}))
- ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac @{clasimpset}
- THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
- ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac @{context} []))
- ORELSE
- SOLVE_TIMEOUT (max_secs div 5) "fast" (ALLGOALS (fast_tac @{claset}))
- ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac @{claset}))
- ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac @{clasimpset}))
- ORELSE
- SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac @{clasimpset}))
-*}
-
-end
--- a/src/HOL/Mirabelle/Mirabelle.thy Wed Mar 23 08:50:42 2011 +0100
+++ b/src/HOL/Mirabelle/Mirabelle.thy Thu Mar 24 10:39:47 2011 +0100
@@ -5,7 +5,7 @@
theory Mirabelle
imports Sledgehammer
uses "Tools/mirabelle.ML"
- "Tools/sledgehammer_tactics.ML"
+ "../ex/sledgehammer_tactics.ML"
begin
(* no multithreading, no parallel proofs *) (* FIXME *)
--- a/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML Wed Mar 23 08:50:42 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-(* Title: HOL/Mirabelle/Tools/sledgehammer_tactics.ML
- Author: Jasmin Blanchette, TU Muenchen
- Copyright 2010
-
-Sledgehammer as a tactic.
-*)
-
-signature SLEDGEHAMMER_TACTICS =
-sig
- val sledgehammer_with_metis_tac : Proof.context -> int -> tactic
- val sledgehammer_as_unsound_oracle_tac : Proof.context -> int -> tactic
- val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
-end;
-
-structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
-struct
-
-fun run_atp force_full_types timeout i n ctxt goal name =
- let
- val chained_ths = [] (* a tactic has no chained ths *)
- val params as {type_sys, relevance_thresholds, max_relevant, ...} =
- ((if force_full_types then [("full_types", "true")] else [])
- @ [("timeout", string_of_int (Time.toSeconds timeout))])
- (* @ [("overlord", "true")] *)
- |> Sledgehammer_Isar.default_params ctxt
- val prover = Sledgehammer_Provers.get_prover ctxt false name
- val default_max_relevant =
- Sledgehammer_Provers.default_max_relevant_for_prover ctxt name
- val is_built_in_const =
- Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
- val relevance_fudge =
- Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
- val relevance_override = {add = [], del = [], only = false}
- val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
- val no_dangerous_types =
- Sledgehammer_ATP_Translate.types_dangerous_types type_sys
- val facts =
- Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
- relevance_thresholds
- (the_default default_max_relevant max_relevant) is_built_in_const
- relevance_fudge relevance_override chained_ths hyp_ts concl_t
- val problem =
- {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
- facts = map Sledgehammer_Provers.Untranslated_Fact facts,
- smt_filter = NONE}
- in
- (case prover params (K "") problem of
- {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
- | _ => NONE)
- handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
- end
-
-fun to_period ("." :: _) = []
- | to_period ("" :: ss) = to_period ss
- | to_period (s :: ss) = s :: to_period ss
- | to_period [] = []
-
-val atp = "vampire" (* or "e" or "spass" etc. *)
-
-fun thms_of_name ctxt name =
- let
- val lex = Keyword.get_lexicons
- val get = maps (ProofContext.get_fact ctxt o fst)
- in
- Source.of_string name
- |> Symbol.source
- |> Token.source {do_recover=SOME false} lex Position.start
- |> Token.source_proper
- |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
- |> Source.exhaust
- end
-
-fun sledgehammer_with_metis_tac ctxt i th =
- let
- val timeout = Time.fromSeconds 30
- in
- case run_atp false timeout i i ctxt th atp of
- SOME facts =>
- Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th
- | NONE => Seq.empty
- end
-
-fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th =
- let
- val thy = ProofContext.theory_of ctxt
- val timeout = Time.fromSeconds 30
- val xs = run_atp force_full_types timeout i i ctxt th atp
- in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
-
-val sledgehammer_as_unsound_oracle_tac =
- generic_sledgehammer_as_oracle_tac false
-val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true
-
-end;
--- a/src/HOL/Mirabelle/etc/settings Wed Mar 23 08:50:42 2011 +0100
+++ b/src/HOL/Mirabelle/etc/settings Thu Mar 24 10:39:47 2011 +0100
@@ -4,7 +4,6 @@
MIRABELLE_LOGIC=HOL
MIRABELLE_THEORY=Main
-MIRABELLE_OUTPUT_PATH=/tmp/mirabelle
MIRABELLE_TIMEOUT=30
ISABELLE_TOOLS="$ISABELLE_TOOLS:$MIRABELLE_HOME/lib/Tools"
--- a/src/HOL/Mirabelle/lib/Tools/mirabelle Wed Mar 23 08:50:42 2011 +0100
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle Thu Mar 24 10:39:47 2011 +0100
@@ -16,7 +16,7 @@
}
function usage() {
- out="$MIRABELLE_OUTPUT_PATH"
+ [ -n "$MIRABELLE_OUTPUT_PATH" ] && out="$MIRABELLE_OUTPUT_PATH" || out="None"
timeout="$MIRABELLE_TIMEOUT"
echo
echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES"
@@ -102,8 +102,14 @@
# setup
+if [ -z "$MIRABELLE_OUTPUT_PATH" ]; then
+ MIRABELLE_OUTPUT_PATH="${ISABELLE_TMP_PREFIX}-mirabelle$$"
+ PURGE_OUTPUT="true"
+fi
+
mkdir -p "$MIRABELLE_OUTPUT_PATH"
+export MIRABELLE_OUTPUT_PATH
## main
@@ -112,3 +118,9 @@
perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE" || fail "Mirabelle failed."
done
+
+## cleanup
+
+if [ -n "$PURGE_OUTPUT" ]; then
+ rm -rf "$MIRABELLE_OUTPUT_PATH"
+fi
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Wed Mar 23 08:50:42 2011 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Thu Mar 24 10:39:47 2011 +0100
@@ -127,16 +127,18 @@
close(LOG_FILE);
my $quiet = "";
+my $output_log = 1;
if (defined $be_quiet and $be_quiet ne "") {
$quiet = " > /dev/null 2>&1";
+ $output_log = 0;
}
-print "Mirabelle: $thy_file\n" if ($quiet ne "");
+if ($output_log) { print "Mirabelle: $thy_file\n"; }
my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
"-e 'use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
-print "Finished: $thy_file\n" if ($quiet ne "");
+if ($output_log) { print "Finished: $thy_file\n"; }
# cleanup
--- a/src/HOL/Tools/Meson/meson_clausify.ML Wed Mar 23 08:50:42 2011 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu Mar 24 10:39:47 2011 +0100
@@ -22,9 +22,9 @@
open Meson
-(* the extra "?" helps prevent clashes *)
-val new_skolem_var_prefix = "?SK"
-val new_nonskolem_var_prefix = "?V"
+(* the extra "Meson" helps prevent clashes (FIXME) *)
+val new_skolem_var_prefix = "MesonSK"
+val new_nonskolem_var_prefix = "MesonV"
(**** Transformation of Elimination Rules into First-Order Formulas****)
--- a/src/HOL/Tools/Nitpick/etc/settings Wed Mar 23 08:50:42 2011 +0100
+++ b/src/HOL/Tools/Nitpick/etc/settings Thu Mar 24 10:39:47 2011 +0100
@@ -1,1 +1,3 @@
+# -*- shell-script -*- :mode=shellscript:
+
ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML Wed Mar 23 08:50:42 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML Thu Mar 24 10:39:47 2011 +0100
@@ -6,6 +6,11 @@
signature SMT_SETUP_SOLVERS =
sig
+ datatype z3_non_commercial =
+ Z3_Non_Commercial_Unknown |
+ Z3_Non_Commercial_Accepted |
+ Z3_Non_Commercial_Declined
+ val z3_non_commercial: unit -> z3_non_commercial
val setup: theory -> theory
end
@@ -95,15 +100,41 @@
(* Z3 *)
+datatype z3_non_commercial =
+ Z3_Non_Commercial_Unknown |
+ Z3_Non_Commercial_Accepted |
+ Z3_Non_Commercial_Declined
+
+
local
val flagN = "Z3_NON_COMMERCIAL"
+ val accepted = member (op =) ["yes", "Yes", "YES"]
+ val declined = member (op =) ["no", "No", "NO"]
+in
+
+fun z3_non_commercial () =
+ if accepted (getenv flagN) then Z3_Non_Commercial_Accepted
+ else if declined (getenv flagN) then Z3_Non_Commercial_Declined
+ else Z3_Non_Commercial_Unknown
+
+fun if_z3_non_commercial f =
+ (case z3_non_commercial () of
+ Z3_Non_Commercial_Accepted => f ()
+ | Z3_Non_Commercial_Declined =>
+ error ("The SMT solver Z3 may only be used for non-commercial " ^
+ "applications.")
+ | Z3_Non_Commercial_Unknown =>
+ error ("The SMT solver Z3 is not activated. To activate it, set " ^
+ "the environment variable " ^ quote flagN ^ " to " ^ quote ("yes") ^
+ "."))
+
+end
+
+
+local
fun z3_make_command is_remote name () =
- if getenv flagN = "yes" then make_command is_remote name ()
- else
- error ("The SMT solver Z3 is not enabled. To enable it, set " ^
- "the environment variable " ^ quote flagN ^ " to " ^ quote ("yes") ^
- ".")
+ if_z3_non_commercial (make_command is_remote name)
fun z3_options ctxt =
["-rs:" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
--- a/src/HOL/ex/ROOT.ML Wed Mar 23 08:50:42 2011 +0100
+++ b/src/HOL/ex/ROOT.ML Thu Mar 24 10:39:47 2011 +0100
@@ -76,6 +76,9 @@
"Set_Algebras"
];
+Unsynchronized.setmp Proofterm.proofs (! Proofterm.proofs)
+ use_thy "TPTP";
+
if getenv "ISABELLE_GHC" = "" then ()
else use_thy "Quickcheck_Narrowing_Examples";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/TPTP.thy Thu Mar 24 10:39:47 2011 +0100
@@ -0,0 +1,57 @@
+(* Title: HOL/ex/TPTP.thy
+ Author: Jasmin Blanchette
+ Copyright 2011
+
+TPTP "IsabelleP" tactic.
+*)
+
+theory TPTP
+imports Main
+uses "sledgehammer_tactics.ML"
+begin
+
+declare mem_def [simp add]
+
+declare [[smt_oracle]]
+
+ML {* Proofterm.proofs := 0 *}
+
+ML {*
+fun SOLVE_TIMEOUT seconds name tac st =
+ let
+ val result =
+ TimeLimit.timeLimit (Time.fromSeconds seconds)
+ (fn () => SINGLE (SOLVE tac) st) ()
+ handle TimeLimit.TimeOut => NONE
+ | ERROR _ => NONE
+ in
+ (case result of
+ NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
+ | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st'))
+ end
+*}
+
+ML {*
+fun isabellep_tac max_secs =
+ SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
+ (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac @{simpset}))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac @{claset}))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac @{clasimpset}
+ THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac @{context} []))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 5) "fast" (ALLGOALS (fast_tac @{claset}))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac @{claset}))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac @{clasimpset}))
+ ORELSE
+ SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac @{clasimpset}))
+*}
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/sledgehammer_tactics.ML Thu Mar 24 10:39:47 2011 +0100
@@ -0,0 +1,94 @@
+(* Title: HOL/ex/sledgehammer_tactics.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2010, 2011
+
+Sledgehammer as a tactic.
+*)
+
+signature SLEDGEHAMMER_TACTICS =
+sig
+ val sledgehammer_with_metis_tac : Proof.context -> int -> tactic
+ val sledgehammer_as_unsound_oracle_tac : Proof.context -> int -> tactic
+ val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
+end;
+
+structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
+struct
+
+fun run_atp force_full_types timeout i n ctxt goal name =
+ let
+ val chained_ths = [] (* a tactic has no chained ths *)
+ val params as {type_sys, relevance_thresholds, max_relevant, ...} =
+ ((if force_full_types then [("full_types", "true")] else [])
+ @ [("timeout", string_of_int (Time.toSeconds timeout))])
+ (* @ [("overlord", "true")] *)
+ |> Sledgehammer_Isar.default_params ctxt
+ val prover = Sledgehammer_Provers.get_prover ctxt false name
+ val default_max_relevant =
+ Sledgehammer_Provers.default_max_relevant_for_prover ctxt name
+ val is_built_in_const =
+ Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
+ val relevance_fudge =
+ Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
+ val relevance_override = {add = [], del = [], only = false}
+ val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
+ val no_dangerous_types =
+ Sledgehammer_ATP_Translate.types_dangerous_types type_sys
+ val facts =
+ Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
+ relevance_thresholds
+ (the_default default_max_relevant max_relevant) is_built_in_const
+ relevance_fudge relevance_override chained_ths hyp_ts concl_t
+ val problem =
+ {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
+ facts = map Sledgehammer_Provers.Untranslated_Fact facts,
+ smt_filter = NONE}
+ in
+ (case prover params (K "") problem of
+ {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
+ | _ => NONE)
+ handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
+ end
+
+fun to_period ("." :: _) = []
+ | to_period ("" :: ss) = to_period ss
+ | to_period (s :: ss) = s :: to_period ss
+ | to_period [] = []
+
+val atp = "e" (* or "vampire" or "spass" etc. *)
+
+fun thms_of_name ctxt name =
+ let
+ val lex = Keyword.get_lexicons
+ val get = maps (ProofContext.get_fact ctxt o fst)
+ in
+ Source.of_string name
+ |> Symbol.source
+ |> Token.source {do_recover=SOME false} lex Position.start
+ |> Token.source_proper
+ |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
+ |> Source.exhaust
+ end
+
+fun sledgehammer_with_metis_tac ctxt i th =
+ let
+ val timeout = Time.fromSeconds 30
+ in
+ case run_atp false timeout i i ctxt th atp of
+ SOME facts =>
+ Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th
+ | NONE => Seq.empty
+ end
+
+fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val timeout = Time.fromSeconds 30
+ val xs = run_atp force_full_types timeout i i ctxt th atp
+ in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
+
+val sledgehammer_as_unsound_oracle_tac =
+ generic_sledgehammer_as_oracle_tac false
+val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true
+
+end;