--- a/doc-src/Sledgehammer/sledgehammer.tex Wed Jul 28 11:42:48 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Jul 28 22:18:35 2010 +0200
@@ -121,28 +121,33 @@
\cite{sutcliffe-2000}, but if you want better performance you will need to
install at least E and SPASS locally.
-There are three main ways to install E and SPASS:
+There are three main ways to install ATPs on your machine:
\begin{enum}
\item[$\bullet$] If you installed an official Isabelle package with everything
inside, it should already include properly setup executables for E and SPASS,
-ready to use.
+ready to use.%
+\footnote{Vampire's license prevents us from doing the same for this otherwise
+wonderful tool.}
-\item[$\bullet$] Otherwise, you can download the Isabelle-aware E and SPASS
+\item[$\bullet$] Alternatively, you can download the Isabelle-aware E and SPASS
binary packages from Isabelle's download page. Extract the archives, then add a
line to your \texttt{\char`\~/.isabelle/etc/components} file with the absolute path to
-E or SPASS. For example, if \texttt{\char`\~/.isabelle/etc/components} does not exist
+E or SPASS. For example, if the \texttt{components} does not exist
yet and you extracted SPASS to \texttt{/usr/local/spass-3.7}, create
-the file \texttt{\char`\~/.isabelle/etc/components} with the single line
+the \texttt{components} file with the single line
\prew
\texttt{/usr/local/spass-3.7}
\postw
-\item[$\bullet$] If you prefer to build E or SPASS yourself, feel free to do so
-and set the environment variable \texttt{E\_HOME} or \texttt{SPASS\_HOME} to the
-directory that contains the \texttt{eproof} or \texttt{SPASS} executable,
-respectively.
+in it.
+
+\item[$\bullet$] If you prefer to build E or SPASS yourself, or obtained a
+Vampire executable from somewhere (e.g., \url{http://www.vprover.org/}),
+set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
+\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
+\texttt{SPASS}, or \texttt{vampire} executable.
\end{enum}
To check whether E and SPASS are installed, follow the example in
@@ -176,29 +181,29 @@
Sledgehammer: ATP ``\textit{e}'' for subgoal 1: \\
$([a] = [b]) = (a = b)$ \\
Try this command: \textbf{by} (\textit{metis hd.simps}). \\
-To minimize the number of lemmas, try this command: \\
+To minimize the number of lemmas, try this: \\
\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount]
%
Sledgehammer: ATP ``\textit{spass}'' for subgoal 1: \\
$([a] = [b]) = (a = b)$ \\
Try this command: \textbf{by} (\textit{metis insert\_Nil last\_ConsL}). \\
-To minimize the number of lemmas, try this command: \\
+To minimize the number of lemmas, try this: \\
\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount]
%
Sledgehammer: ATP ``\textit{remote\_vampire}'' for subgoal 1: \\
$([a] = [b]) = (a = b)$ \\
Try this command: \textbf{by} (\textit{metis One\_nat\_def\_raw empty\_replicate} \\
\phantom{Try this command: \textbf{by} (\textit{metis~}}\textit{insert\_Nil last\_ConsL replicate\_Suc}). \\
-To minimize the number of lemmas, try this command: \\
+To minimize the number of lemmas, try this: \\
\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{remote\_vampire}] \\
\phantom{\textbf{sledgehammer}~}(\textit{One\_nat\_def\_raw empty\_replicate insert\_Nil} \\
\phantom{\textbf{sledgehammer}~(}\textit{last\_ConsL replicate\_Suc}).
\postw
Sledgehammer ran E, SPASS, and the remote version of Vampire in parallel. If E
-and SPASS are not installed (\S\ref{installation}), you will see references to
-their remote American cousins \textit{remote\_e} and \textit{remote\_spass}
-instead of \textit{e} and \textit{spass}.
+is not installed (\S\ref{installation}), you will see references to
+its remote American cousin \textit{remote\_e} instead of
+\textit{e}; and if SPASS is not installed, it will not appear in the output.
Based on each ATP proof, Sledgehammer gives a one-liner proof that uses the
\textit{metis} method. You can click them and insert them into the theory text.
@@ -377,9 +382,6 @@
\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E executes
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
-\item[$\bullet$] \textbf{\textit{remote\_spass}:} The remote version of SPASS
-executes on Geoff Sutcliffe's Miami servers.
-
\item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
Vampire executes on Geoff Sutcliffe's Miami servers. Version 9 is used.
--- a/etc/components Wed Jul 28 11:42:48 2010 +0200
+++ b/etc/components Wed Jul 28 22:18:35 2010 +0200
@@ -13,7 +13,7 @@
#misc components
src/Tools/Code
src/Tools/WWW_Find
-src/HOL/Tools/ATP_Manager
+src/HOL/Tools/ATP
src/HOL/Mirabelle
src/HOL/Library/Sum_Of_Squares
src/HOL/Tools/SMT
--- a/src/HOL/IsaMakefile Wed Jul 28 11:42:48 2010 +0200
+++ b/src/HOL/IsaMakefile Wed Jul 28 22:18:35 2010 +0200
@@ -268,9 +268,9 @@
$(SRC)/Provers/Arith/combine_numerals.ML \
$(SRC)/Provers/Arith/extract_common_term.ML \
$(SRC)/Tools/Metis/metis.ML \
- Tools/ATP_Manager/async_manager.ML \
- Tools/ATP_Manager/atp_problem.ML \
- Tools/ATP_Manager/atp_systems.ML \
+ Tools/ATP/async_manager.ML \
+ Tools/ATP/atp_problem.ML \
+ Tools/ATP/atp_systems.ML \
Tools/choice_specification.ML \
Tools/int_arith.ML \
Tools/groebner.ML \
--- a/src/HOL/Sledgehammer.thy Wed Jul 28 11:42:48 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Wed Jul 28 22:18:35 2010 +0200
@@ -10,9 +10,9 @@
theory Sledgehammer
imports Plain Hilbert_Choice
uses
- ("Tools/ATP_Manager/async_manager.ML")
- ("Tools/ATP_Manager/atp_problem.ML")
- ("Tools/ATP_Manager/atp_systems.ML")
+ ("Tools/ATP/async_manager.ML")
+ ("Tools/ATP/atp_problem.ML")
+ ("Tools/ATP/atp_systems.ML")
("~~/src/Tools/Metis/metis.ML")
("Tools/Sledgehammer/clausifier.ML")
("Tools/Sledgehammer/meson_tactic.ML")
@@ -85,9 +85,9 @@
apply (simp add: COMBC_def)
done
-use "Tools/ATP_Manager/async_manager.ML"
-use "Tools/ATP_Manager/atp_problem.ML"
-use "Tools/ATP_Manager/atp_systems.ML"
+use "Tools/ATP/async_manager.ML"
+use "Tools/ATP/atp_problem.ML"
+use "Tools/ATP/atp_systems.ML"
setup ATP_Systems.setup
use "~~/src/Tools/Metis/metis.ML"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/async_manager.ML Wed Jul 28 22:18:35 2010 +0200
@@ -0,0 +1,241 @@
+(* Title: HOL/Tools/ATP/async_manager.ML
+ Author: Fabian Immler, TU Muenchen
+ Author: Makarius
+ Author: Jasmin Blanchette, TU Muenchen
+
+Central manager for asynchronous diagnosis tool threads.
+*)
+
+signature ASYNC_MANAGER =
+sig
+ val launch :
+ string -> bool -> Time.time -> Time.time -> string -> (unit -> string)
+ -> unit
+ val kill_threads : string -> string -> unit
+ val running_threads : string -> string -> unit
+ val thread_messages : string -> string -> int option -> unit
+end;
+
+structure Async_Manager : ASYNC_MANAGER =
+struct
+
+(** preferences **)
+
+val message_store_limit = 20;
+val message_display_limit = 5;
+
+
+(** thread management **)
+
+(* data structures over threads *)
+
+structure Thread_Heap = Heap
+(
+ type elem = Time.time * Thread.thread;
+ fun ord ((a, _), (b, _)) = Time.compare (a, b);
+);
+
+fun lookup_thread xs = AList.lookup Thread.equal xs;
+fun delete_thread xs = AList.delete Thread.equal xs;
+fun update_thread xs = AList.update Thread.equal xs;
+
+
+(* state of thread manager *)
+
+type state =
+ {manager: Thread.thread option,
+ timeout_heap: Thread_Heap.T,
+ active: (Thread.thread * (string * Time.time * Time.time * string)) list,
+ canceling: (Thread.thread * (string * Time.time * string)) list,
+ messages: (string * string) list,
+ store: (string * string) list}
+
+fun make_state manager timeout_heap active canceling messages store : state =
+ {manager = manager, timeout_heap = timeout_heap, active = active,
+ canceling = canceling, messages = messages, store = store}
+
+val global_state = Synchronized.var "async_manager"
+ (make_state NONE Thread_Heap.empty [] [] [] []);
+
+
+(* unregister thread *)
+
+fun unregister verbose message thread =
+ Synchronized.change global_state
+ (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
+ (case lookup_thread active thread of
+ SOME (tool, birth_time, _, desc) =>
+ let
+ val active' = delete_thread thread active;
+ val now = Time.now ()
+ val canceling' = (thread, (tool, now, desc)) :: canceling
+ val message' =
+ desc ^ "\n" ^ message ^
+ (if verbose then
+ "Total time: " ^ Int.toString (Time.toMilliseconds
+ (Time.- (now, birth_time))) ^ " ms.\n"
+ else
+ "")
+ val messages' = (tool, message') :: messages;
+ val store' = (tool, message') ::
+ (if length store <= message_store_limit then store
+ else #1 (chop message_store_limit store));
+ in make_state manager timeout_heap active' canceling' messages' store' end
+ | NONE => state));
+
+
+(* main manager thread -- only one may exist *)
+
+val min_wait_time = Time.fromMilliseconds 300;
+val max_wait_time = Time.fromSeconds 10;
+
+fun replace_all bef aft =
+ let
+ fun aux seen "" = String.implode (rev seen)
+ | aux seen s =
+ if String.isPrefix bef s then
+ aux seen "" ^ aft ^ aux [] (unprefix bef s)
+ else
+ aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
+ in aux [] end
+
+(* This is a workaround for Proof General's off-by-a-few sendback display bug,
+ whereby "pr" in "proof" is not highlighted. *)
+fun break_into_chunks xs =
+ maps (space_explode "\000" o replace_all "\n\n" "\000" o snd) xs
+
+fun print_new_messages () =
+ case Synchronized.change_result global_state
+ (fn {manager, timeout_heap, active, canceling, messages, store} =>
+ (messages, make_state manager timeout_heap active canceling []
+ store)) of
+ [] => ()
+ | msgs as (tool, _) :: _ =>
+ let val ss = break_into_chunks msgs in
+ List.app priority (tool ^ ": " ^ hd ss :: tl ss)
+ end
+
+fun check_thread_manager verbose = Synchronized.change global_state
+ (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
+ if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
+ else let val manager = SOME (Toplevel.thread false (fn () =>
+ let
+ fun time_limit timeout_heap =
+ (case try Thread_Heap.min timeout_heap of
+ NONE => Time.+ (Time.now (), max_wait_time)
+ | SOME (time, _) => time);
+
+ (*action: find threads whose timeout is reached, and interrupt canceling threads*)
+ fun action {manager, timeout_heap, active, canceling, messages, store} =
+ let val (timeout_threads, timeout_heap') =
+ Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
+ in
+ if null timeout_threads andalso null canceling then
+ NONE
+ else
+ let
+ val _ = List.app (Simple_Thread.interrupt o #1) canceling
+ val canceling' = filter (Thread.isActive o #1) canceling
+ val state' = make_state manager timeout_heap' active canceling' messages store;
+ in SOME (map #2 timeout_threads, state') end
+ end;
+ in
+ while Synchronized.change_result global_state
+ (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
+ if null active andalso null canceling andalso null messages
+ then (false, make_state NONE timeout_heap active canceling messages store)
+ else (true, state))
+ do
+ (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
+ |> these
+ |> List.app (unregister verbose "Timed out.\n");
+ print_new_messages ();
+ (*give threads some time to respond to interrupt*)
+ OS.Process.sleep min_wait_time)
+ end))
+ in make_state manager timeout_heap active canceling messages store end)
+
+
+(* register thread *)
+
+fun register tool verbose birth_time death_time desc thread =
+ (Synchronized.change global_state
+ (fn {manager, timeout_heap, active, canceling, messages, store} =>
+ let
+ val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
+ val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active;
+ val state' = make_state manager timeout_heap' active' canceling messages store;
+ in state' end);
+ check_thread_manager verbose);
+
+
+fun launch tool verbose birth_time death_time desc f =
+ (Toplevel.thread true
+ (fn () =>
+ let
+ val self = Thread.self ()
+ val _ = register tool verbose birth_time death_time desc self
+ val message = f ()
+ in unregister verbose message self end);
+ ())
+
+
+(** user commands **)
+
+(* kill threads *)
+
+fun kill_threads tool workers = Synchronized.change global_state
+ (fn {manager, timeout_heap, active, canceling, messages, store} =>
+ let
+ val killing =
+ map_filter (fn (th, (tool', _, _, desc)) =>
+ if tool' = tool then SOME (th, (tool', Time.now (), desc))
+ else NONE) active
+ val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
+ val _ = if null killing then () else priority ("Killed active " ^ workers ^ ".")
+ in state' end);
+
+
+(* running threads *)
+
+fun seconds time = string_of_int (Time.toSeconds time) ^ " s"
+
+fun running_threads tool workers =
+ let
+ val {active, canceling, ...} = Synchronized.value global_state;
+
+ val now = Time.now ();
+ fun running_info (_, (tool', birth_time, death_time, desc)) =
+ if tool' = tool then
+ SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
+ seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc)
+ else
+ NONE
+ fun canceling_info (_, (tool', death_time, desc)) =
+ if tool' = tool then
+ SOME ("Trying to interrupt thread since " ^
+ seconds (Time.- (now, death_time)) ^ ":\n" ^ desc)
+ else
+ NONE
+ val running =
+ case map_filter running_info active of
+ [] => ["No " ^ workers ^ " running."]
+ | ss => "Running " ^ workers ^ ":" :: ss
+ val interrupting =
+ case map_filter canceling_info canceling of
+ [] => []
+ | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss
+ in priority (space_implode "\n\n" (running @ interrupting)) end
+
+fun thread_messages tool worker opt_limit =
+ let
+ val limit = the_default message_display_limit opt_limit;
+ val tool_store = Synchronized.value global_state
+ |> #store |> filter (curry (op =) tool o fst)
+ val header =
+ "Recent " ^ worker ^ " messages" ^
+ (if length tool_store <= limit then ":"
+ else " (" ^ string_of_int limit ^ " displayed):");
+ in List.app priority (header :: break_into_chunks (#1 (chop limit tool_store))) end
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Jul 28 22:18:35 2010 +0200
@@ -0,0 +1,152 @@
+(* Title: HOL/Tools/ATP/atp_problem.ML
+ Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
+ Author: Jasmin Blanchette, TU Muenchen
+
+TPTP syntax.
+*)
+
+signature ATP_PROBLEM =
+sig
+ datatype 'a fo_term = ATerm of 'a * 'a fo_term list
+ datatype quantifier = AForall | AExists
+ datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
+ datatype ('a, 'b) formula =
+ AQuant of quantifier * 'a list * ('a, 'b) formula |
+ AConn of connective * ('a, 'b) formula list |
+ AAtom of 'b
+
+ datatype kind = Axiom | Conjecture
+ datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
+ type 'a problem = (string * 'a problem_line list) list
+
+ val timestamp : unit -> string
+ val is_tptp_variable : string -> bool
+ val strings_for_tptp_problem :
+ (string * string problem_line list) list -> string list
+ val nice_tptp_problem :
+ bool -> ('a * (string * string) problem_line list) list
+ -> ('a * string problem_line list) list
+ * (string Symtab.table * string Symtab.table) option
+end;
+
+structure ATP_Problem : ATP_PROBLEM =
+struct
+
+(** ATP problem **)
+
+datatype 'a fo_term = ATerm of 'a * 'a fo_term list
+datatype quantifier = AForall | AExists
+datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
+datatype ('a, 'b) formula =
+ AQuant of quantifier * 'a list * ('a, 'b) formula |
+ AConn of connective * ('a, 'b) formula list |
+ AAtom of 'b
+
+datatype kind = Axiom | Conjecture
+datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
+type 'a problem = (string * 'a problem_line list) list
+
+val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
+
+fun string_for_term (ATerm (s, [])) = s
+ | string_for_term (ATerm (s, ts)) =
+ if s = "equal" then space_implode " = " (map string_for_term ts)
+ else s ^ "(" ^ commas (map string_for_term ts) ^ ")"
+fun string_for_quantifier AForall = "!"
+ | string_for_quantifier AExists = "?"
+fun string_for_connective ANot = "~"
+ | string_for_connective AAnd = "&"
+ | string_for_connective AOr = "|"
+ | string_for_connective AImplies = "=>"
+ | string_for_connective AIf = "<="
+ | string_for_connective AIff = "<=>"
+ | string_for_connective ANotIff = "<~>"
+fun string_for_formula (AQuant (q, xs, phi)) =
+ string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^
+ string_for_formula phi
+ | string_for_formula (AConn (ANot, [AAtom (ATerm ("equal", ts))])) =
+ space_implode " != " (map string_for_term ts)
+ | string_for_formula (AConn (c, [phi])) =
+ string_for_connective c ^ " " ^ string_for_formula phi
+ | string_for_formula (AConn (c, phis)) =
+ "(" ^ space_implode (" " ^ string_for_connective c ^ " ")
+ (map string_for_formula phis) ^ ")"
+ | string_for_formula (AAtom tm) = string_for_term tm
+
+fun string_for_problem_line (Fof (ident, kind, phi)) =
+ "fof(" ^ ident ^ ", " ^
+ (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^
+ " (" ^ string_for_formula phi ^ ")).\n"
+fun strings_for_tptp_problem problem =
+ "% This file was generated by Isabelle (most likely Sledgehammer)\n\
+ \% " ^ timestamp () ^ "\n" ::
+ maps (fn (_, []) => []
+ | (heading, lines) =>
+ "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" ::
+ map string_for_problem_line lines) problem
+
+fun is_tptp_variable s = Char.isUpper (String.sub (s, 0))
+
+
+(** Nice names **)
+
+fun empty_name_pool readable_names =
+ if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
+
+fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
+fun pool_map f xs =
+ pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
+
+(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the
+ unreadable "op_1", "op_2", etc., in the problem files. *)
+val reserved_nice_names = ["equal", "op"]
+fun readable_name full_name s =
+ if s = full_name then
+ s
+ else
+ let
+ val s = s |> Long_Name.base_name
+ |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
+ in if member (op =) reserved_nice_names s then full_name else s end
+
+fun nice_name (full_name, _) NONE = (full_name, NONE)
+ | nice_name (full_name, desired_name) (SOME the_pool) =
+ case Symtab.lookup (fst the_pool) full_name of
+ SOME nice_name => (nice_name, SOME the_pool)
+ | NONE =>
+ let
+ val nice_prefix = readable_name full_name desired_name
+ fun add j =
+ let
+ val nice_name = nice_prefix ^
+ (if j = 0 then "" else "_" ^ Int.toString j)
+ in
+ case Symtab.lookup (snd the_pool) nice_name of
+ SOME full_name' =>
+ if full_name = full_name' then (nice_name, the_pool)
+ else add (j + 1)
+ | NONE =>
+ (nice_name,
+ (Symtab.update_new (full_name, nice_name) (fst the_pool),
+ Symtab.update_new (nice_name, full_name) (snd the_pool)))
+ end
+ in add 0 |> apsnd SOME end
+
+
+fun nice_term (ATerm (name, ts)) =
+ nice_name name ##>> pool_map nice_term ts #>> ATerm
+fun nice_formula (AQuant (q, xs, phi)) =
+ pool_map nice_name xs ##>> nice_formula phi
+ #>> (fn (xs, phi) => AQuant (q, xs, phi))
+ | nice_formula (AConn (c, phis)) =
+ pool_map nice_formula phis #>> curry AConn c
+ | nice_formula (AAtom tm) = nice_term tm #>> AAtom
+fun nice_problem_line (Fof (ident, kind, phi)) =
+ nice_formula phi #>> (fn phi => Fof (ident, kind, phi))
+fun nice_problem problem =
+ pool_map (fn (heading, lines) =>
+ pool_map nice_problem_line lines #>> pair heading) problem
+fun nice_tptp_problem readable_names problem =
+ nice_problem problem (empty_name_pool readable_names)
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Jul 28 22:18:35 2010 +0200
@@ -0,0 +1,219 @@
+(* Title: HOL/Tools/ATP/atp_systems.ML
+ Author: Fabian Immler, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
+
+Setup for supported ATPs.
+*)
+
+signature ATP_SYSTEMS =
+sig
+ datatype failure =
+ Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
+ OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
+
+ type prover_config =
+ {executable: string * string,
+ required_executables: (string * string) list,
+ arguments: bool -> Time.time -> string,
+ proof_delims: (string * string) list,
+ known_failures: (failure * string) list,
+ max_new_relevant_facts_per_iter: int,
+ prefers_theory_relevant: bool,
+ explicit_forall: bool}
+
+ val add_prover: string * prover_config -> theory -> theory
+ val get_prover: theory -> string -> prover_config
+ val available_atps: theory -> unit
+ val refresh_systems_on_tptp : unit -> unit
+ val default_atps_param_value : unit -> string
+ val setup : theory -> theory
+end;
+
+structure ATP_Systems : ATP_SYSTEMS =
+struct
+
+(* prover configuration *)
+
+datatype failure =
+ Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
+ OldSpass | MalformedInput | MalformedOutput | UnknownError
+
+type prover_config =
+ {executable: string * string,
+ required_executables: (string * string) list,
+ arguments: bool -> Time.time -> string,
+ proof_delims: (string * string) list,
+ known_failures: (failure * string) list,
+ max_new_relevant_facts_per_iter: int,
+ prefers_theory_relevant: bool,
+ explicit_forall: bool}
+
+
+(* named provers *)
+
+structure Data = Theory_Data
+(
+ type T = (prover_config * stamp) Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ fun merge data : T = Symtab.merge (eq_snd op =) data
+ handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
+)
+
+fun add_prover (name, config) thy =
+ Data.map (Symtab.update_new (name, (config, stamp ()))) thy
+ handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
+
+fun get_prover thy name =
+ the (Symtab.lookup (Data.get thy) name) |> fst
+ handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
+
+fun available_atps thy =
+ priority ("Available ATPs: " ^
+ commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
+
+fun available_atps thy =
+ priority ("Available ATPs: " ^
+ commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
+
+fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000
+
+(* E prover *)
+
+val tstp_proof_delims =
+ ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
+
+val e_config : prover_config =
+ {executable = ("E_HOME", "eproof"),
+ required_executables = [],
+ arguments = fn _ => fn timeout =>
+ "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^
+ string_of_int (to_generous_secs timeout),
+ proof_delims = [tstp_proof_delims],
+ known_failures =
+ [(Unprovable, "SZS status: CounterSatisfiable"),
+ (Unprovable, "SZS status CounterSatisfiable"),
+ (TimedOut, "Failure: Resource limit exceeded (time)"),
+ (TimedOut, "time limit exceeded"),
+ (OutOfResources,
+ "# Cannot determine problem status within resource limit"),
+ (OutOfResources, "SZS status: ResourceOut"),
+ (OutOfResources, "SZS status ResourceOut")],
+ max_new_relevant_facts_per_iter = 80 (* FIXME *),
+ prefers_theory_relevant = false,
+ explicit_forall = false}
+val e = ("e", e_config)
+
+
+(* The "-VarWeight=3" option helps the higher-order problems, probably by
+ counteracting the presence of "hAPP". *)
+val spass_config : prover_config =
+ {executable = ("ISABELLE_ATP", "scripts/spass"),
+ required_executables = [("SPASS_HOME", "SPASS")],
+ (* "div 2" accounts for the fact that SPASS is often run twice. *)
+ arguments = fn complete => fn timeout =>
+ ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
+ \-VarWeight=3 -TimeLimit=" ^
+ string_of_int (to_generous_secs timeout div 2))
+ |> not complete ? prefix "-SOS=1 ",
+ proof_delims = [("Here is a proof", "Formulae used in the proof")],
+ known_failures =
+ [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
+ (TimedOut, "SPASS beiseite: Ran out of time"),
+ (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
+ (MalformedInput, "Undefined symbol"),
+ (MalformedInput, "Free Variable"),
+ (OldSpass, "tptp2dfg")],
+ max_new_relevant_facts_per_iter = 26 (* FIXME *),
+ prefers_theory_relevant = true,
+ explicit_forall = true}
+val spass = ("spass", spass_config)
+
+(* Vampire *)
+
+val vampire_config : prover_config =
+ {executable = ("VAMPIRE_HOME", "vampire"),
+ required_executables = [],
+ arguments = fn _ => fn timeout =>
+ "--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^
+ " --input_file ",
+ proof_delims =
+ [("=========== Refutation ==========",
+ "======= End of refutation ======="),
+ ("% SZS output start Refutation", "% SZS output end Refutation"),
+ ("% SZS output start Proof", "% SZS output end Proof")],
+ known_failures =
+ [(Unprovable, "UNPROVABLE"),
+ (IncompleteUnprovable, "CANNOT PROVE"),
+ (Unprovable, "Satisfiability detected"),
+ (OutOfResources, "Refutation not found")],
+ max_new_relevant_facts_per_iter = 40 (* FIXME *),
+ prefers_theory_relevant = false,
+ explicit_forall = false}
+val vampire = ("vampire", vampire_config)
+
+(* Remote prover invocation via SystemOnTPTP *)
+
+val systems = Synchronized.var "atp_systems" ([]: string list)
+
+fun get_systems () =
+ case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w" of
+ (answer, 0) => split_lines answer
+ | (answer, _) =>
+ error ("Failed to get available systems at SystemOnTPTP:\n" ^
+ perhaps (try (unsuffix "\n")) answer)
+
+fun refresh_systems_on_tptp () =
+ Synchronized.change systems (fn _ => get_systems ())
+
+fun get_system prefix = Synchronized.change_result systems (fn systems =>
+ (if null systems then get_systems () else systems)
+ |> `(find_first (String.isPrefix prefix)));
+
+fun the_system prefix =
+ (case get_system prefix of
+ NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP.")
+ | SOME sys => sys);
+
+val remote_known_failures =
+ [(CantConnect, "HTTP-Error"),
+ (TimedOut, "says Timeout"),
+ (MalformedOutput, "Remote script could not extract proof")]
+
+fun remote_config atp_prefix
+ ({proof_delims, known_failures, max_new_relevant_facts_per_iter,
+ prefers_theory_relevant, explicit_forall, ...} : prover_config)
+ : prover_config =
+ {executable = ("ISABELLE_ATP", "scripts/remote_atp"),
+ required_executables = [],
+ arguments = fn _ => fn timeout =>
+ " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
+ the_system atp_prefix,
+ proof_delims = insert (op =) tstp_proof_delims proof_delims,
+ known_failures = remote_known_failures @ known_failures,
+ max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter,
+ prefers_theory_relevant = prefers_theory_relevant,
+ explicit_forall = explicit_forall}
+
+val remote_name = prefix "remote_"
+
+fun remote_prover (name, config) atp_prefix =
+ (remote_name name, remote_config atp_prefix config)
+
+val remote_e = remote_prover e "EP---"
+val remote_vampire = remote_prover vampire "Vampire---9"
+
+fun is_installed ({executable, required_executables, ...} : prover_config) =
+ forall (curry (op <>) "" o getenv o fst) (executable :: required_executables)
+fun maybe_remote (name, config) =
+ name |> not (is_installed config) ? remote_name
+
+fun default_atps_param_value () =
+ space_implode " " ([maybe_remote e] @
+ (if is_installed (snd spass) then [fst spass] else []) @
+ [remote_name (fst vampire)])
+
+val provers = [e, spass, vampire, remote_e, remote_vampire]
+val setup = fold add_prover provers
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/etc/settings Wed Jul 28 22:18:35 2010 +0200
@@ -0,0 +1,1 @@
+ISABELLE_ATP="$COMPONENT"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/scripts/remote_atp Wed Jul 28 22:18:35 2010 +0200
@@ -0,0 +1,109 @@
+#!/usr/bin/env perl
+#
+# Wrapper for custom remote provers on SystemOnTPTP
+# Author: Fabian Immler, TU Muenchen
+#
+
+use warnings;
+use strict;
+use Getopt::Std;
+use HTTP::Request::Common;
+use LWP;
+
+my $SystemOnTPTPFormReplyURL =
+ "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
+
+# default parameters
+my %URLParameters = (
+ "NoHTML" => 1,
+ "QuietFlag" => "-q01",
+ "SubmitButton" => "RunSelectedSystems",
+ "ProblemSource" => "UPLOAD",
+ "ForceSystem" => "-force",
+ );
+
+#----Get format and transform options if specified
+my %Options;
+getopts("hws:t:c:",\%Options);
+
+#----Usage
+sub usage() {
+ print("Usage: remote_atp [<options>] <File name>\n");
+ print(" <options> are ...\n");
+ print(" -h - print this help\n");
+ print(" -w - list available ATP systems\n");
+ print(" -s<system> - specified system to use\n");
+ print(" -t<timelimit> - CPU time limit for system\n");
+ print(" -c<command> - custom command for system\n");
+ print(" <File name> - TPTP problem file\n");
+ exit(0);
+}
+if (exists($Options{'h'})) {
+ usage();
+}
+
+#----What systems flag
+if (exists($Options{'w'})) {
+ $URLParameters{"SubmitButton"} = "ListSystems";
+ delete($URLParameters{"ProblemSource"});
+}
+
+#----X2TPTP
+if (exists($Options{'x'})) {
+ $URLParameters{"X2TPTP"} = "-S";
+}
+
+#----Selected system
+my $System;
+if (exists($Options{'s'})) {
+ $System = $Options{'s'};
+} else {
+ # use Vampire as default
+ $System = "Vampire---9.0";
+}
+$URLParameters{"System___$System"} = $System;
+
+#----Time limit
+if (exists($Options{'t'})) {
+ $URLParameters{"TimeLimit___$System"} = $Options{'t'};
+}
+#----Custom command
+if (exists($Options{'c'})) {
+ $URLParameters{"Command___$System"} = $Options{'c'};
+}
+
+#----Get single file name
+if (exists($URLParameters{"ProblemSource"})) {
+ if (scalar(@ARGV) >= 1) {
+ $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
+ } else {
+ print("Missing problem file\n");
+ usage();
+ die;
+ }
+}
+
+# Query Server
+my $Agent = LWP::UserAgent->new;
+if (exists($Options{'t'})) {
+ # give server more time to respond
+ $Agent->timeout($Options{'t'} + 10);
+}
+my $Request = POST($SystemOnTPTPFormReplyURL,
+ Content_Type => 'form-data',Content => \%URLParameters);
+my $Response = $Agent->request($Request);
+
+#catch errors / failure
+if(!$Response->is_success) {
+ print "HTTP-Error: " . $Response->message . "\n";
+ exit(-1);
+} elsif (exists($Options{'w'})) {
+ print $Response->content;
+ exit (0);
+} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
+ print "Specified System $1 does not exist\n";
+ exit(-1);
+} else {
+ print $Response->content;
+ exit(0);
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/scripts/spass Wed Jul 28 22:18:35 2010 +0200
@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+#
+# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for
+# Isar proof reconstruction)
+#
+# Author: Jasmin Blanchette, TU Muenchen
+
+options=${@:1:$(($#-1))}
+name=${@:$(($#)):1}
+
+$SPASS_HOME/tptp2dfg $name $name.fof.dfg
+$SPASS_HOME/SPASS -Flotter $name.fof.dfg \
+ | sed 's/description({$/description({*/' \
+ > $name.cnf.dfg
+rm -f $name.fof.dfg
+cat $name.cnf.dfg
+$SPASS_HOME/SPASS $options $name.cnf.dfg \
+ | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
+rm -f $name.cnf.dfg
--- a/src/HOL/Tools/ATP_Manager/SPASS_TPTP Wed Jul 28 11:42:48 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-#!/usr/bin/env bash
-#
-# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for
-# Isar proof reconstruction)
-#
-# Author: Jasmin Blanchette, TU Muenchen
-
-options=${@:1:$(($#-1))}
-name=${@:$(($#)):1}
-
-$SPASS_HOME/tptp2dfg $name $name.fof.dfg
-$SPASS_HOME/SPASS -Flotter $name.fof.dfg \
- | sed 's/description({$/description({*/' \
- > $name.cnf.dfg
-rm -f $name.fof.dfg
-cat $name.cnf.dfg
-$SPASS_HOME/SPASS $options $name.cnf.dfg \
- | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
-rm -f $name.cnf.dfg
--- a/src/HOL/Tools/ATP_Manager/SystemOnTPTP Wed Jul 28 11:42:48 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,142 +0,0 @@
-#!/usr/bin/env perl
-#
-# Wrapper for custom remote provers on SystemOnTPTP
-# Author: Fabian Immler, TU Muenchen
-#
-
-use warnings;
-use strict;
-use Getopt::Std;
-use HTTP::Request::Common;
-use LWP;
-
-my $SystemOnTPTPFormReplyURL =
- "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
-
-# default parameters
-my %URLParameters = (
- "NoHTML" => 1,
- "QuietFlag" => "-q01",
- "SubmitButton" => "RunSelectedSystems",
- "ProblemSource" => "UPLOAD",
- "ForceSystem" => "-force",
- );
-
-#----Get format and transform options if specified
-my %Options;
-getopts("hwxs:t:c:",\%Options);
-
-#----Usage
-sub usage() {
- print("Usage: remote [<options>] <File name>\n");
- print(" <options> are ...\n");
- print(" -h - print this help\n");
- print(" -w - list available ATP systems\n");
- print(" -x - use X2TPTP to convert output of prover\n");
- print(" -s<system> - specified system to use\n");
- print(" -t<timelimit> - CPU time limit for system\n");
- print(" -c<command> - custom command for system\n");
- print(" <File name> - TPTP problem file\n");
- exit(0);
-}
-if (exists($Options{'h'})) {
- usage();
-}
-
-#----What systems flag
-if (exists($Options{'w'})) {
- $URLParameters{"SubmitButton"} = "ListSystems";
- delete($URLParameters{"ProblemSource"});
-}
-
-#----X2TPTP
-if (exists($Options{'x'})) {
- $URLParameters{"X2TPTP"} = "-S";
-}
-
-#----Selected system
-my $System;
-if (exists($Options{'s'})) {
- $System = $Options{'s'};
-} else {
- # use Vampire as default
- $System = "Vampire---9.0";
-}
-$URLParameters{"System___$System"} = $System;
-
-#----Time limit
-if (exists($Options{'t'})) {
- $URLParameters{"TimeLimit___$System"} = $Options{'t'};
-}
-#----Custom command
-if (exists($Options{'c'})) {
- $URLParameters{"Command___$System"} = $Options{'c'};
-}
-
-#----Get single file name
-if (exists($URLParameters{"ProblemSource"})) {
- if (scalar(@ARGV) >= 1) {
- $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
- } else {
- print("Missing problem file\n");
- usage();
- die;
- }
-}
-
-# Query Server
-my $Agent = LWP::UserAgent->new;
-if (exists($Options{'t'})) {
- # give server more time to respond
- $Agent->timeout($Options{'t'} + 10);
-}
-my $Request = POST($SystemOnTPTPFormReplyURL,
- Content_Type => 'form-data',Content => \%URLParameters);
-my $Response = $Agent->request($Request);
-
-#catch errors / failure
-if(!$Response->is_success) {
- print "HTTP-Error: " . $Response->message . "\n";
- exit(-1);
-} elsif (exists($Options{'w'})) {
- print $Response->content;
- exit (0);
-} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
- print "Specified System $1 does not exist\n";
- exit(-1);
-} elsif (exists($Options{'x'}) &&
- $Response->content =~
- /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&
- $Response->content !~ /ERROR: Could not form TPTP format derivation/ )
-{
- # converted output: extract proof
- my @lines = split( /\n/, $Response->content);
- my $extract = "";
- foreach my $line (@lines){
- #ignore comments
- if ($line !~ /^%/ && !($line eq "")) {
- $extract .= "$line";
- }
- }
- # insert newlines after ').'
- $extract =~ s/\s//g;
- $extract =~ s/\)\.cnf/\)\.\ncnf/g;
-
- print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n";
- # orientation for "sledgehammer_proof_reconstruct.ML"
- print "# SZS output start CNFRefutation.\n";
- print "$extract\n";
- print "# SZS output end CNFRefutation.\n";
- # can be useful for debugging; Isabelle ignores this
- print "============== original response from SystemOnTPTP: ==============\n";
- print $Response->content;
- exit(0);
-} elsif (!exists($Options{'x'})) {
- # pass output directly to Isabelle
- print $Response->content;
- exit(0);
-}else {
- print "Remote script could not extract proof:\n".$Response->content;
- exit(-1);
-}
-
--- a/src/HOL/Tools/ATP_Manager/async_manager.ML Wed Jul 28 11:42:48 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,241 +0,0 @@
-(* Title: HOL/Tools/ATP_Manager/async_manager.ML
- Author: Fabian Immler, TU Muenchen
- Author: Makarius
- Author: Jasmin Blanchette, TU Muenchen
-
-Central manager for asynchronous diagnosis tool threads.
-*)
-
-signature ASYNC_MANAGER =
-sig
- val launch :
- string -> bool -> Time.time -> Time.time -> string -> (unit -> string)
- -> unit
- val kill_threads : string -> string -> unit
- val running_threads : string -> string -> unit
- val thread_messages : string -> string -> int option -> unit
-end;
-
-structure Async_Manager : ASYNC_MANAGER =
-struct
-
-(** preferences **)
-
-val message_store_limit = 20;
-val message_display_limit = 5;
-
-
-(** thread management **)
-
-(* data structures over threads *)
-
-structure Thread_Heap = Heap
-(
- type elem = Time.time * Thread.thread;
- fun ord ((a, _), (b, _)) = Time.compare (a, b);
-);
-
-fun lookup_thread xs = AList.lookup Thread.equal xs;
-fun delete_thread xs = AList.delete Thread.equal xs;
-fun update_thread xs = AList.update Thread.equal xs;
-
-
-(* state of thread manager *)
-
-type state =
- {manager: Thread.thread option,
- timeout_heap: Thread_Heap.T,
- active: (Thread.thread * (string * Time.time * Time.time * string)) list,
- canceling: (Thread.thread * (string * Time.time * string)) list,
- messages: (string * string) list,
- store: (string * string) list}
-
-fun make_state manager timeout_heap active canceling messages store : state =
- {manager = manager, timeout_heap = timeout_heap, active = active,
- canceling = canceling, messages = messages, store = store}
-
-val global_state = Synchronized.var "async_manager"
- (make_state NONE Thread_Heap.empty [] [] [] []);
-
-
-(* unregister thread *)
-
-fun unregister verbose message thread =
- Synchronized.change global_state
- (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
- (case lookup_thread active thread of
- SOME (tool, birth_time, _, desc) =>
- let
- val active' = delete_thread thread active;
- val now = Time.now ()
- val canceling' = (thread, (tool, now, desc)) :: canceling
- val message' =
- desc ^ "\n" ^ message ^
- (if verbose then
- "Total time: " ^ Int.toString (Time.toMilliseconds
- (Time.- (now, birth_time))) ^ " ms.\n"
- else
- "")
- val messages' = (tool, message') :: messages;
- val store' = (tool, message') ::
- (if length store <= message_store_limit then store
- else #1 (chop message_store_limit store));
- in make_state manager timeout_heap active' canceling' messages' store' end
- | NONE => state));
-
-
-(* main manager thread -- only one may exist *)
-
-val min_wait_time = Time.fromMilliseconds 300;
-val max_wait_time = Time.fromSeconds 10;
-
-fun replace_all bef aft =
- let
- fun aux seen "" = String.implode (rev seen)
- | aux seen s =
- if String.isPrefix bef s then
- aux seen "" ^ aft ^ aux [] (unprefix bef s)
- else
- aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
- in aux [] end
-
-(* This is a workaround for Proof General's off-by-a-few sendback display bug,
- whereby "pr" in "proof" is not highlighted. *)
-fun break_into_chunks xs =
- maps (space_explode "\000" o replace_all "\n\n" "\000" o snd) xs
-
-fun print_new_messages () =
- case Synchronized.change_result global_state
- (fn {manager, timeout_heap, active, canceling, messages, store} =>
- (messages, make_state manager timeout_heap active canceling []
- store)) of
- [] => ()
- | msgs as (tool, _) :: _ =>
- let val ss = break_into_chunks msgs in
- List.app priority (tool ^ ": " ^ hd ss :: tl ss)
- end
-
-fun check_thread_manager verbose = Synchronized.change global_state
- (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
- if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
- else let val manager = SOME (Toplevel.thread false (fn () =>
- let
- fun time_limit timeout_heap =
- (case try Thread_Heap.min timeout_heap of
- NONE => Time.+ (Time.now (), max_wait_time)
- | SOME (time, _) => time);
-
- (*action: find threads whose timeout is reached, and interrupt canceling threads*)
- fun action {manager, timeout_heap, active, canceling, messages, store} =
- let val (timeout_threads, timeout_heap') =
- Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
- in
- if null timeout_threads andalso null canceling then
- NONE
- else
- let
- val _ = List.app (Simple_Thread.interrupt o #1) canceling
- val canceling' = filter (Thread.isActive o #1) canceling
- val state' = make_state manager timeout_heap' active canceling' messages store;
- in SOME (map #2 timeout_threads, state') end
- end;
- in
- while Synchronized.change_result global_state
- (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
- if null active andalso null canceling andalso null messages
- then (false, make_state NONE timeout_heap active canceling messages store)
- else (true, state))
- do
- (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
- |> these
- |> List.app (unregister verbose "Timed out.\n");
- print_new_messages ();
- (*give threads some time to respond to interrupt*)
- OS.Process.sleep min_wait_time)
- end))
- in make_state manager timeout_heap active canceling messages store end)
-
-
-(* register thread *)
-
-fun register tool verbose birth_time death_time desc thread =
- (Synchronized.change global_state
- (fn {manager, timeout_heap, active, canceling, messages, store} =>
- let
- val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
- val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active;
- val state' = make_state manager timeout_heap' active' canceling messages store;
- in state' end);
- check_thread_manager verbose);
-
-
-fun launch tool verbose birth_time death_time desc f =
- (Toplevel.thread true
- (fn () =>
- let
- val self = Thread.self ()
- val _ = register tool verbose birth_time death_time desc self
- val message = f ()
- in unregister verbose message self end);
- ())
-
-
-(** user commands **)
-
-(* kill threads *)
-
-fun kill_threads tool workers = Synchronized.change global_state
- (fn {manager, timeout_heap, active, canceling, messages, store} =>
- let
- val killing =
- map_filter (fn (th, (tool', _, _, desc)) =>
- if tool' = tool then SOME (th, (tool', Time.now (), desc))
- else NONE) active
- val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
- val _ = if null killing then () else priority ("Killed active " ^ workers ^ ".")
- in state' end);
-
-
-(* running threads *)
-
-fun seconds time = string_of_int (Time.toSeconds time) ^ " s"
-
-fun running_threads tool workers =
- let
- val {active, canceling, ...} = Synchronized.value global_state;
-
- val now = Time.now ();
- fun running_info (_, (tool', birth_time, death_time, desc)) =
- if tool' = tool then
- SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
- seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc)
- else
- NONE
- fun canceling_info (_, (tool', death_time, desc)) =
- if tool' = tool then
- SOME ("Trying to interrupt thread since " ^
- seconds (Time.- (now, death_time)) ^ ":\n" ^ desc)
- else
- NONE
- val running =
- case map_filter running_info active of
- [] => ["No " ^ workers ^ " running."]
- | ss => "Running " ^ workers ^ ":" :: ss
- val interrupting =
- case map_filter canceling_info canceling of
- [] => []
- | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss
- in priority (space_implode "\n\n" (running @ interrupting)) end
-
-fun thread_messages tool worker opt_limit =
- let
- val limit = the_default message_display_limit opt_limit;
- val tool_store = Synchronized.value global_state
- |> #store |> filter (curry (op =) tool o fst)
- val header =
- "Recent " ^ worker ^ " messages" ^
- (if length tool_store <= limit then ":"
- else " (" ^ string_of_int limit ^ " displayed):");
- in List.app priority (header :: break_into_chunks (#1 (chop limit tool_store))) end
-
-end;
--- a/src/HOL/Tools/ATP_Manager/atp_problem.ML Wed Jul 28 11:42:48 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,152 +0,0 @@
-(* Title: HOL/Tools/ATP_Manager/atp_problem.ML
- Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
- Author: Jasmin Blanchette, TU Muenchen
-
-TPTP syntax.
-*)
-
-signature ATP_PROBLEM =
-sig
- datatype 'a fo_term = ATerm of 'a * 'a fo_term list
- datatype quantifier = AForall | AExists
- datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
- datatype ('a, 'b) formula =
- AQuant of quantifier * 'a list * ('a, 'b) formula |
- AConn of connective * ('a, 'b) formula list |
- APred of 'b
-
- datatype kind = Axiom | Conjecture
- datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
- type 'a problem = (string * 'a problem_line list) list
-
- val timestamp : unit -> string
- val is_tptp_variable : string -> bool
- val strings_for_tptp_problem :
- (string * string problem_line list) list -> string list
- val nice_tptp_problem :
- bool -> ('a * (string * string) problem_line list) list
- -> ('a * string problem_line list) list
- * (string Symtab.table * string Symtab.table) option
-end;
-
-structure ATP_Problem : ATP_PROBLEM =
-struct
-
-(** ATP problem **)
-
-datatype 'a fo_term = ATerm of 'a * 'a fo_term list
-datatype quantifier = AForall | AExists
-datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
-datatype ('a, 'b) formula =
- AQuant of quantifier * 'a list * ('a, 'b) formula |
- AConn of connective * ('a, 'b) formula list |
- APred of 'b
-
-datatype kind = Axiom | Conjecture
-datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
-type 'a problem = (string * 'a problem_line list) list
-
-val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
-
-fun string_for_term (ATerm (s, [])) = s
- | string_for_term (ATerm (s, ts)) =
- if s = "equal" then space_implode " = " (map string_for_term ts)
- else s ^ "(" ^ commas (map string_for_term ts) ^ ")"
-fun string_for_quantifier AForall = "!"
- | string_for_quantifier AExists = "?"
-fun string_for_connective ANot = "~"
- | string_for_connective AAnd = "&"
- | string_for_connective AOr = "|"
- | string_for_connective AImplies = "=>"
- | string_for_connective AIf = "<="
- | string_for_connective AIff = "<=>"
- | string_for_connective ANotIff = "<~>"
-fun string_for_formula (AQuant (q, xs, phi)) =
- string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^
- string_for_formula phi
- | string_for_formula (AConn (ANot, [APred (ATerm ("equal", ts))])) =
- space_implode " != " (map string_for_term ts)
- | string_for_formula (AConn (c, [phi])) =
- string_for_connective c ^ " " ^ string_for_formula phi
- | string_for_formula (AConn (c, phis)) =
- "(" ^ space_implode (" " ^ string_for_connective c ^ " ")
- (map string_for_formula phis) ^ ")"
- | string_for_formula (APred tm) = string_for_term tm
-
-fun string_for_problem_line (Fof (ident, kind, phi)) =
- "fof(" ^ ident ^ ", " ^
- (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^
- " (" ^ string_for_formula phi ^ ")).\n"
-fun strings_for_tptp_problem problem =
- "% This file was generated by Isabelle (most likely Sledgehammer)\n\
- \% " ^ timestamp () ^ "\n" ::
- maps (fn (_, []) => []
- | (heading, lines) =>
- "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" ::
- map string_for_problem_line lines) problem
-
-fun is_tptp_variable s = Char.isUpper (String.sub (s, 0))
-
-
-(** Nice names **)
-
-fun empty_name_pool readable_names =
- if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
-
-fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
-fun pool_map f xs =
- pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
-
-(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the
- unreadable "op_1", "op_2", etc., in the problem files. *)
-val reserved_nice_names = ["equal", "op"]
-fun readable_name full_name s =
- if s = full_name then
- s
- else
- let
- val s = s |> Long_Name.base_name
- |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
- in if member (op =) reserved_nice_names s then full_name else s end
-
-fun nice_name (full_name, _) NONE = (full_name, NONE)
- | nice_name (full_name, desired_name) (SOME the_pool) =
- case Symtab.lookup (fst the_pool) full_name of
- SOME nice_name => (nice_name, SOME the_pool)
- | NONE =>
- let
- val nice_prefix = readable_name full_name desired_name
- fun add j =
- let
- val nice_name = nice_prefix ^
- (if j = 0 then "" else "_" ^ Int.toString j)
- in
- case Symtab.lookup (snd the_pool) nice_name of
- SOME full_name' =>
- if full_name = full_name' then (nice_name, the_pool)
- else add (j + 1)
- | NONE =>
- (nice_name,
- (Symtab.update_new (full_name, nice_name) (fst the_pool),
- Symtab.update_new (nice_name, full_name) (snd the_pool)))
- end
- in add 0 |> apsnd SOME end
-
-
-fun nice_term (ATerm (name, ts)) =
- nice_name name ##>> pool_map nice_term ts #>> ATerm
-fun nice_formula (AQuant (q, xs, phi)) =
- pool_map nice_name xs ##>> nice_formula phi
- #>> (fn (xs, phi) => AQuant (q, xs, phi))
- | nice_formula (AConn (c, phis)) =
- pool_map nice_formula phis #>> curry AConn c
- | nice_formula (APred tm) = nice_term tm #>> APred
-fun nice_problem_line (Fof (ident, kind, phi)) =
- nice_formula phi #>> (fn phi => Fof (ident, kind, phi))
-fun nice_problem problem =
- pool_map (fn (heading, lines) =>
- pool_map nice_problem_line lines #>> pair heading) problem
-fun nice_tptp_problem readable_names problem =
- nice_problem problem (empty_name_pool readable_names)
-
-end;
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Wed Jul 28 11:42:48 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,216 +0,0 @@
-(* Title: HOL/Tools/ATP_Manager/atp_systems.ML
- Author: Fabian Immler, TU Muenchen
- Author: Jasmin Blanchette, TU Muenchen
-
-Setup for supported ATPs.
-*)
-
-signature ATP_SYSTEMS =
-sig
- datatype failure =
- Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
- OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
-
- type prover_config =
- {home_var: string,
- executable: string,
- arguments: bool -> Time.time -> string,
- proof_delims: (string * string) list,
- known_failures: (failure * string) list,
- max_new_relevant_facts_per_iter: int,
- prefers_theory_relevant: bool,
- explicit_forall: bool}
-
- val add_prover: string * prover_config -> theory -> theory
- val get_prover: theory -> string -> prover_config
- val available_atps: theory -> unit
- val refresh_systems_on_tptp : unit -> unit
- val default_atps_param_value : unit -> string
- val setup : theory -> theory
-end;
-
-structure ATP_Systems : ATP_SYSTEMS =
-struct
-
-(* prover configuration *)
-
-datatype failure =
- Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
- OldSpass | MalformedInput | MalformedOutput | UnknownError
-
-type prover_config =
- {home_var: string,
- executable: string,
- arguments: bool -> Time.time -> string,
- proof_delims: (string * string) list,
- known_failures: (failure * string) list,
- max_new_relevant_facts_per_iter: int,
- prefers_theory_relevant: bool,
- explicit_forall: bool}
-
-
-(* named provers *)
-
-structure Data = Theory_Data
-(
- type T = (prover_config * stamp) Symtab.table
- val empty = Symtab.empty
- val extend = I
- fun merge data : T = Symtab.merge (eq_snd op =) data
- handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
-)
-
-fun add_prover (name, config) thy =
- Data.map (Symtab.update_new (name, (config, stamp ()))) thy
- handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
-
-fun get_prover thy name =
- the (Symtab.lookup (Data.get thy) name) |> fst
- handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
-
-fun available_atps thy =
- priority ("Available ATPs: " ^
- commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
-
-fun available_atps thy =
- priority ("Available ATPs: " ^
- commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
-
-fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000
-
-(* E prover *)
-
-val tstp_proof_delims =
- ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
-
-val e_config : prover_config =
- {home_var = "E_HOME",
- executable = "eproof",
- arguments = fn _ => fn timeout =>
- "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^
- string_of_int (to_generous_secs timeout),
- proof_delims = [tstp_proof_delims],
- known_failures =
- [(Unprovable, "SZS status: CounterSatisfiable"),
- (Unprovable, "SZS status CounterSatisfiable"),
- (TimedOut, "Failure: Resource limit exceeded (time)"),
- (TimedOut, "time limit exceeded"),
- (OutOfResources,
- "# Cannot determine problem status within resource limit"),
- (OutOfResources, "SZS status: ResourceOut"),
- (OutOfResources, "SZS status ResourceOut")],
- max_new_relevant_facts_per_iter = 80 (* FIXME *),
- prefers_theory_relevant = false,
- explicit_forall = false}
-val e = ("e", e_config)
-
-
-(* The "-VarWeight=3" option helps the higher-order problems, probably by
- counteracting the presence of "hAPP". *)
-val spass_config : prover_config =
- {home_var = "ISABELLE_ATP_MANAGER",
- executable = "SPASS_TPTP",
- (* "div 2" accounts for the fact that SPASS is often run twice. *)
- arguments = fn complete => fn timeout =>
- ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
- \-VarWeight=3 -TimeLimit=" ^
- string_of_int (to_generous_secs timeout div 2))
- |> not complete ? prefix "-SOS=1 ",
- proof_delims = [("Here is a proof", "Formulae used in the proof")],
- known_failures =
- [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
- (TimedOut, "SPASS beiseite: Ran out of time"),
- (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
- (MalformedInput, "Undefined symbol"),
- (MalformedInput, "Free Variable"),
- (OldSpass, "tptp2dfg")],
- max_new_relevant_facts_per_iter = 26 (* FIXME *),
- prefers_theory_relevant = true,
- explicit_forall = true}
-val spass = ("spass", spass_config)
-
-(* Vampire *)
-
-val vampire_config : prover_config =
- {home_var = "VAMPIRE_HOME",
- executable = "vampire",
- arguments = fn _ => fn timeout =>
- "--output_syntax tptp --mode casc -t " ^
- string_of_int (to_generous_secs timeout),
- proof_delims =
- [("=========== Refutation ==========",
- "======= End of refutation ======="),
- ("% SZS output start Refutation", "% SZS output end Refutation")],
- known_failures =
- [(Unprovable, "UNPROVABLE"),
- (IncompleteUnprovable, "CANNOT PROVE"),
- (Unprovable, "Satisfiability detected"),
- (OutOfResources, "Refutation not found")],
- max_new_relevant_facts_per_iter = 40 (* FIXME *),
- prefers_theory_relevant = false,
- explicit_forall = false}
-val vampire = ("vampire", vampire_config)
-
-(* Remote prover invocation via SystemOnTPTP *)
-
-val systems = Synchronized.var "atp_systems" ([]: string list)
-
-fun get_systems () =
- case bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" of
- (answer, 0) => split_lines answer
- | (answer, _) =>
- error ("Failed to get available systems at SystemOnTPTP:\n" ^
- perhaps (try (unsuffix "\n")) answer)
-
-fun refresh_systems_on_tptp () =
- Synchronized.change systems (fn _ => get_systems ())
-
-fun get_system prefix = Synchronized.change_result systems (fn systems =>
- (if null systems then get_systems () else systems)
- |> `(find_first (String.isPrefix prefix)));
-
-fun the_system prefix =
- (case get_system prefix of
- NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP.")
- | SOME sys => sys);
-
-val remote_known_failures =
- [(CantConnect, "HTTP-Error"),
- (TimedOut, "says Timeout"),
- (MalformedOutput, "Remote script could not extract proof")]
-
-fun remote_config atp_prefix args
- ({proof_delims, known_failures, max_new_relevant_facts_per_iter,
- prefers_theory_relevant, explicit_forall, ...} : prover_config)
- : prover_config =
- {home_var = "ISABELLE_ATP_MANAGER",
- executable = "SystemOnTPTP",
- arguments = fn _ => fn timeout =>
- args ^ " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
- the_system atp_prefix,
- proof_delims = insert (op =) tstp_proof_delims proof_delims,
- known_failures = remote_known_failures @ known_failures,
- max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter,
- prefers_theory_relevant = prefers_theory_relevant,
- explicit_forall = explicit_forall}
-
-val remote_name = prefix "remote_"
-
-fun remote_prover prover atp_prefix args config =
- (remote_name (fst prover), remote_config atp_prefix args config)
-
-val remote_e = remote_prover e "EP---" "" e_config
-val remote_spass = remote_prover spass "SPASS---" "-x" spass_config
-val remote_vampire = remote_prover vampire "Vampire---9" "" vampire_config
-
-fun maybe_remote (name, _) ({home_var, ...} : prover_config) =
- name |> getenv home_var = "" ? remote_name
-
-fun default_atps_param_value () =
- space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
- remote_name (fst vampire)]
-
-val provers = [e, spass, vampire, remote_e, remote_spass, remote_vampire]
-val setup = fold add_prover provers
-
-end;
--- a/src/HOL/Tools/ATP_Manager/etc/settings Wed Jul 28 11:42:48 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-ISABELLE_ATP_MANAGER="$COMPONENT"
-
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Jul 28 11:42:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Jul 28 22:18:35 2010 +0200
@@ -41,7 +41,7 @@
output: string,
proof: string,
internal_thm_names: string Vector.vector,
- conjecture_shape: int list,
+ conjecture_shape: int list list,
filtered_clauses: (string * thm) list}
type prover =
params -> minimize_command -> Time.time -> problem -> prover_result
@@ -53,9 +53,9 @@
val running_atps: unit -> unit
val messages: int option -> unit
val get_prover_fun : theory -> string -> prover
- val start_prover_thread :
- params -> int -> int -> relevance_override -> (string -> minimize_command)
- -> Proof.state -> string -> unit
+ val run_sledgehammer :
+ params -> int -> relevance_override -> (string -> minimize_command)
+ -> Proof.state -> unit
val setup : theory -> theory
end;
@@ -112,7 +112,7 @@
output: string,
proof: string,
internal_thm_names: string Vector.vector,
- conjecture_shape: int list,
+ conjecture_shape: int list list,
filtered_clauses: (string * thm) list}
type prover =
@@ -231,7 +231,7 @@
| Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
do_conn bs AIff t1 t2
| _ => (fn ts => do_term bs (Envir.eta_contract t)
- |>> APred ||> union (op =) ts)
+ |>> AAtom ||> union (op =) ts)
in do_formula [] end
(* Converts an elim-rule into an equivalent theorem that does not have the
@@ -336,7 +336,7 @@
| count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
| count_combformula (AConn (_, phis)) = fold count_combformula phis
- | count_combformula (APred tm) = count_combterm tm
+ | count_combformula (AAtom tm) = count_combterm tm
fun count_fol_formula (FOLFormula {combformula, ...}) =
count_combformula combformula
@@ -401,11 +401,6 @@
class_rel_clauses, arity_clauses))
end
-val axiom_prefix = "ax_"
-val conjecture_prefix = "conj_"
-val arity_clause_prefix = "clsarity_"
-val tfrees_name = "tfrees"
-
fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
@@ -418,7 +413,7 @@
| fo_literal_for_type_literal (TyLitFree (class, name)) =
(true, ATerm (class, [ATerm (name, [])]))
-fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot
+fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
fun fo_term_for_combterm full_types =
let
@@ -446,7 +441,7 @@
let
fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
| aux (AConn (c, phis)) = AConn (c, map aux phis)
- | aux (APred tm) = APred (fo_term_for_combterm full_types tm)
+ | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
in aux end
fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
@@ -463,8 +458,8 @@
(ClassRelClause {axiom_name, subclass, superclass, ...}) =
let val ty_arg = ATerm (("T", "T"), []) in
Fof (ascii_of axiom_name, Axiom,
- AConn (AImplies, [APred (ATerm (subclass, [ty_arg])),
- APred (ATerm (superclass, [ty_arg]))]))
+ AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
+ AAtom (ATerm (superclass, [ty_arg]))]))
end
fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
@@ -515,7 +510,7 @@
#> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
| consider_formula (AConn (_, phis)) = fold consider_formula phis
- | consider_formula (APred tm) = consider_term true tm
+ | consider_formula (AAtom tm) = consider_term true tm
fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
fun consider_problem problem = fold (fold consider_problem_line o snd) problem
@@ -601,7 +596,7 @@
fun formula_vars bounds (AQuant (q, xs, phi)) =
formula_vars (xs @ bounds) phi
| formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
- | formula_vars bounds (APred tm) = term_vars bounds tm
+ | formula_vars bounds (AAtom tm) = term_vars bounds tm
in
case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
end
@@ -610,8 +605,8 @@
let
fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
| aux (AConn (c, phis)) = AConn (c, map aux phis)
- | aux (APred tm) =
- APred (tm |> repair_applications_in_term thy full_types const_tab
+ | aux (AAtom tm) =
+ AAtom (tm |> repair_applications_in_term thy full_types const_tab
|> repair_predicates_in_term const_tab)
in aux #> explicit_forall ? close_universally end
@@ -686,15 +681,14 @@
clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part
of this hack. *)
let
- val j0 = hd conjecture_shape
+ val j0 = hd (hd conjecture_shape)
val seq = extract_clause_sequence output
val name_map = extract_clause_formula_relation output
fun renumber_conjecture j =
AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0))
- |> the_single
- |> (fn s => find_index (curry (op =) s) seq + 1)
+ |> map (fn s => find_index (curry (op =) s) seq + 1)
in
- (conjecture_shape |> map renumber_conjecture,
+ (conjecture_shape |> map (maps renumber_conjecture),
seq |> map (the o AList.lookup (op =) name_map)
|> map (fn s => case try (unprefix axiom_prefix) s of
SOME s' => undo_ascii_of s'
@@ -708,9 +702,9 @@
(* generic TPTP-based provers *)
fun prover_fun name
- {home_var, executable, arguments, proof_delims, known_failures,
- max_new_relevant_facts_per_iter, prefers_theory_relevant,
- explicit_forall}
+ {executable, required_executables, arguments, proof_delims,
+ known_failures, max_new_relevant_facts_per_iter,
+ prefers_theory_relevant, explicit_forall}
({debug, overlord, full_types, explicit_apply, relevance_threshold,
relevance_convergence, theory_relevant, defs_relevant, isar_proof,
isar_shrink_factor, ...} : params)
@@ -753,8 +747,7 @@
else error ("No such directory: " ^ the_dest_dir ^ ".")
end;
- val home = getenv home_var
- val command = Path.explode (home ^ "/" ^ executable)
+ val command = Path.explode (getenv (fst executable) ^ "/" ^ snd executable)
(* write out problem file and call prover *)
fun command_line complete probfile =
let
@@ -778,41 +771,45 @@
val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
in (output, as_time t) end;
fun run_on probfile =
- if home = "" then
+ case filter (curry (op =) "" o getenv o fst)
+ (executable :: required_executables) of
+ (home_var, _) :: _ =>
error ("The environment variable " ^ quote home_var ^ " is not set.")
- else if File.exists command then
- let
- fun do_run complete =
- let
- val command = command_line complete probfile
- val ((output, msecs), res_code) =
- bash_output command
- |>> (if overlord then
- prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
- else
- I)
- |>> (if Config.get ctxt measure_runtime then split_time
- else rpair 0)
- val (proof, outcome) =
- extract_proof_and_outcome complete res_code proof_delims
- known_failures output
- in (output, msecs, proof, outcome) end
- val readable_names = debug andalso overlord
- val (pool, conjecture_offset) =
- write_tptp_file thy readable_names explicit_forall full_types
- explicit_apply probfile clauses
- val conjecture_shape =
- conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
- val result =
- do_run false
- |> (fn (_, msecs0, _, SOME _) =>
- do_run true
- |> (fn (output, msecs, proof, outcome) =>
- (output, msecs0 + msecs, proof, outcome))
- | result => result)
- in ((pool, conjecture_shape), result) end
- else
- error ("Bad executable: " ^ Path.implode command ^ ".");
+ | [] =>
+ if File.exists command then
+ let
+ fun do_run complete =
+ let
+ val command = command_line complete probfile
+ val ((output, msecs), res_code) =
+ bash_output command
+ |>> (if overlord then
+ prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
+ else
+ I)
+ |>> (if Config.get ctxt measure_runtime then split_time
+ else rpair 0)
+ val (proof, outcome) =
+ extract_proof_and_outcome complete res_code proof_delims
+ known_failures output
+ in (output, msecs, proof, outcome) end
+ val readable_names = debug andalso overlord
+ val (pool, conjecture_offset) =
+ write_tptp_file thy readable_names explicit_forall full_types
+ explicit_apply probfile clauses
+ val conjecture_shape =
+ conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
+ |> map single
+ val result =
+ do_run false
+ |> (fn (_, msecs0, _, SOME _) =>
+ do_run true
+ |> (fn (output, msecs, proof, outcome) =>
+ (output, msecs0 + msecs, proof, outcome))
+ | result => result)
+ in ((pool, conjecture_shape), result) end
+ else
+ error ("Bad executable: " ^ Path.implode command ^ ".")
(* If the problem file has not been exported, remove it; otherwise, export
the proof file too. *)
@@ -848,7 +845,6 @@
fun get_prover_fun thy name = prover_fun name (get_prover thy name)
-(* start prover thread *)
fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n
relevance_override minimize_command proof_state name =
let
@@ -874,6 +870,19 @@
end)
end
+fun run_sledgehammer {atps = [], ...} _ _ _ _ = error "No ATP is set."
+ | run_sledgehammer (params as {atps, ...}) i relevance_override
+ minimize_command state =
+ case subgoal_count state of
+ 0 => priority "No subgoal!"
+ | n =>
+ let
+ val _ = kill_atps ()
+ val _ = priority "Sledgehammering..."
+ val _ = app (start_prover_thread params i n relevance_override
+ minimize_command state) atps
+ in () end
+
val setup =
dest_dir_setup
#> problem_prefix_setup
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Wed Jul 28 11:42:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Wed Jul 28 22:18:35 2010 +0200
@@ -8,11 +8,11 @@
signature SLEDGEHAMMER_FACT_MINIMIZER =
sig
type params = Sledgehammer.params
- type prover_result = Sledgehammer.prover_result
val minimize_theorems :
params -> int -> int -> Proof.state -> (string * thm list) list
-> (string * thm list) list option * string
+ val run_minimizer : params -> int -> Facts.ref list -> Proof.state -> unit
end;
structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
@@ -20,6 +20,7 @@
open Metis_Clauses
open Sledgehammer_Util
+open Sledgehammer_Fact_Filter
open Sledgehammer_Proof_Reconstruct
open Sledgehammer
@@ -38,7 +39,6 @@
fun sledgehammer_test_theorems (params : params) prover timeout subgoal state
filtered_clauses name_thms_pairs =
let
- val thy = Proof.theory_of state
val num_theorems = length name_thms_pairs
val _ =
priority ("Testing " ^ string_of_int num_theorems ^
@@ -123,4 +123,17 @@
handle ERROR msg => (NONE, "Error: " ^ msg)
end
+fun run_minimizer params i refs state =
+ let
+ val ctxt = Proof.context_of state
+ val chained_ths = #facts (Proof.goal state)
+ val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs
+ in
+ case subgoal_count state of
+ 0 => priority "No subgoal!"
+ | n =>
+ (kill_atps ();
+ priority (#2 (minimize_theorems params i n state name_thms_pairs)))
+ end
+
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 28 11:42:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 28 22:18:35 2010 +0200
@@ -19,7 +19,6 @@
open ATP_Systems
open Sledgehammer_Util
-open Sledgehammer_Fact_Filter
open Sledgehammer
open Sledgehammer_Fact_Minimizer
@@ -188,37 +187,8 @@
fun get_params thy = extract_params (default_raw_params thy)
fun default_params thy = get_params thy o map (apsnd single)
-val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
-
(* Sledgehammer the given subgoal *)
-fun run {atps = [], ...} _ _ _ _ = error "No ATP is set."
- | run (params as {atps, ...}) i relevance_override minimize_command state =
- case subgoal_count state of
- 0 => priority "No subgoal!"
- | n =>
- let
- val _ = kill_atps ()
- val _ = priority "Sledgehammering..."
- val _ = app (start_prover_thread params i n relevance_override
- minimize_command state) atps
- in () end
-
-fun minimize override_params i refs state =
- let
- val thy = Proof.theory_of state
- val ctxt = Proof.context_of state
- val chained_ths = #facts (Proof.goal state)
- val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs
- in
- case subgoal_count state of
- 0 => priority "No subgoal!"
- | n =>
- (kill_atps ();
- priority (#2 (minimize_theorems (get_params thy override_params) i n
- state name_thms_pairs)))
- end
-
val sledgehammerN = "sledgehammer"
val sledgehammer_paramsN = "sledgehammer_params"
@@ -252,12 +222,13 @@
in
if subcommand = runN then
let val i = the_default 1 opt_i in
- run (get_params thy override_params) i relevance_override
- (minimize_command override_params i) state
+ run_sledgehammer (get_params thy override_params) i relevance_override
+ (minimize_command override_params i) state
end
else if subcommand = minimizeN then
- minimize (map (apfst minimizize_raw_param_name) override_params)
- (the_default 1 opt_i) (#add relevance_override) state
+ run_minimizer (get_params thy (map (apfst minimizize_raw_param_name)
+ override_params))
+ (the_default 1 opt_i) (#add relevance_override) state
else if subcommand = messagesN then
messages opt_i
else if subcommand = available_atpsN then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Jul 28 11:42:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Jul 28 22:18:35 2010 +0200
@@ -10,16 +10,20 @@
sig
type minimize_command = string list -> string
+ val axiom_prefix : string
+ val conjecture_prefix : string
+ val arity_clause_prefix : string
+ val tfrees_name : string
val metis_line: bool -> int -> int -> string list -> string
val metis_proof_text:
bool * minimize_command * string * string vector * thm * int
-> string * string list
val isar_proof_text:
- string Symtab.table * bool * int * Proof.context * int list
+ string Symtab.table * bool * int * Proof.context * int list list
-> bool * minimize_command * string * string vector * thm * int
-> string * string list
val proof_text:
- bool -> string Symtab.table * bool * int * Proof.context * int list
+ bool -> string Symtab.table * bool * int * Proof.context * int list list
-> bool * minimize_command * string * string vector * thm * int
-> string * string list
end;
@@ -34,6 +38,11 @@
type minimize_command = string list -> string
+val axiom_prefix = "ax_"
+val conjecture_prefix = "conj_"
+val arity_clause_prefix = "clsarity_"
+val tfrees_name = "tfrees"
+
(* Simple simplifications to ensure that sort annotations don't leave a trail of
spurious "True"s. *)
fun s_not @{const False} = @{const True}
@@ -57,7 +66,8 @@
| mk_anot phi = AConn (ANot, [phi])
fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
-val index_in_shape : int -> int list -> int = find_index o curry (op =)
+val index_in_shape : int -> int list list -> int =
+ find_index o exists o curry (op =)
fun is_axiom_clause_number thm_names num =
num > 0 andalso num <= Vector.length thm_names andalso
Vector.sub (thm_names, num - 1) <> ""
@@ -81,9 +91,10 @@
Definition of 'a * 'b * 'c |
Inference of 'a * 'd * 'e list
-(**** PARSING OF TSTP FORMAT ****)
+fun raw_step_number (Definition (num, _, _)) = num
+ | raw_step_number (Inference (num, _, _)) = num
-datatype int_or_string = Str of string | Int of int
+(**** PARSING OF TSTP FORMAT ****)
(*Strings enclosed in single quotes, e.g. filenames*)
val scan_quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode;
@@ -91,39 +102,55 @@
val scan_dollar_name =
Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s)
-(* needed for SPASS's output format *)
fun repair_name _ "$true" = "c_True"
| repair_name _ "$false" = "c_False"
| repair_name _ "$$e" = "c_equal" (* seen in Vampire proofs *)
- | repair_name _ "equal" = "c_equal" (* probably not needed *)
- | repair_name pool s = Symtab.lookup pool s |> the_default s
+ | repair_name _ "equal" = "c_equal" (* needed by SPASS? *)
+ | repair_name pool s =
+ case Symtab.lookup pool s of
+ SOME s' => s'
+ | NONE =>
+ if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then
+ "c_equal" (* seen in Vampire proofs *)
+ else
+ s
(* Generalized first-order terms, which include file names, numbers, etc. *)
-(* The "x" argument is not strictly necessary, but without it Poly/ML loops
- forever at compile time. *)
-fun parse_generalized_term x =
- (scan_quoted >> (fn s => ATerm (Str s, []))
- || scan_dollar_name
- -- Scan.optional ($$ "(" |-- parse_generalized_terms --| $$ ")") []
- >> (fn (s, gs) => ATerm (Str s, gs))
- || scan_integer >> (fn k => ATerm (Int k, []))
- || $$ "(" |-- parse_generalized_term --| $$ ")"
- || $$ "[" |-- Scan.optional parse_generalized_terms [] --| $$ "]"
- >> curry ATerm (Str "list")) x
-and parse_generalized_terms x =
- (parse_generalized_term ::: Scan.repeat ($$ "," |-- parse_generalized_term)) x
+val parse_potential_integer =
+ (scan_dollar_name || scan_quoted) >> K NONE
+ || scan_integer >> SOME
+fun parse_annotation x =
+ ((parse_potential_integer ::: Scan.repeat ($$ " " |-- parse_potential_integer)
+ >> map_filter I) -- Scan.optional parse_annotation []
+ >> uncurry (union (op =))
+ || $$ "(" |-- parse_annotations --| $$ ")"
+ || $$ "[" |-- parse_annotations --| $$ "]") x
+and parse_annotations x =
+ (Scan.optional (parse_annotation
+ ::: Scan.repeat ($$ "," |-- parse_annotation)) []
+ >> (fn numss => fold (union (op =)) numss [])) x
+
+(* Vampire proof lines sometimes contain needless information such as "(0:3)",
+ which can be hard to disambiguate from function application in an LL(1)
+ parser. As a workaround, we extend the TPTP term syntax with such detritus
+ and ignore it. *)
+val parse_vampire_detritus = scan_integer |-- $$ ":" --| scan_integer >> K []
+
fun parse_term pool x =
((scan_dollar_name >> repair_name pool)
- -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> ATerm) x
+ -- Scan.optional ($$ "(" |-- (parse_vampire_detritus || parse_terms pool)
+ --| $$ ")") []
+ --| Scan.optional ($$ "(" |-- parse_vampire_detritus --| $$ ")") []
+ >> ATerm) x
and parse_terms pool x =
(parse_term pool ::: Scan.repeat ($$ "," |-- parse_term pool)) x
-fun parse_predicate_term pool =
+fun parse_atom pool =
parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "="
-- parse_term pool)
- >> (fn (u, NONE) => APred u
- | (u1, SOME (NONE, u2)) => APred (ATerm ("c_equal", [u1, u2]))
+ >> (fn (u1, NONE) => AAtom u1
+ | (u1, SOME (NONE, u2)) => AAtom (ATerm ("c_equal", [u1, u2]))
| (u1, SOME (SOME _, u2)) =>
- mk_anot (APred (ATerm ("c_equal", [u1, u2]))))
+ mk_anot (AAtom (ATerm ("c_equal", [u1, u2]))))
fun fo_term_head (ATerm (s, _)) = s
@@ -136,7 +163,7 @@
-- parse_formula pool
>> (fn ((q, ts), phi) => AQuant (q, map fo_term_head ts, phi))
|| $$ "~" |-- parse_formula pool >> mk_anot
- || parse_predicate_term pool)
+ || parse_atom pool)
-- Scan.option ((Scan.this_string "=>" >> K AImplies
|| Scan.this_string "<=>" >> K AIff
|| Scan.this_string "<~>" >> K ANotIff
@@ -146,30 +173,34 @@
>> (fn (phi1, NONE) => phi1
| (phi1, SOME (c, phi2)) => mk_aconn c (phi1, phi2))) x
-fun ints_of_generalized_term (ATerm (label, gs)) =
- fold ints_of_generalized_term gs #> (case label of Int k => cons k | _ => I)
-val parse_tstp_annotations =
- Scan.optional ($$ "," |-- parse_generalized_term
- --| Scan.option ($$ "," |-- parse_generalized_terms)
- >> (fn g => ints_of_generalized_term g [])) []
+val parse_tstp_extra_arguments =
+ Scan.optional ($$ "," |-- parse_annotation
+ --| Scan.option ($$ "," |-- parse_annotations)) []
-(* Syntax: (fof|cnf)\(<num>, <formula_role>, <cnf_formula> <annotations>\).
+(* Syntax: (fof|cnf)\(<num>, <formula_role>, <formula> <extra_arguments>\).
The <num> could be an identifier, but we assume integers. *)
fun parse_tstp_line pool =
((Scan.this_string "fof" || Scan.this_string "cnf") -- $$ "(")
|-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ","
- -- parse_formula pool -- parse_tstp_annotations --| $$ ")" --| $$ "."
+ -- parse_formula pool -- parse_tstp_extra_arguments --| $$ ")" --| $$ "."
>> (fn (((num, role), phi), deps) =>
case role of
"definition" =>
(case phi of
- AConn (AIff, [phi1 as APred _, phi2]) =>
+ AConn (AIff, [phi1 as AAtom _, phi2]) =>
Definition (num, phi1, phi2)
- | APred (ATerm ("$$e", _)) =>
+ | AAtom (ATerm ("c_equal", _)) =>
Inference (num, phi, deps) (* Vampire's equality proxy axiom *)
| _ => raise Fail "malformed definition")
| _ => Inference (num, phi, deps))
+(**** PARSING OF VAMPIRE OUTPUT ****)
+
+(* Syntax: <num>. <formula> <annotation> *)
+fun parse_vampire_line pool =
+ scan_integer --| $$ "." -- parse_formula pool -- parse_annotation
+ >> (fn ((num, phi), deps) => Inference (num, phi, deps))
+
(**** PARSING OF SPASS OUTPUT ****)
(* SPASS returns clause references of the form "x.y". We ignore "y", whose role
@@ -182,10 +213,10 @@
(* It is not clear why some literals are followed by sequences of stars and/or
pluses. We ignore them. *)
-fun parse_decorated_predicate_term pool =
- parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
+fun parse_decorated_atom pool =
+ parse_atom pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
-fun mk_horn ([], []) = APred (ATerm ("c_False", []))
+fun mk_horn ([], []) = AAtom (ATerm ("c_False", []))
| mk_horn ([], pos_lits) = foldr1 (mk_aconn AOr) pos_lits
| mk_horn (neg_lits, []) = mk_anot (foldr1 (mk_aconn AAnd) neg_lits)
| mk_horn (neg_lits, pos_lits) =
@@ -193,19 +224,20 @@
foldr1 (mk_aconn AOr) pos_lits)
fun parse_horn_clause pool =
- Scan.repeat (parse_decorated_predicate_term pool) --| $$ "|" --| $$ "|"
- -- Scan.repeat (parse_decorated_predicate_term pool) --| $$ "-" --| $$ ">"
- -- Scan.repeat (parse_decorated_predicate_term pool)
+ Scan.repeat (parse_decorated_atom pool) --| $$ "|" --| $$ "|"
+ -- Scan.repeat (parse_decorated_atom pool) --| $$ "-" --| $$ ">"
+ -- Scan.repeat (parse_decorated_atom pool)
>> (mk_horn o apfst (op @))
(* Syntax: <num>[0:<inference><annotations>]
- <cnf_formulas> || <cnf_formulas> -> <cnf_formulas>. *)
+ <atoms> || <atoms> -> <atoms>. *)
fun parse_spass_line pool =
scan_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
- -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
+ -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
>> (fn ((num, deps), u) => Inference (num, u, deps))
-fun parse_line pool = parse_tstp_line pool || parse_spass_line pool
+fun parse_line pool =
+ parse_tstp_line pool || parse_vampire_line pool || parse_spass_line pool
fun parse_lines pool = Scan.repeat1 (parse_line pool)
fun parse_proof pool =
fst o Scan.finite Symbol.stopper
@@ -395,8 +427,10 @@
AAnd => s_conj
| AOr => s_disj
| AImplies => s_imp
- | AIff => s_iff)
- | APred tm => term_from_pred thy full_types tfrees pos tm
+ | AIf => s_imp o swap
+ | AIff => s_iff
+ | ANotIff => s_not o s_iff)
+ | AAtom tm => term_from_pred thy full_types tfrees pos tm
| _ => raise FORMULA [phi]
in repair_tvar_sorts (do_formula true phi Vartab.empty) end
@@ -438,8 +472,8 @@
fun decode_lines ctxt full_types tfrees lines =
fst (fold_map (decode_line full_types tfrees) lines ctxt)
-fun aint_actual_inference _ (Definition _) = true
- | aint_actual_inference t (Inference (_, t', _)) = not (t aconv t')
+fun is_same_inference _ (Definition _) = false
+ | is_same_inference t (Inference (_, t', _)) = t aconv t'
(* No "real" literals means only type information (tfree_tcs, clsrel, or
clsarity). *)
@@ -461,7 +495,7 @@
if is_only_type_information t then
map (replace_deps_in_line (num, [])) lines
(* Is there a repetition? If so, replace later line by earlier one. *)
- else case take_prefix (aint_actual_inference t) lines of
+ else case take_prefix (not o is_same_inference t) lines of
(_, []) => lines (*no repetition of proof line*)
| (pre, Inference (num', _, _) :: post) =>
pre @ map (replace_deps_in_line (num', [num])) post
@@ -474,9 +508,9 @@
if is_only_type_information t then
Inference (num, t, deps) :: lines
(* Is there a repetition? If so, replace later line by earlier one. *)
- else case take_prefix (aint_actual_inference t) lines of
+ else case take_prefix (not o is_same_inference t) lines of
(* FIXME: Doesn't this code risk conflating proofs involving different
- types?? *)
+ types? *)
(_, []) => Inference (num, t, deps) :: lines
| (pre, Inference (num', t', _) :: post) =>
Inference (num, t', deps) ::
@@ -522,14 +556,30 @@
(* A list consisting of the first number in each line is returned. For TSTP,
interesting lines have the form "fof(108, axiom, ...)", where the number
(108) is extracted. For SPASS, lines have the form "108[0:Inp] ...", where
- the first number (108) is extracted. *)
-fun extract_formula_numbers_in_atp_proof atp_proof =
+ the first number (108) is extracted. For Vampire, we look for
+ "108. ... [input]". *)
+fun used_facts_in_atp_proof thm_names atp_proof =
let
- val tokens_of = String.tokens (not o Char.isAlphaNum)
- fun extract_num ("fof" :: num :: "axiom" :: _) = Int.fromString num
- | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num
- | extract_num _ = NONE
- in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
+ fun axiom_name num =
+ let val j = Int.fromString num |> the_default ~1 in
+ if is_axiom_clause_number thm_names j then
+ SOME (Vector.sub (thm_names, j - 1))
+ else
+ NONE
+ end
+ val tokens_of =
+ String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
+ val thm_name_list = Vector.foldr (op ::) [] thm_names
+ fun do_line ("fof" :: num :: "axiom" :: (rest as _ :: _)) =
+ (case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of
+ SOME name =>
+ if member (op =) rest "file" then SOME name else axiom_name num
+ | NONE => axiom_name num)
+ | do_line (num :: "0" :: "Inp" :: _) = axiom_name num
+ | do_line (num :: rest) =
+ (case List.last rest of "input" => axiom_name num | _ => NONE)
+ | do_line _ = NONE
+ in atp_proof |> split_lines |> map_filter (do_line o tokens_of) end
val indent_size = 2
val no_label = ("", ~1)
@@ -560,15 +610,13 @@
case minimize_command facts of
"" => ""
| command =>
- "To minimize the number of lemmas, try this command: " ^
+ "To minimize the number of lemmas, try this: " ^
Markup.markup Markup.sendback command ^ ".\n"
val unprefix_chained = perhaps (try (unprefix chained_prefix))
fun used_facts thm_names =
- extract_formula_numbers_in_atp_proof
- #> filter (is_axiom_clause_number thm_names)
- #> map (fn i => Vector.sub (thm_names, i - 1))
+ used_facts_in_atp_proof thm_names
#> List.partition (String.isPrefix chained_prefix)
#>> map (unprefix chained_prefix)
#> pairself (sort_distinct string_ord)
@@ -626,8 +674,9 @@
atp_proof conjecture_shape thm_names params frees =
let
val lines =
- atp_proof ^ "$" (* the $ sign acts as a sentinel (FIXME: pick it up) *)
+ atp_proof ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
|> parse_proof pool
+ |> sort (int_ord o pairself raw_step_number)
|> decode_lines ctxt full_types tfrees
|> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
|> rpair [] |-> fold_rev add_nontrivial_line
@@ -693,28 +742,37 @@
conjecture. The second pass flips the proof by contradiction to obtain a
direct proof, introducing case splits when an inference depends on
several facts that depend on the negated conjecture. *)
- fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape)
- val concl_l = (raw_prefix, List.last conjecture_shape)
- fun first_pass ([], contra) = ([], contra)
- | first_pass ((step as Fix _) :: proof, contra) =
- first_pass (proof, contra) |>> cons step
- | first_pass ((step as Let _) :: proof, contra) =
- first_pass (proof, contra) |>> cons step
- | first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) =
- if l = concl_l then
- first_pass (proof, contra ||> l = concl_l ? cons step)
- else
- first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
- | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
- let val step = Have (qs, l, t, ByMetis (ls, ss)) in
- if exists (member (op =) (fst contra)) ls then
- first_pass (proof, contra |>> cons l ||> cons step)
- else
- first_pass (proof, contra) |>> cons step
- end
- | first_pass _ = raise Fail "malformed proof"
+ fun find_hyp num =
+ nth hyp_ts (index_in_shape num conjecture_shape)
+ handle Subscript =>
+ raise Fail ("Cannot find hypothesis " ^ Int.toString num)
+ val concl_ls = map (pair raw_prefix) (List.last conjecture_shape)
+ val canonicalize_labels =
+ map (fn l => if member (op =) concl_ls l then hd concl_ls else l)
+ #> distinct (op =)
+ fun first_pass ([], contra) = ([], contra)
+ | first_pass ((step as Fix _) :: proof, contra) =
+ first_pass (proof, contra) |>> cons step
+ | first_pass ((step as Let _) :: proof, contra) =
+ first_pass (proof, contra) |>> cons step
+ | first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) =
+ if member (op =) concl_ls l then
+ first_pass (proof, contra ||> l = hd concl_ls ? cons step)
+ else
+ first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
+ | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
+ let
+ val ls = canonicalize_labels ls
+ val step = Have (qs, l, t, ByMetis (ls, ss))
+ in
+ if exists (member (op =) (fst contra)) ls then
+ first_pass (proof, contra |>> cons l ||> cons step)
+ else
+ first_pass (proof, contra) |>> cons step
+ end
+ | first_pass _ = raise Fail "malformed proof"
val (proof_top, (contra_ls, contra_proof)) =
- first_pass (proof, ([concl_l], []))
+ first_pass (proof, (concl_ls, []))
val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
fun backpatch_labels patches ls =
fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
@@ -749,7 +807,7 @@
val proofs =
map_filter
(fn l =>
- if l = concl_l then
+ if member (op =) concl_ls l then
NONE
else
let
@@ -953,7 +1011,7 @@
|> kill_useless_labels_in_proof
|> relabel_proof
|> string_for_proof ctxt full_types i n of
- "" => ""
+ "" => "No structured proof available.\n"
| proof => "\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
val isar_proof =
if debug then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 28 11:42:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 28 22:18:35 2010 +0200
@@ -17,6 +17,7 @@
val maybe_quote : string -> string
val monomorphic_term : Type.tyenv -> term -> term
val specialize_type : theory -> (string * typ) -> term -> term
+ val subgoal_count : Proof.state -> int
val strip_subgoal : thm -> int -> (string * typ) list * term list * term
end;
@@ -124,6 +125,8 @@
| NONE => raise Type.TYPE_MATCH
end
+val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
+
fun strip_subgoal goal i =
let
val (t, frees) = Logic.goal_params (prop_of goal) i