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