--- 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*}
--- 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 \
--- 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;
--- 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;