src/HOL/Tools/res_atp_methods.ML
author paulson
Tue May 22 17:56:06 2007 +0200 (2007-05-22)
changeset 23075 69e30a7e8880
parent 19723 7602f74c914b
child 23590 ad95084a5c63
permissions -rw-r--r--
Some hacks for SPASS format
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 =
mengj@19193
    12
    (EVERY' [rtac ccontr,ObjectLogic.atomize_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
mengj@19723
    20
fun vampire_tac st = res_atp_tac false vampire_oracle ResAtp.Auto (!ResAtp.vampire_time) st;
mengj@19723
    21
fun eprover_tac st = res_atp_tac false eprover_oracle ResAtp.Auto (!ResAtp.eprover_time) st;
mengj@19723
    22
fun spass_tac st = res_atp_tac true spass_oracle ResAtp.Auto (!ResAtp.spass_time) st;
mengj@17905
    23
mengj@18271
    24
mengj@19723
    25
fun vampireF_tac st = res_atp_tac false vampire_oracle ResAtp.Fol (!ResAtp.vampire_time) st;
mengj@17905
    26
mengj@19723
    27
fun vampireH_tac st = res_atp_tac false vampire_oracle ResAtp.Hol (!ResAtp.vampire_time) st;
mengj@19723
    28
mengj@19723
    29
fun eproverF_tac st = res_atp_tac false eprover_oracle ResAtp.Fol (!ResAtp.eprover_time) st;
mengj@17905
    30
mengj@19723
    31
fun eproverH_tac st = res_atp_tac false eprover_oracle ResAtp.Hol (!ResAtp.eprover_time) st;
mengj@18271
    32
mengj@19723
    33
fun spassF_tac st = res_atp_tac true spass_oracle ResAtp.Fol (!ResAtp.spass_time) st;
mengj@19723
    34
mengj@19723
    35
fun spassH_tac st = res_atp_tac true spass_oracle ResAtp.Hol (!ResAtp.spass_time) 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