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