src/HOL/Tools/res_atp_methods.ML
author paulson
Fri Aug 10 15:13:18 2007 +0200 (2007-08-10)
changeset 24215 5458fbf18276
parent 23590 ad95084a5c63
child 24300 e170cee91c66
permissions -rw-r--r--
removal of some refs
mengj@17905
     1
(* ID: $Id$
mengj@17907
     2
   Author: Jia Meng, NICTA
mengj@17905
     3
*)
mengj@17905
     4
mengj@17905
     5
mengj@17905
     6
structure ResAtpMethods =
mengj@17905
     7
mengj@17905
     8
struct
mengj@17905
     9
  
mengj@19193
    10
(* convert the negated 1st subgoal into CNF, write to file and call an ATP oracle *)
mengj@19723
    11
fun res_atp_tac dfg res_atp_oracle mode timeLimit ctxt user_thms n thm =
wenzelm@23590
    12
    (EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, skolemize_tac,
mengj@17905
    13
		  METAHYPS(fn negs =>
mengj@17905
    14
			      HEADGOAL(Tactic.rtac 
mengj@17905
    15
					   (res_atp_oracle (ProofContext.theory_of ctxt) 
mengj@19723
    16
							   (ResAtp.write_subgoal_file dfg mode ctxt negs user_thms n, timeLimit))))] n thm) handle (Fail _) => Seq.empty;
mengj@19723
    17
mengj@19723
    18
(* vampire, eprover and spass tactics *)
mengj@17905
    19
paulson@24215
    20
fun vampire_tac st = res_atp_tac false vampire_oracle ResAtp.Auto (!ResAtp.time_limit) st;
paulson@24215
    21
fun eprover_tac st = res_atp_tac false eprover_oracle ResAtp.Auto (!ResAtp.time_limit) st;
paulson@24215
    22
fun spass_tac st = res_atp_tac true spass_oracle ResAtp.Auto (!ResAtp.time_limit) st;
mengj@17905
    23
mengj@18271
    24
paulson@24215
    25
fun vampireF_tac st = res_atp_tac false vampire_oracle ResAtp.Fol (!ResAtp.time_limit) st;
mengj@17905
    26
paulson@24215
    27
fun vampireH_tac st = res_atp_tac false vampire_oracle ResAtp.Hol (!ResAtp.time_limit) st;
mengj@19723
    28
paulson@24215
    29
fun eproverF_tac st = res_atp_tac false eprover_oracle ResAtp.Fol (!ResAtp.time_limit) st;
mengj@17905
    30
paulson@24215
    31
fun eproverH_tac st = res_atp_tac false eprover_oracle ResAtp.Hol (!ResAtp.time_limit) st;
mengj@18271
    32
paulson@24215
    33
fun spassF_tac st = res_atp_tac true spass_oracle ResAtp.Fol (!ResAtp.time_limit) st;
mengj@19723
    34
paulson@24215
    35
fun spassH_tac st = res_atp_tac true spass_oracle ResAtp.Hol (!ResAtp.time_limit) st;
mengj@17905
    36
wenzelm@18708
    37
val ResAtps_setup =
wenzelm@18708
    38
  Method.add_methods 
mengj@19193
    39
    [("vampireF", ResAtp.atp_method vampireF_tac, "Vampire for FOL problems"),
mengj@19193
    40
     ("eproverF", ResAtp.atp_method eproverF_tac, "E prover for FOL problems"),
mengj@19193
    41
     ("vampireH", ResAtp.atp_method vampireH_tac, "Vampire for HOL problems"),
mengj@19193
    42
     ("eproverH", ResAtp.atp_method eproverH_tac, "E prover for HOL problems"),
mengj@19193
    43
     ("eprover", ResAtp.atp_method eprover_tac, "E prover for FOL and HOL problems"),
mengj@19723
    44
     ("vampire", ResAtp.atp_method vampire_tac, "Vampire for FOL and HOL problems"),
mengj@19723
    45
     ("spassF", ResAtp.atp_method spassF_tac, "SPASS for FOL problems"),
mengj@19723
    46
     ("spassH", ResAtp.atp_method spassH_tac, "SPASS for HOL problems"),
mengj@19723
    47
     ("spass", ResAtp.atp_method spass_tac, "SPASS for FOL and HOL problems")];
mengj@17905
    48
mengj@17907
    49
end