src/HOL/Tools/res_atp_methods.ML
changeset 18002 35ec4681d38f
parent 17907 c20e4bddcb11
child 18195 971dc7439088
     1.1 --- a/src/HOL/Tools/res_atp_methods.ML	Fri Oct 28 02:27:19 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp_methods.ML	Fri Oct 28 02:28:20 2005 +0200
     1.3 @@ -25,24 +25,28 @@
     1.4  
     1.5  
     1.6  (* convert the negated 1st subgoal into CNF, write to files and call an ATP oracle *)
     1.7 -fun res_atp_tac res_atp_oracle timeLimit ctxt files tfrees n thm =
     1.8 +fun res_atp_tac res_atp_oracle tptp_form make_nnf timeLimit ctxt files tfrees n thm =
     1.9      SELECT_GOAL
    1.10  	((EVERY1 [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac, 
    1.11  		  METAHYPS(fn negs =>
    1.12  			      HEADGOAL(Tactic.rtac 
    1.13  					   (res_atp_oracle (ProofContext.theory_of ctxt) 
    1.14 -							   ((ResAtpSetup.tptp_form (make_clauses (map make_nnf negs)) n tfrees)::files, timeLimit))))]) handle Fail _ => no_tac) n thm;
    1.15 +							   ((tptp_form (make_clauses (map make_nnf negs)) n tfrees)::files, timeLimit))))]) handle Fail _ => no_tac) n thm;
    1.16  
    1.17 +(* vampire and eprover tactics *)
    1.18 +val vampireF_tac = res_atp_tac vampire_oracle ResAtpSetup.tptp_form make_nnf (!vampire_time);
    1.19  
    1.20 -(* vampire_tac and eprover_tac *)
    1.21 -val vampire_tac = res_atp_tac vampire_oracle (!vampire_time);
    1.22 +val vampireH_tac = res_atp_tac vampire_oracle ResAtpSetup.tptp_formH make_nnf1 (!vampire_time);
    1.23  
    1.24 -val eprover_tac = res_atp_tac eprover_oracle (!eprover_time);
    1.25 +val eproverF_tac = res_atp_tac eprover_oracle ResAtpSetup.tptp_form make_nnf (!eprover_time);
    1.26  
    1.27 +val eproverH_tac = res_atp_tac eprover_oracle ResAtpSetup.tptp_formH make_nnf1 (!eprover_time);
    1.28  
    1.29  val ResAtps_setup = [Method.add_methods 
    1.30 -		 [("vampire", ResAtpSetup.atp_method vampire_tac, "A Vampire method"),
    1.31 -		   ("eprover", ResAtpSetup.atp_method eprover_tac, "A E prover method")]];
    1.32 +		 [("vampireF", ResAtpSetup.atp_method_F vampireF_tac, "A Vampire method for FOL problems"),
    1.33 +		   ("eproverF", ResAtpSetup.atp_method_F eproverF_tac, "A E prover method for FOL problems"),
    1.34 +			("vampireH",ResAtpSetup.atp_method_H vampireH_tac, "A Vampire method for HOL problems"),
    1.35 +				("eproverH",ResAtpSetup.atp_method_H eproverH_tac,"A E prover method for HOL problems")]];
    1.36  
    1.37  
    1.38