src/HOL/Tools/res_atp.ML
author wenzelm
Tue May 08 15:01:30 2007 +0200 (2007-05-08)
changeset 22865 da52c2bd66ae
parent 22824 51bb2f6ecc4a
child 22989 3bcbe6187027
permissions -rw-r--r--
renamed call_atp to sledgehammer;
     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: string ref
    11   val custom_spass: string list ref
    12   val destdir: string ref
    13   val helper_path: string -> string -> string
    14   val problem_name: string ref
    15   val time_limit: int ref
    16   val set_prover: string -> unit
    17 
    18   datatype mode = Auto | Fol | Hol
    19   val linkup_logic_mode : mode ref
    20   val write_subgoal_file: bool -> mode -> Proof.context -> thm list -> thm list -> int -> string
    21   val vampire_time: int ref
    22   val eprover_time: int ref
    23   val spass_time: int ref
    24   val run_vampire: int -> unit
    25   val run_eprover: int -> unit
    26   val run_spass: int -> unit
    27   val vampireLimit: unit -> int
    28   val eproverLimit: unit -> int
    29   val spassLimit: unit -> int
    30   val atp_method: (Proof.context -> thm list -> int -> tactic) ->
    31     Method.src -> Proof.context -> Proof.method
    32   val cond_rm_tmp: string -> unit
    33   val include_all: bool ref
    34   val run_relevance_filter: bool ref
    35   val run_blacklist_filter: bool ref
    36   val blacklist: string list ref
    37   val add_all : unit -> unit
    38   val add_claset : unit -> unit
    39   val add_simpset : unit -> unit
    40   val add_clasimp : unit -> unit
    41   val add_atpset : unit -> unit
    42   val rm_all : unit -> unit
    43   val rm_claset : unit -> unit
    44   val rm_simpset : unit -> unit
    45   val rm_atpset : unit -> unit
    46   val rm_clasimp : unit -> unit
    47   val is_fol_thms : thm list -> bool
    48 end;
    49 
    50 structure ResAtp: RES_ATP =
    51 struct
    52 
    53 fun timestamp s = Output.debug (fn () => ("At " ^ Time.toString (Time.now()) ^ ": " ^ s));
    54 
    55 (********************************************************************)
    56 (* some settings for both background automatic ATP calling procedure*)
    57 (* and also explicit ATP invocation methods                         *)
    58 (********************************************************************)
    59 
    60 (*** background linkup ***)
    61 val call_atp = ref false;
    62 val hook_count = ref 0;
    63 val time_limit = ref 60;
    64 val prover = ref "";
    65 
    66 fun set_prover atp =
    67   case String.map Char.toLower atp of
    68       "e" =>
    69           (ReduceAxiomsN.max_new := 100;
    70            ReduceAxiomsN.theory_const := false;
    71            prover := "E")
    72     | "spass" =>
    73           (ReduceAxiomsN.max_new := 40;
    74            ReduceAxiomsN.theory_const := true;
    75            prover := "spass")
    76     | "vampire" =>
    77           (ReduceAxiomsN.max_new := 60;
    78            ReduceAxiomsN.theory_const := false;
    79            prover := "vampire")
    80     | _ => error ("No such prover: " ^ atp);
    81 
    82 val _ = set_prover "E"; (* use E as the default prover *)
    83 
    84 val custom_spass =   (*specialized options for SPASS*)
    85       ref ["-Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub"];
    86 val destdir = ref "";   (*Empty means write files to /tmp*)
    87 val problem_name = ref "prob";
    88 
    89 (*Return the path to a "helper" like SPASS or tptp2X, first checking that
    90   it exists.  FIXME: modify to use Path primitives and move to some central place.*)
    91 fun helper_path evar base =
    92   case getenv evar of
    93       "" => error  ("Isabelle environment variable " ^ evar ^ " not defined")
    94     | home =>
    95         let val path = home ^ "/" ^ base
    96         in  if File.exists (File.explode_platform_path path) then path
    97             else error ("Could not find the file " ^ path)
    98         end;
    99 
   100 fun probfile_nosuffix _ =
   101   if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
   102   else if File.exists (File.explode_platform_path (!destdir))
   103   then !destdir ^ "/" ^ !problem_name
   104   else error ("No such directory: " ^ !destdir);
   105 
   106 fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n;
   107 
   108 
   109 (*** ATP methods ***)
   110 val vampire_time = ref 60;
   111 val eprover_time = ref 60;
   112 val spass_time = ref 60;
   113 
   114 fun run_vampire time =
   115     if (time >0) then vampire_time:= time
   116     else vampire_time:=60;
   117 
   118 fun run_eprover time =
   119     if (time > 0) then eprover_time:= time
   120     else eprover_time:=60;
   121 
   122 fun run_spass time =
   123     if (time > 0) then spass_time:=time
   124     else spass_time:=60;
   125 
   126 
   127 fun vampireLimit () = !vampire_time;
   128 fun eproverLimit () = !eprover_time;
   129 fun spassLimit () = !spass_time;
   130 
   131 fun atp_input_file () =
   132     let val file = !problem_name
   133     in
   134         if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file))
   135         else if File.exists (File.explode_platform_path (!destdir))
   136         then !destdir ^ "/" ^ file
   137         else error ("No such directory: " ^ !destdir)
   138     end;
   139 
   140 val include_all = ref true;
   141 val include_simpset = ref false;
   142 val include_claset = ref false;
   143 val include_atpset = ref true;
   144 
   145 (*Tests show that follow_defs gives VERY poor results with "include_all"*)
   146 fun add_all() = (include_all:=true; ReduceAxiomsN.follow_defs := false);
   147 fun rm_all() = include_all:=false;
   148 
   149 fun add_simpset() = include_simpset:=true;
   150 fun rm_simpset() = include_simpset:=false;
   151 
   152 fun add_claset() = include_claset:=true;
   153 fun rm_claset() = include_claset:=false;
   154 
   155 fun add_clasimp() = (include_simpset:=true;include_claset:=true);
   156 fun rm_clasimp() = (include_simpset:=false;include_claset:=false);
   157 
   158 fun add_atpset() = include_atpset:=true;
   159 fun rm_atpset() = include_atpset:=false;
   160 
   161 
   162 (**** relevance filter ****)
   163 val run_relevance_filter = ReduceAxiomsN.run_relevance_filter;
   164 val run_blacklist_filter = ref true;
   165 
   166 (******************************************************************)
   167 (* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *)
   168 (******************************************************************)
   169 
   170 datatype logic = FOL | HOL | HOLC | HOLCS;
   171 
   172 fun string_of_logic FOL = "FOL"
   173   | string_of_logic HOL = "HOL"
   174   | string_of_logic HOLC = "HOLC"
   175   | string_of_logic HOLCS = "HOLCS";
   176 
   177 fun is_fol_logic FOL = true
   178   | is_fol_logic  _ = false
   179 
   180 (*HOLCS will not occur here*)
   181 fun upgrade_lg HOLC _ = HOLC
   182   | upgrade_lg HOL HOLC = HOLC
   183   | upgrade_lg HOL _ = HOL
   184   | upgrade_lg FOL lg = lg;
   185 
   186 (* check types *)
   187 fun has_bool_hfn (Type("bool",_)) = true
   188   | has_bool_hfn (Type("fun",_)) = true
   189   | has_bool_hfn (Type(_, Ts)) = exists has_bool_hfn Ts
   190   | has_bool_hfn _ = false;
   191 
   192 fun is_hol_fn tp =
   193     let val (targs,tr) = strip_type tp
   194     in
   195         exists (has_bool_hfn) (tr::targs)
   196     end;
   197 
   198 fun is_hol_pred tp =
   199     let val (targs,tr) = strip_type tp
   200     in
   201         exists (has_bool_hfn) targs
   202     end;
   203 
   204 exception FN_LG of term;
   205 
   206 fun fn_lg (t as Const(f,tp)) (lg,seen) =
   207     if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen)
   208   | fn_lg (t as Free(f,tp)) (lg,seen) =
   209     if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen)
   210   | fn_lg (t as Var(f,tp)) (lg,seen) =
   211     if is_hol_fn tp then (upgrade_lg HOL lg,insert (op =) t seen) else (lg,insert (op =) t seen)
   212   | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,insert (op =) t seen)
   213   | fn_lg f _ = raise FN_LG(f);
   214 
   215 
   216 fun term_lg [] (lg,seen) = (lg,seen)
   217   | term_lg (tm::tms) (FOL,seen) =
   218       let val (f,args) = strip_comb tm
   219           val (lg',seen') = if f mem seen then (FOL,seen)
   220                             else fn_lg f (FOL,seen)
   221       in
   222         if is_fol_logic lg' then ()
   223         else Output.debug (fn () => ("Found a HOL term: " ^ Display.raw_string_of_term f));
   224         term_lg (args@tms) (lg',seen')
   225       end
   226   | term_lg _ (lg,seen) = (lg,seen)
   227 
   228 exception PRED_LG of term;
   229 
   230 fun pred_lg (t as Const(P,tp)) (lg,seen)=
   231       if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen)
   232       else (lg,insert (op =) t seen)
   233   | pred_lg (t as Free(P,tp)) (lg,seen) =
   234       if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen)
   235       else (lg,insert (op =) t seen)
   236   | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, insert (op =) t seen)
   237   | pred_lg P _ = raise PRED_LG(P);
   238 
   239 
   240 fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen)
   241   | lit_lg P (lg,seen) =
   242       let val (pred,args) = strip_comb P
   243           val (lg',seen') = if pred mem seen then (lg,seen)
   244                             else pred_lg pred (lg,seen)
   245       in
   246         if is_fol_logic lg' then ()
   247         else Output.debug (fn () => ("Found a HOL predicate: " ^ Display.raw_string_of_term pred));
   248         term_lg args (lg',seen')
   249       end;
   250 
   251 fun lits_lg [] (lg,seen) = (lg,seen)
   252   | lits_lg (lit::lits) (FOL,seen) =
   253       let val (lg,seen') = lit_lg lit (FOL,seen)
   254       in
   255         if is_fol_logic lg then ()
   256         else Output.debug (fn () => ("Found a HOL literal: " ^ Display.raw_string_of_term lit));
   257         lits_lg lits (lg,seen')
   258       end
   259   | lits_lg lits (lg,seen) = (lg,seen);
   260 
   261 fun dest_disj_aux (Const("Trueprop",_) $ t) disjs = dest_disj_aux t disjs
   262   | dest_disj_aux (Const ("op |", _) $ t $ t') disjs = dest_disj_aux t (dest_disj_aux t' disjs)
   263   | dest_disj_aux t disjs = t::disjs;
   264 
   265 fun dest_disj t = dest_disj_aux t [];
   266 
   267 fun logic_of_clause tm = lits_lg (dest_disj tm);
   268 
   269 fun logic_of_clauses [] (lg,seen) = (lg,seen)
   270   | logic_of_clauses (cls::clss) (FOL,seen) =
   271     let val (lg,seen') = logic_of_clause cls (FOL,seen)
   272         val _ =
   273           if is_fol_logic lg then ()
   274           else Output.debug (fn () => ("Found a HOL clause: " ^ Display.raw_string_of_term cls))
   275     in
   276         logic_of_clauses clss (lg,seen')
   277     end
   278   | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
   279 
   280 fun problem_logic_goals_aux [] (lg,seen) = lg
   281   | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) =
   282     problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen));
   283 
   284 fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]);
   285 
   286 fun is_fol_thms ths = ((fst(logic_of_clauses (map prop_of ths) (FOL,[]))) = FOL);
   287 
   288 (***************************************************************)
   289 (* Retrieving and filtering lemmas                             *)
   290 (***************************************************************)
   291 
   292 (*** white list and black list of lemmas ***)
   293 
   294 (*The rule subsetI is frequently omitted by the relevance filter.*)
   295 val whitelist = ref [subsetI];
   296 
   297 (*Names of theorems and theorem lists to be blacklisted.
   298 
   299   These theorems typically produce clauses that are prolific (match too many equality or
   300   membership literals) and relate to seldom-used facts. Some duplicate other rules.
   301   FIXME: this blacklist needs to be maintained using theory data and added to using
   302   an attribute.*)
   303 val blacklist = ref
   304   ["Datatype.prod.size",
   305    "Divides.dvd_0_left_iff",
   306    "Finite_Set.card_0_eq",
   307    "Finite_Set.card_infinite",
   308    "Finite_Set.Max_ge",
   309    "Finite_Set.Max_in",
   310    "Finite_Set.Max_le_iff",
   311    "Finite_Set.Max_less_iff",
   312    "Finite_Set.max.f_below_strict_below.below_f_conv", (*duplicates in Orderings.*)
   313    "Finite_Set.max.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
   314    "Finite_Set.Min_ge_iff",
   315    "Finite_Set.Min_gr_iff",
   316    "Finite_Set.Min_in",
   317    "Finite_Set.Min_le",
   318    "Finite_Set.min.f_below_strict_below.below_f_conv",        (*duplicates in Orderings.*)
   319    "Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
   320    "Fun.vimage_image_eq",   (*involves an existential quantifier*)
   321    "HOL.split_if_asm",     (*splitting theorem*)
   322    "HOL.split_if",         (*splitting theorem*)
   323    "HOL.All_def",          (*far worse than useless!!*)
   324    "IntDef.abs_split",
   325    "IntDef.Integ.Abs_Integ_inject",
   326    "IntDef.Integ.Abs_Integ_inverse",
   327    "IntDiv.zdvd_0_left",
   328    "List.append_eq_append_conv",
   329    "List.hd_Cons_tl",   (*Says everything is [] or Cons. Probably prolific.*)
   330    "List.in_listsD",
   331    "List.in_listsI",
   332    "List.lists.Cons",
   333    "List.listsE",
   334    "Nat.less_one", (*not directional? obscure*)
   335    "Nat.not_gr0",
   336    "Nat.one_eq_mult_iff", (*duplicate by symmetry*)
   337    "Nat.of_nat_0_eq_iff",
   338    "Nat.of_nat_eq_0_iff",
   339    "Nat.of_nat_le_0_iff",
   340    "NatSimprocs.divide_le_0_iff_number_of",  (*too many clauses*)
   341    "NatSimprocs.divide_less_0_iff_number_of",
   342    "NatSimprocs.equation_minus_iff_1",  (*not directional*)
   343    "NatSimprocs.equation_minus_iff_number_of", (*not directional*)
   344    "NatSimprocs.le_minus_iff_1", (*not directional*)
   345    "NatSimprocs.le_minus_iff_number_of",  (*not directional*)
   346    "NatSimprocs.less_minus_iff_1", (*not directional*)
   347    "NatSimprocs.less_minus_iff_number_of", (*not directional*)
   348    "NatSimprocs.minus_equation_iff_number_of", (*not directional*)
   349    "NatSimprocs.minus_le_iff_1", (*not directional*)
   350    "NatSimprocs.minus_le_iff_number_of", (*not directional*)
   351    "NatSimprocs.minus_less_iff_1", (*not directional*)
   352    "NatSimprocs.mult_le_cancel_left_number_of", (*excessive case analysis*)
   353    "NatSimprocs.mult_le_cancel_right_number_of", (*excessive case analysis*)
   354    "NatSimprocs.mult_less_cancel_left_number_of", (*excessive case analysis*)
   355    "NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*)
   356    "NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*)
   357    "NatSimprocs.zero_less_divide_iff_number_of",
   358    "OrderedGroup.abs_0_eq", (*duplicate by symmetry*)
   359    "OrderedGroup.diff_eq_0_iff_eq", (*prolific?*)
   360    "OrderedGroup.sup_0_eq_0",
   361    "OrderedGroup.inf_0_eq_0",
   362    "OrderedGroup.pprt_eq_0",   (*obscure*)
   363    "OrderedGroup.pprt_eq_id",   (*obscure*)
   364    "OrderedGroup.pprt_mono",   (*obscure*)
   365    "Orderings.split_max",      (*splitting theorem*)
   366    "Orderings.split_min",      (*splitting theorem*)
   367    "Power.zero_less_power_abs_iff",
   368    "Product_Type.split_eta_SetCompr",   (*involves an existential quantifier*)
   369    "Product_Type.split_paired_Ball_Sigma",     (*splitting theorem*)
   370    "Product_Type.split_paired_Bex_Sigma",      (*splitting theorem*)
   371    "Product_Type.split_split_asm",             (*splitting theorem*)
   372    "Product_Type.split_split",                 (*splitting theorem*)
   373    "Product_Type.unit_abs_eta_conv",
   374    "Product_Type.unit_induct",
   375    "Relation.diagI",
   376    "Relation.Domain_def",   (*involves an existential quantifier*)
   377    "Relation.Image_def",   (*involves an existential quantifier*)
   378    "Relation.ImageI",
   379    "Ring_and_Field.divide_cancel_left", (*fields are seldom used & often prolific*)
   380    "Ring_and_Field.divide_cancel_right",
   381    "Ring_and_Field.divide_divide_eq_left",
   382    "Ring_and_Field.divide_divide_eq_right",
   383    "Ring_and_Field.divide_eq_0_iff",
   384    "Ring_and_Field.divide_eq_1_iff",
   385    "Ring_and_Field.divide_eq_eq_1",
   386    "Ring_and_Field.divide_le_0_1_iff",
   387    "Ring_and_Field.divide_le_eq_1_neg",  (*obscure and prolific*)
   388    "Ring_and_Field.divide_le_eq_1_pos",  (*obscure and prolific*)
   389    "Ring_and_Field.divide_less_0_1_iff",
   390    "Ring_and_Field.divide_less_eq_1_neg",  (*obscure and prolific*)
   391    "Ring_and_Field.divide_less_eq_1_pos",  (*obscure and prolific*)
   392    "Ring_and_Field.eq_divide_eq_1", (*duplicate by symmetry*)
   393    "Ring_and_Field.field_mult_cancel_left",
   394    "Ring_and_Field.field_mult_cancel_right",
   395    "Ring_and_Field.inverse_le_iff_le_neg",
   396    "Ring_and_Field.inverse_le_iff_le",
   397    "Ring_and_Field.inverse_less_iff_less_neg",
   398    "Ring_and_Field.inverse_less_iff_less",
   399    "Ring_and_Field.le_divide_eq_1_neg", (*obscure and prolific*)
   400    "Ring_and_Field.le_divide_eq_1_pos", (*obscure and prolific*)
   401    "Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*)
   402    "Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*)
   403    "Ring_and_Field.one_eq_divide_iff",  (*duplicate by symmetry*)
   404    "Set.ball_simps", "Set.bex_simps",  (*quantifier rewriting: useless*)
   405    "Set.Collect_bex_eq",   (*involves an existential quantifier*)
   406    "Set.Collect_ex_eq",   (*involves an existential quantifier*)
   407    "Set.Diff_eq_empty_iff", (*redundant with paramodulation*)
   408    "Set.Diff_insert0",
   409    "Set.empty_Union_conv",   (*redundant with paramodulation*)
   410    "Set.full_SetCompr_eq",   (*involves an existential quantifier*)
   411    "Set.image_Collect",      (*involves Collect and a boolean variable...*)
   412    "Set.image_def",          (*involves an existential quantifier*)
   413    "Set.disjoint_insert", "Set.insert_disjoint",
   414    "Set.Int_UNIV",  (*redundant with paramodulation*)
   415    "Set.Inter_UNIV_conv",
   416    "Set.Inter_iff", (*We already have InterI, InterE*)
   417    "Set.psubsetE",    (*too prolific and obscure*)
   418    "Set.psubsetI",
   419    "Set.singleton_insert_inj_eq'",
   420    "Set.singleton_insert_inj_eq",
   421    "Set.singletonD",  (*these two duplicate some "insert" lemmas*)
   422    "Set.singletonI",
   423    "Set.Un_empty", (*redundant with paramodulation*)
   424    "Set.UNION_def",   (*involves an existential quantifier*)
   425    "Set.Union_empty_conv", (*redundant with paramodulation*)
   426    "Set.Union_iff",              (*We already have UnionI, UnionE*)
   427    "SetInterval.atLeastAtMost_iff", (*obscure and prolific*)
   428    "SetInterval.atLeastLessThan_iff", (*obscure and prolific*)
   429    "SetInterval.greaterThanAtMost_iff", (*obscure and prolific*)
   430    "SetInterval.greaterThanLessThan_iff", (*obscure and prolific*)
   431    "SetInterval.ivl_subset"];  (*excessive case analysis*)
   432 
   433 (*These might be prolific but are probably OK, and min and max are basic.
   434    "Orderings.max_less_iff_conj",
   435    "Orderings.min_less_iff_conj",
   436    "Orderings.min_max.below_inf.below_inf_conv",
   437    "Orderings.min_max.below_sup.above_sup_conv",
   438 Very prolific and somewhat obscure:
   439    "Set.InterD",
   440    "Set.UnionI",
   441 *)
   442 
   443 (*** retrieve lemmas from clasimpset and atpset, may filter them ***)
   444 
   445 (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
   446 
   447 fun setinsert (x,s) = Symtab.update (x,()) s;
   448 
   449 (*Reject theorems with names like "List.filter.filter_list_def" or
   450   "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
   451 fun is_package_def a =
   452   let val names = NameSpace.explode a
   453   in
   454      length names > 2 andalso
   455      not (hd names = "local") andalso
   456      String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a
   457   end;
   458 
   459 (** a hash function from Term.term to int, and also a hash table **)
   460 val xor_words = List.foldl Word.xorb 0w0;
   461 
   462 fun hashw_term ((Const(c,_)), w) = Polyhash.hashw_string (c,w)
   463   | hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w)
   464   | hashw_term ((Var(_,_)), w) = w
   465   | hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w)
   466   | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
   467   | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));
   468 
   469 fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0))
   470   | hash_literal P = hashw_term(P,0w0);
   471 
   472 fun hash_term t = Word.toIntX (xor_words (map hash_literal (dest_disj t)));
   473 
   474 fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
   475 
   476 exception HASH_CLAUSE;
   477 
   478 (*Create a hash table for clauses, of the given size*)
   479 fun mk_clause_table n =
   480       Polyhash.mkTable (hash_term o prop_of, equal_thm)
   481                        (n, HASH_CLAUSE);
   482 
   483 (*Use a hash table to eliminate duplicates from xs. Argument is a list of
   484   (thm * (string * int)) tuples. The theorems are hashed into the table. *)
   485 fun make_unique xs =
   486   let val ht = mk_clause_table 7000
   487   in
   488       Output.debug (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
   489       app (ignore o Polyhash.peekInsert ht) xs;
   490       Polyhash.listItems ht
   491   end;
   492 
   493 (*Remove existing axiom clauses from the conjecture clauses, as this can dramatically
   494   boost an ATP's performance (for some reason)*)
   495 fun subtract_cls c_clauses ax_clauses =
   496   let val ht = mk_clause_table 2200
   497       fun known x = isSome (Polyhash.peek ht x)
   498   in
   499       app (ignore o Polyhash.peekInsert ht) ax_clauses;
   500       filter (not o known) c_clauses
   501   end;
   502 
   503 (*Filter axiom clauses, but keep supplied clauses and clauses in whitelist.
   504   Duplicates are removed later.*)
   505 fun get_relevant_clauses thy cls_thms white_cls goals =
   506   white_cls @ (ReduceAxiomsN.relevance_filter thy cls_thms goals);
   507 
   508 fun all_valid_thms ctxt =
   509   let
   510     val banned_tab = foldl setinsert Symtab.empty (!blacklist)
   511     fun blacklisted s = !run_blacklist_filter andalso
   512                         (isSome (Symtab.lookup banned_tab s) orelse is_package_def s)
   513 
   514     fun extern_valid space (name, ths) =
   515       let
   516         val is_valid = ProofContext.valid_thms ctxt;
   517         val xname = NameSpace.extern space name;
   518       in
   519         if blacklisted name then I
   520         else if is_valid (xname, ths) then cons (xname, ths)
   521         else if is_valid (name, ths) then cons (name, ths)
   522         else I
   523       end;
   524     val thy = ProofContext.theory_of ctxt;
   525     val all_thys = thy :: Theory.ancestors_of thy;
   526 
   527     fun dest_valid (space, tab) = Symtab.fold (extern_valid space) tab [];
   528   in
   529     maps (dest_valid o PureThy.theorems_of) all_thys @
   530     fold (extern_valid (#1 (ProofContext.theorems_of ctxt)))
   531       (FactIndex.find (ProofContext.fact_index_of ctxt) ([], [])) []
   532   end;
   533 
   534 fun multi_name a (th, (n,pairs)) =
   535   (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs)
   536 
   537 fun add_single_names ((a, []), pairs) = pairs
   538   | add_single_names ((a, [th]), pairs) = (a,th)::pairs
   539   | add_single_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
   540 
   541 val multi_base_blacklist =
   542   ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm"];
   543 
   544 (*Ignore blacklisted basenames*)
   545 fun add_multi_names ((a, ths), pairs) =
   546   if (Sign.base_name a) mem_string multi_base_blacklist  then pairs
   547   else add_single_names ((a, ths), pairs);
   548 
   549 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
   550 
   551 (*The single theorems go BEFORE the multiple ones*)
   552 fun name_thm_pairs ctxt =
   553   let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
   554   in  foldl add_single_names  (foldl add_multi_names [] mults) singles end;
   555 
   556 fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false)
   557   | check_named (_,th) = true;
   558 
   559 fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ string_of_thm th);
   560 
   561 (* get lemmas from claset, simpset, atpset and extra supplied rules *)
   562 fun get_clasimp_atp_lemmas ctxt user_thms =
   563   let val included_thms =
   564         if !include_all
   565         then (tap (fn ths => Output.debug
   566                      (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
   567                   (name_thm_pairs ctxt))
   568         else
   569         let val claset_thms =
   570                 if !include_claset then ResAxioms.claset_rules_of ctxt
   571                 else []
   572             val simpset_thms =
   573                 if !include_simpset then ResAxioms.simpset_rules_of ctxt
   574                 else []
   575             val atpset_thms =
   576                 if !include_atpset then ResAxioms.atpset_rules_of ctxt
   577                 else []
   578             val _ = (Output.debug (fn () => "ATP theorems: ");  app display_thm atpset_thms)
   579         in  claset_thms @ simpset_thms @ atpset_thms  end
   580       val user_rules = filter check_named
   581                          (map ResAxioms.pairname
   582                            (if null user_thms then !whitelist else user_thms))
   583   in
   584       (filter check_named included_thms, user_rules)
   585   end;
   586 
   587 (***************************************************************)
   588 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
   589 (***************************************************************)
   590 
   591 fun add_classes (sorts, cset) = foldl setinsert cset (List.concat sorts);
   592 
   593 (*Remove this trivial type class*)
   594 fun delete_type cset = Symtab.delete_safe "HOL.type" cset;
   595 
   596 fun tvar_classes_of_terms ts =
   597   let val sorts_list = map (map #2 o term_tvars) ts
   598   in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
   599 
   600 fun tfree_classes_of_terms ts =
   601   let val sorts_list = map (map #2 o term_tfrees) ts
   602   in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
   603 
   604 (*fold type constructors*)
   605 fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
   606   | fold_type_consts f T x = x;
   607 
   608 val add_type_consts_in_type = fold_type_consts setinsert;
   609 
   610 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
   611 fun add_type_consts_in_term thy =
   612   let val const_typargs = Sign.const_typargs thy
   613       fun add_tcs (Const cT) x = fold add_type_consts_in_type (const_typargs cT) x
   614         | add_tcs (Abs (_, T, u)) x = add_tcs u x
   615         | add_tcs (t $ u) x = add_tcs t (add_tcs u x)
   616         | add_tcs _ x = x
   617   in  add_tcs  end
   618 
   619 fun type_consts_of_terms thy ts =
   620   Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
   621 
   622 
   623 (***************************************************************)
   624 (* ATP invocation methods setup                                *)
   625 (***************************************************************)
   626 
   627 fun cnf_hyps_thms ctxt =
   628     let val ths = Assumption.prems_of ctxt
   629     in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end;
   630 
   631 (*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
   632 datatype mode = Auto | Fol | Hol;
   633 
   634 val linkup_logic_mode = ref Auto;
   635 
   636 (*Ensures that no higher-order theorems "leak out"*)
   637 fun restrict_to_logic thy logic cls =
   638   if is_fol_logic logic then filter (Meson.is_fol_term thy o prop_of o fst) cls
   639                         else cls;
   640 
   641 (**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****)
   642 
   643 (** Too general means, positive equality literal with a variable X as one operand,
   644   when X does not occur properly in the other operand. This rules out clearly
   645   inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **)
   646 
   647 fun occurs ix =
   648     let fun occ(Var (jx,_)) = (ix=jx)
   649           | occ(t1$t2)      = occ t1 orelse occ t2
   650           | occ(Abs(_,_,t)) = occ t
   651           | occ _           = false
   652     in occ end;
   653 
   654 fun is_recordtype T = not (null (RecordPackage.dest_recTs T));
   655 
   656 (*Unwanted equalities include
   657   (1) those between a variable that does not properly occur in the second operand,
   658   (2) those between a variable and a record, since these seem to be prolific "cases" thms
   659 *)
   660 fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T
   661   | too_general_eqterms _ = false;
   662 
   663 fun too_general_equality (Const ("op =", _) $ x $ y) =
   664       too_general_eqterms (x,y) orelse too_general_eqterms(y,x)
   665   | too_general_equality _ = false;
   666 
   667 (* tautologous? *)
   668 fun is_taut (Const ("Trueprop", _) $ Const ("True", _)) = true
   669   | is_taut _ = false;
   670 
   671 (*True if the term contains a variable whose (atomic) type is in the given list.*)
   672 fun has_typed_var tycons =
   673   let fun var_tycon (Var (_, Type(a,_))) = a mem_string tycons
   674         | var_tycon _ = false
   675   in  exists var_tycon o term_vars  end;
   676 
   677 (*Clauses are forbidden to contain variables of these types. The typical reason is that
   678   they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=().
   679   The resulting clause will have no type constraint, yielding false proofs. Even "bool"
   680   leads to many unsound proofs, though (obviously) only for higher-order problems.*)
   681 val unwanted_types = ref ["Product_Type.unit","bool"];
   682 
   683 fun unwanted t =
   684     is_taut t orelse has_typed_var (!unwanted_types) t orelse
   685     forall too_general_equality (dest_disj t);
   686 
   687 (*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
   688   likely to lead to unsound proofs.*)
   689 fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
   690 
   691 fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =
   692     if is_fol_logic logic
   693     then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
   694     else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) user_lemmas;
   695 
   696 fun dfg_writer logic goals filename (axioms,classrels,arities) user_lemmas =
   697     if is_fol_logic logic
   698     then ResClause.dfg_write_file goals filename (axioms, classrels, arities)
   699     else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities) user_lemmas;
   700 
   701 (*Called by the oracle-based methods declared in res_atp_methods.ML*)
   702 fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
   703     let val conj_cls = make_clauses conjectures
   704                          |> ResAxioms.assume_abstract_list "subgoal" |> Meson.finish_cnf
   705         val hyp_cls = cnf_hyps_thms ctxt
   706         val goal_cls = conj_cls@hyp_cls
   707         val goal_tms = map prop_of goal_cls
   708         val thy = ProofContext.theory_of ctxt
   709         val logic = case mode of
   710                             Auto => problem_logic_goals [goal_tms]
   711                           | Fol => FOL
   712                           | Hol => HOL
   713         val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
   714         val cla_simp_atp_clauses = included_thms
   715                                      |> ResAxioms.cnf_rules_pairs |> make_unique
   716                                      |> restrict_to_logic thy logic
   717                                      |> remove_unwanted_clauses
   718         val user_cls = ResAxioms.cnf_rules_pairs user_rules
   719         val axclauses = make_unique (get_relevant_clauses thy cla_simp_atp_clauses user_cls goal_tms)
   720         val subs = tfree_classes_of_terms goal_tms
   721         and axtms = map (prop_of o #1) axclauses
   722         val supers = tvar_classes_of_terms axtms
   723         and tycons = type_consts_of_terms thy (goal_tms@axtms)
   724         (*TFrees in conjecture clauses; TVars in axiom clauses*)
   725         val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
   726         val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   727         val writer = if dfg then dfg_writer else tptp_writer
   728         and file = atp_input_file()
   729         and user_lemmas_names = map #1 user_rules
   730     in
   731         writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
   732         Output.debug (fn () => "Writing to " ^ file);
   733         file
   734     end;
   735 
   736 
   737 (**** remove tmp files ****)
   738 fun cond_rm_tmp file =
   739     if !Output.debugging orelse !destdir <> ""
   740     then Output.debug (fn () => "ATP input kept...")
   741     else OS.FileSys.remove file;
   742 
   743 
   744 (****** setup ATPs as Isabelle methods ******)
   745 
   746 fun atp_meth tac ths ctxt =
   747     let val thy = ProofContext.theory_of ctxt
   748         val _ = ResClause.init thy
   749         val _ = ResHolClause.init thy
   750     in Method.SIMPLE_METHOD' (tac ctxt ths) end;
   751 
   752 fun atp_method tac = Method.thms_ctxt_args (atp_meth tac);
   753 
   754 (***************************************************************)
   755 (* automatic ATP invocation                                    *)
   756 (***************************************************************)
   757 
   758 (* call prover with settings and problem file for the current subgoal *)
   759 fun watcher_call_provers sign sg_terms (childin, childout, pid) =
   760   let
   761     fun make_atp_list [] n = []
   762       | make_atp_list (sg_term::xs) n =
   763           let
   764             val probfile = prob_pathname n
   765             val time = Int.toString (!time_limit)
   766           in
   767             Output.debug (fn () => "problem file in watcher_call_provers is " ^ probfile);
   768             (*options are separated by Watcher.setting_sep, currently #"%"*)
   769             if !prover = "spass"
   770             then
   771               let val spass = helper_path "SPASS_HOME" "SPASS"
   772                   val sopts =
   773    "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
   774               in
   775                   ("spass", spass, sopts, probfile) :: make_atp_list xs (n+1)
   776               end
   777             else if !prover = "vampire"
   778             then
   779               let val vampire = helper_path "VAMPIRE_HOME" "vampire"
   780                   val vopts = "--mode casc%-t " ^ time  (*what about -m 100000?*)
   781               in
   782                   ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1)
   783               end
   784              else if !prover = "E"
   785              then
   786                let val Eprover = helper_path "E_HOME" "eproof"
   787                in
   788                   ("E", Eprover,
   789                      "--tstp-in%--tstp-out%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) ::
   790                    make_atp_list xs (n+1)
   791                end
   792              else error ("Invalid prover name: " ^ !prover)
   793           end
   794 
   795     val atp_list = make_atp_list sg_terms 1
   796   in
   797     Watcher.callResProvers(childout,atp_list);
   798     Output.debug (fn () => "Sent commands to watcher!")
   799   end
   800 
   801 (*For debugging the generated set of theorem names*)
   802 fun trace_vector fname =
   803   let val path = File.explode_platform_path (fname ^ "_thm_names")
   804   in  Vector.app (File.append path o (fn s => s ^ "\n"))  end;
   805 
   806 (*We write out problem files for each subgoal. Argument probfile generates filenames,
   807   and allows the suppression of the suffix "_1" in problem-generation mode.
   808   FIXME: does not cope with &&, and it isn't easy because one could have multiple
   809   subgoals, each involving &&.*)
   810 fun write_problem_files probfile (ctxt,th)  =
   811   let val goals = Thm.prems_of th
   812       val _ = Output.debug (fn () => "number of subgoals = " ^ Int.toString (length goals))
   813       val thy = ProofContext.theory_of ctxt
   814       fun get_neg_subgoals [] _ = []
   815         | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) ::
   816                                          get_neg_subgoals gls (n+1)
   817       val goal_cls = get_neg_subgoals goals 1
   818       val logic = case !linkup_logic_mode of
   819                 Auto => problem_logic_goals (map ((map prop_of)) goal_cls)
   820               | Fol => FOL
   821               | Hol => HOL
   822       val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
   823       val included_cls = included_thms |> ResAxioms.cnf_rules_pairs |> make_unique
   824                                        |> restrict_to_logic thy logic
   825                                        |> remove_unwanted_clauses
   826       val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls))
   827       val white_cls = ResAxioms.cnf_rules_pairs white_thms
   828       (*clauses relevant to goal gl*)
   829       val axcls_list = map (fn ngcls => get_relevant_clauses thy included_cls white_cls (map prop_of ngcls)) goal_cls
   830       val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls)))
   831                   axcls_list
   832       val writer = if !prover = "spass" then dfg_writer else tptp_writer
   833       fun write_all [] [] _ = []
   834         | write_all (ccls::ccls_list) (axcls::axcls_list) k =
   835             let val fname = probfile k
   836                 val _ = Output.debug (fn () => "About to write file " ^ fname)
   837                 val axcls = make_unique axcls
   838                 val _ = Output.debug (fn () => "Conjecture Clauses (before duplicate removal)")
   839                 val _ = app (fn th => Output.debug (fn _ => string_of_thm th)) ccls
   840                 val ccls = subtract_cls ccls axcls
   841                 val _ = Output.debug (fn () => "Conjecture Clauses (AFTER duplicate removal)")
   842                 val _ = app (fn th => Output.debug (fn _ => string_of_thm th)) ccls
   843                 val ccltms = map prop_of ccls
   844                 and axtms = map (prop_of o #1) axcls
   845                 val subs = tfree_classes_of_terms ccltms
   846                 and supers = tvar_classes_of_terms axtms
   847                 and tycons = type_consts_of_terms thy (ccltms@axtms)
   848                 (*TFrees in conjecture clauses; TVars in axiom clauses*)
   849                 val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
   850                 val _ = Output.debug (fn () => "arity clauses = " ^ Int.toString (length arity_clauses))
   851                 val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   852                 val _ = Output.debug (fn () => "classrel clauses = " ^ Int.toString (length classrel_clauses))
   853                 val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
   854                 val thm_names = Vector.fromList clnames
   855                 val _ = if !Output.debugging then trace_vector fname thm_names else ()
   856             in  (thm_names,fname) :: write_all ccls_list axcls_list (k+1)  end
   857       val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
   858   in
   859       (filenames, thm_names_list)
   860   end;
   861 
   862 val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream *
   863                                     Posix.Process.pid * string list) option);
   864 
   865 fun kill_last_watcher () =
   866     (case !last_watcher_pid of
   867          NONE => ()
   868        | SOME (_, _, pid, files) =>
   869           (Output.debug (fn () => "Killing old watcher, pid = " ^ string_of_pid pid);
   870            Watcher.killWatcher pid;
   871            ignore (map (try cond_rm_tmp) files)))
   872      handle OS.SysErr _ => Output.debug (fn () => "Attempt to kill watcher failed");
   873 
   874 (*writes out the current problems and calls ATPs*)
   875 fun isar_atp (ctxt, th) =
   876   if Thm.no_prems th then ()
   877   else
   878     let
   879       val _ = kill_last_watcher()
   880       val (files,thm_names_list) = write_problem_files prob_pathname (ctxt,th)
   881       val (childin, childout, pid) = Watcher.createWatcher (ctxt, th, thm_names_list)
   882     in
   883       last_watcher_pid := SOME (childin, childout, pid, files);
   884       Output.debug (fn () => "problem files: " ^ space_implode ", " files);
   885       Output.debug (fn () => "pid: " ^ string_of_pid pid);
   886       watcher_call_provers (Thm.theory_of_thm th) (Thm.prems_of th) (childin, childout, pid)
   887     end;
   888 
   889 (*For ML scripts, and primarily, for debugging*)
   890 fun callatp () =
   891   let val th = topthm()
   892       val ctxt = ProofContext.init (theory_of_thm th)
   893   in  isar_atp (ctxt, th)  end;
   894 
   895 val isar_atp_writeonly = setmp print_mode []
   896       (fn (ctxt,th) =>
   897        if Thm.no_prems th then ()
   898        else
   899          let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix
   900                             else prob_pathname
   901          in ignore (write_problem_files probfile (ctxt,th)) end);
   902 
   903 
   904 (** the Isar toplevel command **)
   905 
   906 fun sledgehammer state =
   907   let
   908     val (ctxt, (_, goal)) = Proof.get_goal (Toplevel.proof_of state);
   909     val thy = ProofContext.theory_of ctxt;
   910   in
   911     Output.debug (fn () => "subgoals in isar_atp:\n" ^
   912                   Pretty.string_of (ProofContext.pretty_term ctxt
   913                     (Logic.mk_conjunction_list (Thm.prems_of goal))));
   914     Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
   915     inc hook_count;
   916     Output.debug (fn () => "in hook for time: " ^ Int.toString (!hook_count));
   917     ResClause.init thy;
   918     ResHolClause.init thy;
   919     if !time_limit > 0 then isar_atp (ctxt, goal)
   920     else (warning ("Writing problem file only: " ^ !problem_name);
   921           isar_atp_writeonly (ctxt, goal))
   922   end;
   923 
   924 val _ = OuterSyntax.add_parsers
   925   [OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag
   926     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer))];
   927 
   928 end;