src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
author blanchet
Wed Jun 02 17:19:44 2010 +0200 (2010-06-02)
changeset 37323 2f2f0d246d0f
parent 37171 fc1e20373e6a
child 37344 40f379944c1e
permissions -rw-r--r--
handle Vampire's definitions smoothly
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
     2     Author:     Jia Meng, Cambridge University Computer Laboratory, NICTA
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 *)
     5 
     6 signature SLEDGEHAMMER_FACT_FILTER =
     7 sig
     8   type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
     9   type arity_clause = Sledgehammer_FOL_Clause.arity_clause
    10   type axiom_name = Sledgehammer_HOL_Clause.axiom_name
    11   type hol_clause = Sledgehammer_HOL_Clause.hol_clause
    12   type hol_clause_id = Sledgehammer_HOL_Clause.hol_clause_id
    13 
    14   type relevance_override =
    15     {add: Facts.ref list,
    16      del: Facts.ref list,
    17      only: bool}
    18 
    19   val tvar_classes_of_terms : term list -> string list
    20   val tfree_classes_of_terms : term list -> string list
    21   val type_consts_of_terms : theory -> term list -> string list
    22   val get_relevant_facts :
    23     bool -> real -> real -> bool -> int -> bool -> relevance_override
    24     -> Proof.context * (thm list * 'a) -> thm list
    25     -> (thm * (string * int)) list
    26   val prepare_clauses :
    27     bool -> thm list -> thm list -> (thm * (axiom_name * hol_clause_id)) list
    28     -> (thm * (axiom_name * hol_clause_id)) list -> theory
    29     -> axiom_name vector
    30        * (hol_clause list * hol_clause list * hol_clause list *
    31           hol_clause list * classrel_clause list * arity_clause list)
    32 end;
    33 
    34 structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
    35 struct
    36 
    37 open Sledgehammer_FOL_Clause
    38 open Sledgehammer_Fact_Preprocessor
    39 open Sledgehammer_HOL_Clause
    40 
    41 type relevance_override =
    42   {add: Facts.ref list,
    43    del: Facts.ref list,
    44    only: bool}
    45 
    46 (***************************************************************)
    47 (* Relevance Filtering                                         *)
    48 (***************************************************************)
    49 
    50 fun strip_Trueprop (@{const Trueprop} $ t) = t
    51   | strip_Trueprop t = t;
    52 
    53 (*A surprising number of theorems contain only a few significant constants.
    54   These include all induction rules, and other general theorems. Filtering
    55   theorems in clause form reveals these complexities in the form of Skolem 
    56   functions. If we were instead to filter theorems in their natural form,
    57   some other method of measuring theorem complexity would become necessary.*)
    58 
    59 fun log_weight2 (x:real) = 1.0 + 2.0/Math.ln (x+1.0);
    60 
    61 (*The default seems best in practice. A constant function of one ignores
    62   the constant frequencies.*)
    63 val weight_fn = log_weight2;
    64 
    65 
    66 (*Including equality in this list might be expected to stop rules like subset_antisym from
    67   being chosen, but for some reason filtering works better with them listed. The
    68   logical signs All, Ex, &, and --> are omitted because any remaining occurrrences
    69   must be within comprehensions.*)
    70 val standard_consts =
    71   [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all},
    72    @{const_name "=="}, @{const_name "op |"}, @{const_name Not},
    73    @{const_name "op ="}];
    74 
    75 
    76 (*** constants with types ***)
    77 
    78 (*An abstraction of Isabelle types*)
    79 datatype const_typ =  CTVar | CType of string * const_typ list
    80 
    81 (*Is the second type an instance of the first one?*)
    82 fun match_type (CType(con1,args1)) (CType(con2,args2)) = 
    83       con1=con2 andalso match_types args1 args2
    84   | match_type CTVar _ = true
    85   | match_type _ CTVar = false
    86 and match_types [] [] = true
    87   | match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2;
    88 
    89 (*Is there a unifiable constant?*)
    90 fun uni_mem gctab (c,c_typ) =
    91   case Symtab.lookup gctab c of
    92       NONE => false
    93     | SOME ctyps_list => exists (match_types c_typ) ctyps_list;
    94   
    95 (*Maps a "real" type to a const_typ*)
    96 fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) 
    97   | const_typ_of (TFree _) = CTVar
    98   | const_typ_of (TVar _) = CTVar
    99 
   100 (*Pairs a constant with the list of its type instantiations (using const_typ)*)
   101 fun const_with_typ thy (c,typ) = 
   102     let val tvars = Sign.const_typargs thy (c,typ)
   103     in (c, map const_typ_of tvars) end
   104     handle TYPE _ => (c,[]);   (*Variable (locale constant): monomorphic*)   
   105 
   106 (*Add a const/type pair to the table, but a [] entry means a standard connective,
   107   which we ignore.*)
   108 fun add_const_typ_table ((c,ctyps), tab) =
   109   Symtab.map_default (c, [ctyps]) (fn [] => [] | ctyps_list => insert (op =) ctyps ctyps_list) 
   110     tab;
   111 
   112 (*Free variables are included, as well as constants, to handle locales*)
   113 fun add_term_consts_typs_rm thy (Const(c, typ), tab) =
   114       add_const_typ_table (const_with_typ thy (c,typ), tab) 
   115   | add_term_consts_typs_rm thy (Free(c, typ), tab) =
   116       add_const_typ_table (const_with_typ thy (c,typ), tab) 
   117   | add_term_consts_typs_rm thy (t $ u, tab) =
   118       add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab))
   119   | add_term_consts_typs_rm thy (Abs(_,_,t), tab) = add_term_consts_typs_rm thy (t, tab)
   120   | add_term_consts_typs_rm _ (_, tab) = tab;
   121 
   122 (*The empty list here indicates that the constant is being ignored*)
   123 fun add_standard_const (s,tab) = Symtab.update (s,[]) tab;
   124 
   125 val null_const_tab : const_typ list list Symtab.table = 
   126     List.foldl add_standard_const Symtab.empty standard_consts;
   127 
   128 fun get_goal_consts_typs thy = List.foldl (add_term_consts_typs_rm thy) null_const_tab;
   129 
   130 (*Inserts a dummy "constant" referring to the theory name, so that relevance
   131   takes the given theory into account.*)
   132 fun const_prop_of theory_relevant th =
   133  if theory_relevant then
   134   let val name = Context.theory_name (theory_of_thm th)
   135       val t = Const (name ^ ". 1", HOLogic.boolT)
   136   in  t $ prop_of th  end
   137  else prop_of th;
   138 
   139 (**** Constant / Type Frequencies ****)
   140 
   141 (*A two-dimensional symbol table counts frequencies of constants. It's keyed first by
   142   constant name and second by its list of type instantiations. For the latter, we need
   143   a linear ordering on type const_typ list.*)
   144   
   145 local
   146 
   147 fun cons_nr CTVar = 0
   148   | cons_nr (CType _) = 1;
   149 
   150 in
   151 
   152 fun const_typ_ord TU =
   153   case TU of
   154     (CType (a, Ts), CType (b, Us)) =>
   155       (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord)
   156   | (T, U) => int_ord (cons_nr T, cons_nr U);
   157 
   158 end;
   159 
   160 structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord);
   161 
   162 fun count_axiom_consts theory_relevant thy ((thm,_), tab) = 
   163   let fun count_const (a, T, tab) =
   164         let val (c, cts) = const_with_typ thy (a,T)
   165         in  (*Two-dimensional table update. Constant maps to types maps to count.*)
   166             Symtab.map_default (c, CTtab.empty) 
   167                                (CTtab.map_default (cts,0) (fn n => n+1)) tab
   168         end
   169       fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab)
   170         | count_term_consts (Free(a,T), tab) = count_const(a,T,tab)
   171         | count_term_consts (t $ u, tab) =
   172             count_term_consts (t, count_term_consts (u, tab))
   173         | count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
   174         | count_term_consts (_, tab) = tab
   175   in  count_term_consts (const_prop_of theory_relevant thm, tab)  end;
   176 
   177 
   178 (**** Actual Filtering Code ****)
   179 
   180 (*The frequency of a constant is the sum of those of all instances of its type.*)
   181 fun const_frequency ctab (c, cts) =
   182   CTtab.fold (fn (cts', m) => match_types cts cts' ? Integer.add m)
   183              (the (Symtab.lookup ctab c)) 0
   184 
   185 (*Add in a constant's weight, as determined by its frequency.*)
   186 fun add_ct_weight ctab ((c,T), w) =
   187   w + weight_fn (real (const_frequency ctab (c,T)));
   188 
   189 (*Relevant constants are weighted according to frequency, 
   190   but irrelevant constants are simply counted. Otherwise, Skolem functions,
   191   which are rare, would harm a clause's chances of being picked.*)
   192 fun clause_weight ctab gctyps consts_typs =
   193     let val rel = filter (uni_mem gctyps) consts_typs
   194         val rel_weight = List.foldl (add_ct_weight ctab) 0.0 rel
   195     in
   196         rel_weight / (rel_weight + real (length consts_typs - length rel))
   197     end;
   198     
   199 (*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
   200 fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys;
   201 
   202 fun consts_typs_of_term thy t = 
   203   let val tab = add_term_consts_typs_rm thy (t, null_const_tab)
   204   in  Symtab.fold add_expand_pairs tab []  end;
   205 
   206 fun pair_consts_typs_axiom theory_relevant thy (p as (thm, _)) =
   207   (p, (consts_typs_of_term thy (const_prop_of theory_relevant thm)));
   208 
   209 exception ConstFree;
   210 fun dest_ConstFree (Const aT) = aT
   211   | dest_ConstFree (Free aT) = aT
   212   | dest_ConstFree _ = raise ConstFree;
   213 
   214 (*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
   215 fun defines thy thm gctypes =
   216     let val tm = prop_of thm
   217         fun defs lhs rhs =
   218             let val (rator,args) = strip_comb lhs
   219                 val ct = const_with_typ thy (dest_ConstFree rator)
   220             in
   221               forall is_Var args andalso uni_mem gctypes ct andalso
   222                 subset (op =) (Term.add_vars rhs [], Term.add_vars lhs [])
   223             end
   224             handle ConstFree => false
   225     in    
   226         case tm of
   227           @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) => 
   228             defs lhs rhs 
   229         | _ => false
   230     end;
   231 
   232 type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list);
   233        
   234 (*For a reverse sort, putting the largest values first.*)
   235 fun compare_pairs ((_,w1),(_,w2)) = Real.compare (w2,w1);
   236 
   237 (*Limit the number of new clauses, to prevent runaway acceptance.*)
   238 fun take_best max_new (newpairs : (annotd_cls*real) list) =
   239   let val nnew = length newpairs
   240   in
   241     if nnew <= max_new then (map #1 newpairs, [])
   242     else 
   243       let val cls = sort compare_pairs newpairs
   244           val accepted = List.take (cls, max_new)
   245       in
   246         trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^ 
   247                        ", exceeds the limit of " ^ Int.toString (max_new)));
   248         trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
   249         trace_msg (fn () => "Actually passed: " ^
   250           space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
   251 
   252         (map #1 accepted, map #1 (List.drop (cls, max_new)))
   253       end
   254   end;
   255 
   256 fun relevant_clauses ctxt relevance_convergence defs_relevant max_new
   257                      (relevance_override as {add, del, only}) thy ctab =
   258   let
   259     val thms_for_facts =
   260       maps (maps (cnf_axiom thy) o ProofContext.get_fact ctxt)
   261     val add_thms = thms_for_facts add
   262     val del_thms = thms_for_facts del
   263     fun iter p rel_consts =
   264       let
   265         fun relevant ([], _) [] = []  (* Nothing added this iteration *)
   266           | relevant (newpairs,rejects) [] =
   267             let
   268               val (newrels, more_rejects) = take_best max_new newpairs
   269               val new_consts = maps #2 newrels
   270               val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
   271               val newp = p + (1.0 - p) / relevance_convergence
   272             in
   273               trace_msg (fn () => "relevant this iteration: " ^
   274                                   Int.toString (length newrels));
   275               map #1 newrels @ iter newp rel_consts' (more_rejects @ rejects)
   276             end
   277           | relevant (newrels, rejects)
   278                      ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) =
   279             let
   280               val weight = if member Thm.eq_thm del_thms thm then 0.0
   281                            else if member Thm.eq_thm add_thms thm then 1.0
   282                            else if only then 0.0
   283                            else clause_weight ctab rel_consts consts_typs
   284             in
   285               if p <= weight orelse
   286                  (defs_relevant andalso defines thy (#1 clsthm) rel_consts) then
   287                 (trace_msg (fn () => name ^ " clause " ^ Int.toString n ^ 
   288                                      " passes: " ^ Real.toString weight);
   289                 relevant ((ax, weight) :: newrels, rejects) axs)
   290               else
   291                 relevant (newrels, ax :: rejects) axs
   292             end
   293         in
   294           trace_msg (fn () => "relevant_clauses, current pass mark: " ^
   295                               Real.toString p);
   296           relevant ([], [])
   297         end
   298   in iter end
   299         
   300 fun relevance_filter ctxt relevance_threshold relevance_convergence
   301                      defs_relevant max_new theory_relevant relevance_override
   302                      thy axioms goals = 
   303   if relevance_threshold > 0.0 then
   304     let
   305       val const_tab = List.foldl (count_axiom_consts theory_relevant thy)
   306                                  Symtab.empty axioms
   307       val goal_const_tab = get_goal_consts_typs thy goals
   308       val _ =
   309         trace_msg (fn () => "Initial constants: " ^
   310                             commas (Symtab.keys goal_const_tab))
   311       val relevant =
   312         relevant_clauses ctxt relevance_convergence defs_relevant max_new
   313                          relevance_override thy const_tab relevance_threshold
   314                          goal_const_tab
   315                          (map (pair_consts_typs_axiom theory_relevant thy)
   316                               axioms)
   317     in
   318       trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant));
   319       relevant
   320     end
   321   else
   322     axioms;
   323 
   324 (***************************************************************)
   325 (* Retrieving and filtering lemmas                             *)
   326 (***************************************************************)
   327 
   328 (*** retrieve lemmas and filter them ***)
   329 
   330 (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
   331 
   332 fun setinsert (x,s) = Symtab.update (x,()) s;
   333 
   334 (*Reject theorems with names like "List.filter.filter_list_def" or
   335   "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
   336 fun is_package_def a =
   337   let val names = Long_Name.explode a
   338   in
   339      length names > 2 andalso
   340      not (hd names = "local") andalso
   341      String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a
   342   end;
   343 
   344 fun mk_clause_table xs =
   345   fold (Termtab.update o `(prop_of o fst)) xs Termtab.empty
   346 
   347 fun make_unique xs =
   348   Termtab.fold (cons o snd) (mk_clause_table xs) []
   349 
   350 (* Remove existing axiom clauses from the conjecture clauses, as this can
   351    dramatically boost an ATP's performance (for some reason). *)
   352 fun subtract_cls ax_clauses =
   353   filter_out (Termtab.defined (mk_clause_table ax_clauses) o prop_of)
   354 
   355 fun all_valid_thms respect_no_atp ctxt chained_ths =
   356   let
   357     val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
   358     val local_facts = ProofContext.facts_of ctxt;
   359     val full_space =
   360       Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts);
   361 
   362     fun valid_facts facts =
   363       (facts, []) |-> Facts.fold_static (fn (name, ths0) =>
   364         let
   365           fun check_thms a =
   366             (case try (ProofContext.get_thms ctxt) a of
   367               NONE => false
   368             | SOME ths1 => Thm.eq_thms (ths0, ths1));
   369 
   370           val name1 = Facts.extern facts name;
   371           val name2 = Name_Space.extern full_space name;
   372           val ths = filter_out bad_for_atp ths0;
   373         in
   374           if Facts.is_concealed facts name orelse
   375              (respect_no_atp andalso is_package_def name) then
   376             I
   377           else case find_first check_thms [name1, name2, name] of
   378             NONE => I
   379           | SOME name' =>
   380             cons (name' |> forall (member Thm.eq_thm chained_ths) ths
   381                            ? prefix chained_prefix, ths)
   382         end);
   383   in valid_facts global_facts @ valid_facts local_facts end;
   384 
   385 fun multi_name a th (n, pairs) =
   386   (n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs);
   387 
   388 fun add_single_names (a, []) pairs = pairs
   389   | add_single_names (a, [th]) pairs = (a, th) :: pairs
   390   | add_single_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs));
   391 
   392 (*Ignore blacklisted basenames*)
   393 fun add_multi_names (a, ths) pairs =
   394   if member (op =) multi_base_blacklist (Long_Name.base_name a) then pairs
   395   else add_single_names (a, ths) pairs;
   396 
   397 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
   398 
   399 (* The single-name theorems go after the multiple-name ones, so that single
   400    names are preferred when both are available. *)
   401 fun name_thm_pairs respect_no_atp ctxt chained_ths =
   402   let
   403     val (mults, singles) =
   404       List.partition is_multi (all_valid_thms respect_no_atp ctxt chained_ths)
   405     val ps = [] |> fold add_single_names singles
   406                 |> fold add_multi_names mults
   407   in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end;
   408 
   409 fun check_named ("", th) =
   410       (warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false)
   411   | check_named _ = true;
   412 
   413 fun get_all_lemmas respect_no_atp ctxt chained_ths =
   414   let val included_thms =
   415         tap (fn ths => trace_msg
   416                      (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
   417             (name_thm_pairs respect_no_atp ctxt chained_ths)
   418   in
   419     filter check_named included_thms
   420   end;
   421 
   422 (***************************************************************)
   423 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
   424 (***************************************************************)
   425 
   426 fun add_classes (sorts, cset) = List.foldl setinsert cset (flat sorts);
   427 
   428 (*Remove this trivial type class*)
   429 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
   430 
   431 fun tvar_classes_of_terms ts =
   432   let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
   433   in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   434 
   435 fun tfree_classes_of_terms ts =
   436   let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
   437   in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   438 
   439 (*fold type constructors*)
   440 fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
   441   | fold_type_consts _ _ x = x;
   442 
   443 val add_type_consts_in_type = fold_type_consts setinsert;
   444 
   445 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
   446 fun add_type_consts_in_term thy =
   447   let val const_typargs = Sign.const_typargs thy
   448       fun add_tcs (Const cT) x = fold add_type_consts_in_type (const_typargs cT) x
   449         | add_tcs (Abs (_, _, u)) x = add_tcs u x
   450         | add_tcs (t $ u) x = add_tcs t (add_tcs u x)
   451         | add_tcs _ x = x
   452   in  add_tcs  end
   453 
   454 fun type_consts_of_terms thy ts =
   455   Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
   456 
   457 
   458 (***************************************************************)
   459 (* ATP invocation methods setup                                *)
   460 (***************************************************************)
   461 
   462 (*Ensures that no higher-order theorems "leak out"*)
   463 fun restrict_to_logic thy true cls = filter (Meson.is_fol_term thy o prop_of o fst) cls
   464   | restrict_to_logic thy false cls = cls;
   465 
   466 (**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****)
   467 
   468 (** Too general means, positive equality literal with a variable X as one operand,
   469   when X does not occur properly in the other operand. This rules out clearly
   470   inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **)
   471 
   472 fun occurs ix =
   473     let fun occ(Var (jx,_)) = (ix=jx)
   474           | occ(t1$t2)      = occ t1 orelse occ t2
   475           | occ(Abs(_,_,t)) = occ t
   476           | occ _           = false
   477     in occ end;
   478 
   479 fun is_recordtype T = not (null (Record.dest_recTs T));
   480 
   481 (*Unwanted equalities include
   482   (1) those between a variable that does not properly occur in the second operand,
   483   (2) those between a variable and a record, since these seem to be prolific "cases" thms
   484 *)
   485 fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T
   486   | too_general_eqterms _ = false;
   487 
   488 fun too_general_equality (Const (@{const_name "op ="}, _) $ x $ y) =
   489       too_general_eqterms (x,y) orelse too_general_eqterms(y,x)
   490   | too_general_equality _ = false;
   491 
   492 fun has_typed_var tycons = exists_subterm
   493   (fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false);
   494 
   495 (*Clauses are forbidden to contain variables of these types. The typical reason is that
   496   they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=().
   497   The resulting clause will have no type constraint, yielding false proofs. Even "bool"
   498   leads to many unsound proofs, though (obviously) only for higher-order problems.*)
   499 val unwanted_types = [@{type_name unit}, @{type_name bool}];
   500 
   501 fun unwanted t =
   502   t = @{prop True} orelse has_typed_var unwanted_types t orelse
   503   forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t));
   504 
   505 (*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
   506   likely to lead to unsound proofs.*)
   507 fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
   508 
   509 fun is_first_order thy = forall (Meson.is_fol_term thy) o map prop_of
   510 
   511 fun get_relevant_facts respect_no_atp relevance_threshold relevance_convergence
   512                        defs_relevant max_new theory_relevant
   513                        (relevance_override as {add, only, ...})
   514                        (ctxt, (chained_ths, _)) goal_cls =
   515   if (only andalso null add) orelse relevance_threshold > 1.0 then
   516     []
   517   else
   518     let
   519       val thy = ProofContext.theory_of ctxt
   520       val is_FO = is_first_order thy goal_cls
   521       val included_cls = get_all_lemmas respect_no_atp ctxt chained_ths
   522         |> cnf_rules_pairs thy |> make_unique
   523         |> restrict_to_logic thy is_FO
   524         |> remove_unwanted_clauses
   525     in
   526       relevance_filter ctxt relevance_threshold relevance_convergence
   527                        defs_relevant max_new theory_relevant relevance_override
   528                        thy included_cls (map prop_of goal_cls)
   529     end
   530 
   531 (* prepare for passing to writer,
   532    create additional clauses based on the information from extra_cls *)
   533 fun prepare_clauses dfg goal_cls chained_ths axcls extra_cls thy =
   534   let
   535     val is_FO = is_first_order thy goal_cls
   536     val ccls = subtract_cls extra_cls goal_cls
   537     val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
   538     val ccltms = map prop_of ccls
   539     and axtms = map (prop_of o #1) extra_cls
   540     val subs = tfree_classes_of_terms ccltms
   541     and supers = tvar_classes_of_terms axtms
   542     and tycons = type_consts_of_terms thy (ccltms @ axtms)
   543     (*TFrees in conjecture clauses; TVars in axiom clauses*)
   544     val conjectures = make_conjecture_clauses dfg thy ccls
   545     val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses dfg thy extra_cls)
   546     val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses dfg thy axcls)
   547     val helper_clauses = get_helper_clauses dfg thy is_FO (conjectures, extra_cls, [])
   548     val (supers', arity_clauses) = make_arity_clauses_dfg dfg thy tycons supers
   549     val classrel_clauses = make_classrel_clauses thy subs supers'
   550   in
   551     (Vector.fromList clnames,
   552       (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
   553   end
   554 
   555 end;