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