src/HOL/Tools/res_atp_methods.ML
author haftmann
Tue May 09 10:09:37 2006 +0200 (2006-05-09)
changeset 19599 a5c7eb37d14f
parent 19193 45c8db82893d
child 19723 7602f74c914b
permissions -rw-r--r--
added DatatypeHooks
     1 (* ID: $Id$
     2    Author: Jia Meng, NICTA
     3 *)
     4 
     5 
     6 structure ResAtpMethods =
     7 
     8 struct
     9   
    10 (* convert the negated 1st subgoal into CNF, write to file and call an ATP oracle *)
    11 fun res_atp_tac res_atp_oracle mode timeLimit ctxt user_thms n thm =
    12     (EVERY' [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac, 
    13 		  METAHYPS(fn negs =>
    14 			      HEADGOAL(Tactic.rtac 
    15 					   (res_atp_oracle (ProofContext.theory_of ctxt) 
    16 							   (ResAtp.write_subgoal_file mode ctxt negs user_thms n, timeLimit))))] n thm) handle (Fail _) => Seq.empty;
    17 
    18 (* vampire and eprover tactics *)
    19 
    20 fun vampire_tac st = res_atp_tac vampire_oracle ResAtp.Auto (!ResAtp.vampire_time) st;
    21 fun eprover_tac st = res_atp_tac eprover_oracle ResAtp.Auto (!ResAtp.eprover_time) st;
    22 
    23 fun vampireF_tac st = res_atp_tac vampire_oracle ResAtp.Fol (!ResAtp.vampire_time) st;
    24 
    25 fun vampireH_tac st = res_atp_tac vampire_oracle ResAtp.Hol (!ResAtp.vampire_time) st;
    26 
    27 fun eproverF_tac st = res_atp_tac eprover_oracle ResAtp.Fol (!ResAtp.eprover_time) st;
    28 
    29 fun eproverH_tac st = res_atp_tac eprover_oracle ResAtp.Hol (!ResAtp.eprover_time) st;
    30 
    31 val ResAtps_setup =
    32   Method.add_methods 
    33     [("vampireF", ResAtp.atp_method vampireF_tac, "Vampire for FOL problems"),
    34      ("eproverF", ResAtp.atp_method eproverF_tac, "E prover for FOL problems"),
    35      ("vampireH", ResAtp.atp_method vampireH_tac, "Vampire for HOL problems"),
    36      ("eproverH", ResAtp.atp_method eproverH_tac, "E prover for HOL problems"),
    37      ("eprover", ResAtp.atp_method eprover_tac, "E prover for FOL and HOL problems"),
    38      ("vampire", ResAtp.atp_method vampire_tac, "Vampire for FOL and HOL problems")];
    39 
    40 end