--- 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;