# HG changeset patch # User wenzelm # Date 1223040033 -7200 # Node ID 706f8428e3c8629abda3f9a96ec65312dcf47024 # Parent ed1385cb2e0193ffd955ff933c060e327673a96e removed old/unused setup of raw ATP oracles; diff -r ed1385cb2e01 -r 706f8428e3c8 src/HOL/ATP_Linkup.thy --- a/src/HOL/ATP_Linkup.thy Fri Oct 03 14:07:41 2008 +0200 +++ b/src/HOL/ATP_Linkup.thy Fri Oct 03 15:20:33 2008 +0200 @@ -16,8 +16,6 @@ ("Tools/res_reconstruct.ML") ("Tools/watcher.ML") ("Tools/res_atp.ML") - ("Tools/res_atp_provers.ML") - ("Tools/res_atp_methods.ML") "~~/src/Tools/Metis/metis.ML" ("Tools/metis_tools.ML") begin @@ -99,14 +97,6 @@ use "Tools/watcher.ML" use "Tools/res_atp.ML" -use "Tools/res_atp_provers.ML" - -oracle vampire_oracle = {* ResAtpProvers.vampire_o *} -oracle eprover_oracle = {* ResAtpProvers.eprover_o *} -oracle spass_oracle = {* ResAtpProvers.spass_o *} - -use "Tools/res_atp_methods.ML" -setup ResAtpMethods.setup --{*Oracle ATP methods: still useful?*} setup ResReconstruct.setup --{*Config parameters*} diff -r ed1385cb2e01 -r 706f8428e3c8 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Oct 03 14:07:41 2008 +0200 +++ b/src/HOL/IsaMakefile Fri Oct 03 15:20:33 2008 +0200 @@ -227,9 +227,7 @@ Tools/Qelim/presburger.ML \ Tools/Qelim/qelim.ML \ Tools/recdef_package.ML \ - Tools/res_atp_methods.ML \ Tools/res_atp.ML \ - Tools/res_atp_provers.ML \ Tools/res_axioms.ML \ Tools/res_clause.ML \ Tools/res_hol_clause.ML \ diff -r ed1385cb2e01 -r 706f8428e3c8 src/HOL/Tools/res_atp_methods.ML --- a/src/HOL/Tools/res_atp_methods.ML Fri Oct 03 14:07:41 2008 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,69 +0,0 @@ -(* ID: $Id$ - Author: Jia Meng, NICTA -*) - -signature RES_ATP_METHODS = -sig - val vampire_tac: Proof.context -> thm list -> int -> tactic - val eprover_tac: Proof.context -> thm list -> int -> tactic - val spass_tac: Proof.context -> thm list -> int -> tactic - val vampireF_tac: Proof.context -> thm list -> int -> tactic - val vampireH_tac: Proof.context -> thm list -> int -> tactic - val eproverF_tac: Proof.context -> thm list -> int -> tactic - val eproverH_tac: Proof.context -> thm list -> int -> tactic - val spassF_tac: Proof.context -> thm list -> int -> tactic - val spassH_tac: Proof.context -> thm list -> int -> tactic - val setup: theory -> theory -end - -structure ResAtpMethods = -struct - -(* convert the negated 1st subgoal into CNF, write to file and call an ATP oracle *) -fun res_atp_tac dfg res_atp_oracle mode timeLimit ctxt user_thms i st = - (EVERY' - [rtac ccontr, - ObjectLogic.atomize_prems_tac, - Meson.skolemize_tac, - METAHYPS (fn negs => - HEADGOAL (Tactic.rtac - (res_atp_oracle - (ResAtp.write_subgoal_file dfg mode ctxt negs user_thms i, timeLimit))))] i st) handle Fail _ => Seq.empty; - - -(* vampire, eprover and spass tactics *) - -fun vampire_tac st = res_atp_tac false vampire_oracle ResAtp.Auto (!ResAtp.time_limit) st; -fun eprover_tac st = res_atp_tac false eprover_oracle ResAtp.Auto (!ResAtp.time_limit) st; -fun spass_tac st = res_atp_tac true spass_oracle ResAtp.Auto (!ResAtp.time_limit) st; - - -fun vampireF_tac st = res_atp_tac false vampire_oracle ResAtp.Fol (!ResAtp.time_limit) st; - -fun vampireH_tac st = res_atp_tac false vampire_oracle ResAtp.Hol (!ResAtp.time_limit) st; - -fun eproverF_tac st = res_atp_tac false eprover_oracle ResAtp.Fol (!ResAtp.time_limit) st; - -fun eproverH_tac st = res_atp_tac false eprover_oracle ResAtp.Hol (!ResAtp.time_limit) st; - -fun spassF_tac st = res_atp_tac true spass_oracle ResAtp.Fol (!ResAtp.time_limit) st; - -fun spassH_tac st = res_atp_tac true spass_oracle ResAtp.Hol (!ResAtp.time_limit) st; - - -fun atp_method tac = - Method.thms_ctxt_args (fn ths => fn ctxt => Method.SIMPLE_METHOD' (tac ctxt ths)); - -val setup = - Method.add_methods - [("vampireF", atp_method vampireF_tac, "Vampire for FOL problems"), - ("eproverF", atp_method eproverF_tac, "E prover for FOL problems"), - ("vampireH", atp_method vampireH_tac, "Vampire for HOL problems"), - ("eproverH", atp_method eproverH_tac, "E prover for HOL problems"), - ("eprover", atp_method eprover_tac, "E prover for FOL and HOL problems"), - ("vampire", atp_method vampire_tac, "Vampire for FOL and HOL problems"), - ("spassF", atp_method spassF_tac, "SPASS for FOL problems"), - ("spassH", atp_method spassH_tac, "SPASS for HOL problems"), - ("spass", atp_method spass_tac, "SPASS for FOL and HOL problems")]; - -end; diff -r ed1385cb2e01 -r 706f8428e3c8 src/HOL/Tools/res_atp_provers.ML --- a/src/HOL/Tools/res_atp_provers.ML Fri Oct 03 14:07:41 2008 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,58 +0,0 @@ -(* ID: $Id$ - Author: Jia Meng, NICTA - -Functions used for ATP Oracle. -*) - -structure ResAtpProvers = -struct - -fun seek_line s instr = - (case TextIO.inputLine instr of - NONE => false - | SOME thisLine => thisLine = s orelse seek_line s instr); - -fun location s = warning ("ATP input at: " ^ s); - -fun call_vampire (file:string, time: int) = - let val _ = location file - val runtime = "-t " ^ (string_of_int time) - val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire" - val (instr,outstr) = Unix.streamsOf (Unix.execute(vampire, [runtime,"--mode casc",file])) - in seek_line "--------------------- PROVED ----------------------\n" instr - end; - -fun call_eprover (file:string, time:int) = - let val _ = location file - val eprover = ResAtp.helper_path "E_HOME" "eprover" - val runtime = "--cpu-limit=" ^ (string_of_int time) - val (instr,outstr) = Unix.streamsOf (Unix.execute(eprover, - [runtime,"--tstp-in","-tAutoDev","-xAutoDev",file])) - in seek_line "# Proof found!\n" instr - end; - -fun call_spass (file:string, time:int) = - let val _ = location file - val runtime = "-TimeLimit=" ^ (string_of_int time) - val spass = ResAtp.helper_path "SPASS_HOME" "SPASS" - val (instr,outstr) = Unix.streamsOf (Unix.execute(spass, - [runtime,"-Splits=0", "-FullRed=0", "-SOS=1",file])) - in seek_line "SPASS beiseite: Proof found.\n" instr - end; - -fun vampire_o (file,time) = - if call_vampire (file,time) - then (warning file; ResAtp.cond_rm_tmp file; @{cprop False}) - else (ResAtp.cond_rm_tmp file; raise Fail ("vampire oracle failed")); - -fun eprover_o (file,time) = - if call_eprover (file,time) - then (warning file; ResAtp.cond_rm_tmp file; @{cprop False}) - else (ResAtp.cond_rm_tmp file; raise Fail ("eprover oracle failed")); - -fun spass_o (file,time) = - if call_spass (file,time) - then (warning file; ResAtp.cond_rm_tmp file; @{cprop False}) - else (ResAtp.cond_rm_tmp file; raise Fail ("SPASS oracle failed")); - -end;