src/HOL/Tools/res_atp_methods.ML
author wenzelm
Thu Mar 27 14:41:09 2008 +0100 (2008-03-27)
changeset 26424 a6cad32a27b0
parent 24321 e9d99744e40c
child 28290 4cc2b6046258
permissions -rw-r--r--
eliminated theory ProtoPure;
     1 (* ID: $Id$
     2    Author: Jia Meng, NICTA
     3 *)
     4 
     5 signature RES_ATP_METHODS =
     6 sig
     7   val vampire_tac: Proof.context -> thm list -> int -> tactic
     8   val eprover_tac: Proof.context -> thm list -> int -> tactic
     9   val spass_tac: Proof.context -> thm list -> int -> tactic
    10   val vampireF_tac: Proof.context -> thm list -> int -> tactic
    11   val vampireH_tac: Proof.context -> thm list -> int -> tactic
    12   val eproverF_tac: Proof.context -> thm list -> int -> tactic
    13   val eproverH_tac: Proof.context -> thm list -> int -> tactic
    14   val spassF_tac: Proof.context -> thm list -> int -> tactic
    15   val spassH_tac: Proof.context -> thm list -> int -> tactic
    16   val setup: theory -> theory
    17 end
    18 
    19 structure ResAtpMethods =
    20 struct
    21 
    22 (* convert the negated 1st subgoal into CNF, write to file and call an ATP oracle *)
    23 fun res_atp_tac dfg res_atp_oracle mode timeLimit ctxt user_thms i st =
    24   (EVERY'
    25    [rtac ccontr,
    26     ObjectLogic.atomize_prems_tac,
    27     Meson.skolemize_tac,
    28     METAHYPS (fn negs =>
    29       HEADGOAL (Tactic.rtac
    30         (res_atp_oracle (ProofContext.theory_of ctxt)
    31           (ResAtp.write_subgoal_file dfg mode ctxt negs user_thms i, timeLimit))))] i st) handle Fail _ => Seq.empty;
    32 
    33 
    34 (* vampire, eprover and spass tactics *)
    35 
    36 fun vampire_tac st = res_atp_tac false vampire_oracle ResAtp.Auto (!ResAtp.time_limit) st;
    37 fun eprover_tac st = res_atp_tac false eprover_oracle ResAtp.Auto (!ResAtp.time_limit) st;
    38 fun spass_tac st = res_atp_tac true spass_oracle ResAtp.Auto (!ResAtp.time_limit) st;
    39 
    40 
    41 fun vampireF_tac st = res_atp_tac false vampire_oracle ResAtp.Fol (!ResAtp.time_limit) st;
    42 
    43 fun vampireH_tac st = res_atp_tac false vampire_oracle ResAtp.Hol (!ResAtp.time_limit) st;
    44 
    45 fun eproverF_tac st = res_atp_tac false eprover_oracle ResAtp.Fol (!ResAtp.time_limit) st;
    46 
    47 fun eproverH_tac st = res_atp_tac false eprover_oracle ResAtp.Hol (!ResAtp.time_limit) st;
    48 
    49 fun spassF_tac st = res_atp_tac true spass_oracle ResAtp.Fol (!ResAtp.time_limit) st;
    50 
    51 fun spassH_tac st = res_atp_tac true spass_oracle ResAtp.Hol (!ResAtp.time_limit) st;
    52 
    53 
    54 fun atp_method tac =
    55   Method.thms_ctxt_args (fn ths => fn ctxt => Method.SIMPLE_METHOD' (tac ctxt ths));
    56 
    57 val setup =
    58   Method.add_methods
    59     [("vampireF", atp_method vampireF_tac, "Vampire for FOL problems"),
    60      ("eproverF", atp_method eproverF_tac, "E prover for FOL problems"),
    61      ("vampireH", atp_method vampireH_tac, "Vampire for HOL problems"),
    62      ("eproverH", atp_method eproverH_tac, "E prover for HOL problems"),
    63      ("eprover", atp_method eprover_tac, "E prover for FOL and HOL problems"),
    64      ("vampire", atp_method vampire_tac, "Vampire for FOL and HOL problems"),
    65      ("spassF", atp_method spassF_tac, "SPASS for FOL problems"),
    66      ("spassH", atp_method spassH_tac, "SPASS for HOL problems"),
    67      ("spass", atp_method spass_tac, "SPASS for FOL and HOL problems")];
    68 
    69 end;