src/HOL/Tools/res_atp.ML
author paulson
Thu Oct 04 12:32:58 2007 +0200 (2007-10-04)
changeset 24827 646bdc51eb7d
parent 24634 38db11874724
child 24854 0ebcd575d3c6
permissions -rw-r--r--
combinator translation
     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 val multi_base_blacklist =
   610   ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm"];
   611 
   612 (*Ignore blacklisted basenames*)
   613 fun add_multi_names ((a, ths), pairs) =
   614   if (Sign.base_name a) mem_string multi_base_blacklist  then pairs
   615   else add_single_names ((a, ths), pairs);
   616 
   617 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
   618 
   619 (*The single theorems go BEFORE the multiple ones. Blacklist is applied to all.*)
   620 fun name_thm_pairs ctxt =
   621   let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
   622       val ht = mk_clause_table 900   (*ht for blacklisted theorems*)
   623       fun blacklisted x = !run_blacklist_filter andalso isSome (Polyhash.peek ht x)
   624   in
   625       app (fn th => ignore (Polyhash.peekInsert ht (th,()))) (ResBlacklist.get ctxt);
   626       filter (not o blacklisted o #2)
   627         (foldl add_single_names (foldl add_multi_names [] mults) singles)
   628   end;
   629 
   630 fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false)
   631   | check_named (_,th) = true;
   632 
   633 fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ string_of_thm th);
   634 
   635 (* get lemmas from claset, simpset, atpset and extra supplied rules *)
   636 fun get_clasimp_atp_lemmas ctxt user_thms =
   637   let val included_thms =
   638         if !include_all
   639         then (tap (fn ths => Output.debug
   640                      (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
   641                   (name_thm_pairs ctxt))
   642         else
   643         let val claset_thms =
   644                 if !include_claset then ResAxioms.claset_rules_of ctxt
   645                 else []
   646             val simpset_thms =
   647                 if !include_simpset then ResAxioms.simpset_rules_of ctxt
   648                 else []
   649             val atpset_thms =
   650                 if !include_atpset then ResAxioms.atpset_rules_of ctxt
   651                 else []
   652             val _ = (Output.debug (fn () => "ATP theorems: ");  app display_thm atpset_thms)
   653         in  claset_thms @ simpset_thms @ atpset_thms  end
   654       val user_rules = filter check_named
   655                          (map ResAxioms.pairname
   656                            (if null user_thms then whitelist else user_thms))
   657   in
   658       (filter check_named included_thms, user_rules)
   659   end;
   660 
   661 (***************************************************************)
   662 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
   663 (***************************************************************)
   664 
   665 fun add_classes (sorts, cset) = foldl setinsert cset (List.concat sorts);
   666 
   667 (*Remove this trivial type class*)
   668 fun delete_type cset = Symtab.delete_safe "HOL.type" cset;
   669 
   670 fun tvar_classes_of_terms ts =
   671   let val sorts_list = map (map #2 o term_tvars) ts
   672   in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
   673 
   674 fun tfree_classes_of_terms ts =
   675   let val sorts_list = map (map #2 o term_tfrees) ts
   676   in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
   677 
   678 (*fold type constructors*)
   679 fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
   680   | fold_type_consts f T x = x;
   681 
   682 val add_type_consts_in_type = fold_type_consts setinsert;
   683 
   684 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
   685 fun add_type_consts_in_term thy =
   686   let val const_typargs = Sign.const_typargs thy
   687       fun add_tcs (Const cT) x = fold add_type_consts_in_type (const_typargs cT) x
   688         | add_tcs (Abs (_, T, u)) x = add_tcs u x
   689         | add_tcs (t $ u) x = add_tcs t (add_tcs u x)
   690         | add_tcs _ x = x
   691   in  add_tcs  end
   692 
   693 fun type_consts_of_terms thy ts =
   694   Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
   695 
   696 
   697 (***************************************************************)
   698 (* ATP invocation methods setup                                *)
   699 (***************************************************************)
   700 
   701 fun cnf_hyps_thms ctxt =
   702     let val ths = Assumption.prems_of ctxt
   703     in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end;
   704 
   705 (*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
   706 datatype mode = Auto | Fol | Hol;
   707 
   708 val linkup_logic_mode = ref Auto;
   709 
   710 (*Ensures that no higher-order theorems "leak out"*)
   711 fun restrict_to_logic thy logic cls =
   712   if is_fol_logic logic then filter (Meson.is_fol_term thy o prop_of o fst) cls
   713                         else cls;
   714 
   715 (**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****)
   716 
   717 (** Too general means, positive equality literal with a variable X as one operand,
   718   when X does not occur properly in the other operand. This rules out clearly
   719   inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **)
   720 
   721 fun occurs ix =
   722     let fun occ(Var (jx,_)) = (ix=jx)
   723           | occ(t1$t2)      = occ t1 orelse occ t2
   724           | occ(Abs(_,_,t)) = occ t
   725           | occ _           = false
   726     in occ end;
   727 
   728 fun is_recordtype T = not (null (RecordPackage.dest_recTs T));
   729 
   730 (*Unwanted equalities include
   731   (1) those between a variable that does not properly occur in the second operand,
   732   (2) those between a variable and a record, since these seem to be prolific "cases" thms
   733 *)
   734 fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T
   735   | too_general_eqterms _ = false;
   736 
   737 fun too_general_equality (Const ("op =", _) $ x $ y) =
   738       too_general_eqterms (x,y) orelse too_general_eqterms(y,x)
   739   | too_general_equality _ = false;
   740 
   741 (* tautologous? *)
   742 fun is_taut (Const ("Trueprop", _) $ Const ("True", _)) = true
   743   | is_taut _ = false;
   744 
   745 (*True if the term contains a variable whose (atomic) type is in the given list.*)
   746 fun has_typed_var tycons =
   747   let fun var_tycon (Var (_, Type(a,_))) = a mem_string tycons
   748         | var_tycon _ = false
   749   in  exists var_tycon o term_vars  end;
   750 
   751 (*Clauses are forbidden to contain variables of these types. The typical reason is that
   752   they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=().
   753   The resulting clause will have no type constraint, yielding false proofs. Even "bool"
   754   leads to many unsound proofs, though (obviously) only for higher-order problems.*)
   755 val unwanted_types = ["Product_Type.unit","bool"];
   756 
   757 fun unwanted t =
   758     is_taut t orelse has_typed_var unwanted_types t orelse
   759     forall too_general_equality (dest_disj t);
   760 
   761 (*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
   762   likely to lead to unsound proofs.*)
   763 fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
   764 
   765 fun tptp_writer thy logic = ResHolClause.tptp_write_file thy (logic=FOL);
   766 
   767 fun dfg_writer thy logic = ResHolClause.dfg_write_file thy (logic=FOL);
   768 
   769 (*Called by the oracle-based methods declared in res_atp_methods.ML*)
   770 fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
   771     let val conj_cls = Meson.make_clauses conjectures
   772                          |> map ResAxioms.combinators |> Meson.finish_cnf
   773         val hyp_cls = cnf_hyps_thms ctxt
   774         val goal_cls = conj_cls@hyp_cls
   775         val goal_tms = map prop_of goal_cls
   776         val thy = ProofContext.theory_of ctxt
   777         val logic = case mode of
   778                             Auto => problem_logic_goals [goal_tms]
   779                           | Fol => FOL
   780                           | Hol => HOL
   781         val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
   782         val cla_simp_atp_clauses = included_thms
   783                                      |> ResAxioms.cnf_rules_pairs |> make_unique
   784                                      |> restrict_to_logic thy logic
   785                                      |> remove_unwanted_clauses
   786         val user_cls = ResAxioms.cnf_rules_pairs user_rules
   787         val axclauses = make_unique (user_cls @ relevance_filter thy cla_simp_atp_clauses goal_tms)
   788         val subs = tfree_classes_of_terms goal_tms
   789         and axtms = map (prop_of o #1) axclauses
   790         val supers = tvar_classes_of_terms axtms
   791         and tycons = type_consts_of_terms thy (goal_tms@axtms)
   792         (*TFrees in conjecture clauses; TVars in axiom clauses*)
   793         val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
   794         val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   795         val writer = if dfg then dfg_writer else tptp_writer
   796         and file = atp_input_file()
   797         and user_lemmas_names = map #1 user_rules
   798     in
   799         writer thy logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
   800         Output.debug (fn () => "Writing to " ^ file);
   801         file
   802     end;
   803 
   804 
   805 (**** remove tmp files ****)
   806 fun cond_rm_tmp file =
   807     if !Output.debugging orelse !destdir <> ""
   808     then Output.debug (fn () => "ATP input kept...")
   809     else OS.FileSys.remove file;
   810 
   811 
   812 (***************************************************************)
   813 (* automatic ATP invocation                                    *)
   814 (***************************************************************)
   815 
   816 (* call prover with settings and problem file for the current subgoal *)
   817 fun watcher_call_provers sign sg_terms (childin, childout, pid) =
   818   let
   819     fun make_atp_list [] n = []
   820       | make_atp_list (sg_term::xs) n =
   821           let
   822             val probfile = prob_pathname n
   823             val time = Int.toString (!time_limit)
   824           in
   825             Output.debug (fn () => "problem file in watcher_call_provers is " ^ probfile);
   826             (*options are separated by Watcher.setting_sep, currently #"%"*)
   827             case !prover of
   828                 Recon.SPASS =>
   829 		  let val spass = helper_path "SPASS_HOME" "SPASS"
   830 		      val sopts =
   831        "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
   832 		  in
   833 		      ("spass", spass, sopts, probfile) :: make_atp_list xs (n+1)
   834 		  end
   835               | Recon.Vampire =>
   836 		  let val vampire = helper_path "VAMPIRE_HOME" "vampire"
   837 		      val vopts = "--output_syntax tptp%--mode casc%-t " ^ time
   838 		  in
   839 		      ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1)
   840 		  end
   841               | Recon.E =>
   842 		  let val eproof = helper_path "E_HOME" "eproof"
   843                       val eopts = "--tstp-in%--tstp-out%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time
   844 		  in
   845 		     ("E", eproof, eopts, probfile) :: make_atp_list xs (n+1)
   846 		  end
   847           end
   848 
   849     val atp_list = make_atp_list sg_terms 1
   850   in
   851     Watcher.callResProvers(childout,atp_list);
   852     Output.debug (fn () => "Sent commands to watcher!")
   853   end
   854 
   855 (*For debugging the generated set of theorem names*)
   856 fun trace_vector fname =
   857   let val path = File.explode_platform_path (fname ^ "_thm_names")
   858   in  Vector.app (File.append path o (fn s => s ^ "\n"))  end;
   859 
   860 (*We write out problem files for each subgoal. Argument probfile generates filenames,
   861   and allows the suppression of the suffix "_1" in problem-generation mode.
   862   FIXME: does not cope with &&, and it isn't easy because one could have multiple
   863   subgoals, each involving &&.*)
   864 fun write_problem_files probfile (ctxt, chain_ths, th) =
   865   let val goals = Thm.prems_of th
   866       val _ = Output.debug (fn () => "number of subgoals = " ^ Int.toString (length goals))
   867       val thy = ProofContext.theory_of ctxt
   868       fun get_neg_subgoals [] _ = []
   869         | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) ::
   870                                          get_neg_subgoals gls (n+1)
   871       val goal_cls = get_neg_subgoals goals 1
   872       val logic = case !linkup_logic_mode of
   873                 Auto => problem_logic_goals (map (map prop_of) goal_cls)
   874               | Fol => FOL
   875               | Hol => HOL
   876       val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths
   877       val included_cls = included_thms |> ResAxioms.cnf_rules_pairs |> make_unique
   878                                        |> restrict_to_logic thy logic
   879                                        |> remove_unwanted_clauses
   880       val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls))
   881       val white_cls = ResAxioms.cnf_rules_pairs white_thms
   882       (*clauses relevant to goal gl*)
   883       val axcls_list = map (fn ngcls => white_cls @ relevance_filter thy included_cls (map prop_of ngcls)) goal_cls
   884       val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls)))
   885                   axcls_list
   886       val writer = if !prover = Recon.SPASS then dfg_writer else tptp_writer
   887       fun write_all [] [] _ = []
   888         | write_all (ccls::ccls_list) (axcls::axcls_list) k =
   889             let val fname = probfile k
   890                 val _ = Output.debug (fn () => "About to write file " ^ fname)
   891                 val axcls = make_unique axcls
   892                 val _ = Output.debug (fn () => "Conjecture Clauses (before duplicate removal)")
   893                 val _ = app (fn th => Output.debug (fn _ => string_of_thm th)) ccls
   894                 val ccls = subtract_cls ccls axcls
   895                 val _ = Output.debug (fn () => "Conjecture Clauses (AFTER duplicate removal)")
   896                 val _ = app (fn th => Output.debug (fn _ => string_of_thm th)) ccls
   897                 val ccltms = map prop_of ccls
   898                 and axtms = map (prop_of o #1) axcls
   899                 val subs = tfree_classes_of_terms ccltms
   900                 and supers = tvar_classes_of_terms axtms
   901                 and tycons = type_consts_of_terms thy (ccltms@axtms)
   902                 (*TFrees in conjecture clauses; TVars in axiom clauses*)
   903                 val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
   904                 val _ = Output.debug (fn () => "arity clauses = " ^ Int.toString (length arity_clauses))
   905                 val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   906                 val _ = Output.debug (fn () => "classrel clauses = " ^ Int.toString (length classrel_clauses))
   907                 val clnames = writer thy logic ccls fname (axcls,classrel_clauses,arity_clauses) []
   908                 val thm_names = Vector.fromList clnames
   909                 val _ = if !Output.debugging then trace_vector fname thm_names else ()
   910             in  (thm_names,fname) :: write_all ccls_list axcls_list (k+1)  end
   911       val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
   912   in
   913       (filenames, thm_names_list)
   914   end;
   915 
   916 val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream *
   917                                     Posix.Process.pid * string list) option);
   918 
   919 fun kill_last_watcher () =
   920     (case !last_watcher_pid of
   921          NONE => ()
   922        | SOME (_, _, pid, files) =>
   923           (Output.debug (fn () => "Killing old watcher, pid = " ^ string_of_pid pid);
   924            Watcher.killWatcher pid;
   925            ignore (map (try cond_rm_tmp) files)))
   926      handle OS.SysErr _ => Output.debug (fn () => "Attempt to kill watcher failed");
   927 
   928 (*writes out the current problems and calls ATPs*)
   929 fun isar_atp (ctxt, chain_ths, th) =
   930   if Thm.no_prems th then ()
   931   else
   932     let
   933       val _ = kill_last_watcher()
   934       val (files,thm_names_list) = write_problem_files prob_pathname (ctxt, chain_ths, th)
   935       val (childin, childout, pid) = Watcher.createWatcher (ctxt, th, thm_names_list)
   936     in
   937       last_watcher_pid := SOME (childin, childout, pid, files);
   938       Output.debug (fn () => "problem files: " ^ space_implode ", " files);
   939       Output.debug (fn () => "pid: " ^ string_of_pid pid);
   940       watcher_call_provers (Thm.theory_of_thm th) (Thm.prems_of th) (childin, childout, pid)
   941     end;
   942 
   943 (*For ML scripts, and primarily, for debugging*)
   944 fun callatp () =
   945   let val th = topthm()
   946       val ctxt = ProofContext.init (theory_of_thm th)
   947   in  isar_atp (ctxt, [], th)  end;
   948 
   949 val isar_atp_writeonly = PrintMode.setmp []
   950       (fn (ctxt, chain_ths, th) =>
   951        if Thm.no_prems th then ()
   952        else
   953          let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix
   954                             else prob_pathname
   955          in ignore (write_problem_files probfile (ctxt, chain_ths, th)) end);
   956 
   957 
   958 (** the Isar toplevel command **)
   959 
   960 fun sledgehammer state =
   961   let
   962     val (ctxt, (chain_ths, goal)) = Proof.get_goal (Toplevel.proof_of state);
   963     val thy = ProofContext.theory_of ctxt;
   964   in
   965     Output.debug (fn () => "subgoals in isar_atp:\n" ^
   966                   Pretty.string_of (ProofContext.pretty_term ctxt
   967                     (Logic.mk_conjunction_list (Thm.prems_of goal))));
   968     Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
   969     app (fn th => Output.debug (fn _ => "chained: " ^ string_of_thm th)) chain_ths;
   970     if !time_limit > 0 then isar_atp (ctxt, chain_ths, goal)
   971     else (warning ("Writing problem file only: " ^ !problem_name);
   972           isar_atp_writeonly (ctxt, chain_ths, goal))
   973   end;
   974 
   975 val _ = OuterSyntax.add_parsers
   976   [OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag
   977     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer))];
   978 
   979 end;