# HG changeset patch # User wenzelm # Date 1223044629 -7200 # Node ID 9339d4dcec8b48d72c56649ceaf52a9ada4debe6 # Parent 706f8428e3c8629abda3f9a96ec65312dcf47024 version of sledgehammer using threads instead of processes, misc cleanup; (by Fabian Immler); diff -r 706f8428e3c8 -r 9339d4dcec8b src/HOL/ATP_Linkup.thy --- 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 *} diff -r 706f8428e3c8 -r 9339d4dcec8b src/HOL/IsaMakefile --- 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 diff -r 706f8428e3c8 -r 9339d4dcec8b src/HOL/Tools/atp_manager.ML --- /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; diff -r 706f8428e3c8 -r 9339d4dcec8b src/HOL/Tools/atp_thread.ML --- /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; diff -r 706f8428e3c8 -r 9339d4dcec8b src/HOL/Tools/res_atp.ML --- 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; diff -r 706f8428e3c8 -r 9339d4dcec8b src/HOL/Tools/res_reconstruct.ML --- 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; diff -r 706f8428e3c8 -r 9339d4dcec8b src/HOL/Tools/watcher.ML --- 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 *)