# HG changeset patch # User paulson # Date 1162912914 -3600 # Node ID f86b8463af370470994c963fccb010363e78af3b # Parent b3bdc1abc7d39a77759e3b01b625b1c9f8e4c37e Proper theorem names at last, no fakes!! Added set_prover function to set various parameters to improve success rate. Fixed the auto settings for E. diff -r b3bdc1abc7d3 -r f86b8463af37 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Tue Nov 07 15:07:02 2006 +0100 +++ b/src/HOL/Tools/res_atp.ML Tue Nov 07 16:21:54 2006 +0100 @@ -14,6 +14,7 @@ val helper_path: string -> string -> string val problem_name: string ref val time_limit: int ref + val set_prover: string -> unit datatype mode = Auto | Fol | Hol val linkup_logic_mode : mode ref @@ -65,8 +66,27 @@ (*** background linkup ***) val call_atp = ref false; val hook_count = ref 0; -val time_limit = ref 80; -val prover = ref "E"; (* use E as the default prover *) +val time_limit = ref 60; +val prover = ref ""; + +fun set_prover atp = + case String.map Char.toLower atp of + "e" => + (ReduceAxiomsN.max_new := 80; + ReduceAxiomsN.theory_const := false; + prover := "E") + | "spass" => + (ReduceAxiomsN.max_new := 40; + ReduceAxiomsN.theory_const := true; + prover := "spass") + | "vampire" => + (ReduceAxiomsN.max_new := 60; + ReduceAxiomsN.theory_const := false; + prover := "vampire") + | _ => error ("No such prover: " ^ atp); + +val _ = set_prover "E"; (* use E as the default prover *) + val custom_spass = (*specialized options for SPASS*) ref ["-Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub"]; val destdir = ref ""; (*Empty means write files to /tmp*) @@ -303,7 +323,7 @@ val blacklist = ref ["Datatype.prod.size", "Datatype.unit.exhaust", (*"unit" thms cause unsound proofs; unit.nchotomy is caught automatically*) - "Datatype.unit.induct", (*"unit" thms cause unsound proofs; unit.nchotomy is caught automatically*) + "Datatype.unit.induct", "Datatype.unit.inducts", "Datatype.unit.split_asm", "Datatype.unit.split", @@ -520,26 +540,6 @@ fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t []))); -(*Versions ONLY for "faking" a theorem name. Here we take variable names into account - so that similar theorems don't collide. FIXME: this entire business of "faking" - theorem names must end!*) -fun hashw_typ (TVar ((a,i), _), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w)) - | hashw_typ (TFree (a,_), w) = Polyhash.hashw_string (a,w) - | hashw_typ (Type (a, Ts), w) = Polyhash.hashw_string (a, List.foldl hashw_typ w Ts); - -fun full_hashw_term ((Const(c,T)), w) = Polyhash.hashw_string (c, hashw_typ(T,w)) - | full_hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w) - | full_hashw_term ((Var((a,i),_)), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w)) - | full_hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w) - | full_hashw_term ((Abs(_,T,t)), w) = full_hashw_term (t, hashw_typ(T,w)) - | full_hashw_term ((P$Q), w) = full_hashw_term (Q, (full_hashw_term (P, w))); - -fun full_hashw_thm (th,w) = - let val {prop,hyps,...} = rep_thm th - in List.foldl full_hashw_term w (prop::hyps) end - -fun full_hash_thm th = full_hashw_thm (th,0w0); - fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2); (*Create a hash table for clauses, of the given size*) @@ -572,21 +572,27 @@ fun get_relevant_clauses thy cls_thms white_cls goals = white_cls @ (ReduceAxiomsN.relevance_filter thy cls_thms goals); -(*This name is cryptic but short. Unlike gensym, we get the same name each time.*) -fun fake_thm_name th = - Context.theory_name (theory_of_thm th) ^ "." ^ Word.toString (full_hash_thm th); - -fun put_name_pair ("",th) = (fake_thm_name th, th) - | put_name_pair (a,th) = (a,th); - fun display_thms [] = () | display_thms ((name,thm)::nthms) = let val nthm = name ^ ": " ^ (string_of_thm thm) in Output.debug nthm; display_thms nthms end; -fun all_facts_of ctxt = - FactIndex.find (ProofContext.fact_index_of ctxt) ([], []) - |> maps #2 |> map (`Thm.name_of_thm); +fun all_valid_thms ctxt = + PureThy.thms_containing (ProofContext.theory_of ctxt) ([], []) @ + filter (ProofContext.valid_thms ctxt) + (FactIndex.find (ProofContext.fact_index_of ctxt) ([], [])); + +fun multi_name a (th, (n,pairs)) = + (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs) + +fun multi_names ((a, []), pairs) = pairs + | multi_names ((a, [th]), pairs) = (a,th)::pairs + | multi_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths); + +fun name_thm_pairs ctxt = foldl multi_names [] (all_valid_thms ctxt); + +fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false) + | check_named (_,th) = true; (* get lemmas from claset, simpset, atpset and extra supplied rules *) fun get_clasimp_atp_lemmas ctxt user_thms = @@ -594,7 +600,7 @@ if !include_all then (tap (fn ths => Output.debug ("Including all " ^ Int.toString (length ths) ^ " theorems")) - (all_facts_of ctxt @ PureThy.all_thms_of (ProofContext.theory_of ctxt))) + (name_thm_pairs ctxt)) else let val claset_thms = if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt @@ -609,10 +615,11 @@ then (Output.debug "ATP theorems: "; display_thms atpset_thms) else () in claset_thms @ simpset_thms @ atpset_thms end - val user_rules = map (put_name_pair o ResAxioms.pairname) - (if null user_thms then !whitelist else user_thms) + val user_rules = filter check_named + (map (ResAxioms.pairname) + (if null user_thms then !whitelist else user_thms)) in - (map put_name_pair included_thms, user_rules) + (filter check_named included_thms, user_rules) end; (*Remove lemmas that are banned from the backlist. Also remove duplicates. *) @@ -742,7 +749,7 @@ let val Eprover = helper_path "E_HOME" "eproof" in ("E", Eprover, - "--tptp-in%-l5%-xAuto%-tAuto%--silent%--cpu-limit=" ^ time, probfile) :: + "--tptp-in%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) :: make_atp_list xs (n+1) end else error ("Invalid prover name: " ^ !prover)