version of sledgehammer using threads instead of processes, misc cleanup;
(by Fabian Immler);
--- a/src/HOL/ATP_Linkup.thy Fri Oct 03 15:20:33 2008 +0200
+++ b/src/HOL/ATP_Linkup.thy Fri Oct 03 16:37:09 2008 +0200
@@ -4,18 +4,19 @@
Author: Jia Meng, NICTA
*)
-header{* The Isabelle-ATP Linkup *}
+header {* The Isabelle-ATP Linkup *}
theory ATP_Linkup
imports Record Hilbert_Choice
uses
"Tools/polyhash.ML"
"Tools/res_clause.ML"
+ ("Tools/res_axioms.ML")
("Tools/res_hol_clause.ML")
- ("Tools/res_axioms.ML")
("Tools/res_reconstruct.ML")
- ("Tools/watcher.ML")
("Tools/res_atp.ML")
+ ("Tools/atp_manager.ML")
+ ("Tools/atp_thread.ML")
"~~/src/Tools/Metis/metis.ML"
("Tools/metis_tools.ML")
begin
@@ -89,15 +90,12 @@
subsection {* Setup of Vampire, E prover and SPASS *}
-use "Tools/res_axioms.ML" --{*requires the combinators declared above*}
-setup ResAxioms.setup
-
+use "Tools/res_axioms.ML" setup ResAxioms.setup
use "Tools/res_hol_clause.ML"
-use "Tools/res_reconstruct.ML"
-use "Tools/watcher.ML"
+use "Tools/res_reconstruct.ML" setup ResReconstruct.setup
use "Tools/res_atp.ML"
-
-setup ResReconstruct.setup --{*Config parameters*}
+use "Tools/atp_manager.ML"
+use "Tools/atp_thread.ML" setup AtpThread.setup
subsection {* The Metis prover *}
--- a/src/HOL/IsaMakefile Fri Oct 03 15:20:33 2008 +0200
+++ b/src/HOL/IsaMakefile Fri Oct 03 16:37:09 2008 +0200
@@ -216,6 +216,8 @@
Tools/Groebner_Basis/misc.ML \
Tools/Groebner_Basis/normalizer_data.ML \
Tools/Groebner_Basis/normalizer.ML \
+ Tools/atp_manager.ML \
+ Tools/atp_thread.ML \
Tools/meson.ML \
Tools/metis_tools.ML \
Tools/numeral.ML \
@@ -242,8 +244,7 @@
Tools/TFL/thms.ML \
Tools/TFL/thry.ML \
Tools/TFL/usyntax.ML \
- Tools/TFL/utils.ML \
- Tools/watcher.ML
+ Tools/TFL/utils.ML
$(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
@$(ISATOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp_manager.ML Fri Oct 03 16:37:09 2008 +0200
@@ -0,0 +1,272 @@
+(* Title: HOL/Tools/atp_manager.ML
+ ID: $Id$
+ Author: Fabian Immler, TU Muenchen
+
+ATP threads have to be registered here. Threads with the same
+birth-time are seen as one group. All threads of a group are killed
+when one thread of it has been successful, or after a certain time, or
+when the maximum number of threads exceeds; then the oldest thread is
+killed.
+*)
+
+signature PROVERS =
+sig
+ type T
+ val get : Context.theory -> T
+ val init : Context.theory -> Context.theory
+ val map :
+ (T -> T) ->
+ Context.theory -> Context.theory
+ val put : T -> Context.theory -> Context.theory
+end;
+
+signature ATP_MANAGER =
+sig
+ val kill_all: unit -> unit
+ val info: unit -> unit
+ val set_atps: string -> unit
+ val set_max_atp: int -> unit
+ val set_timeout: int -> unit
+ val set_groupkilling: bool -> unit
+ val start: unit -> unit
+ val register: Time.time -> Time.time -> (Thread.thread * string) -> unit
+ val unregister: bool -> unit
+
+ structure Provers : PROVERS
+ val sledgehammer: Toplevel.state -> unit
+end;
+
+structure AtpManager : ATP_MANAGER =
+struct
+
+ structure ThreadHeap = HeapFun (
+ struct
+ type elem = (Time.time * Thread.thread);
+ fun ord ((a,_),(b,_)) = Time.compare (a, b);
+ end);
+
+ (* create global state of threadmanager *)
+ val timeout_heap = ref ThreadHeap.empty
+ val oldest_heap = ref ThreadHeap.empty
+ (* managed threads *)
+ val active = ref ([] : (Thread.thread * Time.time * Time.time * string) list)
+ val cancelling = ref ([] : (Thread.thread * Time.time * Time.time * string) list)
+ (* settings *)
+ val atps = ref "e,spass"
+ val maximum_atps = ref 5 (* ~1 means infinite number of atps*)
+ val timeout = ref 60
+ val groupkilling = ref true
+ (* synchronizing *)
+ val lock = Mutex.mutex () (* to be aquired for changing state *)
+ val state_change = ConditionVar.conditionVar () (* signal when state changes *)
+ (* watches over running threads and interrupts them if required *)
+ val managing_thread = ref (Thread.fork (fn () => (), []))
+
+ (* move a thread from active to cancelling
+ managing_thread trys to interrupt all threads in cancelling
+
+ call from an environment where a lock has already been aquired *)
+ fun unregister_locked thread =
+ let val entrys = (filter (fn (t,_,_,_) => Thread.equal (t, thread))) (! active)
+ val entrys_update = map (fn (th, tb, _, desc) => (th, tb, Time.now(), desc)) entrys
+ val _ = change cancelling (append entrys_update)
+ val _ = change active (filter_out (fn (t,_,_,_) => Thread.equal (t, thread)))
+ in () end;
+
+ (* start a watching thread which runs forever *)
+ (* must *not* be called more than once!! => problem with locks *)
+ fun start () =
+ let
+ val new_thread = Thread.fork (fn () =>
+ let
+ (* never give up lock except for waiting *)
+ val _ = Mutex.lock lock
+ fun wait_for_next_event time =
+ let
+ (* wait for signal or next timeout, give up lock meanwhile *)
+ val _ = ConditionVar.waitUntil (state_change, lock, time)
+ (* move threads with priority less than Time.now() to cancelling *)
+ fun cancelolder heap =
+ if ThreadHeap.is_empty heap then heap else
+ let val (mintime, minthread) = ThreadHeap.min heap
+ in
+ if mintime > Time.now() then heap
+ else (unregister_locked minthread;
+ cancelolder (ThreadHeap.delete_min heap))
+ end
+ val _ = change timeout_heap cancelolder
+ (* try to interrupt threads that are to cancel*)
+ fun interrupt t = Thread.interrupt t handle Thread _ => ()
+ val _ = change cancelling (filter (fn (t,_,_,_) => Thread.isActive t))
+ val _ = map (fn (t, _, _, _) => interrupt t) (! cancelling)
+ (* if there are threads to cancel, send periodic interrupts *)
+ (* TODO: find out what realtime-values are appropriate *)
+ val next_time =
+ if length (! cancelling) > 0 then
+ Time.now() + Time.fromMilliseconds 300
+ else if ThreadHeap.is_empty (! timeout_heap) then
+ Time.now() + Time.fromSeconds 10
+ else
+ #1 (ThreadHeap.min (! timeout_heap))
+ in
+ wait_for_next_event next_time
+ end
+ in wait_for_next_event Time.zeroTime end,
+ [Thread.InterruptState Thread.InterruptDefer])
+ in managing_thread := new_thread end
+
+ (* calling thread registers itself to be managed here with a relative timeout *)
+ fun register birthtime deadtime (thread, name) =
+ let
+ val _ = Mutex.lock lock
+ (* create the atp-managing-thread if this is the first call to register *)
+ val _ = if Thread.isActive (! managing_thread) then () else start ()
+ (* insertion *)
+ val _ = change timeout_heap (ThreadHeap.insert (deadtime, thread))
+ val _ = change oldest_heap (ThreadHeap.insert (birthtime, thread))
+ val _ = change active (cons (thread, birthtime, deadtime, name))
+ (*maximum number of atps must not exceed*)
+ val _ = let
+ fun kill_oldest () =
+ let val (_, oldest_thread) = ThreadHeap.min (!oldest_heap)
+ val _ = change oldest_heap (ThreadHeap.delete_min)
+ in unregister_locked oldest_thread end
+ in
+ while ! maximum_atps > ~1 andalso length (! active) > ! maximum_atps
+ do kill_oldest ()
+ end
+ (* state of threadmanager changed => signal *)
+ val _ = ConditionVar.signal state_change
+ val _ = Mutex.unlock lock
+ in () end
+
+ (* calling Thread unregisters itself from Threadmanager; thread is responsible
+ to terminate after calling this method *)
+ fun unregister success =
+ let val _ = Mutex.lock lock
+ val thread = Thread.self ()
+ (* get birthtime of unregistering thread - for group-killing*)
+ fun get_birthtime [] = Time.zeroTime
+ | get_birthtime ((t,tb,td,desc)::actives) = if Thread.equal (thread, t)
+ then tb
+ else get_birthtime actives
+ val birthtime = get_birthtime (! active)
+ (* remove unregistering thread *)
+ val _ = change active (filter_out (fn (t,_,_,_) => Thread.equal (t, thread)))
+ val _ = if (! groupkilling) andalso success
+ then (* remove all threads of the same group *)
+ let
+ val group_threads = filter (fn (_, tb, _, _) => tb = birthtime) (! active)
+ val _ = change cancelling (append group_threads)
+ val _ = change active (filter_out (fn (_, tb, _, _) => tb = birthtime))
+ in () end
+ else ()
+ val _ = ConditionVar.signal state_change
+ val _ = Mutex.unlock lock
+ in () end;
+
+ (* Move all threads to cancelling *)
+ fun kill_all () =
+ let
+ val _ = Mutex.lock lock
+ val _ = change active (map (fn (th, tb, _, desc) => (th, tb, Time.now(), desc)))
+ val _ = change cancelling (append (! active))
+ val _ = change active (fn _ => [])
+ val _ = ConditionVar.signal state_change
+ val _ = Mutex.unlock lock
+ in () end;
+
+ fun info () =
+ let
+ val _ = Mutex.lock lock
+ fun running_info (_, birth_time, dead_time, desc) =
+ priority ("Running: "
+ ^ ((Int.toString o Time.toSeconds) (Time.now() - birth_time))
+ ^ " s -- "
+ ^ ((Int.toString o Time.toSeconds) (dead_time - Time.now()))
+ ^ " s to live:\n" ^ desc)
+ fun cancelling_info (_, _, dead_time, desc) =
+ priority ("Trying to interrupt thread since "
+ ^ (Int.toString o Time.toSeconds) (Time.now() - dead_time)
+ ^ " s:\n" ^ desc )
+ val _ = if length (! active) = 0 then [priority "No ATPs running."]
+ else (priority "--- RUNNING ATPs ---";
+ map (fn entry => running_info entry) (! active))
+ val _ = if length (! cancelling) = 0 then []
+ else (priority "--- TRYING TO INTERRUPT FOLLOWING ATPs ---";
+ map (fn entry => cancelling_info entry) (! cancelling))
+ val _ = Mutex.unlock lock
+ in () end;
+
+ (* integration into ProofGeneral *)
+
+ fun set_max_atp number = CRITICAL (fn () => maximum_atps := number);
+ fun set_atps str = CRITICAL (fn () => atps := str);
+ fun set_timeout time = CRITICAL (fn () => timeout := time);
+ fun set_groupkilling boolean = CRITICAL (fn () => groupkilling := boolean);
+
+ (* some settings will be accessible via Isabelle -> Settings *)
+ val _ = ProofGeneralPgip.add_preference "Proof"
+ {name = "ATP - Provers (e,vampire,spass)",
+ descr = "Which external automatic provers (seperated by commas)",
+ default = !atps,
+ pgiptype = PgipTypes.Pgipstring,
+ get = fn () => !atps,
+ set = set_atps} handle Error => warning "Preference already exists";
+ val _ = ProofGeneralPgip.add_preference "Proof"
+ {name = "ATP - Maximum number",
+ descr = "How many provers may run parallel",
+ default = Int.toString (! maximum_atps),
+ pgiptype = PgipTypes.Pgipstring,
+ get = fn () => Int.toString (! maximum_atps),
+ set = (fn str => let val int_opt = Int.fromString str
+ val nr = if isSome int_opt then valOf int_opt else 1
+ in set_max_atp nr end)} handle Error => warning "Preference already exists";
+ val _ = ProofGeneralPgip.add_preference "Proof"
+ {name = "ATP - Timeout",
+ descr = "ATPs will be interrupted after this time (in seconds)",
+ default = Int.toString (! timeout),
+ pgiptype = PgipTypes.Pgipstring,
+ get = fn () => Int.toString (! timeout),
+ set = (fn str => let val int_opt = Int.fromString str
+ val nr = if isSome int_opt then valOf int_opt else 60
+ in set_timeout nr end)} handle Error => warning "Preference already exists";
+
+ (* Additional Provers can be added as follows:
+ SPASS with max_new 40 and theory_const false, timeout 60
+ setup{* AtpManager.Provers.map (Symtab.update ("spass2", AtpThread.spass 40 false 60)) *}
+ arbitrary prover supporting tptp-input/output
+ setup{* AtpManagerProvers.map (Symtab.update ("tptp", AtpThread.tptp_prover "path/to/prover -options" 60)) *}
+ *)
+ structure Provers = TheoryDataFun
+ (
+ type T = (Toplevel.state -> (Thread.thread * string)) Symtab.table
+ val empty = Symtab.empty
+ val copy = I
+ val extend = I
+ fun merge _ = Symtab.merge (K true)
+ );
+
+ (* sledghammer: *)
+ fun sledgehammer state =
+ let
+ val proverids = String.tokens (fn c => c = #",") (! atps)
+ (* get context *)
+ val (ctxt, _) = Proof.get_goal (Toplevel.proof_of state)
+ val thy = ProofContext.theory_of ctxt
+ (* get prover-functions *)
+ val lookups = map (fn prover => Symtab.lookup (Provers.get thy) prover)
+ proverids
+ val filtered_calls = filter (fn call => isSome call) lookups
+ val calls = map (fn some => valOf some) filtered_calls
+ (* call provers *)
+ val threads_names = map (fn call => call state) calls
+ val birthtime = Time.now()
+ val deadtime = Time.now() + (Time.fromSeconds (! timeout))
+ val _ = map (register birthtime deadtime) threads_names
+ in () end
+
+ val _ =
+ OuterSyntax.command "sledgehammer" "call all automatic theorem provers" OuterKeyword.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer));
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp_thread.ML Fri Oct 03 16:37:09 2008 +0200
@@ -0,0 +1,201 @@
+(* Title: HOL/Tools/atp_thread.ML
+ ID: $Id$
+ Author: Fabian Immler, TU Muenchen
+
+Automatic provers as managed threads.
+*)
+
+signature ATP_THREAD =
+sig
+ (* basic templates *)
+ val atp_thread: (unit -> 'a option) -> ('a -> unit) -> string -> Thread.thread * string
+ val external_prover:int ->
+ ((int -> Path.T) -> Proof.context * Thm.thm list * Thm.thm -> string list * ResHolClause.axiom_name Vector.vector list) ->
+ string ->
+ (string * int -> bool) ->
+ (string * string vector * Proof.context * Thm.thm * int -> string) ->
+ Toplevel.state -> Thread.thread * string
+ (* settings for writing problemfiles *)
+ val destdir: string ref
+ val problem_name: string ref
+ (* provers as functions returning threads *)
+ val tptp_prover_filter_opts_full: int -> bool -> bool -> string -> Toplevel.state -> (Thread.thread * string)
+ val tptp_prover_filter_opts: int -> bool -> string -> Toplevel.state -> (Thread.thread * string)
+ val full_prover_filter_opts: int -> bool -> string -> Toplevel.state -> (Thread.thread * string)
+ val tptp_prover: string -> Toplevel.state -> (Thread.thread * string)
+ val full_prover: string -> Toplevel.state -> (Thread.thread * string) val spass_filter_opts: int -> bool -> Toplevel.state -> (Thread.thread * string)
+ val eprover_filter_opts: int -> bool -> Toplevel.state -> (Thread.thread * string)
+ val eprover_filter_opts_full: int -> bool -> Toplevel.state -> (Thread.thread * string)
+ val vampire_filter_opts: int -> bool -> Toplevel.state -> (Thread.thread * string)
+ val vampire_filter_opts_full: int -> bool -> Toplevel.state -> (Thread.thread * string)
+ val spass: Toplevel.state -> (Thread.thread * string)
+ val eprover: Toplevel.state -> (Thread.thread * string)
+ val eprover_full: Toplevel.state -> (Thread.thread * string)
+ val vampire: Toplevel.state -> (Thread.thread * string)
+ val vampire_full: Toplevel.state -> (Thread.thread * string)
+ val setup: theory -> theory
+end;
+
+structure AtpThread : ATP_THREAD =
+struct
+
+ structure Recon = ResReconstruct
+
+ (* if a thread calls priority while PG works on a ML{**}-block, PG will not leave the block *)
+ fun delayed_priority s = (OS.Process.sleep (Time.fromMilliseconds 100); priority s);
+
+ (* -------- AUTOMATIC THEOREM PROVERS AS THREADS ----------*)
+
+ (* create an automatic-prover thread, registering has to be done by sledgehammer
+ or manual via AtpManager.register;
+ unregistering is done by thread.
+ *)
+ fun atp_thread call_prover action_success description =
+ let val thread = Thread.fork(fn () =>
+ let
+ val answer = call_prover ()
+ val _ = if isSome answer then action_success (valOf answer)
+ else delayed_priority ("Sledgehammer: " ^ description ^ "\n failed.")
+ in AtpManager.unregister (isSome answer)
+ end
+ handle Interrupt => delayed_priority ("Sledgehammer: " ^ description ^ "\n interrupted.")
+ ,[Thread.EnableBroadcastInterrupt true,
+ Thread.InterruptState Thread.InterruptAsynch])
+ in (thread, description) end
+
+ (* Settings for path and filename to problemfiles *)
+ val destdir = ref ""; (*Empty means write files to /tmp*)
+ val problem_name = ref "prob";
+
+ (*Setting up a Thread for an external prover*)
+ fun external_prover subgoalno write_problem_files command check_success produce_answer state =
+ let
+ (*creating description from provername and subgoal*)
+ val call::path = rev (String.tokens (fn c => c = #"/") command)
+ val name::options = String.tokens (fn c => c = #" ") call
+ val (ctxt, (chain_ths, goal)) = Proof.get_goal (Toplevel.proof_of state)
+ val description = "External prover '" ^ name ^ "' for Subgoal " ^ Int.toString subgoalno
+ ^ ":\n" ^ Display.string_of_cterm (List.nth(cprems_of goal, subgoalno-1))
+ (* path to unique problemfile *)
+ fun prob_pathname nr =
+ let val probfile = Path.basic (!problem_name ^ serial_string () ^ "_" ^ Int.toString nr)
+ in if !destdir = "" then File.tmp_path probfile
+ else if File.exists (Path.explode (!destdir))
+ then (Path.append (Path.explode (!destdir)) probfile)
+ else error ("No such directory: " ^ !destdir)
+ end
+ (* write out problem file and call prover *)
+ fun call_prover () =
+ let
+ val chain_ths = map (Thm.put_name_hint Recon.chained_hint) chain_ths
+ val (filenames, thm_names_list) =
+ write_problem_files prob_pathname (ctxt, chain_ths, goal)
+ val thm_names = List.nth(thm_names_list, subgoalno - 1);(*(i-1)th element for i-th subgoal*)
+ val (proof, rc) = system_out (command ^ " " ^ List.nth(filenames, subgoalno - 1))
+ val _ = map (fn file => OS.FileSys.remove file) filenames
+ in
+ if check_success (proof, rc) then SOME (proof, thm_names, ctxt, goal, subgoalno)
+ else NONE
+ end
+ (* output answer of res_reconstruct with description of subgoal *)
+ fun action_success result =
+ let
+ val answer = produce_answer result
+ val _ = priority ("Sledgehammer: " ^ description ^ "\n Try this command: " ^ answer)
+ in () end
+ in
+ atp_thread call_prover action_success description
+ end;
+
+ (*=========== TEMPLATES FOR AUTOMATIC PROVERS =================*)
+
+ fun tptp_prover_filter_opts_full max_new theory_const full command state =
+ external_prover 1
+ (ResAtp.write_problem_files ResHolClause.tptp_write_file max_new theory_const)
+ command
+ Recon.check_success_e_vamp_spass
+ (if full then Recon.structured_proof else Recon.lemma_list_tstp)
+ state;
+
+ (* arbitrary atp with tptp input/output and problemfile as last argument*)
+ fun tptp_prover_filter_opts max_new theory_const =
+ tptp_prover_filter_opts_full max_new theory_const false;
+ (* default settings*)
+ val tptp_prover = tptp_prover_filter_opts 60 true;
+
+ (* for structured proofs: prover must support tstp! *)
+ fun full_prover_filter_opts max_new theory_const =
+ tptp_prover_filter_opts_full max_new theory_const true;
+ (* default settings*)
+ val full_prover = full_prover_filter_opts 60 true;
+
+ (* Return the path to a "helper" like SPASS, E or Vampire, first checking that
+ it exists. *)
+ fun prover_command path =
+ if File.exists path then File.shell_path path
+ else error ("Could not find the file '" ^ (Path.implode o Path.expand) path ^ "'")
+
+ (* a vampire for first subgoal *)
+ fun vampire_filter_opts max_new theory_const state = tptp_prover_filter_opts
+ max_new theory_const
+ (prover_command (Path.explode "$VAMPIRE_HOME/vampire")
+ ^ " --output_syntax tptp --mode casc -t 3600") (* vampire does not work without timelimit*)
+ state;
+ (* default settings*)
+ val vampire = vampire_filter_opts 60 false;
+ (* a vampire for full proof output *)
+ fun vampire_filter_opts_full max_new theory_const state = full_prover_filter_opts
+ max_new theory_const
+ (prover_command (Path.explode "$VAMPIRE_HOME/vampire")
+ ^ " --output_syntax tptp --mode casc -t 3600") (* vampire does not work without timelimit*)
+ state;
+ (* default settings*)
+ val vampire_full = vampire_filter_opts 60 false;
+
+ (* an E for first subgoal *)
+ fun eprover_filter_opts max_new theory_const state = tptp_prover_filter_opts
+ max_new theory_const
+ (prover_command (Path.explode "$E_HOME/eproof")
+ ^ " --tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent")
+ state;
+ (* default settings *)
+ val eprover = eprover_filter_opts 100 false;
+ (* an E for full proof output*)
+ fun eprover_filter_opts_full max_new theory_const state = full_prover_filter_opts
+ max_new theory_const
+ (prover_command (Path.explode "$E_HOME/eproof")
+ ^ " --tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent")
+ state;
+ (* default settings *)
+ val eprover_full = eprover_filter_opts_full 100 false;
+
+ (* SPASS for first subgoal *)
+ fun spass_filter_opts max_new theory_const state = external_prover 1
+ (ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const)
+ (prover_command (Path.explode "$SPASS_HOME/SPASS")
+ ^ " -Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof")
+ Recon.check_success_e_vamp_spass
+ Recon.lemma_list_dfg
+ state;
+ (* default settings*)
+ val spass = spass_filter_opts 40 true;
+
+ (*TODO: Thread running some selected or recommended provers of "System On TPTP" *)
+
+
+
+ fun add_prover name prover_fun = AtpManager.Provers.map (Symtab.update (name, prover_fun))
+
+ (* include 'original' provers and provers with structured output *)
+ val setup =
+ (* original setups *)
+ add_prover "spass" spass #>
+ add_prover "vampire" vampire #>
+ add_prover "e" eprover #>
+ (* provers with stuctured output *)
+ add_prover "vampire_full" vampire_full #>
+ add_prover "e_full" eprover_full #>
+ (* on some problems better results *)
+ add_prover "spass_no_tc" (spass_filter_opts 40 false);
+
+end;
--- a/src/HOL/Tools/res_atp.ML Fri Oct 03 15:20:33 2008 +0200
+++ b/src/HOL/Tools/res_atp.ML Fri Oct 03 16:37:09 2008 +0200
@@ -1,163 +1,56 @@
(* Author: Jia Meng, Cambridge University Computer Laboratory, NICTA
ID: $Id$
Copyright 2004 University of Cambridge
-
-ATPs with TPTP format input.
*)
signature RES_ATP =
sig
- val prover: ResReconstruct.atp ref
- val destdir: string ref
- val helper_path: string -> string -> string
- val problem_name: string ref
- val time_limit: int ref
- val set_prover: string -> unit
-
datatype mode = Auto | Fol | Hol
- val linkup_logic_mode : mode ref
- val write_subgoal_file: bool -> mode -> Proof.context -> thm list -> thm list -> int -> string
- val cond_rm_tmp: string -> unit
- val include_all: bool ref
- val run_relevance_filter: bool ref
- val run_blacklist_filter: bool ref
- val theory_const : bool ref
- val pass_mark : real ref
- val convergence : real ref
- val max_new : int ref
- val max_sledgehammers : int ref
- val follow_defs : bool ref
- val add_all : unit -> unit
- val add_claset : unit -> unit
- val add_simpset : unit -> unit
- val add_clasimp : unit -> unit
- val add_atpset : unit -> unit
- val rm_all : unit -> unit
- val rm_claset : unit -> unit
- val rm_simpset : unit -> unit
- val rm_atpset : unit -> unit
- val rm_clasimp : unit -> unit
val tvar_classes_of_terms : term list -> string list
val tfree_classes_of_terms : term list -> string list
val type_consts_of_terms : theory -> term list -> string list
+ val write_problem_files : (theory -> bool -> Thm.thm list -> string ->
+ (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list * ResClause.classrelClause list *
+ ResClause.arityClause list -> string list -> ResHolClause.axiom_name list)
+ -> int -> bool
+ -> (int -> Path.T) -> Proof.context * thm list * thm
+ -> string list * ResHolClause.axiom_name Vector.vector list
end;
structure ResAtp: RES_ATP =
struct
-structure Recon = ResReconstruct;
-
-fun timestamp s = Output.debug (fn () => ("At " ^ Time.toString (Time.now()) ^ ": " ^ s));
(********************************************************************)
(* some settings for both background automatic ATP calling procedure*)
(* and also explicit ATP invocation methods *)
(********************************************************************)
+(*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
+datatype mode = Auto | Fol | Hol;
+
+val linkup_logic_mode = Auto;
+
(*** background linkup ***)
-val run_blacklist_filter = ref true;
-val time_limit = ref 60;
-val prover = ref Recon.E;
-val max_sledgehammers = ref 1;
-
+val run_blacklist_filter = true;
(*** relevance filter parameters ***)
-val run_relevance_filter = ref true;
-val theory_const = ref true;
-val pass_mark = ref 0.5;
-val convergence = ref 3.2; (*Higher numbers allow longer inference chains*)
-val max_new = ref 60; (*Limits how many clauses can be picked up per stage*)
-val follow_defs = ref false; (*Follow definitions. Makes problems bigger.*)
-
-(* could both be hidden: *)
-val atp_ref = ref "E";
-
-fun set_prover atp =
- (case String.map Char.toLower atp of
- "e" =>
- (max_new := 100;
- theory_const := false;
- prover := Recon.E)
- | "spass" =>
- (max_new := 40;
- theory_const := true;
- prover := Recon.SPASS)
- | "vampire" =>
- (max_new := 60;
- theory_const := false;
- prover := Recon.Vampire)
- | _ => error ("No such prover: " ^ atp);
- atp_ref := atp);
-
-val _ = ProofGeneralPgip.add_preference "Proof"
- {name = "ATP (e/vampire/spass)",
- descr = "Which external automatic prover",
- default = !atp_ref,
- pgiptype = PgipTypes.Pgipstring,
- get = fn () => !atp_ref,
- set = set_prover};
-
-
-val destdir = ref ""; (*Empty means write files to /tmp*)
-val problem_name = ref "prob";
-
-(*Return the path to a "helper" like SPASS or tptp2X, first checking that
- it exists. FIXME: modify to use Path primitives and move to some central place.*)
-fun helper_path evar base =
- case getenv evar of
- "" => error ("Isabelle environment variable " ^ evar ^ " not defined")
- | home =>
- let val path = home ^ "/" ^ base
- in if File.exists (Path.explode path) then path
- else error ("Could not find the file " ^ path)
- end;
-
-fun probfile_nosuffix _ =
- if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
- else if File.exists (Path.explode (!destdir))
- then !destdir ^ "/" ^ !problem_name
- else error ("No such directory: " ^ !destdir);
-
-fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n;
-
-fun atp_input_file () =
- let val file = !problem_name
- in
- if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file))
- else if File.exists (Path.explode (!destdir))
- then !destdir ^ "/" ^ file
- else error ("No such directory: " ^ !destdir)
- end;
-
-val include_all = ref true;
-val include_simpset = ref false;
-val include_claset = ref false;
-val include_atpset = ref true;
-
-(*Tests show that follow_defs gives VERY poor results with "include_all"*)
-fun add_all() = (include_all:=true; follow_defs := false);
-fun rm_all() = include_all:=false;
-
-fun add_simpset() = include_simpset:=true;
-fun rm_simpset() = include_simpset:=false;
-
-fun add_claset() = include_claset:=true;
-fun rm_claset() = include_claset:=false;
-
-fun add_clasimp() = (include_simpset:=true;include_claset:=true);
-fun rm_clasimp() = (include_simpset:=false;include_claset:=false);
-
-fun add_atpset() = include_atpset:=true;
-fun rm_atpset() = include_atpset:=false;
+val run_relevance_filter = true;
+val pass_mark = 0.5;
+val convergence = 3.2; (*Higher numbers allow longer inference chains*)
+val follow_defs = false; (*Follow definitions. Makes problems bigger.*)
+val include_all = true;
+val include_simpset = false;
+val include_claset = false;
+val include_atpset = true;
+
+(***************************************************************)
+(* Relevance Filtering *)
+(***************************************************************)
fun strip_Trueprop (Const("Trueprop",_) $ t) = t
| strip_Trueprop t = t;
-
-(***************************************************************)
-(* Relevance Filtering *)
-(***************************************************************)
-
(*A surprising number of theorems contain only a few significant constants.
These include all induction rules, and other general theorems. Filtering
theorems in clause form reveals these complexities in the form of Skolem
@@ -168,7 +61,7 @@
(*The default seems best in practice. A constant function of one ignores
the constant frequencies.*)
-val weight_fn = ref log_weight2;
+val weight_fn = log_weight2;
(*Including equality in this list might be expected to stop rules like subset_antisym from
@@ -234,8 +127,8 @@
(*Inserts a dummy "constant" referring to the theory name, so that relevance
takes the given theory into account.*)
-fun const_prop_of th =
- if !theory_const then
+fun const_prop_of theory_const th =
+ if theory_const then
let val name = Context.theory_name (theory_of_thm th)
val t = Const (name ^ ". 1", HOLogic.boolT)
in t $ prop_of th end
@@ -264,7 +157,7 @@
structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord);
-fun count_axiom_consts thy ((thm,_), tab) =
+fun count_axiom_consts theory_const thy ((thm,_), tab) =
let fun count_const (a, T, tab) =
let val (c, cts) = const_with_typ thy (a,T)
in (*Two-dimensional table update. Constant maps to types maps to count.*)
@@ -277,7 +170,7 @@
count_term_consts (t, count_term_consts (u, tab))
| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
| count_term_consts (_, tab) = tab
- in count_term_consts (const_prop_of thm, tab) end;
+ in count_term_consts (const_prop_of theory_const thm, tab) end;
(**** Actual Filtering Code ****)
@@ -290,7 +183,7 @@
(*Add in a constant's weight, as determined by its frequency.*)
fun add_ct_weight ctab ((c,T), w) =
- w + !weight_fn (real (const_frequency ctab (c,T)));
+ w + weight_fn (real (const_frequency ctab (c,T)));
(*Relevant constants are weighted according to frequency,
but irrelevant constants are simply counted. Otherwise, Skolem functions,
@@ -309,8 +202,8 @@
let val tab = add_term_consts_typs_rm thy (t, null_const_tab)
in Symtab.fold add_expand_pairs tab [] end;
-fun pair_consts_typs_axiom thy (thm,name) =
- ((thm,name), (consts_typs_of_term thy (const_prop_of thm)));
+fun pair_consts_typs_axiom theory_const thy (thm,name) =
+ ((thm,name), (consts_typs_of_term thy (const_prop_of theory_const thm)));
exception ConstFree;
fun dest_ConstFree (Const aT) = aT
@@ -340,40 +233,40 @@
fun compare_pairs ((_,w1),(_,w2)) = Real.compare (w2,w1);
(*Limit the number of new clauses, to prevent runaway acceptance.*)
-fun take_best (newpairs : (annotd_cls*real) list) =
+fun take_best max_new (newpairs : (annotd_cls*real) list) =
let val nnew = length newpairs
in
- if nnew <= !max_new then (map #1 newpairs, [])
+ if nnew <= max_new then (map #1 newpairs, [])
else
let val cls = sort compare_pairs newpairs
- val accepted = List.take (cls, !max_new)
+ val accepted = List.take (cls, max_new)
in
Output.debug (fn () => ("Number of candidates, " ^ Int.toString nnew ^
- ", exceeds the limit of " ^ Int.toString (!max_new)));
+ ", exceeds the limit of " ^ Int.toString (max_new)));
Output.debug (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
Output.debug (fn () => "Actually passed: " ^
space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
- (map #1 accepted, map #1 (List.drop (cls, !max_new)))
+ (map #1 accepted, map #1 (List.drop (cls, max_new)))
end
end;
-fun relevant_clauses thy ctab p rel_consts =
+fun relevant_clauses max_new thy ctab p rel_consts =
let fun relevant ([],_) [] = [] : (thm * (string * int)) list (*Nothing added this iteration*)
| relevant (newpairs,rejects) [] =
- let val (newrels,more_rejects) = take_best newpairs
+ let val (newrels,more_rejects) = take_best max_new newpairs
val new_consts = List.concat (map #2 newrels)
val rel_consts' = foldl add_const_typ_table rel_consts new_consts
- val newp = p + (1.0-p) / !convergence
+ val newp = p + (1.0-p) / convergence
in
Output.debug (fn () => ("relevant this iteration: " ^ Int.toString (length newrels)));
(map #1 newrels) @
- (relevant_clauses thy ctab newp rel_consts' (more_rejects@rejects))
+ (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects))
end
| relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) =
let val weight = clause_weight ctab rel_consts consts_typs
in
- if p <= weight orelse (!follow_defs andalso defines thy clsthm rel_consts)
+ if p <= weight orelse (follow_defs andalso defines thy clsthm rel_consts)
then (Output.debug (fn () => (name ^ " clause " ^ Int.toString n ^
" passes: " ^ Real.toString weight));
relevant ((ax,weight)::newrels, rejects) axs)
@@ -383,16 +276,16 @@
relevant ([],[])
end;
-fun relevance_filter thy axioms goals =
- if !run_relevance_filter andalso !pass_mark >= 0.1
+fun relevance_filter max_new theory_const thy axioms goals =
+ if run_relevance_filter andalso pass_mark >= 0.1
then
let val _ = Output.debug (fn () => "Start of relevance filtering");
- val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms
+ val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
val goal_const_tab = get_goal_consts_typs thy goals
val _ = Output.debug (fn () => ("Initial constants: " ^
space_implode ", " (Symtab.keys goal_const_tab)));
- val rels = relevant_clauses thy const_tab (!pass_mark)
- goal_const_tab (map (pair_consts_typs_axiom thy) axioms)
+ val rels = relevant_clauses max_new thy const_tab (pass_mark)
+ goal_const_tab (map (pair_consts_typs_axiom theory_const thy) axioms)
in
Output.debug (fn () => ("Total relevant: " ^ Int.toString (length rels)));
rels
@@ -471,7 +364,7 @@
fun valid_facts facts =
Facts.fold_static (fn (name, ths) =>
- if !run_blacklist_filter andalso is_package_def name then I
+ if run_blacklist_filter andalso is_package_def name then I
else
let val xname = Facts.extern facts name in
if NameSpace.is_hidden xname then I
@@ -502,7 +395,7 @@
fun name_thm_pairs ctxt =
let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
val ht = mk_clause_table 900 (*ht for blacklisted theorems*)
- fun blacklisted x = !run_blacklist_filter andalso isSome (Polyhash.peek ht x)
+ fun blacklisted x = run_blacklist_filter andalso isSome (Polyhash.peek ht x)
in
app (fn th => ignore (Polyhash.peekInsert ht (th,()))) (ResBlacklist.get ctxt);
filter (not o blacklisted o #2)
@@ -517,19 +410,19 @@
(* get lemmas from claset, simpset, atpset and extra supplied rules *)
fun get_clasimp_atp_lemmas ctxt user_thms =
let val included_thms =
- if !include_all
+ if include_all
then (tap (fn ths => Output.debug
(fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
(name_thm_pairs ctxt))
else
let val claset_thms =
- if !include_claset then ResAxioms.claset_rules_of ctxt
+ if include_claset then ResAxioms.claset_rules_of ctxt
else []
val simpset_thms =
- if !include_simpset then ResAxioms.simpset_rules_of ctxt
+ if include_simpset then ResAxioms.simpset_rules_of ctxt
else []
val atpset_thms =
- if !include_atpset then ResAxioms.atpset_rules_of ctxt
+ if include_atpset then ResAxioms.atpset_rules_of ctxt
else []
val _ = (Output.debug (fn () => "ATP theorems: "); app display_thm atpset_thms)
in claset_thms @ simpset_thms @ atpset_thms end
@@ -580,17 +473,6 @@
(* ATP invocation methods setup *)
(***************************************************************)
-fun cnf_hyps_thms ctxt =
- let
- val thy = ProofContext.theory_of ctxt
- val hyps = Assumption.prems_of ctxt
- in fold (fold (insert Thm.eq_thm) o ResAxioms.cnf_axiom thy) hyps [] end;
-
-(*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
-datatype mode = Auto | Fol | Hol;
-
-val linkup_logic_mode = ref Auto;
-
(*Ensures that no higher-order theorems "leak out"*)
fun restrict_to_logic thy true cls = filter (Meson.is_fol_term thy o prop_of o fst) cls
| restrict_to_logic thy false cls = cls;
@@ -645,91 +527,15 @@
likely to lead to unsound proofs.*)
fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
-(*Called by the oracle-based methods declared in res_atp_methods.ML*)
-fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
- let val conj_cls = Meson.make_clauses conjectures
- |> map ResAxioms.combinators |> Meson.finish_cnf
- val hyp_cls = cnf_hyps_thms ctxt
- val goal_cls = conj_cls@hyp_cls
- val goal_tms = map prop_of goal_cls
- val thy = ProofContext.theory_of ctxt
- val isFO = case mode of
- Auto => forall (Meson.is_fol_term thy) goal_tms
- | Fol => true
- | Hol => false
- val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
- val cla_simp_atp_clauses = included_thms
- |> ResAxioms.cnf_rules_pairs thy |> make_unique
- |> restrict_to_logic thy isFO
- |> remove_unwanted_clauses
- val user_cls = ResAxioms.cnf_rules_pairs thy user_rules
- val axclauses = make_unique (user_cls @ relevance_filter thy cla_simp_atp_clauses goal_tms)
- val subs = tfree_classes_of_terms goal_tms
- and axtms = map (prop_of o #1) axclauses
- val supers = tvar_classes_of_terms axtms
- and tycons = type_consts_of_terms thy (goal_tms@axtms)
- (*TFrees in conjecture clauses; TVars in axiom clauses*)
- val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
- val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
- val writer = if dfg then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file
- and file = atp_input_file()
- and user_lemmas_names = map #1 user_rules
- in
- writer thy isFO goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
- Output.debug (fn () => "Writing to " ^ file);
- file
- end;
-
-
-(**** remove tmp files ****)
-fun cond_rm_tmp file =
- if !Output.debugging orelse !destdir <> ""
- then Output.debug (fn () => "ATP input kept...")
- else OS.FileSys.remove file;
-
-
-(***************************************************************)
-(* automatic ATP invocation *)
-(***************************************************************)
-
-(* call prover with settings and problem file for the current subgoal *)
-fun watcher_call_provers files (childin, childout, pid) =
- let val time = Int.toString (!time_limit)
- fun make_atp_list [] = []
- | make_atp_list (file::files) =
- (Output.debug (fn () => "problem file in watcher_call_provers is " ^ file);
- (*options are separated by Watcher.setting_sep, currently #"%"*)
- case !prover of
- Recon.SPASS =>
- let val spass = helper_path "SPASS_HOME" "SPASS"
- val sopts =
- "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
- in ("spass", spass, sopts, file) :: make_atp_list files end
- | Recon.Vampire =>
- let val vampire = helper_path "VAMPIRE_HOME" "vampire"
- val vopts = "--output_syntax tptp%--mode casc%-t " ^ time
- in ("vampire", vampire, vopts, file) :: make_atp_list files end
- | Recon.E =>
- let val eproof = helper_path "E_HOME" "eproof"
- val eopts = "--tstp-in%--tstp-out%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time
- in ("E", eproof, eopts, file) :: make_atp_list files end)
- in
- Watcher.callResProvers(childout, make_atp_list files);
- Output.debug (fn () => "Sent commands to watcher!")
- end
-
-(*For debugging the generated set of theorem names*)
-fun trace_vector fname =
- let val path = Path.explode (fname ^ "_thm_names")
- in Vector.app (File.append path o (fn s => s ^ "\n")) end;
-
-(*We write out problem files for each subgoal. Argument probfile generates filenames,
- and allows the suppression of the suffix "_1" in problem-generation mode.
- FIXME: does not cope with &&, and it isn't easy because one could have multiple
- subgoals, each involving &&.*)
-fun write_problem_files probfile (ctxt, chain_ths, th) =
- let val goals = Library.take (!max_sledgehammers, Thm.prems_of th) (*raises no exception*)
- val _ = Output.debug (fn () => "number of subgoals = " ^ Int.toString (length goals))
+(* TODO: problem file for *one* subgoal would be sufficient *)
+(*Write out problem files for each subgoal.
+ Argument probfile generates filenames from subgoal-number
+ Argument writer is either a tptp_write_file or dfg_write_file from ResHolClause
+ Arguments max_new and theory_const are booleans controlling relevance_filter
+ (necessary for different provers)
+ *)
+fun write_problem_files writer max_new theory_const probfile (ctxt, chain_ths, th) =
+ let val goals = Thm.prems_of th
val thy = ProofContext.theory_of ctxt
fun get_neg_subgoals [] _ = []
| get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) ::
@@ -737,7 +543,7 @@
val goal_cls = get_neg_subgoals goals 1
handle THM ("assume: variables", _, _) =>
error "Sledgehammer: Goal contains type variables (TVars)"
- val isFO = case !linkup_logic_mode of
+ val isFO = case linkup_logic_mode of
Auto => forall (Meson.is_fol_term thy) (map prop_of (List.concat goal_cls))
| Fol => true
| Hol => false
@@ -745,22 +551,15 @@
val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
|> restrict_to_logic thy isFO
|> remove_unwanted_clauses
- val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls))
val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
(*clauses relevant to goal gl*)
- val axcls_list = map (fn ngcls => white_cls @ relevance_filter thy included_cls (map prop_of ngcls)) goal_cls
- val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls)))
- axcls_list
- val writer = if !prover = Recon.SPASS then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file
+ val axcls_list = map (fn ngcls => white_cls @ relevance_filter max_new theory_const thy included_cls (map prop_of ngcls)) goal_cls
fun write_all [] [] _ = []
| write_all (ccls::ccls_list) (axcls::axcls_list) k =
- let val fname = probfile k
- val _ = Output.debug (fn () => "About to write file " ^ fname)
+ let val fname = File.platform_path (probfile k)
val axcls = make_unique axcls
- val _ = Output.debug (fn () => "Conjecture Clauses (before duplicate removal)")
val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
val ccls = subtract_cls ccls axcls
- val _ = Output.debug (fn () => "Conjecture Clauses (AFTER duplicate removal)")
val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
val ccltms = map prop_of ccls
and axtms = map (prop_of o #1) axcls
@@ -769,83 +568,13 @@
and tycons = type_consts_of_terms thy (ccltms@axtms)
(*TFrees in conjecture clauses; TVars in axiom clauses*)
val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
- val _ = Output.debug (fn () => "arity clauses = " ^ Int.toString (length arity_clauses))
val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
- val _ = Output.debug (fn () => "classrel clauses = " ^ Int.toString (length classrel_clauses))
val clnames = writer thy isFO ccls fname (axcls,classrel_clauses,arity_clauses) []
val thm_names = Vector.fromList clnames
- val _ = if !Output.debugging then trace_vector fname thm_names else ()
in (thm_names,fname) :: write_all ccls_list axcls_list (k+1) end
val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
in
(filenames, thm_names_list)
end;
-val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream *
- Posix.Process.pid * string list) option);
-
-fun kill_last_watcher () =
- (case !last_watcher_pid of
- NONE => ()
- | SOME (_, _, pid, files) =>
- (Output.debug (fn () => "Killing old watcher, pid = " ^ string_of_pid pid);
- Watcher.killWatcher pid;
- ignore (map (try cond_rm_tmp) files)))
- handle OS.SysErr _ => Output.debug (fn () => "Attempt to kill watcher failed");
-
-(*writes out the current problems and calls ATPs*)
-fun isar_atp (ctxt, chain_ths, th) =
- if Thm.no_prems th then warning "Nothing to prove"
- else
- let
- val _ = kill_last_watcher()
- val (files,thm_names_list) = write_problem_files prob_pathname (ctxt, chain_ths, th)
- val (childin, childout, pid) = Watcher.createWatcher (ctxt, th, thm_names_list)
- in
- last_watcher_pid := SOME (childin, childout, pid, files);
- Output.debug (fn () => "problem files: " ^ space_implode ", " files);
- Output.debug (fn () => "pid: " ^ string_of_pid pid);
- watcher_call_provers files (childin, childout, pid)
- end;
-
-(*For ML scripts, and primarily, for debugging*)
-fun callatp () =
- let val th = topthm()
- val ctxt = ProofContext.init (theory_of_thm th)
- in isar_atp (ctxt, [], th) end;
-
-val isar_atp_writeonly = PrintMode.setmp []
- (fn (ctxt, chain_ths, th) =>
- if Thm.no_prems th then warning "Nothing to prove"
- else
- let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix
- else prob_pathname
- in ignore (write_problem_files probfile (ctxt, chain_ths, th)) end);
-
-
-(** the Isar toplevel command **)
-
-fun sledgehammer state =
- let
- val (ctxt, (chain_ths, goal)) = Proof.get_goal (Toplevel.proof_of state)
- val chain_ths = map (Thm.put_name_hint Recon.chained_hint) chain_ths
- (*Mark the chained theorems to keep them out of metis calls;
- their original "name hints" may be bad anyway.*)
- val thy = ProofContext.theory_of ctxt
- in
- if exists_type ResAxioms.type_has_empty_sort (prop_of goal)
- then error "Proof state contains the empty sort" else ();
- Output.debug (fn () => "subgoals in isar_atp:\n" ^
- Syntax.string_of_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal)));
- Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
- app (fn th => Output.debug (fn _ => "chained: " ^ Display.string_of_thm th)) chain_ths;
- if !time_limit > 0 then isar_atp (ctxt, chain_ths, goal)
- else (warning ("Writing problem file only: " ^ !problem_name);
- isar_atp_writeonly (ctxt, chain_ths, goal))
- end;
-
-val _ =
- OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer));
-
end;
--- a/src/HOL/Tools/res_reconstruct.ML Fri Oct 03 15:20:33 2008 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Fri Oct 03 16:37:09 2008 +0200
@@ -8,19 +8,8 @@
(***************************************************************************)
signature RES_RECONSTRUCT =
sig
- datatype atp = E | SPASS | Vampire
val chained_hint: string
- val checkEProofFound:
- TextIO.instream * TextIO.outstream * Posix.Process.pid *
- string * Proof.context * thm * int * string Vector.vector -> bool
- val checkVampProofFound:
- TextIO.instream * TextIO.outstream * Posix.Process.pid *
- string * Proof.context * thm * int * string Vector.vector -> bool
- val checkSpassProofFound:
- TextIO.instream * TextIO.outstream * Posix.Process.pid *
- string * Proof.context * thm * int * string Vector.vector -> bool
- val signal_parent: TextIO.outstream * Posix.Process.pid * string * string -> unit
- val txt_path: string -> Path.T
+
val fix_sorts: sort Vartab.table -> term -> term
val invert_const: string -> string
val invert_type_const: string -> string
@@ -28,6 +17,12 @@
val make_tvar: string -> typ
val strip_prefix: string -> string -> string option
val setup: Context.theory -> Context.theory
+ (* extracting lemma list*)
+ val check_success_e_vamp_spass: string * int -> bool
+ val lemma_list_dfg: string * string vector * Proof.context * Thm.thm * int -> string
+ val lemma_list_tstp: string * string vector * Proof.context * Thm.thm * int -> string
+ (* structured proofs *)
+ val structured_proof: string * string vector * Proof.context * Thm.thm * int -> string
end;
structure ResReconstruct : RES_RECONSTRUCT =
@@ -46,12 +41,10 @@
(*Indicates whether to include sort information in generated proofs*)
val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "sledgehammer_sorts" true;
-(*Indicates whether to generate full proofs or just lemma lists*)
-val (full_proofs, full_proofs_setup) = Attrib.config_bool "sledgehammer_full" false;
+(*Indicated whether to generate full proofs or just lemma lists - now via setup of atps*)
+(* val (full_proofs, full_proofs_setup) = Attrib.config_bool "sledgehammer_full" false; *)
-val setup = modulus_setup #> recon_sorts_setup #> full_proofs_setup;
-
-datatype atp = E | SPASS | Vampire;
+val setup = modulus_setup #> recon_sorts_setup;
(**** PARSING OF TSTP FORMAT ****)
@@ -465,219 +458,102 @@
let val msg = "Translation of TSTP raised an exception: " ^ Toplevel.exn_message e
in trace msg; msg end;
-(*Could use split_lines, but it can return blank lines...*)
-val lines = String.tokens (equal #"\n");
-val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c);
-
-val txt_path = Path.ext "txt" o Path.explode o nospaces;
-
-fun signal_success probfile toParent ppid msg =
- let val _ = trace ("\nReporting Success for " ^ probfile ^ "\n" ^ msg)
- in
- (*We write the proof to a file because sending very long lines may fail...*)
- File.write (txt_path probfile) msg;
- TextIO.output (toParent, "Success.\n");
- TextIO.output (toParent, probfile ^ "\n");
- TextIO.flushOut toParent;
- Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
- (*Give the parent time to respond before possibly sending another signal*)
- OS.Process.sleep (Time.fromMilliseconds 600)
- end;
-
-
-(**** retrieve the axioms that were used in the proof ****)
-
-(*Thm.get_name_hint returns "??.unknown" if no name is available.*)
-fun goodhint x = (x <> "??.unknown");
-
-(*Get names of axioms used. Axioms are indexed from 1, while the vector is indexed from 0*)
-fun get_axiom_names (thm_names: string vector) step_nums =
- let fun is_axiom n = n <= Vector.length thm_names
- fun getname i = Vector.sub(thm_names, i-1)
- in
- sort_distinct string_ord (filter goodhint (map getname (filter is_axiom step_nums)))
- end;
-
- (*String contains multiple lines. We want those of the form
- "253[0:Inp] et cetera..."
- A list consisting of the first number in each line is returned. *)
-fun get_spass_linenums proofextract =
- let val toks = String.tokens (not o Char.isAlphaNum)
- fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
- | inputno _ = NONE
- val lines = String.tokens (fn c => c = #"\n") proofextract
- in List.mapPartial (inputno o toks) lines end
-
-fun get_axiom_names_spass proofextract thm_names =
- get_axiom_names thm_names (get_spass_linenums proofextract);
-
-fun not_comma c = c <> #",";
+
+ (* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *)
+
+ val failure_strings_E = ["SZS status: Satisfiable","SZS status: ResourceOut","# Cannot determine problem status"];
+ val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
+ val failure_strings_SPASS = ["SPASS beiseite: Completion found.","SPASS beiseite: Ran out of time.",
+ "SPASS beiseite: Maximal number of loops exceeded."];
+ fun check_success_e_vamp_spass (proof, rc) =
+ not (exists (fn s => String.isSubstring s proof)
+ (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS))
+ andalso (rc = 0);
-(*A valid TSTP axiom line has the form cnf(NNN,axiom,...) where NNN is a positive integer.*)
-fun parse_tstp_line s =
- let val ss = Substring.full (unprefix "cnf(" (nospaces s))
- val (intf,rest) = Substring.splitl not_comma ss
- val (rolef,rest) = Substring.splitl not_comma (Substring.triml 1 rest)
- (*We only allow negated_conjecture because the line number will be removed in
- get_axiom_names above, while suppressing the UNSOUND warning*)
- val ints = if Substring.string rolef mem_string ["axiom","negated_conjecture"]
- then Substring.string intf
- else "error"
- in Int.fromString ints end
- handle Fail _ => NONE;
-
-fun get_axiom_names_tstp proofextract thm_names =
- get_axiom_names thm_names (List.mapPartial parse_tstp_line (split_lines proofextract));
-
- (*String contains multiple lines. We want those of the form
- "*********** [448, input] ***********"
- or possibly those of the form
- "cnf(108, axiom, ..."
- A list consisting of the first number in each line is returned. *)
-fun get_vamp_linenums proofextract =
- let val toks = String.tokens (not o Char.isAlphaNum)
- fun inputno [ntok,"input"] = Int.fromString ntok
- | inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok
- | inputno _ = NONE
- val lines = String.tokens (fn c => c = #"\n") proofextract
- in List.mapPartial (inputno o toks) lines end
-
-fun get_axiom_names_vamp proofextract thm_names =
- get_axiom_names thm_names (get_vamp_linenums proofextract);
-
-fun get_axiom_names_for E = get_axiom_names_tstp
- | get_axiom_names_for SPASS = get_axiom_names_spass
- | get_axiom_names_for Vampire = get_axiom_names_vamp;
-
-fun metis_line [] = "apply metis"
- | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")"
-
-(*Used to label theorems chained into the sledgehammer call*)
-val chained_hint = "CHAINED";
-
-val nochained = filter_out (fn y => y = chained_hint);
-
-(*The signal handler in watcher.ML must be able to read the output of this.*)
-fun lemma_list atp proofextract thm_names probfile toParent ppid =
- (trace "\nlemma_list: ready to signal success";
- signal_success probfile toParent ppid
- (metis_line (nochained (get_axiom_names_for atp proofextract thm_names))));
-
-fun tstp_extract proofextract thm_names probfile toParent ppid ctxt th sgno =
- let val _ = trace "\nAttempting to extract structured proof from TSTP\n"
+ (*=== EXTRACTING PROOF-TEXT === *)
+
+ val begin_proof_strings = ["# SZS output start CNFRefutation.",
+ "=========== Refutation ==========",
+ "Here is a proof"];
+ val end_proof_strings = ["# SZS output end CNFRefutation",
+ "======= End of refutation =======",
+ "Formulae used in the proof"];
+ fun get_proof_extract proof =
+ let
+ (*splits to_split by the first possible of a list of splitters*)
+ fun first_field_any [] to_split = NONE
+ | first_field_any (splitter::splitters) to_split =
+ let
+ val result = (first_field splitter to_split)
+ in
+ if isSome result then result else first_field_any splitters to_split
+ end
+ val (a:string, b:string) = valOf (first_field_any begin_proof_strings proof)
+ val (proofextract:string, c:string) = valOf (first_field_any end_proof_strings b)
+ in proofextract end;
+
+ (* === EXTRACTING LEMMAS === *)
+ (* lines have the form "cnf(108, axiom, ...",
+ the number (108) has to be extracted)*)
+ fun get_step_nums_tstp proofextract =
+ let val toks = String.tokens (not o Char.isAlphaNum)
+ fun inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok
+ | inputno _ = NONE
+ val lines = split_lines proofextract
+ in List.mapPartial (inputno o toks) lines end
+
+ (*String contains multiple lines. We want those of the form
+ "253[0:Inp] et cetera..."
+ A list consisting of the first number in each line is returned. *)
+ fun get_step_nums_dfg proofextract =
+ let val toks = String.tokens (not o Char.isAlphaNum)
+ fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
+ | inputno _ = NONE
+ val lines = split_lines proofextract
+ in List.mapPartial (inputno o toks) lines end
+
+ (*extracting lemmas from tstp-output between the lines from above*)
+ fun extract_lemmas get_step_nums (proof, thm_names, _, _, _) =
+ let
+ (* get the names of axioms from their numbers*)
+ fun get_axiom_names thm_names step_nums =
+ let
+ fun is_axiom n = n <= Vector.length thm_names
+ fun getname i = Vector.sub(thm_names, i-1)
+ in
+ sort_distinct string_ord (filter (fn x => x <> "??.unknown") (map getname (filter is_axiom step_nums)))
+ end
+ val proofextract = get_proof_extract proof
+ in
+ get_axiom_names thm_names (get_step_nums proofextract)
+ end;
+
+ (* metis-command *)
+ fun metis_line [] = "apply metis"
+ | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")"
+
+ (*Used to label theorems chained into the sledgehammer call*)
+ val chained_hint = "CHAINED";
+ fun sendback_metis_nochained lemmas =
+ let val nochained = filter_out (fn y => y = chained_hint)
+ in (Markup.markup Markup.sendback o metis_line) (nochained lemmas) end
+ fun lemma_list_tstp result = sendback_metis_nochained (extract_lemmas get_step_nums_tstp result);
+ fun lemma_list_dfg result = sendback_metis_nochained (extract_lemmas get_step_nums_dfg result);
+
+ (* === Extracting structured Isar-proof === *)
+ fun structured_proof (result as (proof, thm_names, ctxt, goal, subgoalno)) =
+ let
+ (*Could use split_lines, but it can return blank lines...*)
+ val lines = String.tokens (equal #"\n");
+ val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c)
+ val proofextract = get_proof_extract proof
val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
- val _ = trace (Int.toString (length cnfs) ^ " cnfs found")
- val names = get_axiom_names_tstp proofextract thm_names
- val line1 = metis_line (nochained names)
- val _ = trace ("\nExtracted one-line proof: " ^ line1)
- val line2 = if chained_hint mem_string names then ""
- else decode_tstp_file cnfs ctxt th sgno thm_names
- val _ = trace "\ntstp_extract: ready to signal success"
- in
- signal_success probfile toParent ppid (line1 ^ "\n" ^ line2)
- end;
-
-(**** Extracting proofs from an ATP's output ****)
-
-val start_TSTP = "SZS output start CNFRefutation"
-val end_TSTP = "SZS output end CNFRefutation"
-val start_E = "# Proof object starts here."
-val end_E = "# Proof object ends here."
-val start_V8 = "=========== Refutation =========="
-val end_V8 = "======= End of refutation ======="
-val start_SPASS = "Here is a proof"
-val end_SPASS = "Formulae used in the proof"
-
-fun any_substring ss ln = exists (fn s => String.isSubstring s ln) ss;
-
-(*********************************************************************************)
-(* Inspect the output of an ATP process to see if it has found a proof, *)
-(* and if so, transfer output to the input pipe of the main Isabelle process *)
-(*********************************************************************************)
-
-(*Returns "true" if it successfully returns a lemma list, otherwise "false", but this
- return value is currently never used!*)
-fun startTransfer endS (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names) =
- let val atp = if endS = end_V8 then Vampire
- else if endS = end_SPASS then SPASS
- else E
- fun transferInput proofextract =
- case TextIO.inputLine fromChild of
- NONE => (*end of file?*)
- (trace ("\n extraction_failed. End bracket: " ^ endS ^
- "\naccumulated text: " ^ proofextract);
- false)
- | SOME thisLine =>
- if any_substring [endS,end_TSTP] thisLine
- then
- (trace ("\nExtracted proof:\n" ^ proofextract);
- if Config.get ctxt full_proofs andalso String.isPrefix "cnf(" proofextract
- then tstp_extract proofextract thm_names probfile toParent ppid ctxt th sgno
- else lemma_list atp proofextract thm_names probfile toParent ppid;
- true)
- else transferInput (proofextract ^ thisLine)
- in
- transferInput ""
- end
-
+ val one_line_proof = lemma_list_tstp result
+ val structured = if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then ""
+ else decode_tstp_file cnfs ctxt goal subgoalno thm_names
+ in
+ one_line_proof ^ "\n\n" ^ (Markup.markup Markup.sendback) structured
+ end
-(*The signal handler in watcher.ML must be able to read the output of this.*)
-fun signal_parent (toParent, ppid, msg, probfile) =
- (TextIO.output (toParent, msg);
- TextIO.output (toParent, probfile ^ "\n");
- TextIO.flushOut toParent;
- trace ("\nSignalled parent: " ^ msg ^ probfile);
- Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
- (*Give the parent time to respond before possibly sending another signal*)
- OS.Process.sleep (Time.fromMilliseconds 600));
-
-(*FIXME: once TSTP output is produced by all ATPs, these three functions can be combined.*)
-
-(*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
-fun checkVampProofFound (arg as (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names)) =
- (case TextIO.inputLine fromChild of
- NONE => (trace "\nNo proof output seen"; false)
- | SOME thisLine =>
- if any_substring [start_V8,start_TSTP] thisLine
- then startTransfer end_V8 arg
- else if (String.isSubstring "Satisfiability detected" thisLine) orelse
- (String.isSubstring "Refutation not found" thisLine) orelse
- (String.isSubstring "CANNOT PROVE" thisLine)
- then (signal_parent (toParent, ppid, "Failure\n", probfile);
- true)
- else checkVampProofFound arg);
-
-(*Called from watcher. Returns true if the E process has returned a verdict.*)
-fun checkEProofFound (arg as (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names)) =
- (case TextIO.inputLine fromChild of
- NONE => (trace "\nNo proof output seen"; false)
- | SOME thisLine =>
- if any_substring [start_E,start_TSTP] thisLine
- then startTransfer end_E arg
- else if String.isSubstring "SZS status: Satisfiable" thisLine
- then (signal_parent (toParent, ppid, "Invalid\n", probfile);
- true)
- else if String.isSubstring "SZS status: ResourceOut" thisLine orelse
- String.isSubstring "# Cannot determine problem status" thisLine
- then (signal_parent (toParent, ppid, "Failure\n", probfile);
- true)
- else checkEProofFound arg);
-
-(*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
-fun checkSpassProofFound (arg as (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names)) =
- (case TextIO.inputLine fromChild of
- NONE => (trace "\nNo proof output seen"; false)
- | SOME thisLine =>
- if any_substring [start_SPASS,start_TSTP] thisLine
- then startTransfer end_SPASS arg
- else if thisLine = "SPASS beiseite: Completion found.\n"
- then (signal_parent (toParent, ppid, "Invalid\n", probfile);
- true)
- else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse
- thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
- then (signal_parent (toParent, ppid, "Failure\n", probfile);
- true)
- else checkSpassProofFound arg);
-
-end;
+ end;
--- a/src/HOL/Tools/watcher.ML Fri Oct 03 15:20:33 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,414 +0,0 @@
-(* Title: HOL/Tools/watcher.ML
- ID: $Id$
- Author: Claire Quigley
- Copyright 2004 University of Cambridge
- *)
-
-(* The watcher process starts a resolution process when it receives a *)
-(* message from Isabelle *)
-(* Signals Isabelle, puts output of child into pipe to Isabelle, *)
-(* and removes dead processes. Also possible to kill all the resolution *)
-(* processes currently running. *)
-
-signature WATCHER =
-sig
-
-(* Send request to Watcher for multiple spasses to be called for filenames in arg *)
-(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
-
-val callResProvers : TextIO.outstream * (string*string*string*string) list -> unit
-
-(* Send message to watcher to kill resolution provers *)
-val callSlayer : TextIO.outstream -> unit
-
-(* Start a watcher and set up signal handlers*)
-val createWatcher :
- Proof.context * thm * string Vector.vector list ->
- TextIO.instream * TextIO.outstream * Posix.Process.pid
-val killWatcher : Posix.Process.pid -> unit
-val killChild : ('a, 'b) Unix.proc -> OS.Process.status
-val command_sep : char
-val setting_sep : char
-val reapAll : unit -> unit
-end
-
-
-
-structure Watcher: WATCHER =
-struct
-
-(*Field separators, used to pack items onto a text line*)
-val command_sep = #"\t"
-and setting_sep = #"%";
-
-val goals_being_watched = ref 0;
-
-val trace_path = Path.basic "watcher_trace";
-
-fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
- else ();
-
-(*Representation of a watcher process*)
-type proc = {pid : Posix.Process.pid,
- instr : TextIO.instream,
- outstr : TextIO.outstream};
-
-(*Representation of a child (ATP) process*)
-type cmdproc = {
- prover: string, (* Name of the resolution prover used, e.g. "spass"*)
- file: string, (* The file containing the goal for the ATP to prove *)
- proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
- instr : TextIO.instream, (*Output of the child process *)
- outstr : TextIO.outstream}; (*Input to the child process *)
-
-
-fun fdReader (name : string, fd : Posix.IO.file_desc) =
- Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
-
-fun fdWriter (name, fd) =
- Posix.IO.mkTextWriter {
- appendMode = false,
- initBlkMode = true,
- name = name,
- chunkSize=4096,
- fd = fd};
-
-fun openOutFD (name, fd) =
- TextIO.mkOutstream (
- TextIO.StreamIO.mkOutstream (
- fdWriter (name, fd), IO.BLOCK_BUF));
-
-fun openInFD (name, fd) =
- TextIO.mkInstream (
- TextIO.StreamIO.mkInstream (
- fdReader (name, fd), ""));
-
-
-(* Send request to Watcher for a vampire to be called for filename in arg*)
-fun callResProver (toWatcherStr, arg) =
- (TextIO.output (toWatcherStr, arg^"\n");
- TextIO.flushOut toWatcherStr)
-
-(* Send request to Watcher for multiple provers to be called*)
-fun callResProvers (toWatcherStr, []) =
- (TextIO.output (toWatcherStr, "End of calls\n"); TextIO.flushOut toWatcherStr)
- | callResProvers (toWatcherStr,
- (prover,proverCmd,settings,probfile) :: args) =
- (trace (space_implode ", " (["\ncallResProvers:", prover, proverCmd, probfile]));
- (*Uses a special character to separate items sent to watcher*)
- TextIO.output (toWatcherStr,
- space_implode (str command_sep) [prover, proverCmd, settings, probfile, "\n"]);
- inc goals_being_watched;
- TextIO.flushOut toWatcherStr;
- callResProvers (toWatcherStr,args))
-
-
-(*Send message to watcher to kill currently running vampires. NOT USED and possibly
- buggy. Note that killWatcher kills the entire process group anyway.*)
-fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill children\n");
- TextIO.flushOut toWatcherStr)
-
-
-(* Get commands from Isabelle*)
-fun getCmds (toParentStr, fromParentStr, cmdList) =
- let val thisLine = the_default "" (TextIO.inputLine fromParentStr)
- in
- trace("\nGot command from parent: " ^ thisLine);
- if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
- else if thisLine = "Kill children\n"
- then (TextIO.output (toParentStr,thisLine);
- TextIO.flushOut toParentStr;
- [("","Kill children",[],"")])
- else
- let val [prover,proverCmd,settingstr,probfile,_] =
- String.tokens (fn c => c = command_sep) thisLine
- val settings = String.tokens (fn c => c = setting_sep) settingstr
- in
- trace ("\nprover: " ^ prover ^ " prover path: " ^ proverCmd ^
- "\n problem file: " ^ probfile);
- getCmds (toParentStr, fromParentStr,
- (prover, proverCmd, settings, probfile)::cmdList)
- end
- handle Bind =>
- (trace "\ngetCmds: command parsing failed!";
- getCmds (toParentStr, fromParentStr, cmdList))
- end
-
-
-(*Get Io-descriptor for polling of an input stream*)
-fun getInIoDesc someInstr =
- let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
- val _ = TextIO.output (TextIO.stdOut, buf)
- val ioDesc =
- case rd
- of TextPrimIO.RD{ioDesc = SOME iod, ...} => SOME iod
- | _ => NONE
- in (* since getting the reader will have terminated the stream, we need
- * to build a new stream. *)
- TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
- ioDesc
- end
-
-fun pollChild fromStr =
- case getInIoDesc fromStr of
- SOME iod =>
- (case OS.IO.pollDesc iod of
- SOME pd =>
- let val pd' = OS.IO.pollIn pd in
- case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of
- [] => false
- | pd''::_ => OS.IO.isIn pd''
- end
- | NONE => false)
- | NONE => false
-
-
-(*************************************)
-(* Set up a Watcher Process *)
-(*************************************)
-
-fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
-
-val killChildren = List.app (ignore o killChild o #proc_handle) : cmdproc list -> unit;
-
-fun killWatcher (toParentStr, procList) =
- (trace "\nWatcher timeout: Killing proof processes";
- TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
- TextIO.flushOut toParentStr;
- killChildren procList;
- Posix.Process.exit 0w0);
-
-(* take an instream and poll its underlying reader for input *)
-fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) =
- case OS.IO.pollDesc fromParentIOD of
- SOME pd =>
- (case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of
- [] => NONE
- | pd''::_ => if OS.IO.isIn pd''
- then SOME (getCmds (toParentStr, fromParentStr, []))
- else NONE)
- | NONE => NONE;
-
-(*get the number of the subgoal from the filename: the last digit string*)
-fun number_from_filename s =
- let val numbers = "xxx" :: String.tokens (not o Char.isDigit) s
- in valOf (Int.fromString (List.last numbers)) end
- handle Option => (trace ("\nWatcher could not read subgoal nunber! " ^ s);
- error ("Watcher could not read subgoal nunber! " ^ s));
-
-(*Call ATP. Settings should be a list of strings ["-t 300", "-m 100000"],
- which we convert below to ["-t", "300", "-m", "100000"] using String.tokens.
- Otherwise, the SML/NJ version of Unix.execute will escape the spaces, and
- Vampire will reject the switches.*)
-fun execCmds [] procList = procList
- | execCmds ((prover,proverCmd,settings,file)::cmds) procList =
- let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^ file)
- val settings' = List.concat (map (String.tokens Char.isSpace) settings)
- val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc =
- Unix.execute(proverCmd, settings' @ [file])
- val (instr, outstr) = Unix.streamsOf childhandle
- val newProcList = {prover=prover, file=file, proc_handle=childhandle,
- instr=instr, outstr=outstr} :: procList
- val _ = trace ("\nFinished at " ^
- Date.toString(Date.fromTimeLocal(Time.now())))
- in execCmds cmds newProcList end
-
-fun checkChildren (ctxt, th, thm_names_list) toParentStr children =
- let fun check [] = [] (* no children to check *)
- | check (child::children) =
- let val {prover, file, proc_handle, instr=childIn, ...} : cmdproc = child
- val _ = trace ("\nprobfile = " ^ file)
- val i = number_from_filename file (*subgoal number*)
- val thm_names = List.nth(thm_names_list, i-1);
- val ppid = Posix.ProcEnv.getppid()
- in
- if pollChild childIn
- then (* check here for prover label on child*)
- let val _ = trace ("\nInput available from child: " ^ file)
- val childDone = (case prover of
- "vampire" => ResReconstruct.checkVampProofFound
- (childIn, toParentStr, ppid, file, ctxt, th, i, thm_names)
- | "E" => ResReconstruct.checkEProofFound
- (childIn, toParentStr, ppid, file, ctxt, th, i, thm_names)
- | "spass" => ResReconstruct.checkSpassProofFound
- (childIn, toParentStr, ppid, file, ctxt, th, i, thm_names)
- | _ => (trace ("\nBad prover! " ^ prover); true) )
- in
- if childDone (*ATP has reported back (with success OR failure)*)
- then (Unix.reap proc_handle;
- if !Output.debugging then () else OS.FileSys.remove file;
- check children)
- else child :: check children
- end
- else (trace "\nNo child output"; child :: check children)
- end
- in
- trace ("\nIn checkChildren, length of queue: " ^ Int.toString(length children));
- check children
- end;
-
-
-fun setupWatcher (ctxt, th, thm_names_list) =
- let
- val checkc = checkChildren (ctxt, th, thm_names_list)
- val p1 = Posix.IO.pipe() (*pipes for communication between parent and watcher*)
- val p2 = Posix.IO.pipe()
- (****** fork a watcher process and get it set up and going ******)
- fun startWatcher procList =
- case Posix.Process.fork() of
- SOME pid => pid (* parent - i.e. main Isabelle process *)
- | NONE =>
- let (* child - i.e. watcher *)
- val oldchildin = #infd p1
- val fromParent = Posix.FileSys.wordToFD 0w0
- val oldchildout = #outfd p2
- val toParent = Posix.FileSys.wordToFD 0w1
- val fromParentIOD = Posix.FileSys.fdToIOD fromParent
- val fromParentStr = openInFD ("_exec_in_parent", fromParent)
- val toParentStr = openOutFD ("_exec_out_parent", toParent)
- val pid = Posix.ProcEnv.getpid()
- val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid}
- (*set process group id: allows killing all children*)
- val () = trace "\nsubgoals forked to startWatcher"
- val limit = ref 200; (*don't let watcher run forever*)
- (*Watcher Loop : Check running ATP processes for output*)
- fun keepWatching procList =
- (trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^
- " length(procList) = " ^ Int.toString(length procList));
- OS.Process.sleep (Time.fromMilliseconds 100); limit := !limit - 1;
- if !limit < 0 then killWatcher (toParentStr, procList)
- else
- case pollParentInput(fromParentIOD, fromParentStr, toParentStr) of
- SOME [(_,"Kill children",_,_)] =>
- (trace "\nReceived Kill command";
- killChildren procList; keepWatching [])
- | SOME cmds => (* deal with commands from Isabelle process *)
- let val _ = trace("\nCommands from parent: " ^
- Int.toString(length cmds))
- val newProcList' = checkc toParentStr (execCmds cmds procList)
- in trace "\nCommands executed"; keepWatching newProcList' end
- | NONE => (* No new input from Isabelle *)
- (trace "\nNothing from parent...";
- keepWatching(checkc toParentStr procList)))
- handle exn => (*FIXME: exn handler is too general!*)
- (trace ("\nkeepWatching exception handler: " ^ Toplevel.exn_message exn);
- keepWatching procList);
- in
- (*** Sort out pipes ********)
- Posix.IO.close (#outfd p1); Posix.IO.close (#infd p2);
- Posix.IO.dup2{old = oldchildin, new = fromParent};
- Posix.IO.close oldchildin;
- Posix.IO.dup2{old = oldchildout, new = toParent};
- Posix.IO.close oldchildout;
- keepWatching (procList)
- end;
-
- val _ = TextIO.flushOut TextIO.stdOut
- val pid = startWatcher []
- (* communication streams to watcher*)
- val instr = openInFD ("_exec_in", #infd p2)
- val outstr = openOutFD ("_exec_out", #outfd p1)
- in
- (* close the child-side fds*)
- Posix.IO.close (#outfd p2); Posix.IO.close (#infd p1);
- (* set the fds close on exec *)
- Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
- Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
- {pid = pid, instr = instr, outstr = outstr}
- end;
-
-
-
-(**********************************************************)
-(* Start a watcher and set up signal handlers *)
-(**********************************************************)
-
-(*Signal handler to tidy away zombie processes*)
-fun reapAll() =
- (case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of
- SOME _ => reapAll() | NONE => ())
- handle OS.SysErr _ => ()
-
-(*FIXME: does the main process need something like this?
- IsaSignal.signal (IsaSignal.chld, IsaSignal.SIG_HANDLE reap)??*)
-
-fun killWatcher pid =
- (goals_being_watched := 0;
- Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
- reapAll());
-
-fun reapWatcher(pid, instr, outstr) = ignore
- (TextIO.closeIn instr; TextIO.closeOut outstr;
- Posix.Process.waitpid(Posix.Process.W_CHILD pid, []))
- handle OS.SysErr _ => ()
-
-fun string_of_subgoal th i =
- Display.string_of_cterm (List.nth(cprems_of th, i-1))
- handle Subscript => "Subgoal number out of range!"
-
-fun prems_string_of th = cat_lines (map Display.string_of_cterm (cprems_of th))
-
-fun read_proof probfile =
- let val p = ResReconstruct.txt_path probfile
- val _ = trace("\nReading proof from file " ^ Path.implode p)
- val msg = File.read p
- val _ = trace("\nProof:\n" ^ msg)
- in if !Output.debugging then () else File.rm p; msg end;
-
-(*Non-successful outcomes*)
-fun report i s = priority ("Subgoal " ^ Int.toString i ^ ": " ^ s);
-
-(*Successful outcome: auto-insertion of commands into the PG buffer. Thanks to D Aspinall!!*)
-fun report_success i s sgtx =
- let val sgline = "Subgoal " ^ string_of_int i ^ ":"
- val outlines =
- case split_lines s of
- [] => ["Received bad string: " ^ s]
- | line::lines => [" Try this command:", (*Markup.markup Markup.sendback*) line, ""]
- @ lines
- in priority (cat_lines (sgline::sgtx::outlines)) end;
-
-fun createWatcher (ctxt, th, thm_names_list) =
- let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (ctxt,th,thm_names_list)
- fun decr_watched() =
- (goals_being_watched := !goals_being_watched - 1;
- if !goals_being_watched = 0
- then
- (Output.debug (fn () => ("\nReaping a watcher, childpid = " ^ string_of_pid childpid));
- killWatcher childpid (*???; reapWatcher (childpid, childin, childout)*) )
- else ())
- fun proofHandler _ =
- let val _ = trace("\nIn signal handler for pid " ^ string_of_pid childpid)
- val outcome = valOf (TextIO.inputLine childin)
- handle Option => error "watcher: \"outcome\" line is missing"
- val probfile = valOf (TextIO.inputLine childin)
- handle Option => error "watcher: \"probfile\" line is missing"
- val i = number_from_filename probfile
- val text = "\n" ^ string_of_subgoal th i
- in
- Output.debug (fn () => ("In signal handler. outcome = \"" ^ outcome ^
- "\"\nprobfile = " ^ probfile ^
- "\nGoals being watched: "^ Int.toString (!goals_being_watched)));
- if String.isPrefix "Invalid" outcome
- then (report i ("Subgoal is not provable:" ^ text);
- decr_watched())
- else if String.isPrefix "Failure" outcome
- then (report i ("Proof attempt failed:" ^ text);
- decr_watched())
- (* print out a list of rules used from clasimpset*)
- else if String.isPrefix "Success" outcome
- then (report_success i (read_proof probfile) text;
- decr_watched())
- (* if proof translation failed *)
- else if String.isPrefix "Translation failed" outcome
- then (report i (outcome ^ text);
- decr_watched())
- else (report i "System error in proof handler";
- decr_watched())
- end
- in Output.debug (fn () => ("subgoals forked to createWatcher: "^ prems_string_of th));
- IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
- (childin, childout, childpid)
- end
-
-end (* structure Watcher *)