src/HOL/Tools/res_atp.ML
author paulson
Fri Oct 20 11:04:15 2006 +0200 (2006-10-20 ago)
changeset 21070 0a898140fea2
parent 20995 51c41f167adc
child 21132 88d1daae0319
permissions -rw-r--r--
Added more debugging info
     1 (*  Author: Jia Meng, Cambridge University Computer Laboratory, NICTA
     2     ID: $Id$
     3     Copyright 2004 University of Cambridge
     4 
     5 ATPs with TPTP format input.
     6 *)
     7 
     8 (*Currently unused, during debugging*)
     9 signature RES_ATP =
    10 sig
    11   val prover: string ref
    12   val custom_spass: string list ref
    13   val destdir: string ref
    14   val helper_path: string -> string -> string
    15   val problem_name: string ref
    16   val time_limit: int ref
    17    
    18   datatype mode = Auto | Fol | Hol
    19   val linkup_logic_mode : mode ref
    20   val write_subgoal_file: bool -> mode -> Proof.context -> thm list -> thm list -> int -> string
    21   val vampire_time: int ref
    22   val eprover_time: int ref
    23   val spass_time: int ref
    24   val run_vampire: int -> unit
    25   val run_eprover: int -> unit
    26   val run_spass: int -> unit
    27   val vampireLimit: unit -> int
    28   val eproverLimit: unit -> int
    29   val spassLimit: unit -> int
    30   val atp_method: (Proof.context -> thm list -> int -> tactic) ->
    31     Method.src -> Proof.context -> Proof.method
    32   val cond_rm_tmp: string -> unit
    33   val fol_keep_types: bool ref
    34   val hol_full_types: unit -> unit
    35   val hol_partial_types: unit -> unit
    36   val hol_const_types_only: unit -> unit
    37   val hol_no_types: unit -> unit
    38   val hol_typ_level: unit -> ResHolClause.type_level
    39   val include_all: bool ref
    40   val run_relevance_filter: bool ref
    41   val run_blacklist_filter: bool ref
    42   val blacklist: string list ref
    43   val add_all : unit -> unit
    44   val add_claset : unit -> unit
    45   val add_simpset : unit -> unit
    46   val add_clasimp : unit -> unit
    47   val add_atpset : unit -> unit
    48   val rm_all : unit -> unit
    49   val rm_claset : unit -> unit
    50   val rm_simpset : unit -> unit
    51   val rm_atpset : unit -> unit
    52   val rm_clasimp : unit -> unit
    53 end;
    54 
    55 structure ResAtp =
    56 struct
    57 
    58 fun timestamp s = Output.debug ("At " ^ Time.toString (Time.now()) ^ ": " ^ s);
    59 
    60 (********************************************************************)
    61 (* some settings for both background automatic ATP calling procedure*)
    62 (* and also explicit ATP invocation methods                         *)
    63 (********************************************************************)
    64 
    65 (*** background linkup ***)
    66 val call_atp = ref false; 
    67 val hook_count = ref 0;
    68 val time_limit = ref 80;
    69 val prover = ref "E";   (* use E as the default prover *)
    70 val custom_spass =   (*specialized options for SPASS*)
    71       ref ["-Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub"];
    72 val destdir = ref "";   (*Empty means write files to /tmp*)
    73 val problem_name = ref "prob";
    74 
    75 (*Return the path to a "helper" like SPASS or tptp2X, first checking that
    76   it exists.  FIXME: modify to use Path primitives and move to some central place.*)  
    77 fun helper_path evar base =
    78   case getenv evar of
    79       "" => error  ("Isabelle environment variable " ^ evar ^ " not defined")
    80     | home => 
    81         let val path = home ^ "/" ^ base
    82         in  if File.exists (File.unpack_platform_path path) then path 
    83 	    else error ("Could not find the file " ^ path)
    84 	end;  
    85 
    86 fun probfile_nosuffix _ = 
    87   if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
    88   else if File.exists (File.unpack_platform_path (!destdir))
    89   then !destdir ^ "/" ^ !problem_name
    90   else error ("No such directory: " ^ !destdir);
    91 
    92 fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n;
    93 
    94 
    95 (*** ATP methods ***)
    96 val vampire_time = ref 60;
    97 val eprover_time = ref 60;
    98 val spass_time = ref 60;
    99 
   100 fun run_vampire time =  
   101     if (time >0) then vampire_time:= time
   102     else vampire_time:=60;
   103 
   104 fun run_eprover time = 
   105     if (time > 0) then eprover_time:= time
   106     else eprover_time:=60;
   107 
   108 fun run_spass time = 
   109     if (time > 0) then spass_time:=time
   110     else spass_time:=60;
   111 
   112 
   113 fun vampireLimit () = !vampire_time;
   114 fun eproverLimit () = !eprover_time;
   115 fun spassLimit () = !spass_time;
   116 
   117 val fol_keep_types = ResClause.keep_types;
   118 val hol_full_types = ResHolClause.full_types;
   119 val hol_partial_types = ResHolClause.partial_types;
   120 val hol_const_types_only = ResHolClause.const_types_only;
   121 val hol_no_types = ResHolClause.no_types;
   122 fun hol_typ_level () = ResHolClause.find_typ_level ();
   123 fun is_typed_hol () = 
   124     let val tp_level = hol_typ_level()
   125     in
   126 	not (tp_level = ResHolClause.T_NONE)
   127     end;
   128 
   129 fun atp_input_file () =
   130     let val file = !problem_name 
   131     in
   132 	if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file))
   133 	else if File.exists (File.unpack_platform_path (!destdir))
   134 	then !destdir ^ "/" ^ file
   135 	else error ("No such directory: " ^ !destdir)
   136     end;
   137 
   138 val include_all = ref true;
   139 val include_simpset = ref false;
   140 val include_claset = ref false; 
   141 val include_atpset = ref true;
   142 
   143 (*Tests show that follow_defs gives VERY poor results with "include_all"*)
   144 fun add_all() = (include_all:=true; ReduceAxiomsN.follow_defs := false);
   145 fun rm_all() = include_all:=false;
   146 
   147 fun add_simpset() = include_simpset:=true;
   148 fun rm_simpset() = include_simpset:=false;
   149 
   150 fun add_claset() = include_claset:=true;
   151 fun rm_claset() = include_claset:=false;
   152 
   153 fun add_clasimp() = (include_simpset:=true;include_claset:=true);
   154 fun rm_clasimp() = (include_simpset:=false;include_claset:=false);
   155 
   156 fun add_atpset() = include_atpset:=true;
   157 fun rm_atpset() = include_atpset:=false;
   158 
   159 
   160 (**** relevance filter ****)
   161 val run_relevance_filter = ReduceAxiomsN.run_relevance_filter;
   162 val run_blacklist_filter = ref true;
   163 
   164 (******************************************************************)
   165 (* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *)
   166 (******************************************************************)
   167 
   168 datatype logic = FOL | HOL | HOLC | HOLCS;
   169 
   170 fun string_of_logic FOL = "FOL"
   171   | string_of_logic HOL = "HOL"
   172   | string_of_logic HOLC = "HOLC"
   173   | string_of_logic HOLCS = "HOLCS";
   174 
   175 fun is_fol_logic FOL = true
   176   | is_fol_logic  _ = false
   177 
   178 (*HOLCS will not occur here*)
   179 fun upgrade_lg HOLC _ = HOLC
   180   | upgrade_lg HOL HOLC = HOLC
   181   | upgrade_lg HOL _ = HOL
   182   | upgrade_lg FOL lg = lg; 
   183 
   184 (* check types *)
   185 fun has_bool_hfn (Type("bool",_)) = true
   186   | has_bool_hfn (Type("fun",_)) = true
   187   | has_bool_hfn (Type(_, Ts)) = exists has_bool_hfn Ts
   188   | has_bool_hfn _ = false;
   189 
   190 fun is_hol_fn tp =
   191     let val (targs,tr) = strip_type tp
   192     in
   193 	exists (has_bool_hfn) (tr::targs)
   194     end;
   195 
   196 fun is_hol_pred tp =
   197     let val (targs,tr) = strip_type tp
   198     in
   199 	exists (has_bool_hfn) targs
   200     end;
   201 
   202 exception FN_LG of term;
   203 
   204 fun fn_lg (t as Const(f,tp)) (lg,seen) = 
   205     if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) 
   206   | fn_lg (t as Free(f,tp)) (lg,seen) = 
   207     if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) 
   208   | fn_lg (t as Var(f,tp)) (lg,seen) =
   209     if is_hol_fn tp then (upgrade_lg HOL lg,insert (op =) t seen) else (lg,insert (op =) t seen)
   210   | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,insert (op =) t seen)
   211   | fn_lg f _ = raise FN_LG(f); 
   212 
   213 
   214 fun term_lg [] (lg,seen) = (lg,seen)
   215   | term_lg (tm::tms) (FOL,seen) =
   216       let val (f,args) = strip_comb tm
   217 	  val (lg',seen') = if f mem seen then (FOL,seen) 
   218 			    else fn_lg f (FOL,seen)
   219       in
   220 	if is_fol_logic lg' then ()
   221         else Output.debug ("Found a HOL term: " ^ Display.raw_string_of_term f);
   222         term_lg (args@tms) (lg',seen')
   223       end
   224   | term_lg _ (lg,seen) = (lg,seen)
   225 
   226 exception PRED_LG of term;
   227 
   228 fun pred_lg (t as Const(P,tp)) (lg,seen)= 
   229       if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen) 
   230   | pred_lg (t as Free(P,tp)) (lg,seen) =
   231       if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen)
   232   | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, insert (op =) t seen)
   233   | pred_lg P _ = raise PRED_LG(P);
   234 
   235 
   236 fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen)
   237   | lit_lg P (lg,seen) =
   238       let val (pred,args) = strip_comb P
   239 	  val (lg',seen') = if pred mem seen then (lg,seen) 
   240 			    else pred_lg pred (lg,seen)
   241       in
   242 	if is_fol_logic lg' then ()
   243 	else Output.debug ("Found a HOL predicate: " ^ Display.raw_string_of_term pred);
   244 	term_lg args (lg',seen')
   245       end;
   246 
   247 fun lits_lg [] (lg,seen) = (lg,seen)
   248   | lits_lg (lit::lits) (FOL,seen) =
   249       let val (lg,seen') = lit_lg lit (FOL,seen)
   250       in
   251 	if is_fol_logic lg then ()
   252 	else Output.debug ("Found a HOL literal: " ^ Display.raw_string_of_term lit);
   253 	lits_lg lits (lg,seen')
   254       end
   255   | lits_lg lits (lg,seen) = (lg,seen);
   256 
   257 fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs = 
   258     dest_disj_aux t (dest_disj_aux t' disjs)
   259   | dest_disj_aux t disjs = t::disjs;
   260 
   261 fun dest_disj t = dest_disj_aux t [];
   262 
   263 fun logic_of_clause tm (lg,seen) =
   264     let val tm' = HOLogic.dest_Trueprop tm
   265 	val disjs = dest_disj tm'
   266     in
   267 	lits_lg disjs (lg,seen)
   268     end;
   269 
   270 fun logic_of_clauses [] (lg,seen) = (lg,seen)
   271   | logic_of_clauses (cls::clss) (FOL,seen) =
   272     let val (lg,seen') = logic_of_clause cls (FOL,seen)
   273 	val _ =
   274           if is_fol_logic lg then ()
   275           else Output.debug ("Found a HOL clause: " ^ Display.raw_string_of_term cls)
   276     in
   277 	logic_of_clauses clss (lg,seen')
   278     end
   279   | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
   280 
   281 fun problem_logic_goals_aux [] (lg,seen) = lg
   282   | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) = 
   283     problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen));
   284     
   285 fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]);
   286 
   287 (***************************************************************)
   288 (* Retrieving and filtering lemmas                             *)
   289 (***************************************************************)
   290 
   291 (*** white list and black list of lemmas ***)
   292 
   293 (*The rule subsetI is frequently omitted by the relevance filter.*)
   294 val whitelist = ref [subsetI]; 
   295 
   296 (*Names of theorems and theorem lists to be banned. The final numeric suffix of
   297   theorem lists is first removed.
   298 
   299   These theorems typically produce clauses that are prolific (match too many equality or
   300   membership literals) and relate to seldom-used facts. Some duplicate other rules.
   301   FIXME: this blacklist needs to be maintained using theory data and added to using
   302   an attribute.*)
   303 val blacklist = ref
   304   ["Datatype.prod.size",
   305    "Datatype.unit.induct", (*"unit" thms cause unsound proofs; unit.nchotomy is caught automatically*)
   306    "Datatype.unit.inducts",
   307    "Datatype.unit.split_asm", 
   308    "Datatype.unit.split",
   309    "Datatype.unit.splits",
   310    "Divides.dvd_0_left_iff",
   311    "Finite_Set.card_0_eq",
   312    "Finite_Set.card_infinite",
   313    "Finite_Set.Max_ge",
   314    "Finite_Set.Max_in",
   315    "Finite_Set.Max_le_iff",
   316    "Finite_Set.Max_less_iff",
   317    "Finite_Set.max.f_below_strict_below.below_f_conv", (*duplicates in Orderings.*)
   318    "Finite_Set.max.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
   319    "Finite_Set.Min_ge_iff",
   320    "Finite_Set.Min_gr_iff",
   321    "Finite_Set.Min_in",
   322    "Finite_Set.Min_le",
   323    "Finite_Set.min_max.below_inf_sup_Inf_Sup.inf_Sup_absorb", 
   324    "Finite_Set.min_max.below_inf_sup_Inf_Sup.sup_Inf_absorb", 
   325    "Finite_Set.min.f_below_strict_below.below_f_conv",        (*duplicates in Orderings.*)
   326    "Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
   327    "Fun.vimage_image_eq",   (*involves an existential quantifier*)
   328    "HOL.split_if_asm",     (*splitting theorem*)
   329    "HOL.split_if",         (*splitting theorem*)
   330    "IntDef.abs_split",
   331    "IntDef.Integ.Abs_Integ_inject",
   332    "IntDef.Integ.Abs_Integ_inverse",
   333    "IntDiv.zdvd_0_left",
   334    "List.append_eq_append_conv",
   335    "List.hd_Cons_tl",   (*Says everything is [] or Cons. Probably prolific.*)
   336    "List.in_listsD",
   337    "List.in_listsI",
   338    "List.lists.Cons",
   339    "List.listsE",
   340    "Nat.less_one", (*not directional? obscure*)
   341    "Nat.not_gr0",
   342    "Nat.one_eq_mult_iff", (*duplicate by symmetry*)
   343    "NatArith.of_nat_0_eq_iff",
   344    "NatArith.of_nat_eq_0_iff",
   345    "NatArith.of_nat_le_0_iff",
   346    "NatSimprocs.divide_le_0_iff_number_of",  (*too many clauses*)
   347    "NatSimprocs.divide_less_0_iff_number_of",
   348    "NatSimprocs.equation_minus_iff_1",  (*not directional*)
   349    "NatSimprocs.equation_minus_iff_number_of", (*not directional*)
   350    "NatSimprocs.le_minus_iff_1", (*not directional*)
   351    "NatSimprocs.le_minus_iff_number_of",  (*not directional*)
   352    "NatSimprocs.less_minus_iff_1", (*not directional*)
   353    "NatSimprocs.less_minus_iff_number_of", (*not directional*)
   354    "NatSimprocs.minus_equation_iff_number_of", (*not directional*)
   355    "NatSimprocs.minus_le_iff_1", (*not directional*)
   356    "NatSimprocs.minus_le_iff_number_of", (*not directional*)
   357    "NatSimprocs.minus_less_iff_1", (*not directional*)
   358    "NatSimprocs.mult_le_cancel_left_number_of", (*excessive case analysis*)
   359    "NatSimprocs.mult_le_cancel_right_number_of", (*excessive case analysis*)
   360    "NatSimprocs.mult_less_cancel_left_number_of", (*excessive case analysis*)
   361    "NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*)
   362    "NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*)
   363    "NatSimprocs.zero_less_divide_iff_number_of",
   364    "OrderedGroup.abs_0_eq", (*duplicate by symmetry*)
   365    "OrderedGroup.diff_eq_0_iff_eq", (*prolific?*)
   366    "OrderedGroup.join_0_eq_0",
   367    "OrderedGroup.meet_0_eq_0",
   368    "OrderedGroup.pprt_eq_0",   (*obscure*)
   369    "OrderedGroup.pprt_eq_id",   (*obscure*)
   370    "OrderedGroup.pprt_mono",   (*obscure*)
   371    "Orderings.split_max",      (*splitting theorem*)
   372    "Orderings.split_min",      (*splitting theorem*)
   373    "Parity.even_nat_power",   (*obscure, somewhat prolilfic*)
   374    "Parity.power_eq_0_iff_number_of",
   375    "Parity.power_le_zero_eq_number_of",   (*obscure and prolific*)
   376    "Parity.power_less_zero_eq_number_of",
   377    "Parity.zero_le_power_eq_number_of",   (*obscure and prolific*)
   378    "Parity.zero_less_power_eq_number_of",   (*obscure and prolific*)
   379    "Power.zero_less_power_abs_iff",
   380    "Product_Type.split_eta_SetCompr",   (*involves an existential quantifier*)
   381    "Product_Type.split_paired_Ball_Sigma",     (*splitting theorem*)
   382    "Product_Type.split_paired_Bex_Sigma",      (*splitting theorem*)
   383    "Product_Type.split_split_asm",             (*splitting theorem*)
   384    "Product_Type.split_split",                 (*splitting theorem*)
   385    "Product_Type.unit_abs_eta_conv",
   386    "Product_Type.unit_induct",
   387    "Relation.diagI",
   388    "Relation.Domain_def",   (*involves an existential quantifier*)
   389    "Relation.Image_def",   (*involves an existential quantifier*)
   390    "Relation.ImageI",
   391    "Ring_and_Field.divide_cancel_left", (*fields are seldom used & often prolific*)
   392    "Ring_and_Field.divide_cancel_right",
   393    "Ring_and_Field.divide_divide_eq_left",
   394    "Ring_and_Field.divide_divide_eq_right",
   395    "Ring_and_Field.divide_eq_0_iff",
   396    "Ring_and_Field.divide_eq_1_iff",
   397    "Ring_and_Field.divide_eq_eq_1",
   398    "Ring_and_Field.divide_le_0_1_iff",
   399    "Ring_and_Field.divide_le_eq_1_neg",  (*obscure and prolific*)
   400    "Ring_and_Field.divide_le_eq_1_pos",  (*obscure and prolific*)
   401    "Ring_and_Field.divide_less_0_1_iff",
   402    "Ring_and_Field.divide_less_eq_1_neg",  (*obscure and prolific*)
   403    "Ring_and_Field.divide_less_eq_1_pos",  (*obscure and prolific*)
   404    "Ring_and_Field.eq_divide_eq_1", (*duplicate by symmetry*)
   405    "Ring_and_Field.field_mult_cancel_left",
   406    "Ring_and_Field.field_mult_cancel_right",
   407    "Ring_and_Field.inverse_le_iff_le_neg",
   408    "Ring_and_Field.inverse_le_iff_le",
   409    "Ring_and_Field.inverse_less_iff_less_neg",
   410    "Ring_and_Field.inverse_less_iff_less",
   411    "Ring_and_Field.le_divide_eq_1_neg", (*obscure and prolific*)
   412    "Ring_and_Field.le_divide_eq_1_pos", (*obscure and prolific*)
   413    "Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*)
   414    "Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*)
   415    "Ring_and_Field.one_eq_divide_iff",  (*duplicate by symmetry*)
   416    "Set.ball_simps", "Set.bex_simps",   (*quantifier rewriting: useless*)
   417    "Set.Collect_bex_eq",   (*involves an existential quantifier*)
   418    "Set.Collect_ex_eq",   (*involves an existential quantifier*)
   419    "Set.Diff_eq_empty_iff", (*redundant with paramodulation*)
   420    "Set.Diff_insert0",
   421    "Set.disjoint_insert",
   422    "Set.empty_Union_conv",   (*redundant with paramodulation*)
   423    "Set.full_SetCompr_eq",   (*involves an existential quantifier*)
   424    "Set.image_Collect",      (*involves an existential quantifier*)
   425    "Set.image_def",          (*involves an existential quantifier*)
   426    "Set.insert_disjoint",
   427    "Set.Int_UNIV",  (*redundant with paramodulation*)
   428    "Set.Inter_iff", (*We already have InterI, InterE*)
   429    "Set.Inter_UNIV_conv",
   430    "Set.psubsetE",    (*too prolific and obscure*)
   431    "Set.psubsetI",
   432    "Set.singleton_insert_inj_eq'",
   433    "Set.singleton_insert_inj_eq",
   434    "Set.singletonD",  (*these two duplicate some "insert" lemmas*)
   435    "Set.singletonI",
   436    "Set.Un_empty", (*redundant with paramodulation*)
   437    "Set.UNION_def",   (*involves an existential quantifier*)
   438    "Set.Union_empty_conv", (*redundant with paramodulation*)
   439    "Set.Union_iff",              (*We already have UnionI, UnionE*)
   440    "SetInterval.atLeastAtMost_iff", (*obscure and prolific*)
   441    "SetInterval.atLeastLessThan_iff", (*obscure and prolific*)
   442    "SetInterval.greaterThanAtMost_iff", (*obscure and prolific*)
   443    "SetInterval.greaterThanLessThan_iff", (*obscure and prolific*)
   444    "SetInterval.ivl_subset"];  (*excessive case analysis*)
   445 
   446 
   447 (*These might be prolific but are probably OK, and min and max are basic.
   448    "Orderings.max_less_iff_conj", 
   449    "Orderings.min_less_iff_conj",
   450    "Orderings.min_max.below_inf.below_inf_conv",
   451    "Orderings.min_max.below_sup.above_sup_conv",
   452 Very prolific and somewhat obscure:
   453    "Set.InterD",
   454    "Set.UnionI",
   455 *)
   456 
   457 (*** retrieve lemmas from clasimpset and atpset, may filter them ***)
   458 
   459 (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
   460 
   461 exception HASH_CLAUSE and HASH_STRING;
   462 
   463 (*Catches (for deletion) theorems automatically generated from other theorems*)
   464 fun insert_suffixed_names ht x = 
   465      (Polyhash.insert ht (x^"_iff1", ()); 
   466       Polyhash.insert ht (x^"_iff2", ()); 
   467       Polyhash.insert ht (x^"_dest", ())); 
   468 
   469 (*Are all characters in this string digits?*)
   470 fun all_numeric s = null (String.tokens Char.isDigit s);
   471 
   472 (*Delete a suffix of the form _\d+*)
   473 fun delete_numeric_suffix s =
   474   case rev (String.fields (fn c => c = #"_") s) of
   475       last::rest => 
   476           if all_numeric last 
   477           then [s, space_implode "_" (rev rest)]
   478           else [s]
   479     | [] => [s];
   480 
   481 fun banned_thmlist s =
   482   (Sign.base_name s) mem_string ["induct","inducts","split","splits","split_asm"];
   483 
   484 (*Reject theorems with names like "List.filter.filter_list_def" or
   485   "Accessible_Part.acc.defs", as these are definitions arising from packages.
   486   FIXME: this will also block definitions within locales*)
   487 fun is_package_def a =
   488    length (NameSpace.unpack a) > 2 andalso 
   489    String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a;
   490 
   491 fun make_banned_test xs = 
   492   let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
   493                                 (6000, HASH_STRING)
   494       fun banned_aux s = 
   495             isSome (Polyhash.peek ht s) orelse banned_thmlist s orelse is_package_def s
   496       fun banned s = exists banned_aux (delete_numeric_suffix s)
   497   in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
   498       app (insert_suffixed_names ht) (!blacklist @ xs); 
   499       banned
   500   end;
   501 
   502 (** a hash function from Term.term to int, and also a hash table **)
   503 val xor_words = List.foldl Word.xorb 0w0;
   504 
   505 fun hashw_term ((Const(c,_)), w) = Polyhash.hashw_string (c,w)
   506   | hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w)
   507   | hashw_term ((Var(_,_)), w) = w
   508   | hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w)
   509   | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
   510   | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));
   511 
   512 fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0))
   513   | hash_literal P = hashw_term(P,0w0);
   514 
   515 
   516 fun get_literals (Const("Trueprop",_)$P) lits = get_literals P lits
   517   | get_literals (Const("op |",_)$P$Q) lits = get_literals Q (get_literals P lits)
   518   | get_literals lit lits = (lit::lits);
   519 
   520 fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t [])));
   521 
   522 (*Versions ONLY for "faking" a theorem name. Here we take variable names into account
   523   so that similar theorems don't collide.  FIXME: this entire business of "faking" 
   524   theorem names must end!*)
   525 fun hashw_typ (TVar ((a,i), _), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w))
   526   | hashw_typ (TFree (a,_), w) = Polyhash.hashw_string (a,w)
   527   | hashw_typ (Type (a, Ts), w) = Polyhash.hashw_string (a, List.foldl hashw_typ w Ts);
   528 
   529 fun full_hashw_term ((Const(c,T)), w) = Polyhash.hashw_string (c, hashw_typ(T,w))
   530   | full_hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w)
   531   | full_hashw_term ((Var((a,i),_)), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w))
   532   | full_hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w)
   533   | full_hashw_term ((Abs(_,T,t)), w) = full_hashw_term (t, hashw_typ(T,w))
   534   | full_hashw_term ((P$Q), w) = full_hashw_term (Q, (full_hashw_term (P, w)));
   535 
   536 fun full_hashw_thm (th,w) = 
   537   let val {prop,hyps,...} = rep_thm th
   538   in List.foldl full_hashw_term w (prop::hyps) end
   539 
   540 fun full_hash_thm th = full_hashw_thm (th,0w0);
   541 
   542 fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
   543 
   544 (*Create a hash table for clauses, of the given size*)
   545 fun mk_clause_table n =
   546       Polyhash.mkTable (hash_term o prop_of, equal_thm)
   547                        (n, HASH_CLAUSE);
   548 
   549 (*Use a hash table to eliminate duplicates from xs. Argument is a list of
   550   (thm * (string * int)) tuples. The theorems are hashed into the table. *)
   551 fun make_unique xs = 
   552   let val ht = mk_clause_table 7000
   553   in
   554       Output.debug("make_unique gets " ^ Int.toString (length xs) ^ " clauses");
   555       app (ignore o Polyhash.peekInsert ht) xs;  
   556       Polyhash.listItems ht
   557   end;
   558 
   559 (*Remove existing axiom clauses from the conjecture clauses, as this can dramatically
   560   boost an ATP's performance (for some reason)*)
   561 fun subtract_cls c_clauses ax_clauses = 
   562   let val ht = mk_clause_table 2200
   563       fun known x = isSome (Polyhash.peek ht x)
   564   in
   565       app (ignore o Polyhash.peekInsert ht) ax_clauses;  
   566       filter (not o known) c_clauses 
   567   end;
   568 
   569 (*Filter axiom clauses, but keep supplied clauses and clauses in whitelist. 
   570   Duplicates are removed later.*)
   571 fun get_relevant_clauses thy cls_thms white_cls goals =
   572   white_cls @ (ReduceAxiomsN.relevance_filter thy cls_thms goals);
   573 
   574 (*This name is cryptic but short. Unlike gensym, we get the same name each time.*)
   575 fun fake_thm_name th = 
   576     Context.theory_name (theory_of_thm th) ^ "." ^ Word.toString (full_hash_thm th);
   577 
   578 fun put_name_pair ("",th) = (fake_thm_name th, th)
   579   | put_name_pair (a,th)  = (a,th);
   580 
   581 fun display_thms [] = ()
   582   | display_thms ((name,thm)::nthms) = 
   583       let val nthm = name ^ ": " ^ (string_of_thm thm)
   584       in Output.debug nthm; display_thms nthms  end;
   585  
   586 fun all_facts_of ctxt =
   587   FactIndex.find (ProofContext.fact_index_of ctxt) ([], [])
   588   |> maps #2 |> map (`Thm.name_of_thm);
   589 
   590 (* get lemmas from claset, simpset, atpset and extra supplied rules *)
   591 fun get_clasimp_atp_lemmas ctxt user_thms = 
   592   let val included_thms =
   593 	if !include_all 
   594 	then (tap (fn ths => Output.debug
   595 	             ("Including all " ^ Int.toString (length ths) ^ " theorems")) 
   596 	          (all_facts_of ctxt @ PureThy.all_thms_of (ProofContext.theory_of ctxt)))
   597 	else 
   598 	let val claset_thms =
   599 		if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt
   600 		else []
   601 	    val simpset_thms = 
   602 		if !include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt
   603 		else []
   604 	    val atpset_thms =
   605 		if !include_atpset then ResAxioms.atpset_rules_of_ctxt ctxt
   606 		else []
   607 	    val _ = if !Output.show_debug_msgs 
   608 		    then (Output.debug "ATP theorems: "; display_thms atpset_thms) 
   609 		    else ()		 
   610 	in  claset_thms @ simpset_thms @ atpset_thms  end
   611       val user_rules = map (put_name_pair o ResAxioms.pairname)
   612 			   (if null user_thms then !whitelist else user_thms)
   613   in
   614       (map put_name_pair included_thms, user_rules)
   615   end;
   616 
   617 (*Remove lemmas that are banned from the backlist. Also remove duplicates. *)
   618 fun blacklist_filter thms = 
   619   if !run_blacklist_filter then 
   620       let val _ = Output.debug("blacklist filter gets " ^ Int.toString (length thms) ^ " theorems")
   621           val banned = make_banned_test (map #1 thms)
   622 	  fun ok (a,_) = not (banned a)
   623 	  val okthms = filter ok thms
   624           val _ = Output.debug("...and returns " ^ Int.toString (length okthms))
   625       in  okthms end
   626   else thms;
   627 
   628 
   629 (***************************************************************)
   630 (* ATP invocation methods setup                                *)
   631 (***************************************************************)
   632 
   633 fun cnf_hyps_thms ctxt = 
   634     let val ths = Assumption.prems_of ctxt
   635     in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end;
   636 
   637 (*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
   638 datatype mode = Auto | Fol | Hol;
   639 
   640 val linkup_logic_mode = ref Auto;
   641 
   642 (*Ensures that no higher-order theorems "leak out"*)
   643 fun restrict_to_logic logic cls =
   644   if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o fst) cls 
   645 	                else cls;
   646 
   647 fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =
   648     if is_fol_logic logic 
   649     then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
   650     else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) user_lemmas;
   651 
   652 fun dfg_writer logic goals filename (axioms,classrels,arities) user_lemmas =
   653     if is_fol_logic logic 
   654     then ResClause.dfg_write_file goals filename (axioms, classrels, arities)
   655     else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities) user_lemmas;
   656 
   657 (*Called by the oracle-based methods declared in res_atp_methods.ML*)
   658 fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
   659     let val conj_cls = make_clauses conjectures 
   660                          |> ResAxioms.assume_abstract_list |> Meson.finish_cnf
   661 	val hyp_cls = cnf_hyps_thms ctxt
   662 	val goal_cls = conj_cls@hyp_cls
   663 	val logic = case mode of 
   664                             Auto => problem_logic_goals [map prop_of goal_cls]
   665 			  | Fol => FOL
   666 			  | Hol => HOL
   667 	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
   668 	val cla_simp_atp_clauses = included_thms |> blacklist_filter
   669 	                             |> ResAxioms.cnf_rules_pairs |> make_unique 
   670                                      |> restrict_to_logic logic 
   671 	val user_cls = ResAxioms.cnf_rules_pairs user_rules
   672 	val thy = ProofContext.theory_of ctxt
   673 	val axclauses = get_relevant_clauses thy cla_simp_atp_clauses
   674 	                            user_cls (map prop_of goal_cls) |> make_unique
   675 	val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
   676 	val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
   677 	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
   678         val writer = if dfg then dfg_writer else tptp_writer 
   679 	and file = atp_input_file()
   680 	and user_lemmas_names = map #1 user_rules
   681     in
   682 	writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
   683 	Output.debug ("Writing to " ^ file);
   684 	file
   685     end;
   686 
   687 
   688 (**** remove tmp files ****)
   689 fun cond_rm_tmp file = 
   690     if !Output.show_debug_msgs orelse !destdir <> "" then Output.debug "ATP input kept..." 
   691     else OS.FileSys.remove file;
   692 
   693 
   694 (****** setup ATPs as Isabelle methods ******)
   695 fun atp_meth' tac ths ctxt = 
   696     Method.SIMPLE_METHOD' HEADGOAL
   697     (tac ctxt ths);
   698 
   699 fun atp_meth tac ths ctxt = 
   700     let val thy = ProofContext.theory_of ctxt
   701 	val _ = ResClause.init thy
   702 	val _ = ResHolClause.init thy
   703     in
   704 	atp_meth' tac ths ctxt
   705     end;
   706 
   707 fun atp_method tac = Method.thms_ctxt_args (atp_meth tac);
   708 
   709 (***************************************************************)
   710 (* automatic ATP invocation                                    *)
   711 (***************************************************************)
   712 
   713 (* call prover with settings and problem file for the current subgoal *)
   714 fun watcher_call_provers sign sg_terms (childin, childout, pid) =
   715   let
   716     fun make_atp_list [] n = []
   717       | make_atp_list (sg_term::xs) n =
   718           let
   719             val probfile = prob_pathname n
   720             val time = Int.toString (!time_limit)
   721           in
   722             Output.debug ("problem file in watcher_call_provers is " ^ probfile);
   723             (*options are separated by Watcher.setting_sep, currently #"%"*)
   724             if !prover = "spass"
   725             then
   726               let val spass = helper_path "SPASS_HOME" "SPASS"
   727                   val sopts =
   728    "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
   729               in 
   730                   ("spass", spass, sopts, probfile) :: make_atp_list xs (n+1)
   731               end
   732             else if !prover = "vampire"
   733 	    then 
   734               let val vampire = helper_path "VAMPIRE_HOME" "vampire"
   735                   val casc = if !time_limit > 70 then "--mode casc%" else ""
   736                   val vopts = casc ^ "-m 100000%-t " ^ time
   737               in
   738                   ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1)
   739               end
   740       	     else if !prover = "E"
   741       	     then
   742 	       let val Eprover = helper_path "E_HOME" "eproof"
   743 	       in
   744 		  ("E", Eprover, 
   745 		     "--tptp-in%-l5%-xAuto%-tAuto%--silent%--cpu-limit=" ^ time, probfile) ::
   746 		   make_atp_list xs (n+1)
   747 	       end
   748 	     else error ("Invalid prover name: " ^ !prover)
   749           end
   750 
   751     val atp_list = make_atp_list sg_terms 1
   752   in
   753     Watcher.callResProvers(childout,atp_list);
   754     Output.debug "Sent commands to watcher!"
   755   end
   756   
   757 fun trace_array fname =
   758   let val path = File.unpack_platform_path fname
   759   in  Array.app (File.append path o (fn s => s ^ "\n"))  end;
   760 
   761 (*Converting a subgoal into negated conjecture clauses*)
   762 fun neg_clauses th n =
   763   let val tacs = [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac]
   764       val st = Seq.hd (EVERY' tacs n th)
   765       val negs = Option.valOf (metahyps_thms n st)
   766   in make_clauses negs |> ResAxioms.assume_abstract_list |> Meson.finish_cnf end;
   767 		                       
   768 (*We write out problem files for each subgoal. Argument probfile generates filenames,
   769   and allows the suppression of the suffix "_1" in problem-generation mode.
   770   FIXME: does not cope with &&, and it isn't easy because one could have multiple
   771   subgoals, each involving &&.*)
   772 fun write_problem_files probfile (ctxt,th)  =
   773   let val goals = Thm.prems_of th
   774       val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
   775       val thy = ProofContext.theory_of ctxt
   776       fun get_neg_subgoals [] _ = []
   777         | get_neg_subgoals (gl::gls) n = neg_clauses th n :: get_neg_subgoals gls (n+1)
   778       val goal_cls = get_neg_subgoals goals 1
   779       val logic = case !linkup_logic_mode of
   780 		Auto => problem_logic_goals (map ((map prop_of)) goal_cls)
   781 	      | Fol => FOL
   782 	      | Hol => HOL
   783       val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
   784       val included_cls = included_thms |> blacklist_filter
   785                                        |> ResAxioms.cnf_rules_pairs |> make_unique 
   786                                        |> restrict_to_logic logic 
   787       val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls))
   788       val white_cls = ResAxioms.cnf_rules_pairs white_thms
   789       (*clauses relevant to goal gl*)
   790       val axcls_list = map (fn gl => get_relevant_clauses thy included_cls white_cls [gl])
   791                            goals
   792       val _ = app (fn axcls => Output.debug ("filtered clauses = " ^ Int.toString(length axcls)))
   793                   axcls_list
   794       val keep_types = if is_fol_logic logic then !ResClause.keep_types 
   795                        else is_typed_hol ()
   796       val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy
   797                              else []
   798       val _ = Output.debug ("classrel clauses = " ^ 
   799                             Int.toString (length classrel_clauses))
   800       val arity_clauses = if keep_types then ResClause.arity_clause_thy thy 
   801                           else []
   802       val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
   803       val writer = if !prover = "spass" then dfg_writer else tptp_writer 
   804       fun write_all [] [] _ = []
   805 	| write_all (ccls::ccls_list) (axcls::axcls_list) k =
   806             let val fname = probfile k
   807                 val axcls = make_unique axcls
   808                 val ccls = subtract_cls ccls axcls
   809                 val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
   810                 val thm_names = Array.fromList clnames
   811                 val _ = if !Output.show_debug_msgs 
   812                         then trace_array (fname ^ "_thm_names") thm_names else ()
   813             in  (thm_names,fname) :: write_all ccls_list axcls_list (k+1)  end
   814       val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
   815   in
   816       (filenames, thm_names_list)
   817   end;
   818 
   819 val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
   820                                     Posix.Process.pid * string list) option);
   821 
   822 fun kill_last_watcher () =
   823     (case !last_watcher_pid of 
   824          NONE => ()
   825        | SOME (_, _, pid, files) => 
   826 	  (Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid);
   827 	   Watcher.killWatcher pid;  
   828 	   ignore (map (try cond_rm_tmp) files)))
   829      handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed";
   830 
   831 (*writes out the current clasimpset to a tptp file;
   832   turns off xsymbol at start of function, restoring it at end    *)
   833 fun isar_atp_body (ctxt, th) =
   834   if Thm.no_prems th then ()
   835   else
   836     let
   837       val _ = kill_last_watcher()
   838       val (files,thm_names_list) = write_problem_files prob_pathname (ctxt,th)
   839       val (childin, childout, pid) = Watcher.createWatcher (th, thm_names_list)
   840     in
   841       last_watcher_pid := SOME (childin, childout, pid, files);
   842       Output.debug ("problem files: " ^ space_implode ", " files); 
   843       Output.debug ("pid: " ^ string_of_pid pid);
   844       watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
   845     end;
   846 
   847 val isar_atp = setmp print_mode [] isar_atp_body;
   848 
   849 (*For ML scripts, and primarily, for debugging*)
   850 fun callatp () = 
   851   let val th = topthm()
   852       val ctxt = ProofContext.init (theory_of_thm th)
   853   in  isar_atp_body (ctxt, th)  end;
   854 
   855 val isar_atp_writeonly = setmp print_mode [] 
   856       (fn (ctxt,th) =>
   857        if Thm.no_prems th then ()
   858        else 
   859          let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix 
   860           	            else prob_pathname
   861          in ignore (write_problem_files probfile (ctxt,th)) end);
   862 
   863 
   864 (** the Isar toplevel hook **)
   865 
   866 fun invoke_atp_ml (ctxt, goal) =
   867   let val thy = ProofContext.theory_of ctxt;
   868   in
   869     Output.debug ("subgoals in isar_atp:\n" ^ 
   870 		  Pretty.string_of (ProofContext.pretty_term ctxt
   871 		    (Logic.mk_conjunction_list (Thm.prems_of goal))));
   872     Output.debug ("current theory: " ^ Context.theory_name thy);
   873     inc hook_count;
   874     Output.debug ("in hook for time: " ^ Int.toString (!hook_count));
   875     ResClause.init thy;
   876     ResHolClause.init thy;
   877     if !destdir = "" andalso !time_limit > 0 then isar_atp (ctxt, goal)
   878     else isar_atp_writeonly (ctxt, goal)
   879   end;
   880 
   881 val invoke_atp = Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep
   882  (fn state =>
   883   let val (ctxt, (_, goal)) = Proof.get_goal (Toplevel.proof_of state)
   884   in  invoke_atp_ml (ctxt, goal)  end);
   885 
   886 val call_atpP =
   887   OuterSyntax.command 
   888     "ProofGeneral.call_atp" 
   889     "call automatic theorem provers" 
   890     OuterKeyword.diag
   891     (Scan.succeed invoke_atp);
   892 
   893 val _ = OuterSyntax.add_parsers [call_atpP];
   894 
   895 end;