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