src/HOL/Tools/res_atp_methods.ML
author haftmann
Fri Dec 16 09:00:11 2005 +0100 (2005-12-16)
changeset 18418 bf448d999b7e
parent 18271 0e9a851db989
child 18708 4b3dadb4fe33
permissions -rw-r--r--
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
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@17905
    10
mengj@17905
    11
val vampire_time = ref 60;
mengj@17905
    12
val eprover_time = ref 60;
mengj@17905
    13
mengj@17905
    14
fun run_vampire time =  
mengj@17905
    15
    if (time >0) then vampire_time:= time
mengj@17905
    16
    else vampire_time:=60;
mengj@17905
    17
mengj@17905
    18
fun run_eprover time = 
mengj@17905
    19
    if (time > 0) then eprover_time:= time
mengj@17905
    20
    else eprover_time:=60;
mengj@17905
    21
mengj@17905
    22
fun vampireLimit () = !vampire_time;
mengj@17905
    23
fun eproverLimit () = !eprover_time;
mengj@17905
    24
mengj@17905
    25
mengj@17905
    26
mengj@17905
    27
(* convert the negated 1st subgoal into CNF, write to files and call an ATP oracle *)
mengj@18271
    28
fun res_atp_tac res_atp_oracle mode timeLimit ctxt user_thms n thm =
mengj@17905
    29
    SELECT_GOAL
mengj@17905
    30
	((EVERY1 [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac, 
mengj@17905
    31
		  METAHYPS(fn negs =>
mengj@17905
    32
			      HEADGOAL(Tactic.rtac 
mengj@17905
    33
					   (res_atp_oracle (ProofContext.theory_of ctxt) 
mengj@18271
    34
							   (ResAtpSetup.prep_atp_input mode ctxt negs user_thms n, timeLimit))))]) handle Fail _ => no_tac) n thm;
mengj@17905
    35
mengj@18002
    36
(* vampire and eprover tactics *)
mengj@17905
    37
mengj@18271
    38
val vampire_tac = res_atp_tac vampire_oracle ResAtpSetup.Auto (!vampire_time);
mengj@18271
    39
val eprover_tac = res_atp_tac eprover_oracle ResAtpSetup.Auto(!eprover_time);
mengj@18271
    40
mengj@18271
    41
val vampireF_tac = res_atp_tac vampire_oracle ResAtpSetup.Fol(!vampire_time);
mengj@17905
    42
mengj@18271
    43
val vampireH_tac = res_atp_tac vampire_oracle ResAtpSetup.Hol (!vampire_time);
mengj@17905
    44
mengj@18271
    45
val eproverF_tac = res_atp_tac eprover_oracle ResAtpSetup.Fol (!eprover_time);
mengj@18271
    46
mengj@18271
    47
val eproverH_tac = res_atp_tac eprover_oracle ResAtpSetup.Hol (!eprover_time);
mengj@17905
    48
mengj@17905
    49
val ResAtps_setup = [Method.add_methods 
mengj@18271
    50
		 [("vampireF", ResAtpSetup.atp_method vampireF_tac, "A Vampire method for FOL problems"),
mengj@18271
    51
		   ("eproverF", ResAtpSetup.atp_method eproverF_tac, "A E prover method for FOL problems"),
mengj@18271
    52
			("vampireH",ResAtpSetup.atp_method vampireH_tac, "A Vampire method for HOL problems"),
mengj@18271
    53
				("eproverH",ResAtpSetup.atp_method eproverH_tac,"A E prover method for HOL problems"),
mengj@18271
    54
				("eprover",ResAtpSetup.atp_method eprover_tac,"A E prover method for FOL and HOL problems"),
mengj@18271
    55
				("vampire",ResAtpSetup.atp_method vampire_tac,"A Vampire method for FOL and HOL problems")
mengj@18271
    56
]];
mengj@17905
    57
mengj@17905
    58
mengj@17905
    59
mengj@17905
    60
mengj@17907
    61
end