1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex Wed Jul 28 11:42:48 2010 +0200
1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Jul 28 22:18:35 2010 +0200
1.3 @@ -121,28 +121,33 @@
1.4 \cite{sutcliffe-2000}, but if you want better performance you will need to
1.5 install at least E and SPASS locally.
1.6
1.7 -There are three main ways to install E and SPASS:
1.8 +There are three main ways to install ATPs on your machine:
1.9
1.10 \begin{enum}
1.11 \item[$\bullet$] If you installed an official Isabelle package with everything
1.12 inside, it should already include properly setup executables for E and SPASS,
1.13 -ready to use.
1.14 +ready to use.%
1.15 +\footnote{Vampire's license prevents us from doing the same for this otherwise
1.16 +wonderful tool.}
1.17
1.18 -\item[$\bullet$] Otherwise, you can download the Isabelle-aware E and SPASS
1.19 +\item[$\bullet$] Alternatively, you can download the Isabelle-aware E and SPASS
1.20 binary packages from Isabelle's download page. Extract the archives, then add a
1.21 line to your \texttt{\char`\~/.isabelle/etc/components} file with the absolute path to
1.22 -E or SPASS. For example, if \texttt{\char`\~/.isabelle/etc/components} does not exist
1.23 +E or SPASS. For example, if the \texttt{components} does not exist
1.24 yet and you extracted SPASS to \texttt{/usr/local/spass-3.7}, create
1.25 -the file \texttt{\char`\~/.isabelle/etc/components} with the single line
1.26 +the \texttt{components} file with the single line
1.27
1.28 \prew
1.29 \texttt{/usr/local/spass-3.7}
1.30 \postw
1.31
1.32 -\item[$\bullet$] If you prefer to build E or SPASS yourself, feel free to do so
1.33 -and set the environment variable \texttt{E\_HOME} or \texttt{SPASS\_HOME} to the
1.34 -directory that contains the \texttt{eproof} or \texttt{SPASS} executable,
1.35 -respectively.
1.36 +in it.
1.37 +
1.38 +\item[$\bullet$] If you prefer to build E or SPASS yourself, or obtained a
1.39 +Vampire executable from somewhere (e.g., \url{http://www.vprover.org/}),
1.40 +set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
1.41 +\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
1.42 +\texttt{SPASS}, or \texttt{vampire} executable.
1.43 \end{enum}
1.44
1.45 To check whether E and SPASS are installed, follow the example in
1.46 @@ -176,29 +181,29 @@
1.47 Sledgehammer: ATP ``\textit{e}'' for subgoal 1: \\
1.48 $([a] = [b]) = (a = b)$ \\
1.49 Try this command: \textbf{by} (\textit{metis hd.simps}). \\
1.50 -To minimize the number of lemmas, try this command: \\
1.51 +To minimize the number of lemmas, try this: \\
1.52 \textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount]
1.53 %
1.54 Sledgehammer: ATP ``\textit{spass}'' for subgoal 1: \\
1.55 $([a] = [b]) = (a = b)$ \\
1.56 Try this command: \textbf{by} (\textit{metis insert\_Nil last\_ConsL}). \\
1.57 -To minimize the number of lemmas, try this command: \\
1.58 +To minimize the number of lemmas, try this: \\
1.59 \textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount]
1.60 %
1.61 Sledgehammer: ATP ``\textit{remote\_vampire}'' for subgoal 1: \\
1.62 $([a] = [b]) = (a = b)$ \\
1.63 Try this command: \textbf{by} (\textit{metis One\_nat\_def\_raw empty\_replicate} \\
1.64 \phantom{Try this command: \textbf{by} (\textit{metis~}}\textit{insert\_Nil last\_ConsL replicate\_Suc}). \\
1.65 -To minimize the number of lemmas, try this command: \\
1.66 +To minimize the number of lemmas, try this: \\
1.67 \textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{remote\_vampire}] \\
1.68 \phantom{\textbf{sledgehammer}~}(\textit{One\_nat\_def\_raw empty\_replicate insert\_Nil} \\
1.69 \phantom{\textbf{sledgehammer}~(}\textit{last\_ConsL replicate\_Suc}).
1.70 \postw
1.71
1.72 Sledgehammer ran E, SPASS, and the remote version of Vampire in parallel. If E
1.73 -and SPASS are not installed (\S\ref{installation}), you will see references to
1.74 -their remote American cousins \textit{remote\_e} and \textit{remote\_spass}
1.75 -instead of \textit{e} and \textit{spass}.
1.76 +is not installed (\S\ref{installation}), you will see references to
1.77 +its remote American cousin \textit{remote\_e} instead of
1.78 +\textit{e}; and if SPASS is not installed, it will not appear in the output.
1.79
1.80 Based on each ATP proof, Sledgehammer gives a one-liner proof that uses the
1.81 \textit{metis} method. You can click them and insert them into the theory text.
1.82 @@ -377,9 +382,6 @@
1.83 \item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E executes
1.84 on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
1.85
1.86 -\item[$\bullet$] \textbf{\textit{remote\_spass}:} The remote version of SPASS
1.87 -executes on Geoff Sutcliffe's Miami servers.
1.88 -
1.89 \item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
1.90 Vampire executes on Geoff Sutcliffe's Miami servers. Version 9 is used.
1.91
2.1 --- a/etc/components Wed Jul 28 11:42:48 2010 +0200
2.2 +++ b/etc/components Wed Jul 28 22:18:35 2010 +0200
2.3 @@ -13,7 +13,7 @@
2.4 #misc components
2.5 src/Tools/Code
2.6 src/Tools/WWW_Find
2.7 -src/HOL/Tools/ATP_Manager
2.8 +src/HOL/Tools/ATP
2.9 src/HOL/Mirabelle
2.10 src/HOL/Library/Sum_Of_Squares
2.11 src/HOL/Tools/SMT
3.1 --- a/src/HOL/IsaMakefile Wed Jul 28 11:42:48 2010 +0200
3.2 +++ b/src/HOL/IsaMakefile Wed Jul 28 22:18:35 2010 +0200
3.3 @@ -268,9 +268,9 @@
3.4 $(SRC)/Provers/Arith/combine_numerals.ML \
3.5 $(SRC)/Provers/Arith/extract_common_term.ML \
3.6 $(SRC)/Tools/Metis/metis.ML \
3.7 - Tools/ATP_Manager/async_manager.ML \
3.8 - Tools/ATP_Manager/atp_problem.ML \
3.9 - Tools/ATP_Manager/atp_systems.ML \
3.10 + Tools/ATP/async_manager.ML \
3.11 + Tools/ATP/atp_problem.ML \
3.12 + Tools/ATP/atp_systems.ML \
3.13 Tools/choice_specification.ML \
3.14 Tools/int_arith.ML \
3.15 Tools/groebner.ML \
4.1 --- a/src/HOL/Sledgehammer.thy Wed Jul 28 11:42:48 2010 +0200
4.2 +++ b/src/HOL/Sledgehammer.thy Wed Jul 28 22:18:35 2010 +0200
4.3 @@ -10,9 +10,9 @@
4.4 theory Sledgehammer
4.5 imports Plain Hilbert_Choice
4.6 uses
4.7 - ("Tools/ATP_Manager/async_manager.ML")
4.8 - ("Tools/ATP_Manager/atp_problem.ML")
4.9 - ("Tools/ATP_Manager/atp_systems.ML")
4.10 + ("Tools/ATP/async_manager.ML")
4.11 + ("Tools/ATP/atp_problem.ML")
4.12 + ("Tools/ATP/atp_systems.ML")
4.13 ("~~/src/Tools/Metis/metis.ML")
4.14 ("Tools/Sledgehammer/clausifier.ML")
4.15 ("Tools/Sledgehammer/meson_tactic.ML")
4.16 @@ -85,9 +85,9 @@
4.17 apply (simp add: COMBC_def)
4.18 done
4.19
4.20 -use "Tools/ATP_Manager/async_manager.ML"
4.21 -use "Tools/ATP_Manager/atp_problem.ML"
4.22 -use "Tools/ATP_Manager/atp_systems.ML"
4.23 +use "Tools/ATP/async_manager.ML"
4.24 +use "Tools/ATP/atp_problem.ML"
4.25 +use "Tools/ATP/atp_systems.ML"
4.26 setup ATP_Systems.setup
4.27
4.28 use "~~/src/Tools/Metis/metis.ML"
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/Tools/ATP/async_manager.ML Wed Jul 28 22:18:35 2010 +0200
5.3 @@ -0,0 +1,241 @@
5.4 +(* Title: HOL/Tools/ATP/async_manager.ML
5.5 + Author: Fabian Immler, TU Muenchen
5.6 + Author: Makarius
5.7 + Author: Jasmin Blanchette, TU Muenchen
5.8 +
5.9 +Central manager for asynchronous diagnosis tool threads.
5.10 +*)
5.11 +
5.12 +signature ASYNC_MANAGER =
5.13 +sig
5.14 + val launch :
5.15 + string -> bool -> Time.time -> Time.time -> string -> (unit -> string)
5.16 + -> unit
5.17 + val kill_threads : string -> string -> unit
5.18 + val running_threads : string -> string -> unit
5.19 + val thread_messages : string -> string -> int option -> unit
5.20 +end;
5.21 +
5.22 +structure Async_Manager : ASYNC_MANAGER =
5.23 +struct
5.24 +
5.25 +(** preferences **)
5.26 +
5.27 +val message_store_limit = 20;
5.28 +val message_display_limit = 5;
5.29 +
5.30 +
5.31 +(** thread management **)
5.32 +
5.33 +(* data structures over threads *)
5.34 +
5.35 +structure Thread_Heap = Heap
5.36 +(
5.37 + type elem = Time.time * Thread.thread;
5.38 + fun ord ((a, _), (b, _)) = Time.compare (a, b);
5.39 +);
5.40 +
5.41 +fun lookup_thread xs = AList.lookup Thread.equal xs;
5.42 +fun delete_thread xs = AList.delete Thread.equal xs;
5.43 +fun update_thread xs = AList.update Thread.equal xs;
5.44 +
5.45 +
5.46 +(* state of thread manager *)
5.47 +
5.48 +type state =
5.49 + {manager: Thread.thread option,
5.50 + timeout_heap: Thread_Heap.T,
5.51 + active: (Thread.thread * (string * Time.time * Time.time * string)) list,
5.52 + canceling: (Thread.thread * (string * Time.time * string)) list,
5.53 + messages: (string * string) list,
5.54 + store: (string * string) list}
5.55 +
5.56 +fun make_state manager timeout_heap active canceling messages store : state =
5.57 + {manager = manager, timeout_heap = timeout_heap, active = active,
5.58 + canceling = canceling, messages = messages, store = store}
5.59 +
5.60 +val global_state = Synchronized.var "async_manager"
5.61 + (make_state NONE Thread_Heap.empty [] [] [] []);
5.62 +
5.63 +
5.64 +(* unregister thread *)
5.65 +
5.66 +fun unregister verbose message thread =
5.67 + Synchronized.change global_state
5.68 + (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
5.69 + (case lookup_thread active thread of
5.70 + SOME (tool, birth_time, _, desc) =>
5.71 + let
5.72 + val active' = delete_thread thread active;
5.73 + val now = Time.now ()
5.74 + val canceling' = (thread, (tool, now, desc)) :: canceling
5.75 + val message' =
5.76 + desc ^ "\n" ^ message ^
5.77 + (if verbose then
5.78 + "Total time: " ^ Int.toString (Time.toMilliseconds
5.79 + (Time.- (now, birth_time))) ^ " ms.\n"
5.80 + else
5.81 + "")
5.82 + val messages' = (tool, message') :: messages;
5.83 + val store' = (tool, message') ::
5.84 + (if length store <= message_store_limit then store
5.85 + else #1 (chop message_store_limit store));
5.86 + in make_state manager timeout_heap active' canceling' messages' store' end
5.87 + | NONE => state));
5.88 +
5.89 +
5.90 +(* main manager thread -- only one may exist *)
5.91 +
5.92 +val min_wait_time = Time.fromMilliseconds 300;
5.93 +val max_wait_time = Time.fromSeconds 10;
5.94 +
5.95 +fun replace_all bef aft =
5.96 + let
5.97 + fun aux seen "" = String.implode (rev seen)
5.98 + | aux seen s =
5.99 + if String.isPrefix bef s then
5.100 + aux seen "" ^ aft ^ aux [] (unprefix bef s)
5.101 + else
5.102 + aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
5.103 + in aux [] end
5.104 +
5.105 +(* This is a workaround for Proof General's off-by-a-few sendback display bug,
5.106 + whereby "pr" in "proof" is not highlighted. *)
5.107 +fun break_into_chunks xs =
5.108 + maps (space_explode "\000" o replace_all "\n\n" "\000" o snd) xs
5.109 +
5.110 +fun print_new_messages () =
5.111 + case Synchronized.change_result global_state
5.112 + (fn {manager, timeout_heap, active, canceling, messages, store} =>
5.113 + (messages, make_state manager timeout_heap active canceling []
5.114 + store)) of
5.115 + [] => ()
5.116 + | msgs as (tool, _) :: _ =>
5.117 + let val ss = break_into_chunks msgs in
5.118 + List.app priority (tool ^ ": " ^ hd ss :: tl ss)
5.119 + end
5.120 +
5.121 +fun check_thread_manager verbose = Synchronized.change global_state
5.122 + (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
5.123 + if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
5.124 + else let val manager = SOME (Toplevel.thread false (fn () =>
5.125 + let
5.126 + fun time_limit timeout_heap =
5.127 + (case try Thread_Heap.min timeout_heap of
5.128 + NONE => Time.+ (Time.now (), max_wait_time)
5.129 + | SOME (time, _) => time);
5.130 +
5.131 + (*action: find threads whose timeout is reached, and interrupt canceling threads*)
5.132 + fun action {manager, timeout_heap, active, canceling, messages, store} =
5.133 + let val (timeout_threads, timeout_heap') =
5.134 + Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
5.135 + in
5.136 + if null timeout_threads andalso null canceling then
5.137 + NONE
5.138 + else
5.139 + let
5.140 + val _ = List.app (Simple_Thread.interrupt o #1) canceling
5.141 + val canceling' = filter (Thread.isActive o #1) canceling
5.142 + val state' = make_state manager timeout_heap' active canceling' messages store;
5.143 + in SOME (map #2 timeout_threads, state') end
5.144 + end;
5.145 + in
5.146 + while Synchronized.change_result global_state
5.147 + (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
5.148 + if null active andalso null canceling andalso null messages
5.149 + then (false, make_state NONE timeout_heap active canceling messages store)
5.150 + else (true, state))
5.151 + do
5.152 + (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
5.153 + |> these
5.154 + |> List.app (unregister verbose "Timed out.\n");
5.155 + print_new_messages ();
5.156 + (*give threads some time to respond to interrupt*)
5.157 + OS.Process.sleep min_wait_time)
5.158 + end))
5.159 + in make_state manager timeout_heap active canceling messages store end)
5.160 +
5.161 +
5.162 +(* register thread *)
5.163 +
5.164 +fun register tool verbose birth_time death_time desc thread =
5.165 + (Synchronized.change global_state
5.166 + (fn {manager, timeout_heap, active, canceling, messages, store} =>
5.167 + let
5.168 + val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
5.169 + val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active;
5.170 + val state' = make_state manager timeout_heap' active' canceling messages store;
5.171 + in state' end);
5.172 + check_thread_manager verbose);
5.173 +
5.174 +
5.175 +fun launch tool verbose birth_time death_time desc f =
5.176 + (Toplevel.thread true
5.177 + (fn () =>
5.178 + let
5.179 + val self = Thread.self ()
5.180 + val _ = register tool verbose birth_time death_time desc self
5.181 + val message = f ()
5.182 + in unregister verbose message self end);
5.183 + ())
5.184 +
5.185 +
5.186 +(** user commands **)
5.187 +
5.188 +(* kill threads *)
5.189 +
5.190 +fun kill_threads tool workers = Synchronized.change global_state
5.191 + (fn {manager, timeout_heap, active, canceling, messages, store} =>
5.192 + let
5.193 + val killing =
5.194 + map_filter (fn (th, (tool', _, _, desc)) =>
5.195 + if tool' = tool then SOME (th, (tool', Time.now (), desc))
5.196 + else NONE) active
5.197 + val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
5.198 + val _ = if null killing then () else priority ("Killed active " ^ workers ^ ".")
5.199 + in state' end);
5.200 +
5.201 +
5.202 +(* running threads *)
5.203 +
5.204 +fun seconds time = string_of_int (Time.toSeconds time) ^ " s"
5.205 +
5.206 +fun running_threads tool workers =
5.207 + let
5.208 + val {active, canceling, ...} = Synchronized.value global_state;
5.209 +
5.210 + val now = Time.now ();
5.211 + fun running_info (_, (tool', birth_time, death_time, desc)) =
5.212 + if tool' = tool then
5.213 + SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
5.214 + seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc)
5.215 + else
5.216 + NONE
5.217 + fun canceling_info (_, (tool', death_time, desc)) =
5.218 + if tool' = tool then
5.219 + SOME ("Trying to interrupt thread since " ^
5.220 + seconds (Time.- (now, death_time)) ^ ":\n" ^ desc)
5.221 + else
5.222 + NONE
5.223 + val running =
5.224 + case map_filter running_info active of
5.225 + [] => ["No " ^ workers ^ " running."]
5.226 + | ss => "Running " ^ workers ^ ":" :: ss
5.227 + val interrupting =
5.228 + case map_filter canceling_info canceling of
5.229 + [] => []
5.230 + | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss
5.231 + in priority (space_implode "\n\n" (running @ interrupting)) end
5.232 +
5.233 +fun thread_messages tool worker opt_limit =
5.234 + let
5.235 + val limit = the_default message_display_limit opt_limit;
5.236 + val tool_store = Synchronized.value global_state
5.237 + |> #store |> filter (curry (op =) tool o fst)
5.238 + val header =
5.239 + "Recent " ^ worker ^ " messages" ^
5.240 + (if length tool_store <= limit then ":"
5.241 + else " (" ^ string_of_int limit ^ " displayed):");
5.242 + in List.app priority (header :: break_into_chunks (#1 (chop limit tool_store))) end
5.243 +
5.244 +end;
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Jul 28 22:18:35 2010 +0200
6.3 @@ -0,0 +1,152 @@
6.4 +(* Title: HOL/Tools/ATP/atp_problem.ML
6.5 + Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
6.6 + Author: Jasmin Blanchette, TU Muenchen
6.7 +
6.8 +TPTP syntax.
6.9 +*)
6.10 +
6.11 +signature ATP_PROBLEM =
6.12 +sig
6.13 + datatype 'a fo_term = ATerm of 'a * 'a fo_term list
6.14 + datatype quantifier = AForall | AExists
6.15 + datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
6.16 + datatype ('a, 'b) formula =
6.17 + AQuant of quantifier * 'a list * ('a, 'b) formula |
6.18 + AConn of connective * ('a, 'b) formula list |
6.19 + AAtom of 'b
6.20 +
6.21 + datatype kind = Axiom | Conjecture
6.22 + datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
6.23 + type 'a problem = (string * 'a problem_line list) list
6.24 +
6.25 + val timestamp : unit -> string
6.26 + val is_tptp_variable : string -> bool
6.27 + val strings_for_tptp_problem :
6.28 + (string * string problem_line list) list -> string list
6.29 + val nice_tptp_problem :
6.30 + bool -> ('a * (string * string) problem_line list) list
6.31 + -> ('a * string problem_line list) list
6.32 + * (string Symtab.table * string Symtab.table) option
6.33 +end;
6.34 +
6.35 +structure ATP_Problem : ATP_PROBLEM =
6.36 +struct
6.37 +
6.38 +(** ATP problem **)
6.39 +
6.40 +datatype 'a fo_term = ATerm of 'a * 'a fo_term list
6.41 +datatype quantifier = AForall | AExists
6.42 +datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
6.43 +datatype ('a, 'b) formula =
6.44 + AQuant of quantifier * 'a list * ('a, 'b) formula |
6.45 + AConn of connective * ('a, 'b) formula list |
6.46 + AAtom of 'b
6.47 +
6.48 +datatype kind = Axiom | Conjecture
6.49 +datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
6.50 +type 'a problem = (string * 'a problem_line list) list
6.51 +
6.52 +val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
6.53 +
6.54 +fun string_for_term (ATerm (s, [])) = s
6.55 + | string_for_term (ATerm (s, ts)) =
6.56 + if s = "equal" then space_implode " = " (map string_for_term ts)
6.57 + else s ^ "(" ^ commas (map string_for_term ts) ^ ")"
6.58 +fun string_for_quantifier AForall = "!"
6.59 + | string_for_quantifier AExists = "?"
6.60 +fun string_for_connective ANot = "~"
6.61 + | string_for_connective AAnd = "&"
6.62 + | string_for_connective AOr = "|"
6.63 + | string_for_connective AImplies = "=>"
6.64 + | string_for_connective AIf = "<="
6.65 + | string_for_connective AIff = "<=>"
6.66 + | string_for_connective ANotIff = "<~>"
6.67 +fun string_for_formula (AQuant (q, xs, phi)) =
6.68 + string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^
6.69 + string_for_formula phi
6.70 + | string_for_formula (AConn (ANot, [AAtom (ATerm ("equal", ts))])) =
6.71 + space_implode " != " (map string_for_term ts)
6.72 + | string_for_formula (AConn (c, [phi])) =
6.73 + string_for_connective c ^ " " ^ string_for_formula phi
6.74 + | string_for_formula (AConn (c, phis)) =
6.75 + "(" ^ space_implode (" " ^ string_for_connective c ^ " ")
6.76 + (map string_for_formula phis) ^ ")"
6.77 + | string_for_formula (AAtom tm) = string_for_term tm
6.78 +
6.79 +fun string_for_problem_line (Fof (ident, kind, phi)) =
6.80 + "fof(" ^ ident ^ ", " ^
6.81 + (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^
6.82 + " (" ^ string_for_formula phi ^ ")).\n"
6.83 +fun strings_for_tptp_problem problem =
6.84 + "% This file was generated by Isabelle (most likely Sledgehammer)\n\
6.85 + \% " ^ timestamp () ^ "\n" ::
6.86 + maps (fn (_, []) => []
6.87 + | (heading, lines) =>
6.88 + "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" ::
6.89 + map string_for_problem_line lines) problem
6.90 +
6.91 +fun is_tptp_variable s = Char.isUpper (String.sub (s, 0))
6.92 +
6.93 +
6.94 +(** Nice names **)
6.95 +
6.96 +fun empty_name_pool readable_names =
6.97 + if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
6.98 +
6.99 +fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
6.100 +fun pool_map f xs =
6.101 + pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
6.102 +
6.103 +(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the
6.104 + unreadable "op_1", "op_2", etc., in the problem files. *)
6.105 +val reserved_nice_names = ["equal", "op"]
6.106 +fun readable_name full_name s =
6.107 + if s = full_name then
6.108 + s
6.109 + else
6.110 + let
6.111 + val s = s |> Long_Name.base_name
6.112 + |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
6.113 + in if member (op =) reserved_nice_names s then full_name else s end
6.114 +
6.115 +fun nice_name (full_name, _) NONE = (full_name, NONE)
6.116 + | nice_name (full_name, desired_name) (SOME the_pool) =
6.117 + case Symtab.lookup (fst the_pool) full_name of
6.118 + SOME nice_name => (nice_name, SOME the_pool)
6.119 + | NONE =>
6.120 + let
6.121 + val nice_prefix = readable_name full_name desired_name
6.122 + fun add j =
6.123 + let
6.124 + val nice_name = nice_prefix ^
6.125 + (if j = 0 then "" else "_" ^ Int.toString j)
6.126 + in
6.127 + case Symtab.lookup (snd the_pool) nice_name of
6.128 + SOME full_name' =>
6.129 + if full_name = full_name' then (nice_name, the_pool)
6.130 + else add (j + 1)
6.131 + | NONE =>
6.132 + (nice_name,
6.133 + (Symtab.update_new (full_name, nice_name) (fst the_pool),
6.134 + Symtab.update_new (nice_name, full_name) (snd the_pool)))
6.135 + end
6.136 + in add 0 |> apsnd SOME end
6.137 +
6.138 +
6.139 +fun nice_term (ATerm (name, ts)) =
6.140 + nice_name name ##>> pool_map nice_term ts #>> ATerm
6.141 +fun nice_formula (AQuant (q, xs, phi)) =
6.142 + pool_map nice_name xs ##>> nice_formula phi
6.143 + #>> (fn (xs, phi) => AQuant (q, xs, phi))
6.144 + | nice_formula (AConn (c, phis)) =
6.145 + pool_map nice_formula phis #>> curry AConn c
6.146 + | nice_formula (AAtom tm) = nice_term tm #>> AAtom
6.147 +fun nice_problem_line (Fof (ident, kind, phi)) =
6.148 + nice_formula phi #>> (fn phi => Fof (ident, kind, phi))
6.149 +fun nice_problem problem =
6.150 + pool_map (fn (heading, lines) =>
6.151 + pool_map nice_problem_line lines #>> pair heading) problem
6.152 +fun nice_tptp_problem readable_names problem =
6.153 + nice_problem problem (empty_name_pool readable_names)
6.154 +
6.155 +end;
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Jul 28 22:18:35 2010 +0200
7.3 @@ -0,0 +1,219 @@
7.4 +(* Title: HOL/Tools/ATP/atp_systems.ML
7.5 + Author: Fabian Immler, TU Muenchen
7.6 + Author: Jasmin Blanchette, TU Muenchen
7.7 +
7.8 +Setup for supported ATPs.
7.9 +*)
7.10 +
7.11 +signature ATP_SYSTEMS =
7.12 +sig
7.13 + datatype failure =
7.14 + Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
7.15 + OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
7.16 +
7.17 + type prover_config =
7.18 + {executable: string * string,
7.19 + required_executables: (string * string) list,
7.20 + arguments: bool -> Time.time -> string,
7.21 + proof_delims: (string * string) list,
7.22 + known_failures: (failure * string) list,
7.23 + max_new_relevant_facts_per_iter: int,
7.24 + prefers_theory_relevant: bool,
7.25 + explicit_forall: bool}
7.26 +
7.27 + val add_prover: string * prover_config -> theory -> theory
7.28 + val get_prover: theory -> string -> prover_config
7.29 + val available_atps: theory -> unit
7.30 + val refresh_systems_on_tptp : unit -> unit
7.31 + val default_atps_param_value : unit -> string
7.32 + val setup : theory -> theory
7.33 +end;
7.34 +
7.35 +structure ATP_Systems : ATP_SYSTEMS =
7.36 +struct
7.37 +
7.38 +(* prover configuration *)
7.39 +
7.40 +datatype failure =
7.41 + Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
7.42 + OldSpass | MalformedInput | MalformedOutput | UnknownError
7.43 +
7.44 +type prover_config =
7.45 + {executable: string * string,
7.46 + required_executables: (string * string) list,
7.47 + arguments: bool -> Time.time -> string,
7.48 + proof_delims: (string * string) list,
7.49 + known_failures: (failure * string) list,
7.50 + max_new_relevant_facts_per_iter: int,
7.51 + prefers_theory_relevant: bool,
7.52 + explicit_forall: bool}
7.53 +
7.54 +
7.55 +(* named provers *)
7.56 +
7.57 +structure Data = Theory_Data
7.58 +(
7.59 + type T = (prover_config * stamp) Symtab.table
7.60 + val empty = Symtab.empty
7.61 + val extend = I
7.62 + fun merge data : T = Symtab.merge (eq_snd op =) data
7.63 + handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
7.64 +)
7.65 +
7.66 +fun add_prover (name, config) thy =
7.67 + Data.map (Symtab.update_new (name, (config, stamp ()))) thy
7.68 + handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
7.69 +
7.70 +fun get_prover thy name =
7.71 + the (Symtab.lookup (Data.get thy) name) |> fst
7.72 + handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
7.73 +
7.74 +fun available_atps thy =
7.75 + priority ("Available ATPs: " ^
7.76 + commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
7.77 +
7.78 +fun available_atps thy =
7.79 + priority ("Available ATPs: " ^
7.80 + commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
7.81 +
7.82 +fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000
7.83 +
7.84 +(* E prover *)
7.85 +
7.86 +val tstp_proof_delims =
7.87 + ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
7.88 +
7.89 +val e_config : prover_config =
7.90 + {executable = ("E_HOME", "eproof"),
7.91 + required_executables = [],
7.92 + arguments = fn _ => fn timeout =>
7.93 + "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^
7.94 + string_of_int (to_generous_secs timeout),
7.95 + proof_delims = [tstp_proof_delims],
7.96 + known_failures =
7.97 + [(Unprovable, "SZS status: CounterSatisfiable"),
7.98 + (Unprovable, "SZS status CounterSatisfiable"),
7.99 + (TimedOut, "Failure: Resource limit exceeded (time)"),
7.100 + (TimedOut, "time limit exceeded"),
7.101 + (OutOfResources,
7.102 + "# Cannot determine problem status within resource limit"),
7.103 + (OutOfResources, "SZS status: ResourceOut"),
7.104 + (OutOfResources, "SZS status ResourceOut")],
7.105 + max_new_relevant_facts_per_iter = 80 (* FIXME *),
7.106 + prefers_theory_relevant = false,
7.107 + explicit_forall = false}
7.108 +val e = ("e", e_config)
7.109 +
7.110 +
7.111 +(* The "-VarWeight=3" option helps the higher-order problems, probably by
7.112 + counteracting the presence of "hAPP". *)
7.113 +val spass_config : prover_config =
7.114 + {executable = ("ISABELLE_ATP", "scripts/spass"),
7.115 + required_executables = [("SPASS_HOME", "SPASS")],
7.116 + (* "div 2" accounts for the fact that SPASS is often run twice. *)
7.117 + arguments = fn complete => fn timeout =>
7.118 + ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
7.119 + \-VarWeight=3 -TimeLimit=" ^
7.120 + string_of_int (to_generous_secs timeout div 2))
7.121 + |> not complete ? prefix "-SOS=1 ",
7.122 + proof_delims = [("Here is a proof", "Formulae used in the proof")],
7.123 + known_failures =
7.124 + [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
7.125 + (TimedOut, "SPASS beiseite: Ran out of time"),
7.126 + (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
7.127 + (MalformedInput, "Undefined symbol"),
7.128 + (MalformedInput, "Free Variable"),
7.129 + (OldSpass, "tptp2dfg")],
7.130 + max_new_relevant_facts_per_iter = 26 (* FIXME *),
7.131 + prefers_theory_relevant = true,
7.132 + explicit_forall = true}
7.133 +val spass = ("spass", spass_config)
7.134 +
7.135 +(* Vampire *)
7.136 +
7.137 +val vampire_config : prover_config =
7.138 + {executable = ("VAMPIRE_HOME", "vampire"),
7.139 + required_executables = [],
7.140 + arguments = fn _ => fn timeout =>
7.141 + "--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^
7.142 + " --input_file ",
7.143 + proof_delims =
7.144 + [("=========== Refutation ==========",
7.145 + "======= End of refutation ======="),
7.146 + ("% SZS output start Refutation", "% SZS output end Refutation"),
7.147 + ("% SZS output start Proof", "% SZS output end Proof")],
7.148 + known_failures =
7.149 + [(Unprovable, "UNPROVABLE"),
7.150 + (IncompleteUnprovable, "CANNOT PROVE"),
7.151 + (Unprovable, "Satisfiability detected"),
7.152 + (OutOfResources, "Refutation not found")],
7.153 + max_new_relevant_facts_per_iter = 40 (* FIXME *),
7.154 + prefers_theory_relevant = false,
7.155 + explicit_forall = false}
7.156 +val vampire = ("vampire", vampire_config)
7.157 +
7.158 +(* Remote prover invocation via SystemOnTPTP *)
7.159 +
7.160 +val systems = Synchronized.var "atp_systems" ([]: string list)
7.161 +
7.162 +fun get_systems () =
7.163 + case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w" of
7.164 + (answer, 0) => split_lines answer
7.165 + | (answer, _) =>
7.166 + error ("Failed to get available systems at SystemOnTPTP:\n" ^
7.167 + perhaps (try (unsuffix "\n")) answer)
7.168 +
7.169 +fun refresh_systems_on_tptp () =
7.170 + Synchronized.change systems (fn _ => get_systems ())
7.171 +
7.172 +fun get_system prefix = Synchronized.change_result systems (fn systems =>
7.173 + (if null systems then get_systems () else systems)
7.174 + |> `(find_first (String.isPrefix prefix)));
7.175 +
7.176 +fun the_system prefix =
7.177 + (case get_system prefix of
7.178 + NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP.")
7.179 + | SOME sys => sys);
7.180 +
7.181 +val remote_known_failures =
7.182 + [(CantConnect, "HTTP-Error"),
7.183 + (TimedOut, "says Timeout"),
7.184 + (MalformedOutput, "Remote script could not extract proof")]
7.185 +
7.186 +fun remote_config atp_prefix
7.187 + ({proof_delims, known_failures, max_new_relevant_facts_per_iter,
7.188 + prefers_theory_relevant, explicit_forall, ...} : prover_config)
7.189 + : prover_config =
7.190 + {executable = ("ISABELLE_ATP", "scripts/remote_atp"),
7.191 + required_executables = [],
7.192 + arguments = fn _ => fn timeout =>
7.193 + " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
7.194 + the_system atp_prefix,
7.195 + proof_delims = insert (op =) tstp_proof_delims proof_delims,
7.196 + known_failures = remote_known_failures @ known_failures,
7.197 + max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter,
7.198 + prefers_theory_relevant = prefers_theory_relevant,
7.199 + explicit_forall = explicit_forall}
7.200 +
7.201 +val remote_name = prefix "remote_"
7.202 +
7.203 +fun remote_prover (name, config) atp_prefix =
7.204 + (remote_name name, remote_config atp_prefix config)
7.205 +
7.206 +val remote_e = remote_prover e "EP---"
7.207 +val remote_vampire = remote_prover vampire "Vampire---9"
7.208 +
7.209 +fun is_installed ({executable, required_executables, ...} : prover_config) =
7.210 + forall (curry (op <>) "" o getenv o fst) (executable :: required_executables)
7.211 +fun maybe_remote (name, config) =
7.212 + name |> not (is_installed config) ? remote_name
7.213 +
7.214 +fun default_atps_param_value () =
7.215 + space_implode " " ([maybe_remote e] @
7.216 + (if is_installed (snd spass) then [fst spass] else []) @
7.217 + [remote_name (fst vampire)])
7.218 +
7.219 +val provers = [e, spass, vampire, remote_e, remote_vampire]
7.220 +val setup = fold add_prover provers
7.221 +
7.222 +end;
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/HOL/Tools/ATP/etc/settings Wed Jul 28 22:18:35 2010 +0200
8.3 @@ -0,0 +1,1 @@
8.4 +ISABELLE_ATP="$COMPONENT"
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/HOL/Tools/ATP/scripts/remote_atp Wed Jul 28 22:18:35 2010 +0200
9.3 @@ -0,0 +1,109 @@
9.4 +#!/usr/bin/env perl
9.5 +#
9.6 +# Wrapper for custom remote provers on SystemOnTPTP
9.7 +# Author: Fabian Immler, TU Muenchen
9.8 +#
9.9 +
9.10 +use warnings;
9.11 +use strict;
9.12 +use Getopt::Std;
9.13 +use HTTP::Request::Common;
9.14 +use LWP;
9.15 +
9.16 +my $SystemOnTPTPFormReplyURL =
9.17 + "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
9.18 +
9.19 +# default parameters
9.20 +my %URLParameters = (
9.21 + "NoHTML" => 1,
9.22 + "QuietFlag" => "-q01",
9.23 + "SubmitButton" => "RunSelectedSystems",
9.24 + "ProblemSource" => "UPLOAD",
9.25 + "ForceSystem" => "-force",
9.26 + );
9.27 +
9.28 +#----Get format and transform options if specified
9.29 +my %Options;
9.30 +getopts("hws:t:c:",\%Options);
9.31 +
9.32 +#----Usage
9.33 +sub usage() {
9.34 + print("Usage: remote_atp [<options>] <File name>\n");
9.35 + print(" <options> are ...\n");
9.36 + print(" -h - print this help\n");
9.37 + print(" -w - list available ATP systems\n");
9.38 + print(" -s<system> - specified system to use\n");
9.39 + print(" -t<timelimit> - CPU time limit for system\n");
9.40 + print(" -c<command> - custom command for system\n");
9.41 + print(" <File name> - TPTP problem file\n");
9.42 + exit(0);
9.43 +}
9.44 +if (exists($Options{'h'})) {
9.45 + usage();
9.46 +}
9.47 +
9.48 +#----What systems flag
9.49 +if (exists($Options{'w'})) {
9.50 + $URLParameters{"SubmitButton"} = "ListSystems";
9.51 + delete($URLParameters{"ProblemSource"});
9.52 +}
9.53 +
9.54 +#----X2TPTP
9.55 +if (exists($Options{'x'})) {
9.56 + $URLParameters{"X2TPTP"} = "-S";
9.57 +}
9.58 +
9.59 +#----Selected system
9.60 +my $System;
9.61 +if (exists($Options{'s'})) {
9.62 + $System = $Options{'s'};
9.63 +} else {
9.64 + # use Vampire as default
9.65 + $System = "Vampire---9.0";
9.66 +}
9.67 +$URLParameters{"System___$System"} = $System;
9.68 +
9.69 +#----Time limit
9.70 +if (exists($Options{'t'})) {
9.71 + $URLParameters{"TimeLimit___$System"} = $Options{'t'};
9.72 +}
9.73 +#----Custom command
9.74 +if (exists($Options{'c'})) {
9.75 + $URLParameters{"Command___$System"} = $Options{'c'};
9.76 +}
9.77 +
9.78 +#----Get single file name
9.79 +if (exists($URLParameters{"ProblemSource"})) {
9.80 + if (scalar(@ARGV) >= 1) {
9.81 + $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
9.82 + } else {
9.83 + print("Missing problem file\n");
9.84 + usage();
9.85 + die;
9.86 + }
9.87 +}
9.88 +
9.89 +# Query Server
9.90 +my $Agent = LWP::UserAgent->new;
9.91 +if (exists($Options{'t'})) {
9.92 + # give server more time to respond
9.93 + $Agent->timeout($Options{'t'} + 10);
9.94 +}
9.95 +my $Request = POST($SystemOnTPTPFormReplyURL,
9.96 + Content_Type => 'form-data',Content => \%URLParameters);
9.97 +my $Response = $Agent->request($Request);
9.98 +
9.99 +#catch errors / failure
9.100 +if(!$Response->is_success) {
9.101 + print "HTTP-Error: " . $Response->message . "\n";
9.102 + exit(-1);
9.103 +} elsif (exists($Options{'w'})) {
9.104 + print $Response->content;
9.105 + exit (0);
9.106 +} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
9.107 + print "Specified System $1 does not exist\n";
9.108 + exit(-1);
9.109 +} else {
9.110 + print $Response->content;
9.111 + exit(0);
9.112 +}
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/HOL/Tools/ATP/scripts/spass Wed Jul 28 22:18:35 2010 +0200
10.3 @@ -0,0 +1,19 @@
10.4 +#!/usr/bin/env bash
10.5 +#
10.6 +# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for
10.7 +# Isar proof reconstruction)
10.8 +#
10.9 +# Author: Jasmin Blanchette, TU Muenchen
10.10 +
10.11 +options=${@:1:$(($#-1))}
10.12 +name=${@:$(($#)):1}
10.13 +
10.14 +$SPASS_HOME/tptp2dfg $name $name.fof.dfg
10.15 +$SPASS_HOME/SPASS -Flotter $name.fof.dfg \
10.16 + | sed 's/description({$/description({*/' \
10.17 + > $name.cnf.dfg
10.18 +rm -f $name.fof.dfg
10.19 +cat $name.cnf.dfg
10.20 +$SPASS_HOME/SPASS $options $name.cnf.dfg \
10.21 + | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
10.22 +rm -f $name.cnf.dfg
11.1 --- a/src/HOL/Tools/ATP_Manager/SPASS_TPTP Wed Jul 28 11:42:48 2010 +0200
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,19 +0,0 @@
11.4 -#!/usr/bin/env bash
11.5 -#
11.6 -# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for
11.7 -# Isar proof reconstruction)
11.8 -#
11.9 -# Author: Jasmin Blanchette, TU Muenchen
11.10 -
11.11 -options=${@:1:$(($#-1))}
11.12 -name=${@:$(($#)):1}
11.13 -
11.14 -$SPASS_HOME/tptp2dfg $name $name.fof.dfg
11.15 -$SPASS_HOME/SPASS -Flotter $name.fof.dfg \
11.16 - | sed 's/description({$/description({*/' \
11.17 - > $name.cnf.dfg
11.18 -rm -f $name.fof.dfg
11.19 -cat $name.cnf.dfg
11.20 -$SPASS_HOME/SPASS $options $name.cnf.dfg \
11.21 - | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
11.22 -rm -f $name.cnf.dfg
12.1 --- a/src/HOL/Tools/ATP_Manager/SystemOnTPTP Wed Jul 28 11:42:48 2010 +0200
12.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
12.3 @@ -1,142 +0,0 @@
12.4 -#!/usr/bin/env perl
12.5 -#
12.6 -# Wrapper for custom remote provers on SystemOnTPTP
12.7 -# Author: Fabian Immler, TU Muenchen
12.8 -#
12.9 -
12.10 -use warnings;
12.11 -use strict;
12.12 -use Getopt::Std;
12.13 -use HTTP::Request::Common;
12.14 -use LWP;
12.15 -
12.16 -my $SystemOnTPTPFormReplyURL =
12.17 - "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
12.18 -
12.19 -# default parameters
12.20 -my %URLParameters = (
12.21 - "NoHTML" => 1,
12.22 - "QuietFlag" => "-q01",
12.23 - "SubmitButton" => "RunSelectedSystems",
12.24 - "ProblemSource" => "UPLOAD",
12.25 - "ForceSystem" => "-force",
12.26 - );
12.27 -
12.28 -#----Get format and transform options if specified
12.29 -my %Options;
12.30 -getopts("hwxs:t:c:",\%Options);
12.31 -
12.32 -#----Usage
12.33 -sub usage() {
12.34 - print("Usage: remote [<options>] <File name>\n");
12.35 - print(" <options> are ...\n");
12.36 - print(" -h - print this help\n");
12.37 - print(" -w - list available ATP systems\n");
12.38 - print(" -x - use X2TPTP to convert output of prover\n");
12.39 - print(" -s<system> - specified system to use\n");
12.40 - print(" -t<timelimit> - CPU time limit for system\n");
12.41 - print(" -c<command> - custom command for system\n");
12.42 - print(" <File name> - TPTP problem file\n");
12.43 - exit(0);
12.44 -}
12.45 -if (exists($Options{'h'})) {
12.46 - usage();
12.47 -}
12.48 -
12.49 -#----What systems flag
12.50 -if (exists($Options{'w'})) {
12.51 - $URLParameters{"SubmitButton"} = "ListSystems";
12.52 - delete($URLParameters{"ProblemSource"});
12.53 -}
12.54 -
12.55 -#----X2TPTP
12.56 -if (exists($Options{'x'})) {
12.57 - $URLParameters{"X2TPTP"} = "-S";
12.58 -}
12.59 -
12.60 -#----Selected system
12.61 -my $System;
12.62 -if (exists($Options{'s'})) {
12.63 - $System = $Options{'s'};
12.64 -} else {
12.65 - # use Vampire as default
12.66 - $System = "Vampire---9.0";
12.67 -}
12.68 -$URLParameters{"System___$System"} = $System;
12.69 -
12.70 -#----Time limit
12.71 -if (exists($Options{'t'})) {
12.72 - $URLParameters{"TimeLimit___$System"} = $Options{'t'};
12.73 -}
12.74 -#----Custom command
12.75 -if (exists($Options{'c'})) {
12.76 - $URLParameters{"Command___$System"} = $Options{'c'};
12.77 -}
12.78 -
12.79 -#----Get single file name
12.80 -if (exists($URLParameters{"ProblemSource"})) {
12.81 - if (scalar(@ARGV) >= 1) {
12.82 - $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
12.83 - } else {
12.84 - print("Missing problem file\n");
12.85 - usage();
12.86 - die;
12.87 - }
12.88 -}
12.89 -
12.90 -# Query Server
12.91 -my $Agent = LWP::UserAgent->new;
12.92 -if (exists($Options{'t'})) {
12.93 - # give server more time to respond
12.94 - $Agent->timeout($Options{'t'} + 10);
12.95 -}
12.96 -my $Request = POST($SystemOnTPTPFormReplyURL,
12.97 - Content_Type => 'form-data',Content => \%URLParameters);
12.98 -my $Response = $Agent->request($Request);
12.99 -
12.100 -#catch errors / failure
12.101 -if(!$Response->is_success) {
12.102 - print "HTTP-Error: " . $Response->message . "\n";
12.103 - exit(-1);
12.104 -} elsif (exists($Options{'w'})) {
12.105 - print $Response->content;
12.106 - exit (0);
12.107 -} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
12.108 - print "Specified System $1 does not exist\n";
12.109 - exit(-1);
12.110 -} elsif (exists($Options{'x'}) &&
12.111 - $Response->content =~
12.112 - /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&
12.113 - $Response->content !~ /ERROR: Could not form TPTP format derivation/ )
12.114 -{
12.115 - # converted output: extract proof
12.116 - my @lines = split( /\n/, $Response->content);
12.117 - my $extract = "";
12.118 - foreach my $line (@lines){
12.119 - #ignore comments
12.120 - if ($line !~ /^%/ && !($line eq "")) {
12.121 - $extract .= "$line";
12.122 - }
12.123 - }
12.124 - # insert newlines after ').'
12.125 - $extract =~ s/\s//g;
12.126 - $extract =~ s/\)\.cnf/\)\.\ncnf/g;
12.127 -
12.128 - print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n";
12.129 - # orientation for "sledgehammer_proof_reconstruct.ML"
12.130 - print "# SZS output start CNFRefutation.\n";
12.131 - print "$extract\n";
12.132 - print "# SZS output end CNFRefutation.\n";
12.133 - # can be useful for debugging; Isabelle ignores this
12.134 - print "============== original response from SystemOnTPTP: ==============\n";
12.135 - print $Response->content;
12.136 - exit(0);
12.137 -} elsif (!exists($Options{'x'})) {
12.138 - # pass output directly to Isabelle
12.139 - print $Response->content;
12.140 - exit(0);
12.141 -}else {
12.142 - print "Remote script could not extract proof:\n".$Response->content;
12.143 - exit(-1);
12.144 -}
12.145 -
13.1 --- a/src/HOL/Tools/ATP_Manager/async_manager.ML Wed Jul 28 11:42:48 2010 +0200
13.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
13.3 @@ -1,241 +0,0 @@
13.4 -(* Title: HOL/Tools/ATP_Manager/async_manager.ML
13.5 - Author: Fabian Immler, TU Muenchen
13.6 - Author: Makarius
13.7 - Author: Jasmin Blanchette, TU Muenchen
13.8 -
13.9 -Central manager for asynchronous diagnosis tool threads.
13.10 -*)
13.11 -
13.12 -signature ASYNC_MANAGER =
13.13 -sig
13.14 - val launch :
13.15 - string -> bool -> Time.time -> Time.time -> string -> (unit -> string)
13.16 - -> unit
13.17 - val kill_threads : string -> string -> unit
13.18 - val running_threads : string -> string -> unit
13.19 - val thread_messages : string -> string -> int option -> unit
13.20 -end;
13.21 -
13.22 -structure Async_Manager : ASYNC_MANAGER =
13.23 -struct
13.24 -
13.25 -(** preferences **)
13.26 -
13.27 -val message_store_limit = 20;
13.28 -val message_display_limit = 5;
13.29 -
13.30 -
13.31 -(** thread management **)
13.32 -
13.33 -(* data structures over threads *)
13.34 -
13.35 -structure Thread_Heap = Heap
13.36 -(
13.37 - type elem = Time.time * Thread.thread;
13.38 - fun ord ((a, _), (b, _)) = Time.compare (a, b);
13.39 -);
13.40 -
13.41 -fun lookup_thread xs = AList.lookup Thread.equal xs;
13.42 -fun delete_thread xs = AList.delete Thread.equal xs;
13.43 -fun update_thread xs = AList.update Thread.equal xs;
13.44 -
13.45 -
13.46 -(* state of thread manager *)
13.47 -
13.48 -type state =
13.49 - {manager: Thread.thread option,
13.50 - timeout_heap: Thread_Heap.T,
13.51 - active: (Thread.thread * (string * Time.time * Time.time * string)) list,
13.52 - canceling: (Thread.thread * (string * Time.time * string)) list,
13.53 - messages: (string * string) list,
13.54 - store: (string * string) list}
13.55 -
13.56 -fun make_state manager timeout_heap active canceling messages store : state =
13.57 - {manager = manager, timeout_heap = timeout_heap, active = active,
13.58 - canceling = canceling, messages = messages, store = store}
13.59 -
13.60 -val global_state = Synchronized.var "async_manager"
13.61 - (make_state NONE Thread_Heap.empty [] [] [] []);
13.62 -
13.63 -
13.64 -(* unregister thread *)
13.65 -
13.66 -fun unregister verbose message thread =
13.67 - Synchronized.change global_state
13.68 - (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
13.69 - (case lookup_thread active thread of
13.70 - SOME (tool, birth_time, _, desc) =>
13.71 - let
13.72 - val active' = delete_thread thread active;
13.73 - val now = Time.now ()
13.74 - val canceling' = (thread, (tool, now, desc)) :: canceling
13.75 - val message' =
13.76 - desc ^ "\n" ^ message ^
13.77 - (if verbose then
13.78 - "Total time: " ^ Int.toString (Time.toMilliseconds
13.79 - (Time.- (now, birth_time))) ^ " ms.\n"
13.80 - else
13.81 - "")
13.82 - val messages' = (tool, message') :: messages;
13.83 - val store' = (tool, message') ::
13.84 - (if length store <= message_store_limit then store
13.85 - else #1 (chop message_store_limit store));
13.86 - in make_state manager timeout_heap active' canceling' messages' store' end
13.87 - | NONE => state));
13.88 -
13.89 -
13.90 -(* main manager thread -- only one may exist *)
13.91 -
13.92 -val min_wait_time = Time.fromMilliseconds 300;
13.93 -val max_wait_time = Time.fromSeconds 10;
13.94 -
13.95 -fun replace_all bef aft =
13.96 - let
13.97 - fun aux seen "" = String.implode (rev seen)
13.98 - | aux seen s =
13.99 - if String.isPrefix bef s then
13.100 - aux seen "" ^ aft ^ aux [] (unprefix bef s)
13.101 - else
13.102 - aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
13.103 - in aux [] end
13.104 -
13.105 -(* This is a workaround for Proof General's off-by-a-few sendback display bug,
13.106 - whereby "pr" in "proof" is not highlighted. *)
13.107 -fun break_into_chunks xs =
13.108 - maps (space_explode "\000" o replace_all "\n\n" "\000" o snd) xs
13.109 -
13.110 -fun print_new_messages () =
13.111 - case Synchronized.change_result global_state
13.112 - (fn {manager, timeout_heap, active, canceling, messages, store} =>
13.113 - (messages, make_state manager timeout_heap active canceling []
13.114 - store)) of
13.115 - [] => ()
13.116 - | msgs as (tool, _) :: _ =>
13.117 - let val ss = break_into_chunks msgs in
13.118 - List.app priority (tool ^ ": " ^ hd ss :: tl ss)
13.119 - end
13.120 -
13.121 -fun check_thread_manager verbose = Synchronized.change global_state
13.122 - (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
13.123 - if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
13.124 - else let val manager = SOME (Toplevel.thread false (fn () =>
13.125 - let
13.126 - fun time_limit timeout_heap =
13.127 - (case try Thread_Heap.min timeout_heap of
13.128 - NONE => Time.+ (Time.now (), max_wait_time)
13.129 - | SOME (time, _) => time);
13.130 -
13.131 - (*action: find threads whose timeout is reached, and interrupt canceling threads*)
13.132 - fun action {manager, timeout_heap, active, canceling, messages, store} =
13.133 - let val (timeout_threads, timeout_heap') =
13.134 - Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
13.135 - in
13.136 - if null timeout_threads andalso null canceling then
13.137 - NONE
13.138 - else
13.139 - let
13.140 - val _ = List.app (Simple_Thread.interrupt o #1) canceling
13.141 - val canceling' = filter (Thread.isActive o #1) canceling
13.142 - val state' = make_state manager timeout_heap' active canceling' messages store;
13.143 - in SOME (map #2 timeout_threads, state') end
13.144 - end;
13.145 - in
13.146 - while Synchronized.change_result global_state
13.147 - (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
13.148 - if null active andalso null canceling andalso null messages
13.149 - then (false, make_state NONE timeout_heap active canceling messages store)
13.150 - else (true, state))
13.151 - do
13.152 - (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
13.153 - |> these
13.154 - |> List.app (unregister verbose "Timed out.\n");
13.155 - print_new_messages ();
13.156 - (*give threads some time to respond to interrupt*)
13.157 - OS.Process.sleep min_wait_time)
13.158 - end))
13.159 - in make_state manager timeout_heap active canceling messages store end)
13.160 -
13.161 -
13.162 -(* register thread *)
13.163 -
13.164 -fun register tool verbose birth_time death_time desc thread =
13.165 - (Synchronized.change global_state
13.166 - (fn {manager, timeout_heap, active, canceling, messages, store} =>
13.167 - let
13.168 - val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
13.169 - val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active;
13.170 - val state' = make_state manager timeout_heap' active' canceling messages store;
13.171 - in state' end);
13.172 - check_thread_manager verbose);
13.173 -
13.174 -
13.175 -fun launch tool verbose birth_time death_time desc f =
13.176 - (Toplevel.thread true
13.177 - (fn () =>
13.178 - let
13.179 - val self = Thread.self ()
13.180 - val _ = register tool verbose birth_time death_time desc self
13.181 - val message = f ()
13.182 - in unregister verbose message self end);
13.183 - ())
13.184 -
13.185 -
13.186 -(** user commands **)
13.187 -
13.188 -(* kill threads *)
13.189 -
13.190 -fun kill_threads tool workers = Synchronized.change global_state
13.191 - (fn {manager, timeout_heap, active, canceling, messages, store} =>
13.192 - let
13.193 - val killing =
13.194 - map_filter (fn (th, (tool', _, _, desc)) =>
13.195 - if tool' = tool then SOME (th, (tool', Time.now (), desc))
13.196 - else NONE) active
13.197 - val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
13.198 - val _ = if null killing then () else priority ("Killed active " ^ workers ^ ".")
13.199 - in state' end);
13.200 -
13.201 -
13.202 -(* running threads *)
13.203 -
13.204 -fun seconds time = string_of_int (Time.toSeconds time) ^ " s"
13.205 -
13.206 -fun running_threads tool workers =
13.207 - let
13.208 - val {active, canceling, ...} = Synchronized.value global_state;
13.209 -
13.210 - val now = Time.now ();
13.211 - fun running_info (_, (tool', birth_time, death_time, desc)) =
13.212 - if tool' = tool then
13.213 - SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
13.214 - seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc)
13.215 - else
13.216 - NONE
13.217 - fun canceling_info (_, (tool', death_time, desc)) =
13.218 - if tool' = tool then
13.219 - SOME ("Trying to interrupt thread since " ^
13.220 - seconds (Time.- (now, death_time)) ^ ":\n" ^ desc)
13.221 - else
13.222 - NONE
13.223 - val running =
13.224 - case map_filter running_info active of
13.225 - [] => ["No " ^ workers ^ " running."]
13.226 - | ss => "Running " ^ workers ^ ":" :: ss
13.227 - val interrupting =
13.228 - case map_filter canceling_info canceling of
13.229 - [] => []
13.230 - | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss
13.231 - in priority (space_implode "\n\n" (running @ interrupting)) end
13.232 -
13.233 -fun thread_messages tool worker opt_limit =
13.234 - let
13.235 - val limit = the_default message_display_limit opt_limit;
13.236 - val tool_store = Synchronized.value global_state
13.237 - |> #store |> filter (curry (op =) tool o fst)
13.238 - val header =
13.239 - "Recent " ^ worker ^ " messages" ^
13.240 - (if length tool_store <= limit then ":"
13.241 - else " (" ^ string_of_int limit ^ " displayed):");
13.242 - in List.app priority (header :: break_into_chunks (#1 (chop limit tool_store))) end
13.243 -
13.244 -end;
14.1 --- a/src/HOL/Tools/ATP_Manager/atp_problem.ML Wed Jul 28 11:42:48 2010 +0200
14.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
14.3 @@ -1,152 +0,0 @@
14.4 -(* Title: HOL/Tools/ATP_Manager/atp_problem.ML
14.5 - Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
14.6 - Author: Jasmin Blanchette, TU Muenchen
14.7 -
14.8 -TPTP syntax.
14.9 -*)
14.10 -
14.11 -signature ATP_PROBLEM =
14.12 -sig
14.13 - datatype 'a fo_term = ATerm of 'a * 'a fo_term list
14.14 - datatype quantifier = AForall | AExists
14.15 - datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
14.16 - datatype ('a, 'b) formula =
14.17 - AQuant of quantifier * 'a list * ('a, 'b) formula |
14.18 - AConn of connective * ('a, 'b) formula list |
14.19 - APred of 'b
14.20 -
14.21 - datatype kind = Axiom | Conjecture
14.22 - datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
14.23 - type 'a problem = (string * 'a problem_line list) list
14.24 -
14.25 - val timestamp : unit -> string
14.26 - val is_tptp_variable : string -> bool
14.27 - val strings_for_tptp_problem :
14.28 - (string * string problem_line list) list -> string list
14.29 - val nice_tptp_problem :
14.30 - bool -> ('a * (string * string) problem_line list) list
14.31 - -> ('a * string problem_line list) list
14.32 - * (string Symtab.table * string Symtab.table) option
14.33 -end;
14.34 -
14.35 -structure ATP_Problem : ATP_PROBLEM =
14.36 -struct
14.37 -
14.38 -(** ATP problem **)
14.39 -
14.40 -datatype 'a fo_term = ATerm of 'a * 'a fo_term list
14.41 -datatype quantifier = AForall | AExists
14.42 -datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
14.43 -datatype ('a, 'b) formula =
14.44 - AQuant of quantifier * 'a list * ('a, 'b) formula |
14.45 - AConn of connective * ('a, 'b) formula list |
14.46 - APred of 'b
14.47 -
14.48 -datatype kind = Axiom | Conjecture
14.49 -datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
14.50 -type 'a problem = (string * 'a problem_line list) list
14.51 -
14.52 -val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
14.53 -
14.54 -fun string_for_term (ATerm (s, [])) = s
14.55 - | string_for_term (ATerm (s, ts)) =
14.56 - if s = "equal" then space_implode " = " (map string_for_term ts)
14.57 - else s ^ "(" ^ commas (map string_for_term ts) ^ ")"
14.58 -fun string_for_quantifier AForall = "!"
14.59 - | string_for_quantifier AExists = "?"
14.60 -fun string_for_connective ANot = "~"
14.61 - | string_for_connective AAnd = "&"
14.62 - | string_for_connective AOr = "|"
14.63 - | string_for_connective AImplies = "=>"
14.64 - | string_for_connective AIf = "<="
14.65 - | string_for_connective AIff = "<=>"
14.66 - | string_for_connective ANotIff = "<~>"
14.67 -fun string_for_formula (AQuant (q, xs, phi)) =
14.68 - string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^
14.69 - string_for_formula phi
14.70 - | string_for_formula (AConn (ANot, [APred (ATerm ("equal", ts))])) =
14.71 - space_implode " != " (map string_for_term ts)
14.72 - | string_for_formula (AConn (c, [phi])) =
14.73 - string_for_connective c ^ " " ^ string_for_formula phi
14.74 - | string_for_formula (AConn (c, phis)) =
14.75 - "(" ^ space_implode (" " ^ string_for_connective c ^ " ")
14.76 - (map string_for_formula phis) ^ ")"
14.77 - | string_for_formula (APred tm) = string_for_term tm
14.78 -
14.79 -fun string_for_problem_line (Fof (ident, kind, phi)) =
14.80 - "fof(" ^ ident ^ ", " ^
14.81 - (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^
14.82 - " (" ^ string_for_formula phi ^ ")).\n"
14.83 -fun strings_for_tptp_problem problem =
14.84 - "% This file was generated by Isabelle (most likely Sledgehammer)\n\
14.85 - \% " ^ timestamp () ^ "\n" ::
14.86 - maps (fn (_, []) => []
14.87 - | (heading, lines) =>
14.88 - "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" ::
14.89 - map string_for_problem_line lines) problem
14.90 -
14.91 -fun is_tptp_variable s = Char.isUpper (String.sub (s, 0))
14.92 -
14.93 -
14.94 -(** Nice names **)
14.95 -
14.96 -fun empty_name_pool readable_names =
14.97 - if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
14.98 -
14.99 -fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
14.100 -fun pool_map f xs =
14.101 - pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
14.102 -
14.103 -(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the
14.104 - unreadable "op_1", "op_2", etc., in the problem files. *)
14.105 -val reserved_nice_names = ["equal", "op"]
14.106 -fun readable_name full_name s =
14.107 - if s = full_name then
14.108 - s
14.109 - else
14.110 - let
14.111 - val s = s |> Long_Name.base_name
14.112 - |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
14.113 - in if member (op =) reserved_nice_names s then full_name else s end
14.114 -
14.115 -fun nice_name (full_name, _) NONE = (full_name, NONE)
14.116 - | nice_name (full_name, desired_name) (SOME the_pool) =
14.117 - case Symtab.lookup (fst the_pool) full_name of
14.118 - SOME nice_name => (nice_name, SOME the_pool)
14.119 - | NONE =>
14.120 - let
14.121 - val nice_prefix = readable_name full_name desired_name
14.122 - fun add j =
14.123 - let
14.124 - val nice_name = nice_prefix ^
14.125 - (if j = 0 then "" else "_" ^ Int.toString j)
14.126 - in
14.127 - case Symtab.lookup (snd the_pool) nice_name of
14.128 - SOME full_name' =>
14.129 - if full_name = full_name' then (nice_name, the_pool)
14.130 - else add (j + 1)
14.131 - | NONE =>
14.132 - (nice_name,
14.133 - (Symtab.update_new (full_name, nice_name) (fst the_pool),
14.134 - Symtab.update_new (nice_name, full_name) (snd the_pool)))
14.135 - end
14.136 - in add 0 |> apsnd SOME end
14.137 -
14.138 -
14.139 -fun nice_term (ATerm (name, ts)) =
14.140 - nice_name name ##>> pool_map nice_term ts #>> ATerm
14.141 -fun nice_formula (AQuant (q, xs, phi)) =
14.142 - pool_map nice_name xs ##>> nice_formula phi
14.143 - #>> (fn (xs, phi) => AQuant (q, xs, phi))
14.144 - | nice_formula (AConn (c, phis)) =
14.145 - pool_map nice_formula phis #>> curry AConn c
14.146 - | nice_formula (APred tm) = nice_term tm #>> APred
14.147 -fun nice_problem_line (Fof (ident, kind, phi)) =
14.148 - nice_formula phi #>> (fn phi => Fof (ident, kind, phi))
14.149 -fun nice_problem problem =
14.150 - pool_map (fn (heading, lines) =>
14.151 - pool_map nice_problem_line lines #>> pair heading) problem
14.152 -fun nice_tptp_problem readable_names problem =
14.153 - nice_problem problem (empty_name_pool readable_names)
14.154 -
14.155 -end;
15.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Wed Jul 28 11:42:48 2010 +0200
15.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
15.3 @@ -1,216 +0,0 @@
15.4 -(* Title: HOL/Tools/ATP_Manager/atp_systems.ML
15.5 - Author: Fabian Immler, TU Muenchen
15.6 - Author: Jasmin Blanchette, TU Muenchen
15.7 -
15.8 -Setup for supported ATPs.
15.9 -*)
15.10 -
15.11 -signature ATP_SYSTEMS =
15.12 -sig
15.13 - datatype failure =
15.14 - Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
15.15 - OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
15.16 -
15.17 - type prover_config =
15.18 - {home_var: string,
15.19 - executable: string,
15.20 - arguments: bool -> Time.time -> string,
15.21 - proof_delims: (string * string) list,
15.22 - known_failures: (failure * string) list,
15.23 - max_new_relevant_facts_per_iter: int,
15.24 - prefers_theory_relevant: bool,
15.25 - explicit_forall: bool}
15.26 -
15.27 - val add_prover: string * prover_config -> theory -> theory
15.28 - val get_prover: theory -> string -> prover_config
15.29 - val available_atps: theory -> unit
15.30 - val refresh_systems_on_tptp : unit -> unit
15.31 - val default_atps_param_value : unit -> string
15.32 - val setup : theory -> theory
15.33 -end;
15.34 -
15.35 -structure ATP_Systems : ATP_SYSTEMS =
15.36 -struct
15.37 -
15.38 -(* prover configuration *)
15.39 -
15.40 -datatype failure =
15.41 - Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
15.42 - OldSpass | MalformedInput | MalformedOutput | UnknownError
15.43 -
15.44 -type prover_config =
15.45 - {home_var: string,
15.46 - executable: string,
15.47 - arguments: bool -> Time.time -> string,
15.48 - proof_delims: (string * string) list,
15.49 - known_failures: (failure * string) list,
15.50 - max_new_relevant_facts_per_iter: int,
15.51 - prefers_theory_relevant: bool,
15.52 - explicit_forall: bool}
15.53 -
15.54 -
15.55 -(* named provers *)
15.56 -
15.57 -structure Data = Theory_Data
15.58 -(
15.59 - type T = (prover_config * stamp) Symtab.table
15.60 - val empty = Symtab.empty
15.61 - val extend = I
15.62 - fun merge data : T = Symtab.merge (eq_snd op =) data
15.63 - handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
15.64 -)
15.65 -
15.66 -fun add_prover (name, config) thy =
15.67 - Data.map (Symtab.update_new (name, (config, stamp ()))) thy
15.68 - handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
15.69 -
15.70 -fun get_prover thy name =
15.71 - the (Symtab.lookup (Data.get thy) name) |> fst
15.72 - handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
15.73 -
15.74 -fun available_atps thy =
15.75 - priority ("Available ATPs: " ^
15.76 - commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
15.77 -
15.78 -fun available_atps thy =
15.79 - priority ("Available ATPs: " ^
15.80 - commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
15.81 -
15.82 -fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000
15.83 -
15.84 -(* E prover *)
15.85 -
15.86 -val tstp_proof_delims =
15.87 - ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
15.88 -
15.89 -val e_config : prover_config =
15.90 - {home_var = "E_HOME",
15.91 - executable = "eproof",
15.92 - arguments = fn _ => fn timeout =>
15.93 - "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^
15.94 - string_of_int (to_generous_secs timeout),
15.95 - proof_delims = [tstp_proof_delims],
15.96 - known_failures =
15.97 - [(Unprovable, "SZS status: CounterSatisfiable"),
15.98 - (Unprovable, "SZS status CounterSatisfiable"),
15.99 - (TimedOut, "Failure: Resource limit exceeded (time)"),
15.100 - (TimedOut, "time limit exceeded"),
15.101 - (OutOfResources,
15.102 - "# Cannot determine problem status within resource limit"),
15.103 - (OutOfResources, "SZS status: ResourceOut"),
15.104 - (OutOfResources, "SZS status ResourceOut")],
15.105 - max_new_relevant_facts_per_iter = 80 (* FIXME *),
15.106 - prefers_theory_relevant = false,
15.107 - explicit_forall = false}
15.108 -val e = ("e", e_config)
15.109 -
15.110 -
15.111 -(* The "-VarWeight=3" option helps the higher-order problems, probably by
15.112 - counteracting the presence of "hAPP". *)
15.113 -val spass_config : prover_config =
15.114 - {home_var = "ISABELLE_ATP_MANAGER",
15.115 - executable = "SPASS_TPTP",
15.116 - (* "div 2" accounts for the fact that SPASS is often run twice. *)
15.117 - arguments = fn complete => fn timeout =>
15.118 - ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
15.119 - \-VarWeight=3 -TimeLimit=" ^
15.120 - string_of_int (to_generous_secs timeout div 2))
15.121 - |> not complete ? prefix "-SOS=1 ",
15.122 - proof_delims = [("Here is a proof", "Formulae used in the proof")],
15.123 - known_failures =
15.124 - [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
15.125 - (TimedOut, "SPASS beiseite: Ran out of time"),
15.126 - (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
15.127 - (MalformedInput, "Undefined symbol"),
15.128 - (MalformedInput, "Free Variable"),
15.129 - (OldSpass, "tptp2dfg")],
15.130 - max_new_relevant_facts_per_iter = 26 (* FIXME *),
15.131 - prefers_theory_relevant = true,
15.132 - explicit_forall = true}
15.133 -val spass = ("spass", spass_config)
15.134 -
15.135 -(* Vampire *)
15.136 -
15.137 -val vampire_config : prover_config =
15.138 - {home_var = "VAMPIRE_HOME",
15.139 - executable = "vampire",
15.140 - arguments = fn _ => fn timeout =>
15.141 - "--output_syntax tptp --mode casc -t " ^
15.142 - string_of_int (to_generous_secs timeout),
15.143 - proof_delims =
15.144 - [("=========== Refutation ==========",
15.145 - "======= End of refutation ======="),
15.146 - ("% SZS output start Refutation", "% SZS output end Refutation")],
15.147 - known_failures =
15.148 - [(Unprovable, "UNPROVABLE"),
15.149 - (IncompleteUnprovable, "CANNOT PROVE"),
15.150 - (Unprovable, "Satisfiability detected"),
15.151 - (OutOfResources, "Refutation not found")],
15.152 - max_new_relevant_facts_per_iter = 40 (* FIXME *),
15.153 - prefers_theory_relevant = false,
15.154 - explicit_forall = false}
15.155 -val vampire = ("vampire", vampire_config)
15.156 -
15.157 -(* Remote prover invocation via SystemOnTPTP *)
15.158 -
15.159 -val systems = Synchronized.var "atp_systems" ([]: string list)
15.160 -
15.161 -fun get_systems () =
15.162 - case bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" of
15.163 - (answer, 0) => split_lines answer
15.164 - | (answer, _) =>
15.165 - error ("Failed to get available systems at SystemOnTPTP:\n" ^
15.166 - perhaps (try (unsuffix "\n")) answer)
15.167 -
15.168 -fun refresh_systems_on_tptp () =
15.169 - Synchronized.change systems (fn _ => get_systems ())
15.170 -
15.171 -fun get_system prefix = Synchronized.change_result systems (fn systems =>
15.172 - (if null systems then get_systems () else systems)
15.173 - |> `(find_first (String.isPrefix prefix)));
15.174 -
15.175 -fun the_system prefix =
15.176 - (case get_system prefix of
15.177 - NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP.")
15.178 - | SOME sys => sys);
15.179 -
15.180 -val remote_known_failures =
15.181 - [(CantConnect, "HTTP-Error"),
15.182 - (TimedOut, "says Timeout"),
15.183 - (MalformedOutput, "Remote script could not extract proof")]
15.184 -
15.185 -fun remote_config atp_prefix args
15.186 - ({proof_delims, known_failures, max_new_relevant_facts_per_iter,
15.187 - prefers_theory_relevant, explicit_forall, ...} : prover_config)
15.188 - : prover_config =
15.189 - {home_var = "ISABELLE_ATP_MANAGER",
15.190 - executable = "SystemOnTPTP",
15.191 - arguments = fn _ => fn timeout =>
15.192 - args ^ " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
15.193 - the_system atp_prefix,
15.194 - proof_delims = insert (op =) tstp_proof_delims proof_delims,
15.195 - known_failures = remote_known_failures @ known_failures,
15.196 - max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter,
15.197 - prefers_theory_relevant = prefers_theory_relevant,
15.198 - explicit_forall = explicit_forall}
15.199 -
15.200 -val remote_name = prefix "remote_"
15.201 -
15.202 -fun remote_prover prover atp_prefix args config =
15.203 - (remote_name (fst prover), remote_config atp_prefix args config)
15.204 -
15.205 -val remote_e = remote_prover e "EP---" "" e_config
15.206 -val remote_spass = remote_prover spass "SPASS---" "-x" spass_config
15.207 -val remote_vampire = remote_prover vampire "Vampire---9" "" vampire_config
15.208 -
15.209 -fun maybe_remote (name, _) ({home_var, ...} : prover_config) =
15.210 - name |> getenv home_var = "" ? remote_name
15.211 -
15.212 -fun default_atps_param_value () =
15.213 - space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
15.214 - remote_name (fst vampire)]
15.215 -
15.216 -val provers = [e, spass, vampire, remote_e, remote_spass, remote_vampire]
15.217 -val setup = fold add_prover provers
15.218 -
15.219 -end;
16.1 --- a/src/HOL/Tools/ATP_Manager/etc/settings Wed Jul 28 11:42:48 2010 +0200
16.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
16.3 @@ -1,2 +0,0 @@
16.4 -ISABELLE_ATP_MANAGER="$COMPONENT"
16.5 -
17.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Jul 28 11:42:48 2010 +0200
17.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Jul 28 22:18:35 2010 +0200
17.3 @@ -41,7 +41,7 @@
17.4 output: string,
17.5 proof: string,
17.6 internal_thm_names: string Vector.vector,
17.7 - conjecture_shape: int list,
17.8 + conjecture_shape: int list list,
17.9 filtered_clauses: (string * thm) list}
17.10 type prover =
17.11 params -> minimize_command -> Time.time -> problem -> prover_result
17.12 @@ -53,9 +53,9 @@
17.13 val running_atps: unit -> unit
17.14 val messages: int option -> unit
17.15 val get_prover_fun : theory -> string -> prover
17.16 - val start_prover_thread :
17.17 - params -> int -> int -> relevance_override -> (string -> minimize_command)
17.18 - -> Proof.state -> string -> unit
17.19 + val run_sledgehammer :
17.20 + params -> int -> relevance_override -> (string -> minimize_command)
17.21 + -> Proof.state -> unit
17.22 val setup : theory -> theory
17.23 end;
17.24
17.25 @@ -112,7 +112,7 @@
17.26 output: string,
17.27 proof: string,
17.28 internal_thm_names: string Vector.vector,
17.29 - conjecture_shape: int list,
17.30 + conjecture_shape: int list list,
17.31 filtered_clauses: (string * thm) list}
17.32
17.33 type prover =
17.34 @@ -231,7 +231,7 @@
17.35 | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
17.36 do_conn bs AIff t1 t2
17.37 | _ => (fn ts => do_term bs (Envir.eta_contract t)
17.38 - |>> APred ||> union (op =) ts)
17.39 + |>> AAtom ||> union (op =) ts)
17.40 in do_formula [] end
17.41
17.42 (* Converts an elim-rule into an equivalent theorem that does not have the
17.43 @@ -336,7 +336,7 @@
17.44 | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
17.45 fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
17.46 | count_combformula (AConn (_, phis)) = fold count_combformula phis
17.47 - | count_combformula (APred tm) = count_combterm tm
17.48 + | count_combformula (AAtom tm) = count_combterm tm
17.49 fun count_fol_formula (FOLFormula {combformula, ...}) =
17.50 count_combformula combformula
17.51
17.52 @@ -401,11 +401,6 @@
17.53 class_rel_clauses, arity_clauses))
17.54 end
17.55
17.56 -val axiom_prefix = "ax_"
17.57 -val conjecture_prefix = "conj_"
17.58 -val arity_clause_prefix = "clsarity_"
17.59 -val tfrees_name = "tfrees"
17.60 -
17.61 fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
17.62
17.63 fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
17.64 @@ -418,7 +413,7 @@
17.65 | fo_literal_for_type_literal (TyLitFree (class, name)) =
17.66 (true, ATerm (class, [ATerm (name, [])]))
17.67
17.68 -fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot
17.69 +fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
17.70
17.71 fun fo_term_for_combterm full_types =
17.72 let
17.73 @@ -446,7 +441,7 @@
17.74 let
17.75 fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
17.76 | aux (AConn (c, phis)) = AConn (c, map aux phis)
17.77 - | aux (APred tm) = APred (fo_term_for_combterm full_types tm)
17.78 + | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
17.79 in aux end
17.80
17.81 fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
17.82 @@ -463,8 +458,8 @@
17.83 (ClassRelClause {axiom_name, subclass, superclass, ...}) =
17.84 let val ty_arg = ATerm (("T", "T"), []) in
17.85 Fof (ascii_of axiom_name, Axiom,
17.86 - AConn (AImplies, [APred (ATerm (subclass, [ty_arg])),
17.87 - APred (ATerm (superclass, [ty_arg]))]))
17.88 + AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
17.89 + AAtom (ATerm (superclass, [ty_arg]))]))
17.90 end
17.91
17.92 fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
17.93 @@ -515,7 +510,7 @@
17.94 #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
17.95 fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
17.96 | consider_formula (AConn (_, phis)) = fold consider_formula phis
17.97 - | consider_formula (APred tm) = consider_term true tm
17.98 + | consider_formula (AAtom tm) = consider_term true tm
17.99
17.100 fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
17.101 fun consider_problem problem = fold (fold consider_problem_line o snd) problem
17.102 @@ -601,7 +596,7 @@
17.103 fun formula_vars bounds (AQuant (q, xs, phi)) =
17.104 formula_vars (xs @ bounds) phi
17.105 | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
17.106 - | formula_vars bounds (APred tm) = term_vars bounds tm
17.107 + | formula_vars bounds (AAtom tm) = term_vars bounds tm
17.108 in
17.109 case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
17.110 end
17.111 @@ -610,8 +605,8 @@
17.112 let
17.113 fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
17.114 | aux (AConn (c, phis)) = AConn (c, map aux phis)
17.115 - | aux (APred tm) =
17.116 - APred (tm |> repair_applications_in_term thy full_types const_tab
17.117 + | aux (AAtom tm) =
17.118 + AAtom (tm |> repair_applications_in_term thy full_types const_tab
17.119 |> repair_predicates_in_term const_tab)
17.120 in aux #> explicit_forall ? close_universally end
17.121
17.122 @@ -686,15 +681,14 @@
17.123 clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part
17.124 of this hack. *)
17.125 let
17.126 - val j0 = hd conjecture_shape
17.127 + val j0 = hd (hd conjecture_shape)
17.128 val seq = extract_clause_sequence output
17.129 val name_map = extract_clause_formula_relation output
17.130 fun renumber_conjecture j =
17.131 AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0))
17.132 - |> the_single
17.133 - |> (fn s => find_index (curry (op =) s) seq + 1)
17.134 + |> map (fn s => find_index (curry (op =) s) seq + 1)
17.135 in
17.136 - (conjecture_shape |> map renumber_conjecture,
17.137 + (conjecture_shape |> map (maps renumber_conjecture),
17.138 seq |> map (the o AList.lookup (op =) name_map)
17.139 |> map (fn s => case try (unprefix axiom_prefix) s of
17.140 SOME s' => undo_ascii_of s'
17.141 @@ -708,9 +702,9 @@
17.142 (* generic TPTP-based provers *)
17.143
17.144 fun prover_fun name
17.145 - {home_var, executable, arguments, proof_delims, known_failures,
17.146 - max_new_relevant_facts_per_iter, prefers_theory_relevant,
17.147 - explicit_forall}
17.148 + {executable, required_executables, arguments, proof_delims,
17.149 + known_failures, max_new_relevant_facts_per_iter,
17.150 + prefers_theory_relevant, explicit_forall}
17.151 ({debug, overlord, full_types, explicit_apply, relevance_threshold,
17.152 relevance_convergence, theory_relevant, defs_relevant, isar_proof,
17.153 isar_shrink_factor, ...} : params)
17.154 @@ -753,8 +747,7 @@
17.155 else error ("No such directory: " ^ the_dest_dir ^ ".")
17.156 end;
17.157
17.158 - val home = getenv home_var
17.159 - val command = Path.explode (home ^ "/" ^ executable)
17.160 + val command = Path.explode (getenv (fst executable) ^ "/" ^ snd executable)
17.161 (* write out problem file and call prover *)
17.162 fun command_line complete probfile =
17.163 let
17.164 @@ -778,41 +771,45 @@
17.165 val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
17.166 in (output, as_time t) end;
17.167 fun run_on probfile =
17.168 - if home = "" then
17.169 + case filter (curry (op =) "" o getenv o fst)
17.170 + (executable :: required_executables) of
17.171 + (home_var, _) :: _ =>
17.172 error ("The environment variable " ^ quote home_var ^ " is not set.")
17.173 - else if File.exists command then
17.174 - let
17.175 - fun do_run complete =
17.176 - let
17.177 - val command = command_line complete probfile
17.178 - val ((output, msecs), res_code) =
17.179 - bash_output command
17.180 - |>> (if overlord then
17.181 - prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
17.182 - else
17.183 - I)
17.184 - |>> (if Config.get ctxt measure_runtime then split_time
17.185 - else rpair 0)
17.186 - val (proof, outcome) =
17.187 - extract_proof_and_outcome complete res_code proof_delims
17.188 - known_failures output
17.189 - in (output, msecs, proof, outcome) end
17.190 - val readable_names = debug andalso overlord
17.191 - val (pool, conjecture_offset) =
17.192 - write_tptp_file thy readable_names explicit_forall full_types
17.193 - explicit_apply probfile clauses
17.194 - val conjecture_shape =
17.195 - conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
17.196 - val result =
17.197 - do_run false
17.198 - |> (fn (_, msecs0, _, SOME _) =>
17.199 - do_run true
17.200 - |> (fn (output, msecs, proof, outcome) =>
17.201 - (output, msecs0 + msecs, proof, outcome))
17.202 - | result => result)
17.203 - in ((pool, conjecture_shape), result) end
17.204 - else
17.205 - error ("Bad executable: " ^ Path.implode command ^ ".");
17.206 + | [] =>
17.207 + if File.exists command then
17.208 + let
17.209 + fun do_run complete =
17.210 + let
17.211 + val command = command_line complete probfile
17.212 + val ((output, msecs), res_code) =
17.213 + bash_output command
17.214 + |>> (if overlord then
17.215 + prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
17.216 + else
17.217 + I)
17.218 + |>> (if Config.get ctxt measure_runtime then split_time
17.219 + else rpair 0)
17.220 + val (proof, outcome) =
17.221 + extract_proof_and_outcome complete res_code proof_delims
17.222 + known_failures output
17.223 + in (output, msecs, proof, outcome) end
17.224 + val readable_names = debug andalso overlord
17.225 + val (pool, conjecture_offset) =
17.226 + write_tptp_file thy readable_names explicit_forall full_types
17.227 + explicit_apply probfile clauses
17.228 + val conjecture_shape =
17.229 + conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
17.230 + |> map single
17.231 + val result =
17.232 + do_run false
17.233 + |> (fn (_, msecs0, _, SOME _) =>
17.234 + do_run true
17.235 + |> (fn (output, msecs, proof, outcome) =>
17.236 + (output, msecs0 + msecs, proof, outcome))
17.237 + | result => result)
17.238 + in ((pool, conjecture_shape), result) end
17.239 + else
17.240 + error ("Bad executable: " ^ Path.implode command ^ ".")
17.241
17.242 (* If the problem file has not been exported, remove it; otherwise, export
17.243 the proof file too. *)
17.244 @@ -848,7 +845,6 @@
17.245
17.246 fun get_prover_fun thy name = prover_fun name (get_prover thy name)
17.247
17.248 -(* start prover thread *)
17.249 fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n
17.250 relevance_override minimize_command proof_state name =
17.251 let
17.252 @@ -874,6 +870,19 @@
17.253 end)
17.254 end
17.255
17.256 +fun run_sledgehammer {atps = [], ...} _ _ _ _ = error "No ATP is set."
17.257 + | run_sledgehammer (params as {atps, ...}) i relevance_override
17.258 + minimize_command state =
17.259 + case subgoal_count state of
17.260 + 0 => priority "No subgoal!"
17.261 + | n =>
17.262 + let
17.263 + val _ = kill_atps ()
17.264 + val _ = priority "Sledgehammering..."
17.265 + val _ = app (start_prover_thread params i n relevance_override
17.266 + minimize_command state) atps
17.267 + in () end
17.268 +
17.269 val setup =
17.270 dest_dir_setup
17.271 #> problem_prefix_setup
18.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Wed Jul 28 11:42:48 2010 +0200
18.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Wed Jul 28 22:18:35 2010 +0200
18.3 @@ -8,11 +8,11 @@
18.4 signature SLEDGEHAMMER_FACT_MINIMIZER =
18.5 sig
18.6 type params = Sledgehammer.params
18.7 - type prover_result = Sledgehammer.prover_result
18.8
18.9 val minimize_theorems :
18.10 params -> int -> int -> Proof.state -> (string * thm list) list
18.11 -> (string * thm list) list option * string
18.12 + val run_minimizer : params -> int -> Facts.ref list -> Proof.state -> unit
18.13 end;
18.14
18.15 structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
18.16 @@ -20,6 +20,7 @@
18.17
18.18 open Metis_Clauses
18.19 open Sledgehammer_Util
18.20 +open Sledgehammer_Fact_Filter
18.21 open Sledgehammer_Proof_Reconstruct
18.22 open Sledgehammer
18.23
18.24 @@ -38,7 +39,6 @@
18.25 fun sledgehammer_test_theorems (params : params) prover timeout subgoal state
18.26 filtered_clauses name_thms_pairs =
18.27 let
18.28 - val thy = Proof.theory_of state
18.29 val num_theorems = length name_thms_pairs
18.30 val _ =
18.31 priority ("Testing " ^ string_of_int num_theorems ^
18.32 @@ -123,4 +123,17 @@
18.33 handle ERROR msg => (NONE, "Error: " ^ msg)
18.34 end
18.35
18.36 +fun run_minimizer params i refs state =
18.37 + let
18.38 + val ctxt = Proof.context_of state
18.39 + val chained_ths = #facts (Proof.goal state)
18.40 + val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs
18.41 + in
18.42 + case subgoal_count state of
18.43 + 0 => priority "No subgoal!"
18.44 + | n =>
18.45 + (kill_atps ();
18.46 + priority (#2 (minimize_theorems params i n state name_thms_pairs)))
18.47 + end
18.48 +
18.49 end;
19.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 28 11:42:48 2010 +0200
19.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 28 22:18:35 2010 +0200
19.3 @@ -19,7 +19,6 @@
19.4
19.5 open ATP_Systems
19.6 open Sledgehammer_Util
19.7 -open Sledgehammer_Fact_Filter
19.8 open Sledgehammer
19.9 open Sledgehammer_Fact_Minimizer
19.10
19.11 @@ -188,37 +187,8 @@
19.12 fun get_params thy = extract_params (default_raw_params thy)
19.13 fun default_params thy = get_params thy o map (apsnd single)
19.14
19.15 -val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
19.16 -
19.17 (* Sledgehammer the given subgoal *)
19.18
19.19 -fun run {atps = [], ...} _ _ _ _ = error "No ATP is set."
19.20 - | run (params as {atps, ...}) i relevance_override minimize_command state =
19.21 - case subgoal_count state of
19.22 - 0 => priority "No subgoal!"
19.23 - | n =>
19.24 - let
19.25 - val _ = kill_atps ()
19.26 - val _ = priority "Sledgehammering..."
19.27 - val _ = app (start_prover_thread params i n relevance_override
19.28 - minimize_command state) atps
19.29 - in () end
19.30 -
19.31 -fun minimize override_params i refs state =
19.32 - let
19.33 - val thy = Proof.theory_of state
19.34 - val ctxt = Proof.context_of state
19.35 - val chained_ths = #facts (Proof.goal state)
19.36 - val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs
19.37 - in
19.38 - case subgoal_count state of
19.39 - 0 => priority "No subgoal!"
19.40 - | n =>
19.41 - (kill_atps ();
19.42 - priority (#2 (minimize_theorems (get_params thy override_params) i n
19.43 - state name_thms_pairs)))
19.44 - end
19.45 -
19.46 val sledgehammerN = "sledgehammer"
19.47 val sledgehammer_paramsN = "sledgehammer_params"
19.48
19.49 @@ -252,12 +222,13 @@
19.50 in
19.51 if subcommand = runN then
19.52 let val i = the_default 1 opt_i in
19.53 - run (get_params thy override_params) i relevance_override
19.54 - (minimize_command override_params i) state
19.55 + run_sledgehammer (get_params thy override_params) i relevance_override
19.56 + (minimize_command override_params i) state
19.57 end
19.58 else if subcommand = minimizeN then
19.59 - minimize (map (apfst minimizize_raw_param_name) override_params)
19.60 - (the_default 1 opt_i) (#add relevance_override) state
19.61 + run_minimizer (get_params thy (map (apfst minimizize_raw_param_name)
19.62 + override_params))
19.63 + (the_default 1 opt_i) (#add relevance_override) state
19.64 else if subcommand = messagesN then
19.65 messages opt_i
19.66 else if subcommand = available_atpsN then
20.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Jul 28 11:42:48 2010 +0200
20.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Jul 28 22:18:35 2010 +0200
20.3 @@ -10,16 +10,20 @@
20.4 sig
20.5 type minimize_command = string list -> string
20.6
20.7 + val axiom_prefix : string
20.8 + val conjecture_prefix : string
20.9 + val arity_clause_prefix : string
20.10 + val tfrees_name : string
20.11 val metis_line: bool -> int -> int -> string list -> string
20.12 val metis_proof_text:
20.13 bool * minimize_command * string * string vector * thm * int
20.14 -> string * string list
20.15 val isar_proof_text:
20.16 - string Symtab.table * bool * int * Proof.context * int list
20.17 + string Symtab.table * bool * int * Proof.context * int list list
20.18 -> bool * minimize_command * string * string vector * thm * int
20.19 -> string * string list
20.20 val proof_text:
20.21 - bool -> string Symtab.table * bool * int * Proof.context * int list
20.22 + bool -> string Symtab.table * bool * int * Proof.context * int list list
20.23 -> bool * minimize_command * string * string vector * thm * int
20.24 -> string * string list
20.25 end;
20.26 @@ -34,6 +38,11 @@
20.27
20.28 type minimize_command = string list -> string
20.29
20.30 +val axiom_prefix = "ax_"
20.31 +val conjecture_prefix = "conj_"
20.32 +val arity_clause_prefix = "clsarity_"
20.33 +val tfrees_name = "tfrees"
20.34 +
20.35 (* Simple simplifications to ensure that sort annotations don't leave a trail of
20.36 spurious "True"s. *)
20.37 fun s_not @{const False} = @{const True}
20.38 @@ -57,7 +66,8 @@
20.39 | mk_anot phi = AConn (ANot, [phi])
20.40 fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
20.41
20.42 -val index_in_shape : int -> int list -> int = find_index o curry (op =)
20.43 +val index_in_shape : int -> int list list -> int =
20.44 + find_index o exists o curry (op =)
20.45 fun is_axiom_clause_number thm_names num =
20.46 num > 0 andalso num <= Vector.length thm_names andalso
20.47 Vector.sub (thm_names, num - 1) <> ""
20.48 @@ -81,49 +91,66 @@
20.49 Definition of 'a * 'b * 'c |
20.50 Inference of 'a * 'd * 'e list
20.51
20.52 +fun raw_step_number (Definition (num, _, _)) = num
20.53 + | raw_step_number (Inference (num, _, _)) = num
20.54 +
20.55 (**** PARSING OF TSTP FORMAT ****)
20.56
20.57 -datatype int_or_string = Str of string | Int of int
20.58 -
20.59 (*Strings enclosed in single quotes, e.g. filenames*)
20.60 val scan_quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode;
20.61
20.62 val scan_dollar_name =
20.63 Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s)
20.64
20.65 -(* needed for SPASS's output format *)
20.66 fun repair_name _ "$true" = "c_True"
20.67 | repair_name _ "$false" = "c_False"
20.68 | repair_name _ "$$e" = "c_equal" (* seen in Vampire proofs *)
20.69 - | repair_name _ "equal" = "c_equal" (* probably not needed *)
20.70 - | repair_name pool s = Symtab.lookup pool s |> the_default s
20.71 + | repair_name _ "equal" = "c_equal" (* needed by SPASS? *)
20.72 + | repair_name pool s =
20.73 + case Symtab.lookup pool s of
20.74 + SOME s' => s'
20.75 + | NONE =>
20.76 + if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then
20.77 + "c_equal" (* seen in Vampire proofs *)
20.78 + else
20.79 + s
20.80 (* Generalized first-order terms, which include file names, numbers, etc. *)
20.81 -(* The "x" argument is not strictly necessary, but without it Poly/ML loops
20.82 - forever at compile time. *)
20.83 -fun parse_generalized_term x =
20.84 - (scan_quoted >> (fn s => ATerm (Str s, []))
20.85 - || scan_dollar_name
20.86 - -- Scan.optional ($$ "(" |-- parse_generalized_terms --| $$ ")") []
20.87 - >> (fn (s, gs) => ATerm (Str s, gs))
20.88 - || scan_integer >> (fn k => ATerm (Int k, []))
20.89 - || $$ "(" |-- parse_generalized_term --| $$ ")"
20.90 - || $$ "[" |-- Scan.optional parse_generalized_terms [] --| $$ "]"
20.91 - >> curry ATerm (Str "list")) x
20.92 -and parse_generalized_terms x =
20.93 - (parse_generalized_term ::: Scan.repeat ($$ "," |-- parse_generalized_term)) x
20.94 +val parse_potential_integer =
20.95 + (scan_dollar_name || scan_quoted) >> K NONE
20.96 + || scan_integer >> SOME
20.97 +fun parse_annotation x =
20.98 + ((parse_potential_integer ::: Scan.repeat ($$ " " |-- parse_potential_integer)
20.99 + >> map_filter I) -- Scan.optional parse_annotation []
20.100 + >> uncurry (union (op =))
20.101 + || $$ "(" |-- parse_annotations --| $$ ")"
20.102 + || $$ "[" |-- parse_annotations --| $$ "]") x
20.103 +and parse_annotations x =
20.104 + (Scan.optional (parse_annotation
20.105 + ::: Scan.repeat ($$ "," |-- parse_annotation)) []
20.106 + >> (fn numss => fold (union (op =)) numss [])) x
20.107 +
20.108 +(* Vampire proof lines sometimes contain needless information such as "(0:3)",
20.109 + which can be hard to disambiguate from function application in an LL(1)
20.110 + parser. As a workaround, we extend the TPTP term syntax with such detritus
20.111 + and ignore it. *)
20.112 +val parse_vampire_detritus = scan_integer |-- $$ ":" --| scan_integer >> K []
20.113 +
20.114 fun parse_term pool x =
20.115 ((scan_dollar_name >> repair_name pool)
20.116 - -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> ATerm) x
20.117 + -- Scan.optional ($$ "(" |-- (parse_vampire_detritus || parse_terms pool)
20.118 + --| $$ ")") []
20.119 + --| Scan.optional ($$ "(" |-- parse_vampire_detritus --| $$ ")") []
20.120 + >> ATerm) x
20.121 and parse_terms pool x =
20.122 (parse_term pool ::: Scan.repeat ($$ "," |-- parse_term pool)) x
20.123
20.124 -fun parse_predicate_term pool =
20.125 +fun parse_atom pool =
20.126 parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "="
20.127 -- parse_term pool)
20.128 - >> (fn (u, NONE) => APred u
20.129 - | (u1, SOME (NONE, u2)) => APred (ATerm ("c_equal", [u1, u2]))
20.130 + >> (fn (u1, NONE) => AAtom u1
20.131 + | (u1, SOME (NONE, u2)) => AAtom (ATerm ("c_equal", [u1, u2]))
20.132 | (u1, SOME (SOME _, u2)) =>
20.133 - mk_anot (APred (ATerm ("c_equal", [u1, u2]))))
20.134 + mk_anot (AAtom (ATerm ("c_equal", [u1, u2]))))
20.135
20.136 fun fo_term_head (ATerm (s, _)) = s
20.137
20.138 @@ -136,7 +163,7 @@
20.139 -- parse_formula pool
20.140 >> (fn ((q, ts), phi) => AQuant (q, map fo_term_head ts, phi))
20.141 || $$ "~" |-- parse_formula pool >> mk_anot
20.142 - || parse_predicate_term pool)
20.143 + || parse_atom pool)
20.144 -- Scan.option ((Scan.this_string "=>" >> K AImplies
20.145 || Scan.this_string "<=>" >> K AIff
20.146 || Scan.this_string "<~>" >> K ANotIff
20.147 @@ -146,30 +173,34 @@
20.148 >> (fn (phi1, NONE) => phi1
20.149 | (phi1, SOME (c, phi2)) => mk_aconn c (phi1, phi2))) x
20.150
20.151 -fun ints_of_generalized_term (ATerm (label, gs)) =
20.152 - fold ints_of_generalized_term gs #> (case label of Int k => cons k | _ => I)
20.153 -val parse_tstp_annotations =
20.154 - Scan.optional ($$ "," |-- parse_generalized_term
20.155 - --| Scan.option ($$ "," |-- parse_generalized_terms)
20.156 - >> (fn g => ints_of_generalized_term g [])) []
20.157 +val parse_tstp_extra_arguments =
20.158 + Scan.optional ($$ "," |-- parse_annotation
20.159 + --| Scan.option ($$ "," |-- parse_annotations)) []
20.160
20.161 -(* Syntax: (fof|cnf)\(<num>, <formula_role>, <cnf_formula> <annotations>\).
20.162 +(* Syntax: (fof|cnf)\(<num>, <formula_role>, <formula> <extra_arguments>\).
20.163 The <num> could be an identifier, but we assume integers. *)
20.164 fun parse_tstp_line pool =
20.165 ((Scan.this_string "fof" || Scan.this_string "cnf") -- $$ "(")
20.166 |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ","
20.167 - -- parse_formula pool -- parse_tstp_annotations --| $$ ")" --| $$ "."
20.168 + -- parse_formula pool -- parse_tstp_extra_arguments --| $$ ")" --| $$ "."
20.169 >> (fn (((num, role), phi), deps) =>
20.170 case role of
20.171 "definition" =>
20.172 (case phi of
20.173 - AConn (AIff, [phi1 as APred _, phi2]) =>
20.174 + AConn (AIff, [phi1 as AAtom _, phi2]) =>
20.175 Definition (num, phi1, phi2)
20.176 - | APred (ATerm ("$$e", _)) =>
20.177 + | AAtom (ATerm ("c_equal", _)) =>
20.178 Inference (num, phi, deps) (* Vampire's equality proxy axiom *)
20.179 | _ => raise Fail "malformed definition")
20.180 | _ => Inference (num, phi, deps))
20.181
20.182 +(**** PARSING OF VAMPIRE OUTPUT ****)
20.183 +
20.184 +(* Syntax: <num>. <formula> <annotation> *)
20.185 +fun parse_vampire_line pool =
20.186 + scan_integer --| $$ "." -- parse_formula pool -- parse_annotation
20.187 + >> (fn ((num, phi), deps) => Inference (num, phi, deps))
20.188 +
20.189 (**** PARSING OF SPASS OUTPUT ****)
20.190
20.191 (* SPASS returns clause references of the form "x.y". We ignore "y", whose role
20.192 @@ -182,10 +213,10 @@
20.193
20.194 (* It is not clear why some literals are followed by sequences of stars and/or
20.195 pluses. We ignore them. *)
20.196 -fun parse_decorated_predicate_term pool =
20.197 - parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
20.198 +fun parse_decorated_atom pool =
20.199 + parse_atom pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
20.200
20.201 -fun mk_horn ([], []) = APred (ATerm ("c_False", []))
20.202 +fun mk_horn ([], []) = AAtom (ATerm ("c_False", []))
20.203 | mk_horn ([], pos_lits) = foldr1 (mk_aconn AOr) pos_lits
20.204 | mk_horn (neg_lits, []) = mk_anot (foldr1 (mk_aconn AAnd) neg_lits)
20.205 | mk_horn (neg_lits, pos_lits) =
20.206 @@ -193,19 +224,20 @@
20.207 foldr1 (mk_aconn AOr) pos_lits)
20.208
20.209 fun parse_horn_clause pool =
20.210 - Scan.repeat (parse_decorated_predicate_term pool) --| $$ "|" --| $$ "|"
20.211 - -- Scan.repeat (parse_decorated_predicate_term pool) --| $$ "-" --| $$ ">"
20.212 - -- Scan.repeat (parse_decorated_predicate_term pool)
20.213 + Scan.repeat (parse_decorated_atom pool) --| $$ "|" --| $$ "|"
20.214 + -- Scan.repeat (parse_decorated_atom pool) --| $$ "-" --| $$ ">"
20.215 + -- Scan.repeat (parse_decorated_atom pool)
20.216 >> (mk_horn o apfst (op @))
20.217
20.218 (* Syntax: <num>[0:<inference><annotations>]
20.219 - <cnf_formulas> || <cnf_formulas> -> <cnf_formulas>. *)
20.220 + <atoms> || <atoms> -> <atoms>. *)
20.221 fun parse_spass_line pool =
20.222 scan_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
20.223 - -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
20.224 + -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
20.225 >> (fn ((num, deps), u) => Inference (num, u, deps))
20.226
20.227 -fun parse_line pool = parse_tstp_line pool || parse_spass_line pool
20.228 +fun parse_line pool =
20.229 + parse_tstp_line pool || parse_vampire_line pool || parse_spass_line pool
20.230 fun parse_lines pool = Scan.repeat1 (parse_line pool)
20.231 fun parse_proof pool =
20.232 fst o Scan.finite Symbol.stopper
20.233 @@ -395,8 +427,10 @@
20.234 AAnd => s_conj
20.235 | AOr => s_disj
20.236 | AImplies => s_imp
20.237 - | AIff => s_iff)
20.238 - | APred tm => term_from_pred thy full_types tfrees pos tm
20.239 + | AIf => s_imp o swap
20.240 + | AIff => s_iff
20.241 + | ANotIff => s_not o s_iff)
20.242 + | AAtom tm => term_from_pred thy full_types tfrees pos tm
20.243 | _ => raise FORMULA [phi]
20.244 in repair_tvar_sorts (do_formula true phi Vartab.empty) end
20.245
20.246 @@ -438,8 +472,8 @@
20.247 fun decode_lines ctxt full_types tfrees lines =
20.248 fst (fold_map (decode_line full_types tfrees) lines ctxt)
20.249
20.250 -fun aint_actual_inference _ (Definition _) = true
20.251 - | aint_actual_inference t (Inference (_, t', _)) = not (t aconv t')
20.252 +fun is_same_inference _ (Definition _) = false
20.253 + | is_same_inference t (Inference (_, t', _)) = t aconv t'
20.254
20.255 (* No "real" literals means only type information (tfree_tcs, clsrel, or
20.256 clsarity). *)
20.257 @@ -461,7 +495,7 @@
20.258 if is_only_type_information t then
20.259 map (replace_deps_in_line (num, [])) lines
20.260 (* Is there a repetition? If so, replace later line by earlier one. *)
20.261 - else case take_prefix (aint_actual_inference t) lines of
20.262 + else case take_prefix (not o is_same_inference t) lines of
20.263 (_, []) => lines (*no repetition of proof line*)
20.264 | (pre, Inference (num', _, _) :: post) =>
20.265 pre @ map (replace_deps_in_line (num', [num])) post
20.266 @@ -474,9 +508,9 @@
20.267 if is_only_type_information t then
20.268 Inference (num, t, deps) :: lines
20.269 (* Is there a repetition? If so, replace later line by earlier one. *)
20.270 - else case take_prefix (aint_actual_inference t) lines of
20.271 + else case take_prefix (not o is_same_inference t) lines of
20.272 (* FIXME: Doesn't this code risk conflating proofs involving different
20.273 - types?? *)
20.274 + types? *)
20.275 (_, []) => Inference (num, t, deps) :: lines
20.276 | (pre, Inference (num', t', _) :: post) =>
20.277 Inference (num, t', deps) ::
20.278 @@ -522,14 +556,30 @@
20.279 (* A list consisting of the first number in each line is returned. For TSTP,
20.280 interesting lines have the form "fof(108, axiom, ...)", where the number
20.281 (108) is extracted. For SPASS, lines have the form "108[0:Inp] ...", where
20.282 - the first number (108) is extracted. *)
20.283 -fun extract_formula_numbers_in_atp_proof atp_proof =
20.284 + the first number (108) is extracted. For Vampire, we look for
20.285 + "108. ... [input]". *)
20.286 +fun used_facts_in_atp_proof thm_names atp_proof =
20.287 let
20.288 - val tokens_of = String.tokens (not o Char.isAlphaNum)
20.289 - fun extract_num ("fof" :: num :: "axiom" :: _) = Int.fromString num
20.290 - | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num
20.291 - | extract_num _ = NONE
20.292 - in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
20.293 + fun axiom_name num =
20.294 + let val j = Int.fromString num |> the_default ~1 in
20.295 + if is_axiom_clause_number thm_names j then
20.296 + SOME (Vector.sub (thm_names, j - 1))
20.297 + else
20.298 + NONE
20.299 + end
20.300 + val tokens_of =
20.301 + String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
20.302 + val thm_name_list = Vector.foldr (op ::) [] thm_names
20.303 + fun do_line ("fof" :: num :: "axiom" :: (rest as _ :: _)) =
20.304 + (case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of
20.305 + SOME name =>
20.306 + if member (op =) rest "file" then SOME name else axiom_name num
20.307 + | NONE => axiom_name num)
20.308 + | do_line (num :: "0" :: "Inp" :: _) = axiom_name num
20.309 + | do_line (num :: rest) =
20.310 + (case List.last rest of "input" => axiom_name num | _ => NONE)
20.311 + | do_line _ = NONE
20.312 + in atp_proof |> split_lines |> map_filter (do_line o tokens_of) end
20.313
20.314 val indent_size = 2
20.315 val no_label = ("", ~1)
20.316 @@ -560,15 +610,13 @@
20.317 case minimize_command facts of
20.318 "" => ""
20.319 | command =>
20.320 - "To minimize the number of lemmas, try this command: " ^
20.321 + "To minimize the number of lemmas, try this: " ^
20.322 Markup.markup Markup.sendback command ^ ".\n"
20.323
20.324 val unprefix_chained = perhaps (try (unprefix chained_prefix))
20.325
20.326 fun used_facts thm_names =
20.327 - extract_formula_numbers_in_atp_proof
20.328 - #> filter (is_axiom_clause_number thm_names)
20.329 - #> map (fn i => Vector.sub (thm_names, i - 1))
20.330 + used_facts_in_atp_proof thm_names
20.331 #> List.partition (String.isPrefix chained_prefix)
20.332 #>> map (unprefix chained_prefix)
20.333 #> pairself (sort_distinct string_ord)
20.334 @@ -626,8 +674,9 @@
20.335 atp_proof conjecture_shape thm_names params frees =
20.336 let
20.337 val lines =
20.338 - atp_proof ^ "$" (* the $ sign acts as a sentinel (FIXME: pick it up) *)
20.339 + atp_proof ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
20.340 |> parse_proof pool
20.341 + |> sort (int_ord o pairself raw_step_number)
20.342 |> decode_lines ctxt full_types tfrees
20.343 |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
20.344 |> rpair [] |-> fold_rev add_nontrivial_line
20.345 @@ -693,28 +742,37 @@
20.346 conjecture. The second pass flips the proof by contradiction to obtain a
20.347 direct proof, introducing case splits when an inference depends on
20.348 several facts that depend on the negated conjecture. *)
20.349 - fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape)
20.350 - val concl_l = (raw_prefix, List.last conjecture_shape)
20.351 - fun first_pass ([], contra) = ([], contra)
20.352 - | first_pass ((step as Fix _) :: proof, contra) =
20.353 - first_pass (proof, contra) |>> cons step
20.354 - | first_pass ((step as Let _) :: proof, contra) =
20.355 - first_pass (proof, contra) |>> cons step
20.356 - | first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) =
20.357 - if l = concl_l then
20.358 - first_pass (proof, contra ||> l = concl_l ? cons step)
20.359 - else
20.360 - first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
20.361 - | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
20.362 - let val step = Have (qs, l, t, ByMetis (ls, ss)) in
20.363 - if exists (member (op =) (fst contra)) ls then
20.364 - first_pass (proof, contra |>> cons l ||> cons step)
20.365 - else
20.366 - first_pass (proof, contra) |>> cons step
20.367 - end
20.368 - | first_pass _ = raise Fail "malformed proof"
20.369 + fun find_hyp num =
20.370 + nth hyp_ts (index_in_shape num conjecture_shape)
20.371 + handle Subscript =>
20.372 + raise Fail ("Cannot find hypothesis " ^ Int.toString num)
20.373 + val concl_ls = map (pair raw_prefix) (List.last conjecture_shape)
20.374 + val canonicalize_labels =
20.375 + map (fn l => if member (op =) concl_ls l then hd concl_ls else l)
20.376 + #> distinct (op =)
20.377 + fun first_pass ([], contra) = ([], contra)
20.378 + | first_pass ((step as Fix _) :: proof, contra) =
20.379 + first_pass (proof, contra) |>> cons step
20.380 + | first_pass ((step as Let _) :: proof, contra) =
20.381 + first_pass (proof, contra) |>> cons step
20.382 + | first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) =
20.383 + if member (op =) concl_ls l then
20.384 + first_pass (proof, contra ||> l = hd concl_ls ? cons step)
20.385 + else
20.386 + first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
20.387 + | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
20.388 + let
20.389 + val ls = canonicalize_labels ls
20.390 + val step = Have (qs, l, t, ByMetis (ls, ss))
20.391 + in
20.392 + if exists (member (op =) (fst contra)) ls then
20.393 + first_pass (proof, contra |>> cons l ||> cons step)
20.394 + else
20.395 + first_pass (proof, contra) |>> cons step
20.396 + end
20.397 + | first_pass _ = raise Fail "malformed proof"
20.398 val (proof_top, (contra_ls, contra_proof)) =
20.399 - first_pass (proof, ([concl_l], []))
20.400 + first_pass (proof, (concl_ls, []))
20.401 val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
20.402 fun backpatch_labels patches ls =
20.403 fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
20.404 @@ -749,7 +807,7 @@
20.405 val proofs =
20.406 map_filter
20.407 (fn l =>
20.408 - if l = concl_l then
20.409 + if member (op =) concl_ls l then
20.410 NONE
20.411 else
20.412 let
20.413 @@ -953,7 +1011,7 @@
20.414 |> kill_useless_labels_in_proof
20.415 |> relabel_proof
20.416 |> string_for_proof ctxt full_types i n of
20.417 - "" => ""
20.418 + "" => "No structured proof available.\n"
20.419 | proof => "\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
20.420 val isar_proof =
20.421 if debug then
21.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 28 11:42:48 2010 +0200
21.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 28 22:18:35 2010 +0200
21.3 @@ -17,6 +17,7 @@
21.4 val maybe_quote : string -> string
21.5 val monomorphic_term : Type.tyenv -> term -> term
21.6 val specialize_type : theory -> (string * typ) -> term -> term
21.7 + val subgoal_count : Proof.state -> int
21.8 val strip_subgoal : thm -> int -> (string * typ) list * term list * term
21.9 end;
21.10
21.11 @@ -124,6 +125,8 @@
21.12 | NONE => raise Type.TYPE_MATCH
21.13 end
21.14
21.15 +val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
21.16 +
21.17 fun strip_subgoal goal i =
21.18 let
21.19 val (t, frees) = Logic.goal_params (prop_of goal) i