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