src/HOL/Tools/res_atp.ML
author wenzelm
Tue Apr 15 18:49:15 2008 +0200 (2008-04-15)
changeset 26662 39483503705f
parent 26501 494f418cc51c
child 26675 fba93ce71435
permissions -rw-r--r--
Facts.dest_table;
     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 signature RES_ATP =
     9 sig
    10   val prover: ResReconstruct.atp ref
    11   val destdir: string ref
    12   val helper_path: string -> string -> string
    13   val problem_name: string ref
    14   val time_limit: int ref
    15   val set_prover: string -> unit
    16 
    17   datatype mode = Auto | Fol | Hol
    18   val linkup_logic_mode : mode ref
    19   val write_subgoal_file: bool -> mode -> Proof.context -> thm list -> thm list -> int -> string
    20   val cond_rm_tmp: string -> unit
    21   val include_all: bool ref
    22   val run_relevance_filter: bool ref
    23   val run_blacklist_filter: bool ref
    24   val theory_const : bool ref
    25   val pass_mark    : real ref
    26   val convergence  : real ref
    27   val max_new      : int ref
    28   val max_sledgehammers : int ref
    29   val follow_defs  : bool ref
    30   val add_all : unit -> unit
    31   val add_claset : unit -> unit
    32   val add_simpset : unit -> unit
    33   val add_clasimp : unit -> unit
    34   val add_atpset : unit -> unit
    35   val rm_all : unit -> unit
    36   val rm_claset : unit -> unit
    37   val rm_simpset : unit -> unit
    38   val rm_atpset : unit -> unit
    39   val rm_clasimp : unit -> unit
    40   val tvar_classes_of_terms : term list -> string list
    41   val tfree_classes_of_terms : term list -> string list
    42   val type_consts_of_terms : theory -> term list -> string list
    43 end;
    44 
    45 structure ResAtp: RES_ATP =
    46 struct
    47 
    48 structure Recon = ResReconstruct;
    49 
    50 fun timestamp s = Output.debug (fn () => ("At " ^ Time.toString (Time.now()) ^ ": " ^ s));
    51 
    52 (********************************************************************)
    53 (* some settings for both background automatic ATP calling procedure*)
    54 (* and also explicit ATP invocation methods                         *)
    55 (********************************************************************)
    56 
    57 (*** background linkup ***)
    58 val run_blacklist_filter = ref true;
    59 val time_limit = ref 60;
    60 val prover = ref Recon.E;
    61 val max_sledgehammers = ref 1;
    62 
    63 
    64 (*** relevance filter parameters ***)
    65 val run_relevance_filter = ref true;
    66 val theory_const = ref true;
    67 val pass_mark = ref 0.5;
    68 val convergence = ref 3.2;    (*Higher numbers allow longer inference chains*)
    69 val max_new = ref 60;         (*Limits how many clauses can be picked up per stage*)
    70 val follow_defs = ref false;  (*Follow definitions. Makes problems bigger.*)
    71 
    72 fun set_prover atp =
    73   case String.map Char.toLower atp of
    74       "e" =>
    75           (max_new := 100;
    76            theory_const := false;
    77            prover := Recon.E)
    78     | "spass" =>
    79           (max_new := 40;
    80            theory_const := true;
    81            prover := Recon.SPASS)
    82     | "vampire" =>
    83           (max_new := 60;
    84            theory_const := false;
    85            prover := Recon.Vampire)
    86     | _ => error ("No such prover: " ^ atp);
    87 
    88 val _ = set_prover "E"; (* use E as the default prover *)
    89 
    90 val destdir = ref "";   (*Empty means write files to /tmp*)
    91 val problem_name = ref "prob";
    92 
    93 (*Return the path to a "helper" like SPASS or tptp2X, first checking that
    94   it exists.  FIXME: modify to use Path primitives and move to some central place.*)
    95 fun helper_path evar base =
    96   case getenv evar of
    97       "" => error  ("Isabelle environment variable " ^ evar ^ " not defined")
    98     | home =>
    99         let val path = home ^ "/" ^ base
   100         in  if File.exists (Path.explode path) then path
   101             else error ("Could not find the file " ^ path)
   102         end;
   103 
   104 fun probfile_nosuffix _ =
   105   if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
   106   else if File.exists (Path.explode (!destdir))
   107   then !destdir ^ "/" ^ !problem_name
   108   else error ("No such directory: " ^ !destdir);
   109 
   110 fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n;
   111 
   112 fun atp_input_file () =
   113     let val file = !problem_name
   114     in
   115         if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file))
   116         else if File.exists (Path.explode (!destdir))
   117         then !destdir ^ "/" ^ file
   118         else error ("No such directory: " ^ !destdir)
   119     end;
   120 
   121 val include_all = ref true;
   122 val include_simpset = ref false;
   123 val include_claset = ref false;
   124 val include_atpset = ref true;
   125 
   126 (*Tests show that follow_defs gives VERY poor results with "include_all"*)
   127 fun add_all() = (include_all:=true; follow_defs := false);
   128 fun rm_all() = include_all:=false;
   129 
   130 fun add_simpset() = include_simpset:=true;
   131 fun rm_simpset() = include_simpset:=false;
   132 
   133 fun add_claset() = include_claset:=true;
   134 fun rm_claset() = include_claset:=false;
   135 
   136 fun add_clasimp() = (include_simpset:=true;include_claset:=true);
   137 fun rm_clasimp() = (include_simpset:=false;include_claset:=false);
   138 
   139 fun add_atpset() = include_atpset:=true;
   140 fun rm_atpset() = include_atpset:=false;
   141 
   142 fun strip_Trueprop (Const("Trueprop",_) $ t) = t
   143   | strip_Trueprop t = t;
   144 
   145 
   146 (***************************************************************)
   147 (* Relevance Filtering                                         *)
   148 (***************************************************************)
   149 
   150 (*A surprising number of theorems contain only a few significant constants.
   151   These include all induction rules, and other general theorems. Filtering
   152   theorems in clause form reveals these complexities in the form of Skolem 
   153   functions. If we were instead to filter theorems in their natural form,
   154   some other method of measuring theorem complexity would become necessary.*)
   155 
   156 fun log_weight2 (x:real) = 1.0 + 2.0/Math.ln (x+1.0);
   157 
   158 (*The default seems best in practice. A constant function of one ignores
   159   the constant frequencies.*)
   160 val weight_fn = ref log_weight2;
   161 
   162 
   163 (*Including equality in this list might be expected to stop rules like subset_antisym from
   164   being chosen, but for some reason filtering works better with them listed. The
   165   logical signs All, Ex, &, and --> are omitted because any remaining occurrrences
   166   must be within comprehensions.*)
   167 val standard_consts = ["Trueprop","==>","all","==","op |","Not","op ="];
   168 
   169 
   170 (*** constants with types ***)
   171 
   172 (*An abstraction of Isabelle types*)
   173 datatype const_typ =  CTVar | CType of string * const_typ list
   174 
   175 (*Is the second type an instance of the first one?*)
   176 fun match_type (CType(con1,args1)) (CType(con2,args2)) = 
   177       con1=con2 andalso match_types args1 args2
   178   | match_type CTVar _ = true
   179   | match_type _ CTVar = false
   180 and match_types [] [] = true
   181   | match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2;
   182 
   183 (*Is there a unifiable constant?*)
   184 fun uni_mem gctab (c,c_typ) =
   185   case Symtab.lookup gctab c of
   186       NONE => false
   187     | SOME ctyps_list => exists (match_types c_typ) ctyps_list;
   188   
   189 (*Maps a "real" type to a const_typ*)
   190 fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) 
   191   | const_typ_of (TFree _) = CTVar
   192   | const_typ_of (TVar _) = CTVar
   193 
   194 (*Pairs a constant with the list of its type instantiations (using const_typ)*)
   195 fun const_with_typ thy (c,typ) = 
   196     let val tvars = Sign.const_typargs thy (c,typ)
   197     in (c, map const_typ_of tvars) end
   198     handle TYPE _ => (c,[]);   (*Variable (locale constant): monomorphic*)   
   199 
   200 (*Add a const/type pair to the table, but a [] entry means a standard connective,
   201   which we ignore.*)
   202 fun add_const_typ_table ((c,ctyps), tab) =
   203   Symtab.map_default (c, [ctyps]) (fn [] => [] | ctyps_list => insert (op =) ctyps ctyps_list) 
   204     tab;
   205 
   206 (*Free variables are included, as well as constants, to handle locales*)
   207 fun add_term_consts_typs_rm thy (Const(c, typ), tab) =
   208       add_const_typ_table (const_with_typ thy (c,typ), tab) 
   209   | add_term_consts_typs_rm thy (Free(c, typ), tab) =
   210       add_const_typ_table (const_with_typ thy (c,typ), tab) 
   211   | add_term_consts_typs_rm thy (t $ u, tab) =
   212       add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab))
   213   | add_term_consts_typs_rm thy (Abs(_,_,t), tab) = add_term_consts_typs_rm thy (t, tab)
   214   | add_term_consts_typs_rm thy (_, tab) = tab;
   215 
   216 (*The empty list here indicates that the constant is being ignored*)
   217 fun add_standard_const (s,tab) = Symtab.update (s,[]) tab;
   218 
   219 val null_const_tab : const_typ list list Symtab.table = 
   220     foldl add_standard_const Symtab.empty standard_consts;
   221 
   222 fun get_goal_consts_typs thy = foldl (add_term_consts_typs_rm thy) null_const_tab;
   223 
   224 (*Inserts a dummy "constant" referring to the theory name, so that relevance
   225   takes the given theory into account.*)
   226 fun const_prop_of th =
   227  if !theory_const then
   228   let val name = Context.theory_name (theory_of_thm th)
   229       val t = Const (name ^ ". 1", HOLogic.boolT)
   230   in  t $ prop_of th  end
   231  else prop_of th;
   232 
   233 (**** Constant / Type Frequencies ****)
   234 
   235 (*A two-dimensional symbol table counts frequencies of constants. It's keyed first by
   236   constant name and second by its list of type instantiations. For the latter, we need
   237   a linear ordering on type const_typ list.*)
   238   
   239 local
   240 
   241 fun cons_nr CTVar = 0
   242   | cons_nr (CType _) = 1;
   243 
   244 in
   245 
   246 fun const_typ_ord TU =
   247   case TU of
   248     (CType (a, Ts), CType (b, Us)) =>
   249       (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord)
   250   | (T, U) => int_ord (cons_nr T, cons_nr U);
   251 
   252 end;
   253 
   254 structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord);
   255 
   256 fun count_axiom_consts thy ((thm,_), tab) = 
   257   let fun count_const (a, T, tab) =
   258 	let val (c, cts) = const_with_typ thy (a,T)
   259 	in  (*Two-dimensional table update. Constant maps to types maps to count.*)
   260 	    Symtab.map_default (c, CTtab.empty) 
   261 	                       (CTtab.map_default (cts,0) (fn n => n+1)) tab
   262 	end
   263       fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab)
   264 	| count_term_consts (Free(a,T), tab) = count_const(a,T,tab)
   265 	| count_term_consts (t $ u, tab) =
   266 	    count_term_consts (t, count_term_consts (u, tab))
   267 	| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
   268 	| count_term_consts (_, tab) = tab
   269   in  count_term_consts (const_prop_of thm, tab)  end;
   270 
   271 
   272 (**** Actual Filtering Code ****)
   273 
   274 (*The frequency of a constant is the sum of those of all instances of its type.*)
   275 fun const_frequency ctab (c, cts) =
   276   let val pairs = CTtab.dest (the (Symtab.lookup ctab c))
   277       fun add ((cts',m), n) = if match_types cts cts' then m+n else n
   278   in  List.foldl add 0 pairs  end;
   279 
   280 (*Add in a constant's weight, as determined by its frequency.*)
   281 fun add_ct_weight ctab ((c,T), w) =
   282   w + !weight_fn (real (const_frequency ctab (c,T)));
   283 
   284 (*Relevant constants are weighted according to frequency, 
   285   but irrelevant constants are simply counted. Otherwise, Skolem functions,
   286   which are rare, would harm a clause's chances of being picked.*)
   287 fun clause_weight ctab gctyps consts_typs =
   288     let val rel = filter (uni_mem gctyps) consts_typs
   289         val rel_weight = List.foldl (add_ct_weight ctab) 0.0 rel
   290     in
   291 	rel_weight / (rel_weight + real (length consts_typs - length rel))
   292     end;
   293     
   294 (*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
   295 fun add_expand_pairs (x,ys) xys = foldl (fn (y,acc) => (x,y)::acc) xys ys;
   296 
   297 fun consts_typs_of_term thy t = 
   298   let val tab = add_term_consts_typs_rm thy (t, null_const_tab)
   299   in  Symtab.fold add_expand_pairs tab []  end;
   300 
   301 fun pair_consts_typs_axiom thy (thm,name) =
   302     ((thm,name), (consts_typs_of_term thy (const_prop_of thm)));
   303 
   304 exception ConstFree;
   305 fun dest_ConstFree (Const aT) = aT
   306   | dest_ConstFree (Free aT) = aT
   307   | dest_ConstFree _ = raise ConstFree;
   308 
   309 (*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
   310 fun defines thy (thm,(name,n)) gctypes =
   311     let val tm = prop_of thm
   312 	fun defs lhs rhs =
   313             let val (rator,args) = strip_comb lhs
   314 		val ct = const_with_typ thy (dest_ConstFree rator)
   315             in  forall is_Var args andalso uni_mem gctypes ct andalso
   316                 Term.add_vars rhs [] subset Term.add_vars lhs []
   317             end
   318 	    handle ConstFree => false
   319     in    
   320 	case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) => 
   321 		   defs lhs rhs andalso
   322 		   (Output.debug (fn () => "Definition found: " ^ name ^ "_" ^ Int.toString n); true)
   323 		 | _ => false
   324     end;
   325 
   326 type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list);
   327        
   328 (*For a reverse sort, putting the largest values first.*)
   329 fun compare_pairs ((_,w1),(_,w2)) = Real.compare (w2,w1);
   330 
   331 (*Limit the number of new clauses, to prevent runaway acceptance.*)
   332 fun take_best (newpairs : (annotd_cls*real) list) =
   333   let val nnew = length newpairs
   334   in
   335     if nnew <= !max_new then (map #1 newpairs, [])
   336     else 
   337       let val cls = sort compare_pairs newpairs
   338           val accepted = List.take (cls, !max_new)
   339       in
   340         Output.debug (fn () => ("Number of candidates, " ^ Int.toString nnew ^ 
   341 		       ", exceeds the limit of " ^ Int.toString (!max_new)));
   342         Output.debug (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
   343         Output.debug (fn () => "Actually passed: " ^
   344           space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
   345 
   346 	(map #1 accepted, map #1 (List.drop (cls, !max_new)))
   347       end
   348   end;
   349 
   350 fun relevant_clauses thy ctab p rel_consts =
   351   let fun relevant ([],_) [] = [] : (thm * (string * int)) list  (*Nothing added this iteration*)
   352 	| relevant (newpairs,rejects) [] =
   353 	    let val (newrels,more_rejects) = take_best newpairs
   354 		val new_consts = List.concat (map #2 newrels)
   355 		val rel_consts' = foldl add_const_typ_table rel_consts new_consts
   356 		val newp = p + (1.0-p) / !convergence
   357 	    in
   358               Output.debug (fn () => ("relevant this iteration: " ^ Int.toString (length newrels)));
   359 	       (map #1 newrels) @ 
   360 	       (relevant_clauses thy ctab newp rel_consts' (more_rejects@rejects))
   361 	    end
   362 	| relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) =
   363 	    let val weight = clause_weight ctab rel_consts consts_typs
   364 	    in
   365 	      if p <= weight orelse (!follow_defs andalso defines thy clsthm rel_consts)
   366 	      then (Output.debug (fn () => (name ^ " clause " ^ Int.toString n ^ 
   367 	                                    " passes: " ^ Real.toString weight));
   368 	            relevant ((ax,weight)::newrels, rejects) axs)
   369 	      else relevant (newrels, ax::rejects) axs
   370 	    end
   371     in  Output.debug (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
   372         relevant ([],[]) 
   373     end;
   374 	
   375 fun relevance_filter thy axioms goals = 
   376  if !run_relevance_filter andalso !pass_mark >= 0.1
   377  then
   378   let val _ = Output.debug (fn () => "Start of relevance filtering");
   379       val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms
   380       val goal_const_tab = get_goal_consts_typs thy goals
   381       val _ = Output.debug (fn () => ("Initial constants: " ^
   382                                  space_implode ", " (Symtab.keys goal_const_tab)));
   383       val rels = relevant_clauses thy const_tab (!pass_mark) 
   384                    goal_const_tab  (map (pair_consts_typs_axiom thy) axioms)
   385   in
   386       Output.debug (fn () => ("Total relevant: " ^ Int.toString (length rels)));
   387       rels
   388   end
   389  else axioms;
   390 
   391 (***************************************************************)
   392 (* Retrieving and filtering lemmas                             *)
   393 (***************************************************************)
   394 
   395 (*** white list and black list of lemmas ***)
   396 
   397 (*The rule subsetI is frequently omitted by the relevance filter. This could be theory data
   398   or identified with ATPset (which however is too big currently)*)
   399 val whitelist = [subsetI];
   400 
   401 (*** retrieve lemmas from clasimpset and atpset, may filter them ***)
   402 
   403 (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
   404 
   405 fun setinsert (x,s) = Symtab.update (x,()) s;
   406 
   407 (*Reject theorems with names like "List.filter.filter_list_def" or
   408   "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
   409 fun is_package_def a =
   410   let val names = NameSpace.explode a
   411   in
   412      length names > 2 andalso
   413      not (hd names = "local") andalso
   414      String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a
   415   end;
   416 
   417 (** a hash function from Term.term to int, and also a hash table **)
   418 val xor_words = List.foldl Word.xorb 0w0;
   419 
   420 fun hashw_term ((Const(c,_)), w) = Polyhash.hashw_string (c,w)
   421   | hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w)
   422   | hashw_term ((Var(_,_)), w) = w
   423   | hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w)
   424   | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
   425   | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));
   426 
   427 fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0))
   428   | hash_literal P = hashw_term(P,0w0);
   429 
   430 fun hash_term t = Word.toIntX (xor_words (map hash_literal (HOLogic.disjuncts (strip_Trueprop t))));
   431 
   432 fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
   433 
   434 exception HASH_CLAUSE;
   435 
   436 (*Create a hash table for clauses, of the given size*)
   437 fun mk_clause_table n =
   438       Polyhash.mkTable (hash_term o prop_of, equal_thm)
   439                        (n, HASH_CLAUSE);
   440 
   441 (*Use a hash table to eliminate duplicates from xs. Argument is a list of
   442   (thm * (string * int)) tuples. The theorems are hashed into the table. *)
   443 fun make_unique xs =
   444   let val ht = mk_clause_table 7000
   445   in
   446       Output.debug (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
   447       app (ignore o Polyhash.peekInsert ht) xs;
   448       Polyhash.listItems ht
   449   end;
   450 
   451 (*Remove existing axiom clauses from the conjecture clauses, as this can dramatically
   452   boost an ATP's performance (for some reason)*)
   453 fun subtract_cls c_clauses ax_clauses =
   454   let val ht = mk_clause_table 2200
   455       fun known x = isSome (Polyhash.peek ht x)
   456   in
   457       app (ignore o Polyhash.peekInsert ht) ax_clauses;
   458       filter (not o known) c_clauses
   459   end;
   460 
   461 fun all_valid_thms ctxt =
   462   let
   463     fun blacklisted s = !run_blacklist_filter andalso is_package_def s
   464 
   465     fun extern_valid space (name, ths) =
   466       let
   467         val is_valid = ProofContext.valid_thms ctxt;
   468         val xname = NameSpace.extern space name;
   469       in
   470         if blacklisted name then I
   471         else if is_valid (xname, ths) then cons (xname, filter_out ResAxioms.bad_for_atp ths)
   472         else if is_valid (name, ths) then cons (name, filter_out ResAxioms.bad_for_atp ths)
   473         else I
   474       end;
   475     val thy = ProofContext.theory_of ctxt;
   476     val all_thys = thy :: Theory.ancestors_of thy;
   477 
   478     val local_facts = ProofContext.facts_of ctxt;
   479 
   480     fun dest_valid (space, tab) = Symtab.fold (extern_valid space) tab [];
   481   in
   482     maps (dest_valid o PureThy.theorems_of) all_thys @
   483     fold (extern_valid (Facts.space_of local_facts)) (Facts.dest_table local_facts) []
   484   end;
   485 
   486 fun multi_name a (th, (n,pairs)) =
   487   (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs)
   488 
   489 fun add_single_names ((a, []), pairs) = pairs
   490   | add_single_names ((a, [th]), pairs) = (a,th)::pairs
   491   | add_single_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
   492 
   493 (*Ignore blacklisted basenames*)
   494 fun add_multi_names ((a, ths), pairs) =
   495   if (Sign.base_name a) mem_string ResAxioms.multi_base_blacklist  then pairs
   496   else add_single_names ((a, ths), pairs);
   497 
   498 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
   499 
   500 (*The single theorems go BEFORE the multiple ones. Blacklist is applied to all.*)
   501 fun name_thm_pairs ctxt =
   502   let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
   503       val ht = mk_clause_table 900   (*ht for blacklisted theorems*)
   504       fun blacklisted x = !run_blacklist_filter andalso isSome (Polyhash.peek ht x)
   505   in
   506       app (fn th => ignore (Polyhash.peekInsert ht (th,()))) (ResBlacklist.get ctxt);
   507       filter (not o blacklisted o #2)
   508         (foldl add_single_names (foldl add_multi_names [] mults) singles)
   509   end;
   510 
   511 fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false)
   512   | check_named (_,th) = true;
   513 
   514 fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ string_of_thm th);
   515 
   516 (* get lemmas from claset, simpset, atpset and extra supplied rules *)
   517 fun get_clasimp_atp_lemmas ctxt user_thms =
   518   let val included_thms =
   519         if !include_all
   520         then (tap (fn ths => Output.debug
   521                      (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
   522                   (name_thm_pairs ctxt))
   523         else
   524         let val claset_thms =
   525                 if !include_claset then ResAxioms.claset_rules_of ctxt
   526                 else []
   527             val simpset_thms =
   528                 if !include_simpset then ResAxioms.simpset_rules_of ctxt
   529                 else []
   530             val atpset_thms =
   531                 if !include_atpset then ResAxioms.atpset_rules_of ctxt
   532                 else []
   533             val _ = (Output.debug (fn () => "ATP theorems: ");  app display_thm atpset_thms)
   534         in  claset_thms @ simpset_thms @ atpset_thms  end
   535       val user_rules = filter check_named
   536                          (map ResAxioms.pairname
   537                            (if null user_thms then whitelist else user_thms))
   538   in
   539       (filter check_named included_thms, user_rules)
   540   end;
   541 
   542 (***************************************************************)
   543 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
   544 (***************************************************************)
   545 
   546 fun add_classes (sorts, cset) = foldl setinsert cset (List.concat sorts);
   547 
   548 (*Remove this trivial type class*)
   549 fun delete_type cset = Symtab.delete_safe "HOL.type" cset;
   550 
   551 fun tvar_classes_of_terms ts =
   552   let val sorts_list = map (map #2 o term_tvars) ts
   553   in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
   554 
   555 fun tfree_classes_of_terms ts =
   556   let val sorts_list = map (map #2 o term_tfrees) ts
   557   in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
   558 
   559 (*fold type constructors*)
   560 fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
   561   | fold_type_consts f T x = x;
   562 
   563 val add_type_consts_in_type = fold_type_consts setinsert;
   564 
   565 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
   566 fun add_type_consts_in_term thy =
   567   let val const_typargs = Sign.const_typargs thy
   568       fun add_tcs (Const cT) x = fold add_type_consts_in_type (const_typargs cT) x
   569         | add_tcs (Abs (_, T, u)) x = add_tcs u x
   570         | add_tcs (t $ u) x = add_tcs t (add_tcs u x)
   571         | add_tcs _ x = x
   572   in  add_tcs  end
   573 
   574 fun type_consts_of_terms thy ts =
   575   Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
   576 
   577 
   578 (***************************************************************)
   579 (* ATP invocation methods setup                                *)
   580 (***************************************************************)
   581 
   582 fun cnf_hyps_thms ctxt =
   583     let val ths = Assumption.prems_of ctxt
   584     in fold (fold (insert Thm.eq_thm) o ResAxioms.cnf_axiom) ths [] end;
   585 
   586 (*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
   587 datatype mode = Auto | Fol | Hol;
   588 
   589 val linkup_logic_mode = ref Auto;
   590 
   591 (*Ensures that no higher-order theorems "leak out"*)
   592 fun restrict_to_logic thy true cls = filter (Meson.is_fol_term thy o prop_of o fst) cls
   593   | restrict_to_logic thy false cls = cls;
   594 
   595 (**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****)
   596 
   597 (** Too general means, positive equality literal with a variable X as one operand,
   598   when X does not occur properly in the other operand. This rules out clearly
   599   inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **)
   600 
   601 fun occurs ix =
   602     let fun occ(Var (jx,_)) = (ix=jx)
   603           | occ(t1$t2)      = occ t1 orelse occ t2
   604           | occ(Abs(_,_,t)) = occ t
   605           | occ _           = false
   606     in occ end;
   607 
   608 fun is_recordtype T = not (null (RecordPackage.dest_recTs T));
   609 
   610 (*Unwanted equalities include
   611   (1) those between a variable that does not properly occur in the second operand,
   612   (2) those between a variable and a record, since these seem to be prolific "cases" thms
   613 *)
   614 fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T
   615   | too_general_eqterms _ = false;
   616 
   617 fun too_general_equality (Const ("op =", _) $ x $ y) =
   618       too_general_eqterms (x,y) orelse too_general_eqterms(y,x)
   619   | too_general_equality _ = false;
   620 
   621 (* tautologous? *)
   622 fun is_taut (Const ("Trueprop", _) $ Const ("True", _)) = true
   623   | is_taut _ = false;
   624 
   625 (*True if the term contains a variable whose (atomic) type is in the given list.*)
   626 fun has_typed_var tycons =
   627   let fun var_tycon (Var (_, Type(a,_))) = a mem_string tycons
   628         | var_tycon _ = false
   629   in  exists var_tycon o term_vars  end;
   630 
   631 (*Clauses are forbidden to contain variables of these types. The typical reason is that
   632   they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=().
   633   The resulting clause will have no type constraint, yielding false proofs. Even "bool"
   634   leads to many unsound proofs, though (obviously) only for higher-order problems.*)
   635 val unwanted_types = ["Product_Type.unit","bool"];
   636 
   637 fun unwanted t =
   638   is_taut t orelse has_typed_var unwanted_types t orelse
   639   forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t));
   640 
   641 (*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
   642   likely to lead to unsound proofs.*)
   643 fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
   644 
   645 (*Called by the oracle-based methods declared in res_atp_methods.ML*)
   646 fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
   647     let val conj_cls = Meson.make_clauses conjectures
   648                          |> map ResAxioms.combinators |> Meson.finish_cnf
   649         val hyp_cls = cnf_hyps_thms ctxt
   650         val goal_cls = conj_cls@hyp_cls
   651         val goal_tms = map prop_of goal_cls
   652         val thy = ProofContext.theory_of ctxt
   653         val isFO = case mode of
   654                             Auto => forall (Meson.is_fol_term thy) goal_tms
   655                           | Fol => true
   656                           | Hol => false
   657         val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
   658         val cla_simp_atp_clauses = included_thms
   659                                      |> ResAxioms.cnf_rules_pairs |> make_unique
   660                                      |> restrict_to_logic thy isFO
   661                                      |> remove_unwanted_clauses
   662         val user_cls = ResAxioms.cnf_rules_pairs user_rules
   663         val axclauses = make_unique (user_cls @ relevance_filter thy cla_simp_atp_clauses goal_tms)
   664         val subs = tfree_classes_of_terms goal_tms
   665         and axtms = map (prop_of o #1) axclauses
   666         val supers = tvar_classes_of_terms axtms
   667         and tycons = type_consts_of_terms thy (goal_tms@axtms)
   668         (*TFrees in conjecture clauses; TVars in axiom clauses*)
   669         val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
   670         val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   671         val writer = if dfg then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file
   672         and file = atp_input_file()
   673         and user_lemmas_names = map #1 user_rules
   674     in
   675         writer thy isFO goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
   676         Output.debug (fn () => "Writing to " ^ file);
   677         file
   678     end;
   679 
   680 
   681 (**** remove tmp files ****)
   682 fun cond_rm_tmp file =
   683     if !Output.debugging orelse !destdir <> ""
   684     then Output.debug (fn () => "ATP input kept...")
   685     else OS.FileSys.remove file;
   686 
   687 
   688 (***************************************************************)
   689 (* automatic ATP invocation                                    *)
   690 (***************************************************************)
   691 
   692 (* call prover with settings and problem file for the current subgoal *)
   693 fun watcher_call_provers files (childin, childout, pid) =
   694   let val time = Int.toString (!time_limit)
   695       fun make_atp_list [] = []
   696 	| make_atp_list (file::files) =
   697 	   (Output.debug (fn () => "problem file in watcher_call_provers is " ^ file);
   698 	    (*options are separated by Watcher.setting_sep, currently #"%"*)
   699 	    case !prover of
   700 		Recon.SPASS =>
   701 		  let val spass = helper_path "SPASS_HOME" "SPASS"
   702 		      val sopts =
   703        "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
   704 		  in  ("spass", spass, sopts, file) :: make_atp_list files  end
   705 	      | Recon.Vampire =>
   706 		  let val vampire = helper_path "VAMPIRE_HOME" "vampire"
   707 		      val vopts = "--output_syntax tptp%--mode casc%-t " ^ time
   708 		  in  ("vampire", vampire, vopts, file) :: make_atp_list files  end
   709 	      | Recon.E =>
   710 		  let val eproof = helper_path "E_HOME" "eproof"
   711 		      val eopts = "--tstp-in%--tstp-out%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time
   712 		  in  ("E", eproof, eopts, file) :: make_atp_list files  end)
   713   in
   714     Watcher.callResProvers(childout, make_atp_list files);
   715     Output.debug (fn () => "Sent commands to watcher!")
   716   end
   717 
   718 (*For debugging the generated set of theorem names*)
   719 fun trace_vector fname =
   720   let val path = Path.explode (fname ^ "_thm_names")
   721   in  Vector.app (File.append path o (fn s => s ^ "\n"))  end;
   722 
   723 (*We write out problem files for each subgoal. Argument probfile generates filenames,
   724   and allows the suppression of the suffix "_1" in problem-generation mode.
   725   FIXME: does not cope with &&, and it isn't easy because one could have multiple
   726   subgoals, each involving &&.*)
   727 fun write_problem_files probfile (ctxt, chain_ths, th) =
   728   let val goals = Library.take (!max_sledgehammers, Thm.prems_of th)  (*raises no exception*)
   729       val _ = Output.debug (fn () => "number of subgoals = " ^ Int.toString (length goals))
   730       val thy = ProofContext.theory_of ctxt
   731       fun get_neg_subgoals [] _ = []
   732         | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) ::
   733                                          get_neg_subgoals gls (n+1)
   734       val goal_cls = get_neg_subgoals goals 1
   735                      handle THM ("assume: variables", _, _) => 
   736                        error "Sledgehammer: Goal contains type variables (TVars)"                       
   737       val isFO = case !linkup_logic_mode of
   738 			  Auto => forall (Meson.is_fol_term thy) (map prop_of (List.concat goal_cls))
   739 			| Fol => true
   740 			| Hol => false
   741       val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths
   742       val included_cls = included_thms |> ResAxioms.cnf_rules_pairs |> make_unique
   743                                        |> restrict_to_logic thy isFO
   744                                        |> remove_unwanted_clauses
   745       val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls))
   746       val white_cls = ResAxioms.cnf_rules_pairs white_thms
   747       (*clauses relevant to goal gl*)
   748       val axcls_list = map (fn ngcls => white_cls @ relevance_filter thy included_cls (map prop_of ngcls)) goal_cls
   749       val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls)))
   750                   axcls_list
   751       val writer = if !prover = Recon.SPASS then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file
   752       fun write_all [] [] _ = []
   753         | write_all (ccls::ccls_list) (axcls::axcls_list) k =
   754             let val fname = probfile k
   755                 val _ = Output.debug (fn () => "About to write file " ^ fname)
   756                 val axcls = make_unique axcls
   757                 val _ = Output.debug (fn () => "Conjecture Clauses (before duplicate removal)")
   758                 val _ = app (fn th => Output.debug (fn _ => string_of_thm th)) ccls
   759                 val ccls = subtract_cls ccls axcls
   760                 val _ = Output.debug (fn () => "Conjecture Clauses (AFTER duplicate removal)")
   761                 val _ = app (fn th => Output.debug (fn _ => string_of_thm th)) ccls
   762                 val ccltms = map prop_of ccls
   763                 and axtms = map (prop_of o #1) axcls
   764                 val subs = tfree_classes_of_terms ccltms
   765                 and supers = tvar_classes_of_terms axtms
   766                 and tycons = type_consts_of_terms thy (ccltms@axtms)
   767                 (*TFrees in conjecture clauses; TVars in axiom clauses*)
   768                 val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
   769                 val _ = Output.debug (fn () => "arity clauses = " ^ Int.toString (length arity_clauses))
   770                 val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   771                 val _ = Output.debug (fn () => "classrel clauses = " ^ Int.toString (length classrel_clauses))
   772                 val clnames = writer thy isFO ccls fname (axcls,classrel_clauses,arity_clauses) []
   773                 val thm_names = Vector.fromList clnames
   774                 val _ = if !Output.debugging then trace_vector fname thm_names else ()
   775             in  (thm_names,fname) :: write_all ccls_list axcls_list (k+1)  end
   776       val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
   777   in
   778       (filenames, thm_names_list)
   779   end;
   780 
   781 val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream *
   782                                     Posix.Process.pid * string list) option);
   783 
   784 fun kill_last_watcher () =
   785     (case !last_watcher_pid of
   786          NONE => ()
   787        | SOME (_, _, pid, files) =>
   788           (Output.debug (fn () => "Killing old watcher, pid = " ^ string_of_pid pid);
   789            Watcher.killWatcher pid;
   790            ignore (map (try cond_rm_tmp) files)))
   791      handle OS.SysErr _ => Output.debug (fn () => "Attempt to kill watcher failed");
   792 
   793 (*writes out the current problems and calls ATPs*)
   794 fun isar_atp (ctxt, chain_ths, th) =
   795   if Thm.no_prems th then warning "Nothing to prove"
   796   else
   797     let
   798       val _ = kill_last_watcher()
   799       val (files,thm_names_list) = write_problem_files prob_pathname (ctxt, chain_ths, th)
   800       val (childin, childout, pid) = Watcher.createWatcher (ctxt, th, thm_names_list)
   801     in
   802       last_watcher_pid := SOME (childin, childout, pid, files);
   803       Output.debug (fn () => "problem files: " ^ space_implode ", " files);
   804       Output.debug (fn () => "pid: " ^ string_of_pid pid);
   805       watcher_call_provers files (childin, childout, pid)
   806     end;
   807 
   808 (*For ML scripts, and primarily, for debugging*)
   809 fun callatp () =
   810   let val th = topthm()
   811       val ctxt = ProofContext.init (theory_of_thm th)
   812   in  isar_atp (ctxt, [], th)  end;
   813 
   814 val isar_atp_writeonly = PrintMode.setmp []
   815       (fn (ctxt, chain_ths, th) =>
   816        if Thm.no_prems th then warning "Nothing to prove"
   817        else
   818          let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix
   819                             else prob_pathname
   820          in ignore (write_problem_files probfile (ctxt, chain_ths, th)) end);
   821 
   822 
   823 (** the Isar toplevel command **)
   824 
   825 fun sledgehammer state =
   826   let
   827     val (ctxt, (chain_ths, goal)) = Proof.get_goal (Toplevel.proof_of state)
   828     val chain_ths = map (PureThy.put_name_hint Recon.chained_hint) chain_ths
   829                     (*Mark the chained theorems to keep them out of metis calls;
   830                       their original "name hints" may be bad anyway.*)
   831     val thy = ProofContext.theory_of ctxt
   832   in
   833     if exists_type ResAxioms.type_has_empty_sort (prop_of goal)  
   834     then error "Proof state contains the empty sort" else ();
   835     Output.debug (fn () => "subgoals in isar_atp:\n" ^
   836                   Syntax.string_of_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal)));
   837     Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
   838     app (fn th => Output.debug (fn _ => "chained: " ^ string_of_thm th)) chain_ths;
   839     if !time_limit > 0 then isar_atp (ctxt, chain_ths, goal)
   840     else (warning ("Writing problem file only: " ^ !problem_name);
   841           isar_atp_writeonly (ctxt, chain_ths, goal))
   842   end;
   843 
   844 val _ =
   845   OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag
   846     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer));
   847 
   848 end;