src/HOL/Tools/res_atp.ML
author wenzelm
Tue Apr 15 22:09:23 2008 +0200 (2008-04-15)
changeset 26675 fba93ce71435
parent 26662 39483503705f
child 26691 520c99e0b9a0
permissions -rw-r--r--
all_valid_thms: use new facts tables;
     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 valid_facts facts =
   462   Facts.dest_table facts
   463   |> filter_out (fn (name, _) => !run_blacklist_filter andalso is_package_def name)
   464   |> map (apfst (Facts.extern facts))
   465   |> filter_out (NameSpace.is_hidden o #1)
   466   |> map (apsnd (filter_out ResAxioms.bad_for_atp));
   467 
   468 fun all_valid_thms ctxt =
   469   let
   470     val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
   471     val local_facts = ProofContext.facts_of ctxt;
   472   in valid_facts global_facts @ valid_facts local_facts end;
   473 
   474 fun multi_name a (th, (n,pairs)) =
   475   (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs)
   476 
   477 fun add_single_names ((a, []), pairs) = pairs
   478   | add_single_names ((a, [th]), pairs) = (a,th)::pairs
   479   | add_single_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
   480 
   481 (*Ignore blacklisted basenames*)
   482 fun add_multi_names ((a, ths), pairs) =
   483   if (Sign.base_name a) mem_string ResAxioms.multi_base_blacklist  then pairs
   484   else add_single_names ((a, ths), pairs);
   485 
   486 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
   487 
   488 (*The single theorems go BEFORE the multiple ones. Blacklist is applied to all.*)
   489 fun name_thm_pairs ctxt =
   490   let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
   491       val ht = mk_clause_table 900   (*ht for blacklisted theorems*)
   492       fun blacklisted x = !run_blacklist_filter andalso isSome (Polyhash.peek ht x)
   493   in
   494       app (fn th => ignore (Polyhash.peekInsert ht (th,()))) (ResBlacklist.get ctxt);
   495       filter (not o blacklisted o #2)
   496         (foldl add_single_names (foldl add_multi_names [] mults) singles)
   497   end;
   498 
   499 fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false)
   500   | check_named (_,th) = true;
   501 
   502 fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ string_of_thm th);
   503 
   504 (* get lemmas from claset, simpset, atpset and extra supplied rules *)
   505 fun get_clasimp_atp_lemmas ctxt user_thms =
   506   let val included_thms =
   507         if !include_all
   508         then (tap (fn ths => Output.debug
   509                      (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
   510                   (name_thm_pairs ctxt))
   511         else
   512         let val claset_thms =
   513                 if !include_claset then ResAxioms.claset_rules_of ctxt
   514                 else []
   515             val simpset_thms =
   516                 if !include_simpset then ResAxioms.simpset_rules_of ctxt
   517                 else []
   518             val atpset_thms =
   519                 if !include_atpset then ResAxioms.atpset_rules_of ctxt
   520                 else []
   521             val _ = (Output.debug (fn () => "ATP theorems: ");  app display_thm atpset_thms)
   522         in  claset_thms @ simpset_thms @ atpset_thms  end
   523       val user_rules = filter check_named
   524                          (map ResAxioms.pairname
   525                            (if null user_thms then whitelist else user_thms))
   526   in
   527       (filter check_named included_thms, user_rules)
   528   end;
   529 
   530 (***************************************************************)
   531 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
   532 (***************************************************************)
   533 
   534 fun add_classes (sorts, cset) = foldl setinsert cset (List.concat sorts);
   535 
   536 (*Remove this trivial type class*)
   537 fun delete_type cset = Symtab.delete_safe "HOL.type" cset;
   538 
   539 fun tvar_classes_of_terms ts =
   540   let val sorts_list = map (map #2 o term_tvars) ts
   541   in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
   542 
   543 fun tfree_classes_of_terms ts =
   544   let val sorts_list = map (map #2 o term_tfrees) ts
   545   in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
   546 
   547 (*fold type constructors*)
   548 fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
   549   | fold_type_consts f T x = x;
   550 
   551 val add_type_consts_in_type = fold_type_consts setinsert;
   552 
   553 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
   554 fun add_type_consts_in_term thy =
   555   let val const_typargs = Sign.const_typargs thy
   556       fun add_tcs (Const cT) x = fold add_type_consts_in_type (const_typargs cT) x
   557         | add_tcs (Abs (_, T, u)) x = add_tcs u x
   558         | add_tcs (t $ u) x = add_tcs t (add_tcs u x)
   559         | add_tcs _ x = x
   560   in  add_tcs  end
   561 
   562 fun type_consts_of_terms thy ts =
   563   Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
   564 
   565 
   566 (***************************************************************)
   567 (* ATP invocation methods setup                                *)
   568 (***************************************************************)
   569 
   570 fun cnf_hyps_thms ctxt =
   571     let val ths = Assumption.prems_of ctxt
   572     in fold (fold (insert Thm.eq_thm) o ResAxioms.cnf_axiom) ths [] end;
   573 
   574 (*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
   575 datatype mode = Auto | Fol | Hol;
   576 
   577 val linkup_logic_mode = ref Auto;
   578 
   579 (*Ensures that no higher-order theorems "leak out"*)
   580 fun restrict_to_logic thy true cls = filter (Meson.is_fol_term thy o prop_of o fst) cls
   581   | restrict_to_logic thy false cls = cls;
   582 
   583 (**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****)
   584 
   585 (** Too general means, positive equality literal with a variable X as one operand,
   586   when X does not occur properly in the other operand. This rules out clearly
   587   inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **)
   588 
   589 fun occurs ix =
   590     let fun occ(Var (jx,_)) = (ix=jx)
   591           | occ(t1$t2)      = occ t1 orelse occ t2
   592           | occ(Abs(_,_,t)) = occ t
   593           | occ _           = false
   594     in occ end;
   595 
   596 fun is_recordtype T = not (null (RecordPackage.dest_recTs T));
   597 
   598 (*Unwanted equalities include
   599   (1) those between a variable that does not properly occur in the second operand,
   600   (2) those between a variable and a record, since these seem to be prolific "cases" thms
   601 *)
   602 fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T
   603   | too_general_eqterms _ = false;
   604 
   605 fun too_general_equality (Const ("op =", _) $ x $ y) =
   606       too_general_eqterms (x,y) orelse too_general_eqterms(y,x)
   607   | too_general_equality _ = false;
   608 
   609 (* tautologous? *)
   610 fun is_taut (Const ("Trueprop", _) $ Const ("True", _)) = true
   611   | is_taut _ = false;
   612 
   613 (*True if the term contains a variable whose (atomic) type is in the given list.*)
   614 fun has_typed_var tycons =
   615   let fun var_tycon (Var (_, Type(a,_))) = a mem_string tycons
   616         | var_tycon _ = false
   617   in  exists var_tycon o term_vars  end;
   618 
   619 (*Clauses are forbidden to contain variables of these types. The typical reason is that
   620   they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=().
   621   The resulting clause will have no type constraint, yielding false proofs. Even "bool"
   622   leads to many unsound proofs, though (obviously) only for higher-order problems.*)
   623 val unwanted_types = ["Product_Type.unit","bool"];
   624 
   625 fun unwanted t =
   626   is_taut t orelse has_typed_var unwanted_types t orelse
   627   forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t));
   628 
   629 (*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
   630   likely to lead to unsound proofs.*)
   631 fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
   632 
   633 (*Called by the oracle-based methods declared in res_atp_methods.ML*)
   634 fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
   635     let val conj_cls = Meson.make_clauses conjectures
   636                          |> map ResAxioms.combinators |> Meson.finish_cnf
   637         val hyp_cls = cnf_hyps_thms ctxt
   638         val goal_cls = conj_cls@hyp_cls
   639         val goal_tms = map prop_of goal_cls
   640         val thy = ProofContext.theory_of ctxt
   641         val isFO = case mode of
   642                             Auto => forall (Meson.is_fol_term thy) goal_tms
   643                           | Fol => true
   644                           | Hol => false
   645         val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
   646         val cla_simp_atp_clauses = included_thms
   647                                      |> ResAxioms.cnf_rules_pairs |> make_unique
   648                                      |> restrict_to_logic thy isFO
   649                                      |> remove_unwanted_clauses
   650         val user_cls = ResAxioms.cnf_rules_pairs user_rules
   651         val axclauses = make_unique (user_cls @ relevance_filter thy cla_simp_atp_clauses goal_tms)
   652         val subs = tfree_classes_of_terms goal_tms
   653         and axtms = map (prop_of o #1) axclauses
   654         val supers = tvar_classes_of_terms axtms
   655         and tycons = type_consts_of_terms thy (goal_tms@axtms)
   656         (*TFrees in conjecture clauses; TVars in axiom clauses*)
   657         val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
   658         val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   659         val writer = if dfg then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file
   660         and file = atp_input_file()
   661         and user_lemmas_names = map #1 user_rules
   662     in
   663         writer thy isFO goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
   664         Output.debug (fn () => "Writing to " ^ file);
   665         file
   666     end;
   667 
   668 
   669 (**** remove tmp files ****)
   670 fun cond_rm_tmp file =
   671     if !Output.debugging orelse !destdir <> ""
   672     then Output.debug (fn () => "ATP input kept...")
   673     else OS.FileSys.remove file;
   674 
   675 
   676 (***************************************************************)
   677 (* automatic ATP invocation                                    *)
   678 (***************************************************************)
   679 
   680 (* call prover with settings and problem file for the current subgoal *)
   681 fun watcher_call_provers files (childin, childout, pid) =
   682   let val time = Int.toString (!time_limit)
   683       fun make_atp_list [] = []
   684 	| make_atp_list (file::files) =
   685 	   (Output.debug (fn () => "problem file in watcher_call_provers is " ^ file);
   686 	    (*options are separated by Watcher.setting_sep, currently #"%"*)
   687 	    case !prover of
   688 		Recon.SPASS =>
   689 		  let val spass = helper_path "SPASS_HOME" "SPASS"
   690 		      val sopts =
   691        "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
   692 		  in  ("spass", spass, sopts, file) :: make_atp_list files  end
   693 	      | Recon.Vampire =>
   694 		  let val vampire = helper_path "VAMPIRE_HOME" "vampire"
   695 		      val vopts = "--output_syntax tptp%--mode casc%-t " ^ time
   696 		  in  ("vampire", vampire, vopts, file) :: make_atp_list files  end
   697 	      | Recon.E =>
   698 		  let val eproof = helper_path "E_HOME" "eproof"
   699 		      val eopts = "--tstp-in%--tstp-out%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time
   700 		  in  ("E", eproof, eopts, file) :: make_atp_list files  end)
   701   in
   702     Watcher.callResProvers(childout, make_atp_list files);
   703     Output.debug (fn () => "Sent commands to watcher!")
   704   end
   705 
   706 (*For debugging the generated set of theorem names*)
   707 fun trace_vector fname =
   708   let val path = Path.explode (fname ^ "_thm_names")
   709   in  Vector.app (File.append path o (fn s => s ^ "\n"))  end;
   710 
   711 (*We write out problem files for each subgoal. Argument probfile generates filenames,
   712   and allows the suppression of the suffix "_1" in problem-generation mode.
   713   FIXME: does not cope with &&, and it isn't easy because one could have multiple
   714   subgoals, each involving &&.*)
   715 fun write_problem_files probfile (ctxt, chain_ths, th) =
   716   let val goals = Library.take (!max_sledgehammers, Thm.prems_of th)  (*raises no exception*)
   717       val _ = Output.debug (fn () => "number of subgoals = " ^ Int.toString (length goals))
   718       val thy = ProofContext.theory_of ctxt
   719       fun get_neg_subgoals [] _ = []
   720         | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) ::
   721                                          get_neg_subgoals gls (n+1)
   722       val goal_cls = get_neg_subgoals goals 1
   723                      handle THM ("assume: variables", _, _) => 
   724                        error "Sledgehammer: Goal contains type variables (TVars)"                       
   725       val isFO = case !linkup_logic_mode of
   726 			  Auto => forall (Meson.is_fol_term thy) (map prop_of (List.concat goal_cls))
   727 			| Fol => true
   728 			| Hol => false
   729       val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths
   730       val included_cls = included_thms |> ResAxioms.cnf_rules_pairs |> make_unique
   731                                        |> restrict_to_logic thy isFO
   732                                        |> remove_unwanted_clauses
   733       val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls))
   734       val white_cls = ResAxioms.cnf_rules_pairs white_thms
   735       (*clauses relevant to goal gl*)
   736       val axcls_list = map (fn ngcls => white_cls @ relevance_filter thy included_cls (map prop_of ngcls)) goal_cls
   737       val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls)))
   738                   axcls_list
   739       val writer = if !prover = Recon.SPASS then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file
   740       fun write_all [] [] _ = []
   741         | write_all (ccls::ccls_list) (axcls::axcls_list) k =
   742             let val fname = probfile k
   743                 val _ = Output.debug (fn () => "About to write file " ^ fname)
   744                 val axcls = make_unique axcls
   745                 val _ = Output.debug (fn () => "Conjecture Clauses (before duplicate removal)")
   746                 val _ = app (fn th => Output.debug (fn _ => string_of_thm th)) ccls
   747                 val ccls = subtract_cls ccls axcls
   748                 val _ = Output.debug (fn () => "Conjecture Clauses (AFTER duplicate removal)")
   749                 val _ = app (fn th => Output.debug (fn _ => string_of_thm th)) ccls
   750                 val ccltms = map prop_of ccls
   751                 and axtms = map (prop_of o #1) axcls
   752                 val subs = tfree_classes_of_terms ccltms
   753                 and supers = tvar_classes_of_terms axtms
   754                 and tycons = type_consts_of_terms thy (ccltms@axtms)
   755                 (*TFrees in conjecture clauses; TVars in axiom clauses*)
   756                 val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
   757                 val _ = Output.debug (fn () => "arity clauses = " ^ Int.toString (length arity_clauses))
   758                 val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   759                 val _ = Output.debug (fn () => "classrel clauses = " ^ Int.toString (length classrel_clauses))
   760                 val clnames = writer thy isFO ccls fname (axcls,classrel_clauses,arity_clauses) []
   761                 val thm_names = Vector.fromList clnames
   762                 val _ = if !Output.debugging then trace_vector fname thm_names else ()
   763             in  (thm_names,fname) :: write_all ccls_list axcls_list (k+1)  end
   764       val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
   765   in
   766       (filenames, thm_names_list)
   767   end;
   768 
   769 val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream *
   770                                     Posix.Process.pid * string list) option);
   771 
   772 fun kill_last_watcher () =
   773     (case !last_watcher_pid of
   774          NONE => ()
   775        | SOME (_, _, pid, files) =>
   776           (Output.debug (fn () => "Killing old watcher, pid = " ^ string_of_pid pid);
   777            Watcher.killWatcher pid;
   778            ignore (map (try cond_rm_tmp) files)))
   779      handle OS.SysErr _ => Output.debug (fn () => "Attempt to kill watcher failed");
   780 
   781 (*writes out the current problems and calls ATPs*)
   782 fun isar_atp (ctxt, chain_ths, th) =
   783   if Thm.no_prems th then warning "Nothing to prove"
   784   else
   785     let
   786       val _ = kill_last_watcher()
   787       val (files,thm_names_list) = write_problem_files prob_pathname (ctxt, chain_ths, th)
   788       val (childin, childout, pid) = Watcher.createWatcher (ctxt, th, thm_names_list)
   789     in
   790       last_watcher_pid := SOME (childin, childout, pid, files);
   791       Output.debug (fn () => "problem files: " ^ space_implode ", " files);
   792       Output.debug (fn () => "pid: " ^ string_of_pid pid);
   793       watcher_call_provers files (childin, childout, pid)
   794     end;
   795 
   796 (*For ML scripts, and primarily, for debugging*)
   797 fun callatp () =
   798   let val th = topthm()
   799       val ctxt = ProofContext.init (theory_of_thm th)
   800   in  isar_atp (ctxt, [], th)  end;
   801 
   802 val isar_atp_writeonly = PrintMode.setmp []
   803       (fn (ctxt, chain_ths, th) =>
   804        if Thm.no_prems th then warning "Nothing to prove"
   805        else
   806          let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix
   807                             else prob_pathname
   808          in ignore (write_problem_files probfile (ctxt, chain_ths, th)) end);
   809 
   810 
   811 (** the Isar toplevel command **)
   812 
   813 fun sledgehammer state =
   814   let
   815     val (ctxt, (chain_ths, goal)) = Proof.get_goal (Toplevel.proof_of state)
   816     val chain_ths = map (PureThy.put_name_hint Recon.chained_hint) chain_ths
   817                     (*Mark the chained theorems to keep them out of metis calls;
   818                       their original "name hints" may be bad anyway.*)
   819     val thy = ProofContext.theory_of ctxt
   820   in
   821     if exists_type ResAxioms.type_has_empty_sort (prop_of goal)  
   822     then error "Proof state contains the empty sort" else ();
   823     Output.debug (fn () => "subgoals in isar_atp:\n" ^
   824                   Syntax.string_of_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal)));
   825     Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
   826     app (fn th => Output.debug (fn _ => "chained: " ^ string_of_thm th)) chain_ths;
   827     if !time_limit > 0 then isar_atp (ctxt, chain_ths, goal)
   828     else (warning ("Writing problem file only: " ^ !problem_name);
   829           isar_atp_writeonly (ctxt, chain_ths, goal))
   830   end;
   831 
   832 val _ =
   833   OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag
   834     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer));
   835 
   836 end;