src/HOL/Tools/res_atp_methods.ML
author haftmann
Fri Feb 10 09:09:07 2006 +0100 (2006-02-10)
changeset 19008 14c1b2f5dda4
parent 18739 ade018a62450
child 19128 495ecbefc5df
permissions -rw-r--r--
improved code generator devarification
     1 (* ID: $Id$
     2    Author: Jia Meng, NICTA
     3 *)
     4 
     5 
     6 structure ResAtpMethods =
     7 
     8 struct
     9   
    10 
    11 val vampire_time = ref 60;
    12 val eprover_time = ref 60;
    13 
    14 fun run_vampire time =  
    15     if (time >0) then vampire_time:= time
    16     else vampire_time:=60;
    17 
    18 fun run_eprover time = 
    19     if (time > 0) then eprover_time:= time
    20     else eprover_time:=60;
    21 
    22 fun vampireLimit () = !vampire_time;
    23 fun eproverLimit () = !eprover_time;
    24 
    25 
    26 
    27 (* convert the negated 1st subgoal into CNF, write to files and call an ATP oracle *)
    28 fun res_atp_tac res_atp_oracle mode timeLimit ctxt user_thms n thm =
    29     SELECT_GOAL
    30 	((EVERY1 [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac, 
    31 		  METAHYPS(fn negs =>
    32 			      HEADGOAL(Tactic.rtac 
    33 					   (res_atp_oracle (ProofContext.theory_of ctxt) 
    34 							   (ResAtpSetup.prep_atp_input mode ctxt negs user_thms n, timeLimit))))]) handle Fail _ => no_tac) n thm;
    35 
    36 (* vampire and eprover tactics *)
    37 
    38 fun vampire_tac st = res_atp_tac vampire_oracle ResAtpSetup.Auto (!vampire_time) st;
    39 fun eprover_tac st = res_atp_tac eprover_oracle ResAtpSetup.Auto (!eprover_time) st;
    40 
    41 fun vampireF_tac st = res_atp_tac vampire_oracle ResAtpSetup.Fol (!vampire_time) st;
    42 
    43 fun vampireH_tac st = res_atp_tac vampire_oracle ResAtpSetup.Hol (!vampire_time) st;
    44 
    45 fun eproverF_tac st = res_atp_tac eprover_oracle ResAtpSetup.Fol (!eprover_time) st;
    46 
    47 fun eproverH_tac st = res_atp_tac eprover_oracle ResAtpSetup.Hol (!eprover_time) st;
    48 
    49 val ResAtps_setup =
    50   Method.add_methods 
    51     [("vampireF", ResAtpSetup.atp_method vampireF_tac, "Vampire for FOL problems"),
    52      ("eproverF", ResAtpSetup.atp_method eproverF_tac, "E prover for FOL problems"),
    53      ("vampireH", ResAtpSetup.atp_method vampireH_tac, "Vampire for HOL problems"),
    54      ("eproverH", ResAtpSetup.atp_method eproverH_tac, "E prover for HOL problems"),
    55      ("eprover", ResAtpSetup.atp_method eprover_tac, "E prover for FOL and HOL problems"),
    56      ("vampire", ResAtpSetup.atp_method vampire_tac, "Vampire for FOL and HOL problems")];
    57 
    58 end