src/HOL/Tools/res_atp.ML
author wenzelm
Wed Nov 08 13:48:29 2006 +0100 (2006-11-08)
changeset 21243 afffe1f72143
parent 21224 f86b8463af37
child 21290 33b6bb5d6ab8
permissions -rw-r--r--
removed theory NatArith (now part of Nat);
     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 fol_keep_types: bool ref
    35   val hol_full_types: unit -> unit
    36   val hol_partial_types: unit -> unit
    37   val hol_const_types_only: unit -> unit
    38   val hol_no_types: unit -> unit
    39   val hol_typ_level: unit -> ResHolClause.type_level
    40   val include_all: bool ref
    41   val run_relevance_filter: bool ref
    42   val run_blacklist_filter: bool ref
    43   val blacklist: string list ref
    44   val add_all : unit -> unit
    45   val add_claset : unit -> unit
    46   val add_simpset : unit -> unit
    47   val add_clasimp : unit -> unit
    48   val add_atpset : unit -> unit
    49   val rm_all : unit -> unit
    50   val rm_claset : unit -> unit
    51   val rm_simpset : unit -> unit
    52   val rm_atpset : unit -> unit
    53   val rm_clasimp : unit -> unit
    54 end;
    55 
    56 structure ResAtp =
    57 struct
    58 
    59 fun timestamp s = Output.debug ("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 := 80;
    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.unpack_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.unpack_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 fol_keep_types = ResClause.keep_types;
   138 val hol_full_types = ResHolClause.full_types;
   139 val hol_partial_types = ResHolClause.partial_types;
   140 val hol_const_types_only = ResHolClause.const_types_only;
   141 val hol_no_types = ResHolClause.no_types;
   142 fun hol_typ_level () = ResHolClause.find_typ_level ();
   143 fun is_typed_hol () = 
   144     let val tp_level = hol_typ_level()
   145     in
   146 	not (tp_level = ResHolClause.T_NONE)
   147     end;
   148 
   149 fun atp_input_file () =
   150     let val file = !problem_name 
   151     in
   152 	if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file))
   153 	else if File.exists (File.unpack_platform_path (!destdir))
   154 	then !destdir ^ "/" ^ file
   155 	else error ("No such directory: " ^ !destdir)
   156     end;
   157 
   158 val include_all = ref true;
   159 val include_simpset = ref false;
   160 val include_claset = ref false; 
   161 val include_atpset = ref true;
   162 
   163 (*Tests show that follow_defs gives VERY poor results with "include_all"*)
   164 fun add_all() = (include_all:=true; ReduceAxiomsN.follow_defs := false);
   165 fun rm_all() = include_all:=false;
   166 
   167 fun add_simpset() = include_simpset:=true;
   168 fun rm_simpset() = include_simpset:=false;
   169 
   170 fun add_claset() = include_claset:=true;
   171 fun rm_claset() = include_claset:=false;
   172 
   173 fun add_clasimp() = (include_simpset:=true;include_claset:=true);
   174 fun rm_clasimp() = (include_simpset:=false;include_claset:=false);
   175 
   176 fun add_atpset() = include_atpset:=true;
   177 fun rm_atpset() = include_atpset:=false;
   178 
   179 
   180 (**** relevance filter ****)
   181 val run_relevance_filter = ReduceAxiomsN.run_relevance_filter;
   182 val run_blacklist_filter = ref true;
   183 
   184 (******************************************************************)
   185 (* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *)
   186 (******************************************************************)
   187 
   188 datatype logic = FOL | HOL | HOLC | HOLCS;
   189 
   190 fun string_of_logic FOL = "FOL"
   191   | string_of_logic HOL = "HOL"
   192   | string_of_logic HOLC = "HOLC"
   193   | string_of_logic HOLCS = "HOLCS";
   194 
   195 fun is_fol_logic FOL = true
   196   | is_fol_logic  _ = false
   197 
   198 (*HOLCS will not occur here*)
   199 fun upgrade_lg HOLC _ = HOLC
   200   | upgrade_lg HOL HOLC = HOLC
   201   | upgrade_lg HOL _ = HOL
   202   | upgrade_lg FOL lg = lg; 
   203 
   204 (* check types *)
   205 fun has_bool_hfn (Type("bool",_)) = true
   206   | has_bool_hfn (Type("fun",_)) = true
   207   | has_bool_hfn (Type(_, Ts)) = exists has_bool_hfn Ts
   208   | has_bool_hfn _ = false;
   209 
   210 fun is_hol_fn tp =
   211     let val (targs,tr) = strip_type tp
   212     in
   213 	exists (has_bool_hfn) (tr::targs)
   214     end;
   215 
   216 fun is_hol_pred tp =
   217     let val (targs,tr) = strip_type tp
   218     in
   219 	exists (has_bool_hfn) targs
   220     end;
   221 
   222 exception FN_LG of term;
   223 
   224 fun fn_lg (t as Const(f,tp)) (lg,seen) = 
   225     if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) 
   226   | fn_lg (t as Free(f,tp)) (lg,seen) = 
   227     if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) 
   228   | fn_lg (t as Var(f,tp)) (lg,seen) =
   229     if is_hol_fn tp then (upgrade_lg HOL lg,insert (op =) t seen) else (lg,insert (op =) t seen)
   230   | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,insert (op =) t seen)
   231   | fn_lg f _ = raise FN_LG(f); 
   232 
   233 
   234 fun term_lg [] (lg,seen) = (lg,seen)
   235   | term_lg (tm::tms) (FOL,seen) =
   236       let val (f,args) = strip_comb tm
   237 	  val (lg',seen') = if f mem seen then (FOL,seen) 
   238 			    else fn_lg f (FOL,seen)
   239       in
   240 	if is_fol_logic lg' then ()
   241         else Output.debug ("Found a HOL term: " ^ Display.raw_string_of_term f);
   242         term_lg (args@tms) (lg',seen')
   243       end
   244   | term_lg _ (lg,seen) = (lg,seen)
   245 
   246 exception PRED_LG of term;
   247 
   248 fun pred_lg (t as Const(P,tp)) (lg,seen)= 
   249       if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) 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) else (lg,insert (op =) t seen)
   252   | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, insert (op =) t seen)
   253   | pred_lg P _ = raise PRED_LG(P);
   254 
   255 
   256 fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen)
   257   | lit_lg P (lg,seen) =
   258       let val (pred,args) = strip_comb P
   259 	  val (lg',seen') = if pred mem seen then (lg,seen) 
   260 			    else pred_lg pred (lg,seen)
   261       in
   262 	if is_fol_logic lg' then ()
   263 	else Output.debug ("Found a HOL predicate: " ^ Display.raw_string_of_term pred);
   264 	term_lg args (lg',seen')
   265       end;
   266 
   267 fun lits_lg [] (lg,seen) = (lg,seen)
   268   | lits_lg (lit::lits) (FOL,seen) =
   269       let val (lg,seen') = lit_lg lit (FOL,seen)
   270       in
   271 	if is_fol_logic lg then ()
   272 	else Output.debug ("Found a HOL literal: " ^ Display.raw_string_of_term lit);
   273 	lits_lg lits (lg,seen')
   274       end
   275   | lits_lg lits (lg,seen) = (lg,seen);
   276 
   277 fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs = 
   278     dest_disj_aux t (dest_disj_aux t' disjs)
   279   | dest_disj_aux t disjs = t::disjs;
   280 
   281 fun dest_disj t = dest_disj_aux t [];
   282 
   283 fun logic_of_clause tm (lg,seen) =
   284     let val tm' = HOLogic.dest_Trueprop tm
   285 	val disjs = dest_disj tm'
   286     in
   287 	lits_lg disjs (lg,seen)
   288     end;
   289 
   290 fun logic_of_clauses [] (lg,seen) = (lg,seen)
   291   | logic_of_clauses (cls::clss) (FOL,seen) =
   292     let val (lg,seen') = logic_of_clause cls (FOL,seen)
   293 	val _ =
   294           if is_fol_logic lg then ()
   295           else Output.debug ("Found a HOL clause: " ^ Display.raw_string_of_term cls)
   296     in
   297 	logic_of_clauses clss (lg,seen')
   298     end
   299   | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
   300 
   301 fun problem_logic_goals_aux [] (lg,seen) = lg
   302   | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) = 
   303     problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen));
   304     
   305 fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]);
   306 
   307 (***************************************************************)
   308 (* Retrieving and filtering lemmas                             *)
   309 (***************************************************************)
   310 
   311 (*** white list and black list of lemmas ***)
   312 
   313 (*The rule subsetI is frequently omitted by the relevance filter.*)
   314 val whitelist = ref [subsetI]; 
   315 
   316 (*Names of theorems and theorem lists to be banned. The final numeric suffix of
   317   theorem lists is first removed.
   318 
   319   These theorems typically produce clauses that are prolific (match too many equality or
   320   membership literals) and relate to seldom-used facts. Some duplicate other rules.
   321   FIXME: this blacklist needs to be maintained using theory data and added to using
   322   an attribute.*)
   323 val blacklist = ref
   324   ["Datatype.prod.size",
   325    "Datatype.unit.exhaust", (*"unit" thms cause unsound proofs; unit.nchotomy is caught automatically*)
   326    "Datatype.unit.induct", 
   327    "Datatype.unit.inducts",
   328    "Datatype.unit.split_asm", 
   329    "Datatype.unit.split",
   330    "Datatype.unit.splits",
   331    "Divides.dvd_0_left_iff",
   332    "Finite_Set.card_0_eq",
   333    "Finite_Set.card_infinite",
   334    "Finite_Set.Max_ge",
   335    "Finite_Set.Max_in",
   336    "Finite_Set.Max_le_iff",
   337    "Finite_Set.Max_less_iff",
   338    "Finite_Set.max.f_below_strict_below.below_f_conv", (*duplicates in Orderings.*)
   339    "Finite_Set.max.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
   340    "Finite_Set.Min_ge_iff",
   341    "Finite_Set.Min_gr_iff",
   342    "Finite_Set.Min_in",
   343    "Finite_Set.Min_le",
   344    "Finite_Set.min_max.below_inf_sup_Inf_Sup.inf_Sup_absorb", 
   345    "Finite_Set.min_max.below_inf_sup_Inf_Sup.sup_Inf_absorb", 
   346    "Finite_Set.min.f_below_strict_below.below_f_conv",        (*duplicates in Orderings.*)
   347    "Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
   348    "Fun.vimage_image_eq",   (*involves an existential quantifier*)
   349    "HOL.split_if_asm",     (*splitting theorem*)
   350    "HOL.split_if",         (*splitting theorem*)
   351    "IntDef.abs_split",
   352    "IntDef.Integ.Abs_Integ_inject",
   353    "IntDef.Integ.Abs_Integ_inverse",
   354    "IntDiv.zdvd_0_left",
   355    "List.append_eq_append_conv",
   356    "List.hd_Cons_tl",   (*Says everything is [] or Cons. Probably prolific.*)
   357    "List.in_listsD",
   358    "List.in_listsI",
   359    "List.lists.Cons",
   360    "List.listsE",
   361    "Nat.less_one", (*not directional? obscure*)
   362    "Nat.not_gr0",
   363    "Nat.one_eq_mult_iff", (*duplicate by symmetry*)
   364    "Nat.of_nat_0_eq_iff",
   365    "Nat.of_nat_eq_0_iff",
   366    "Nat.of_nat_le_0_iff",
   367    "NatSimprocs.divide_le_0_iff_number_of",  (*too many clauses*)
   368    "NatSimprocs.divide_less_0_iff_number_of",
   369    "NatSimprocs.equation_minus_iff_1",  (*not directional*)
   370    "NatSimprocs.equation_minus_iff_number_of", (*not directional*)
   371    "NatSimprocs.le_minus_iff_1", (*not directional*)
   372    "NatSimprocs.le_minus_iff_number_of",  (*not directional*)
   373    "NatSimprocs.less_minus_iff_1", (*not directional*)
   374    "NatSimprocs.less_minus_iff_number_of", (*not directional*)
   375    "NatSimprocs.minus_equation_iff_number_of", (*not directional*)
   376    "NatSimprocs.minus_le_iff_1", (*not directional*)
   377    "NatSimprocs.minus_le_iff_number_of", (*not directional*)
   378    "NatSimprocs.minus_less_iff_1", (*not directional*)
   379    "NatSimprocs.mult_le_cancel_left_number_of", (*excessive case analysis*)
   380    "NatSimprocs.mult_le_cancel_right_number_of", (*excessive case analysis*)
   381    "NatSimprocs.mult_less_cancel_left_number_of", (*excessive case analysis*)
   382    "NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*)
   383    "NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*)
   384    "NatSimprocs.zero_less_divide_iff_number_of",
   385    "OrderedGroup.abs_0_eq", (*duplicate by symmetry*)
   386    "OrderedGroup.diff_eq_0_iff_eq", (*prolific?*)
   387    "OrderedGroup.join_0_eq_0",
   388    "OrderedGroup.meet_0_eq_0",
   389    "OrderedGroup.pprt_eq_0",   (*obscure*)
   390    "OrderedGroup.pprt_eq_id",   (*obscure*)
   391    "OrderedGroup.pprt_mono",   (*obscure*)
   392    "Orderings.split_max",      (*splitting theorem*)
   393    "Orderings.split_min",      (*splitting theorem*)
   394    "Parity.even_nat_power",   (*obscure, somewhat prolilfic*)
   395    "Parity.power_eq_0_iff_number_of",
   396    "Parity.power_le_zero_eq_number_of",   (*obscure and prolific*)
   397    "Parity.power_less_zero_eq_number_of",
   398    "Parity.zero_le_power_eq_number_of",   (*obscure and prolific*)
   399    "Parity.zero_less_power_eq_number_of",   (*obscure and prolific*)
   400    "Power.zero_less_power_abs_iff",
   401    "Product_Type.split_eta_SetCompr",   (*involves an existential quantifier*)
   402    "Product_Type.split_paired_Ball_Sigma",     (*splitting theorem*)
   403    "Product_Type.split_paired_Bex_Sigma",      (*splitting theorem*)
   404    "Product_Type.split_split_asm",             (*splitting theorem*)
   405    "Product_Type.split_split",                 (*splitting theorem*)
   406    "Product_Type.unit_abs_eta_conv",
   407    "Product_Type.unit_induct",
   408    "Relation.diagI",
   409    "Relation.Domain_def",   (*involves an existential quantifier*)
   410    "Relation.Image_def",   (*involves an existential quantifier*)
   411    "Relation.ImageI",
   412    "Ring_and_Field.divide_cancel_left", (*fields are seldom used & often prolific*)
   413    "Ring_and_Field.divide_cancel_right",
   414    "Ring_and_Field.divide_divide_eq_left",
   415    "Ring_and_Field.divide_divide_eq_right",
   416    "Ring_and_Field.divide_eq_0_iff",
   417    "Ring_and_Field.divide_eq_1_iff",
   418    "Ring_and_Field.divide_eq_eq_1",
   419    "Ring_and_Field.divide_le_0_1_iff",
   420    "Ring_and_Field.divide_le_eq_1_neg",  (*obscure and prolific*)
   421    "Ring_and_Field.divide_le_eq_1_pos",  (*obscure and prolific*)
   422    "Ring_and_Field.divide_less_0_1_iff",
   423    "Ring_and_Field.divide_less_eq_1_neg",  (*obscure and prolific*)
   424    "Ring_and_Field.divide_less_eq_1_pos",  (*obscure and prolific*)
   425    "Ring_and_Field.eq_divide_eq_1", (*duplicate by symmetry*)
   426    "Ring_and_Field.field_mult_cancel_left",
   427    "Ring_and_Field.field_mult_cancel_right",
   428    "Ring_and_Field.inverse_le_iff_le_neg",
   429    "Ring_and_Field.inverse_le_iff_le",
   430    "Ring_and_Field.inverse_less_iff_less_neg",
   431    "Ring_and_Field.inverse_less_iff_less",
   432    "Ring_and_Field.le_divide_eq_1_neg", (*obscure and prolific*)
   433    "Ring_and_Field.le_divide_eq_1_pos", (*obscure and prolific*)
   434    "Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*)
   435    "Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*)
   436    "Ring_and_Field.one_eq_divide_iff",  (*duplicate by symmetry*)
   437    "Set.ball_simps", "Set.bex_simps",   (*quantifier rewriting: useless*)
   438    "Set.Collect_bex_eq",   (*involves an existential quantifier*)
   439    "Set.Collect_ex_eq",   (*involves an existential quantifier*)
   440    "Set.Diff_eq_empty_iff", (*redundant with paramodulation*)
   441    "Set.Diff_insert0",
   442    "Set.disjoint_insert",
   443    "Set.empty_Union_conv",   (*redundant with paramodulation*)
   444    "Set.full_SetCompr_eq",   (*involves an existential quantifier*)
   445    "Set.image_Collect",      (*involves an existential quantifier*)
   446    "Set.image_def",          (*involves an existential quantifier*)
   447    "Set.insert_disjoint",
   448    "Set.Int_UNIV",  (*redundant with paramodulation*)
   449    "Set.Inter_iff", (*We already have InterI, InterE*)
   450    "Set.Inter_UNIV_conv",
   451    "Set.psubsetE",    (*too prolific and obscure*)
   452    "Set.psubsetI",
   453    "Set.singleton_insert_inj_eq'",
   454    "Set.singleton_insert_inj_eq",
   455    "Set.singletonD",  (*these two duplicate some "insert" lemmas*)
   456    "Set.singletonI",
   457    "Set.Un_empty", (*redundant with paramodulation*)
   458    "Set.UNION_def",   (*involves an existential quantifier*)
   459    "Set.Union_empty_conv", (*redundant with paramodulation*)
   460    "Set.Union_iff",              (*We already have UnionI, UnionE*)
   461    "SetInterval.atLeastAtMost_iff", (*obscure and prolific*)
   462    "SetInterval.atLeastLessThan_iff", (*obscure and prolific*)
   463    "SetInterval.greaterThanAtMost_iff", (*obscure and prolific*)
   464    "SetInterval.greaterThanLessThan_iff", (*obscure and prolific*)
   465    "SetInterval.ivl_subset"];  (*excessive case analysis*)
   466 
   467 
   468 (*These might be prolific but are probably OK, and min and max are basic.
   469    "Orderings.max_less_iff_conj", 
   470    "Orderings.min_less_iff_conj",
   471    "Orderings.min_max.below_inf.below_inf_conv",
   472    "Orderings.min_max.below_sup.above_sup_conv",
   473 Very prolific and somewhat obscure:
   474    "Set.InterD",
   475    "Set.UnionI",
   476 *)
   477 
   478 (*** retrieve lemmas from clasimpset and atpset, may filter them ***)
   479 
   480 (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
   481 
   482 exception HASH_CLAUSE and HASH_STRING;
   483 
   484 (*Catches (for deletion) theorems automatically generated from other theorems*)
   485 fun insert_suffixed_names ht x = 
   486      (Polyhash.insert ht (x^"_iff1", ()); 
   487       Polyhash.insert ht (x^"_iff2", ()); 
   488       Polyhash.insert ht (x^"_dest", ())); 
   489 
   490 (*Are all characters in this string digits?*)
   491 fun all_numeric s = null (String.tokens Char.isDigit s);
   492 
   493 (*Delete a suffix of the form _\d+*)
   494 fun delete_numeric_suffix s =
   495   case rev (String.fields (fn c => c = #"_") s) of
   496       last::rest => 
   497           if all_numeric last 
   498           then [s, space_implode "_" (rev rest)]
   499           else [s]
   500     | [] => [s];
   501 
   502 fun banned_thmlist s =
   503   (Sign.base_name s) mem_string ["induct","inducts","split","splits","split_asm"];
   504 
   505 (*Reject theorems with names like "List.filter.filter_list_def" or
   506   "Accessible_Part.acc.defs", as these are definitions arising from packages.
   507   FIXME: this will also block definitions within locales*)
   508 fun is_package_def a =
   509    length (NameSpace.unpack a) > 2 andalso 
   510    String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a;
   511 
   512 fun make_banned_test xs = 
   513   let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
   514                                 (6000, HASH_STRING)
   515       fun banned_aux s = 
   516             isSome (Polyhash.peek ht s) orelse banned_thmlist s orelse is_package_def s
   517       fun banned s = exists banned_aux (delete_numeric_suffix s)
   518   in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
   519       app (insert_suffixed_names ht) (!blacklist @ xs); 
   520       banned
   521   end;
   522 
   523 (** a hash function from Term.term to int, and also a hash table **)
   524 val xor_words = List.foldl Word.xorb 0w0;
   525 
   526 fun hashw_term ((Const(c,_)), w) = Polyhash.hashw_string (c,w)
   527   | hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w)
   528   | hashw_term ((Var(_,_)), w) = w
   529   | hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w)
   530   | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
   531   | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));
   532 
   533 fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0))
   534   | hash_literal P = hashw_term(P,0w0);
   535 
   536 
   537 fun get_literals (Const("Trueprop",_)$P) lits = get_literals P lits
   538   | get_literals (Const("op |",_)$P$Q) lits = get_literals Q (get_literals P lits)
   539   | get_literals lit lits = (lit::lits);
   540 
   541 fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t [])));
   542 
   543 fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
   544 
   545 (*Create a hash table for clauses, of the given size*)
   546 fun mk_clause_table n =
   547       Polyhash.mkTable (hash_term o prop_of, equal_thm)
   548                        (n, HASH_CLAUSE);
   549 
   550 (*Use a hash table to eliminate duplicates from xs. Argument is a list of
   551   (thm * (string * int)) tuples. The theorems are hashed into the table. *)
   552 fun make_unique xs = 
   553   let val ht = mk_clause_table 7000
   554   in
   555       Output.debug("make_unique gets " ^ Int.toString (length xs) ^ " clauses");
   556       app (ignore o Polyhash.peekInsert ht) xs;  
   557       Polyhash.listItems ht
   558   end;
   559 
   560 (*Remove existing axiom clauses from the conjecture clauses, as this can dramatically
   561   boost an ATP's performance (for some reason)*)
   562 fun subtract_cls c_clauses ax_clauses = 
   563   let val ht = mk_clause_table 2200
   564       fun known x = isSome (Polyhash.peek ht x)
   565   in
   566       app (ignore o Polyhash.peekInsert ht) ax_clauses;  
   567       filter (not o known) c_clauses 
   568   end;
   569 
   570 (*Filter axiom clauses, but keep supplied clauses and clauses in whitelist. 
   571   Duplicates are removed later.*)
   572 fun get_relevant_clauses thy cls_thms white_cls goals =
   573   white_cls @ (ReduceAxiomsN.relevance_filter thy cls_thms goals);
   574 
   575 fun display_thms [] = ()
   576   | display_thms ((name,thm)::nthms) = 
   577       let val nthm = name ^ ": " ^ (string_of_thm thm)
   578       in Output.debug nthm; display_thms nthms  end;
   579  
   580 fun all_valid_thms ctxt =
   581   PureThy.thms_containing (ProofContext.theory_of ctxt) ([], []) @
   582   filter (ProofContext.valid_thms ctxt)
   583     (FactIndex.find (ProofContext.fact_index_of ctxt) ([], []));
   584 
   585 fun multi_name a (th, (n,pairs)) = 
   586   (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs)
   587 
   588 fun multi_names ((a, []), pairs) = pairs
   589   | multi_names ((a, [th]), pairs) = (a,th)::pairs
   590   | multi_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
   591 
   592 fun name_thm_pairs ctxt = foldl multi_names [] (all_valid_thms ctxt);
   593 
   594 fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false)
   595   | check_named (_,th) = true;
   596 
   597 (* get lemmas from claset, simpset, atpset and extra supplied rules *)
   598 fun get_clasimp_atp_lemmas ctxt user_thms = 
   599   let val included_thms =
   600 	if !include_all 
   601 	then (tap (fn ths => Output.debug
   602 	             ("Including all " ^ Int.toString (length ths) ^ " theorems")) 
   603 	          (name_thm_pairs ctxt))
   604 	else 
   605 	let val claset_thms =
   606 		if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt
   607 		else []
   608 	    val simpset_thms = 
   609 		if !include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt
   610 		else []
   611 	    val atpset_thms =
   612 		if !include_atpset then ResAxioms.atpset_rules_of_ctxt ctxt
   613 		else []
   614 	    val _ = if !Output.show_debug_msgs 
   615 		    then (Output.debug "ATP theorems: "; display_thms atpset_thms) 
   616 		    else ()		 
   617 	in  claset_thms @ simpset_thms @ atpset_thms  end
   618       val user_rules = filter check_named 
   619                          (map (ResAxioms.pairname)
   620 			   (if null user_thms then !whitelist else user_thms))
   621   in
   622       (filter check_named included_thms, user_rules)
   623   end;
   624 
   625 (*Remove lemmas that are banned from the backlist. Also remove duplicates. *)
   626 fun blacklist_filter thms = 
   627   if !run_blacklist_filter then 
   628       let val _ = Output.debug("blacklist filter gets " ^ Int.toString (length thms) ^ " theorems")
   629           val banned = make_banned_test (map #1 thms)
   630 	  fun ok (a,_) = not (banned a)
   631 	  val okthms = filter ok thms
   632           val _ = Output.debug("...and returns " ^ Int.toString (length okthms))
   633       in  okthms end
   634   else thms;
   635 
   636 
   637 (***************************************************************)
   638 (* ATP invocation methods setup                                *)
   639 (***************************************************************)
   640 
   641 fun cnf_hyps_thms ctxt = 
   642     let val ths = Assumption.prems_of ctxt
   643     in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end;
   644 
   645 (*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
   646 datatype mode = Auto | Fol | Hol;
   647 
   648 val linkup_logic_mode = ref Auto;
   649 
   650 (*Ensures that no higher-order theorems "leak out"*)
   651 fun restrict_to_logic logic cls =
   652   if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o fst) cls 
   653 	                else cls;
   654 
   655 fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =
   656     if is_fol_logic logic 
   657     then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
   658     else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) user_lemmas;
   659 
   660 fun dfg_writer logic goals filename (axioms,classrels,arities) user_lemmas =
   661     if is_fol_logic logic 
   662     then ResClause.dfg_write_file goals filename (axioms, classrels, arities)
   663     else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities) user_lemmas;
   664 
   665 (*Called by the oracle-based methods declared in res_atp_methods.ML*)
   666 fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
   667     let val conj_cls = make_clauses conjectures 
   668                          |> ResAxioms.assume_abstract_list |> Meson.finish_cnf
   669 	val hyp_cls = cnf_hyps_thms ctxt
   670 	val goal_cls = conj_cls@hyp_cls
   671 	val logic = case mode of 
   672                             Auto => problem_logic_goals [map prop_of goal_cls]
   673 			  | Fol => FOL
   674 			  | Hol => HOL
   675 	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
   676 	val cla_simp_atp_clauses = included_thms |> blacklist_filter
   677 	                             |> ResAxioms.cnf_rules_pairs |> make_unique 
   678                                      |> restrict_to_logic logic 
   679 	val user_cls = ResAxioms.cnf_rules_pairs user_rules
   680 	val thy = ProofContext.theory_of ctxt
   681 	val axclauses = get_relevant_clauses thy cla_simp_atp_clauses
   682 	                            user_cls (map prop_of goal_cls) |> make_unique
   683 	val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
   684 	val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
   685 	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
   686         val writer = if dfg then dfg_writer else tptp_writer 
   687 	and file = atp_input_file()
   688 	and user_lemmas_names = map #1 user_rules
   689     in
   690 	writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
   691 	Output.debug ("Writing to " ^ file);
   692 	file
   693     end;
   694 
   695 
   696 (**** remove tmp files ****)
   697 fun cond_rm_tmp file = 
   698     if !Output.show_debug_msgs orelse !destdir <> "" then Output.debug "ATP input kept..." 
   699     else OS.FileSys.remove file;
   700 
   701 
   702 (****** setup ATPs as Isabelle methods ******)
   703 fun atp_meth' tac ths ctxt = 
   704     Method.SIMPLE_METHOD' HEADGOAL
   705     (tac ctxt ths);
   706 
   707 fun atp_meth tac ths ctxt = 
   708     let val thy = ProofContext.theory_of ctxt
   709 	val _ = ResClause.init thy
   710 	val _ = ResHolClause.init thy
   711     in
   712 	atp_meth' tac ths ctxt
   713     end;
   714 
   715 fun atp_method tac = Method.thms_ctxt_args (atp_meth tac);
   716 
   717 (***************************************************************)
   718 (* automatic ATP invocation                                    *)
   719 (***************************************************************)
   720 
   721 (* call prover with settings and problem file for the current subgoal *)
   722 fun watcher_call_provers sign sg_terms (childin, childout, pid) =
   723   let
   724     fun make_atp_list [] n = []
   725       | make_atp_list (sg_term::xs) n =
   726           let
   727             val probfile = prob_pathname n
   728             val time = Int.toString (!time_limit)
   729           in
   730             Output.debug ("problem file in watcher_call_provers is " ^ probfile);
   731             (*options are separated by Watcher.setting_sep, currently #"%"*)
   732             if !prover = "spass"
   733             then
   734               let val spass = helper_path "SPASS_HOME" "SPASS"
   735                   val sopts =
   736    "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
   737               in 
   738                   ("spass", spass, sopts, probfile) :: make_atp_list xs (n+1)
   739               end
   740             else if !prover = "vampire"
   741 	    then 
   742               let val vampire = helper_path "VAMPIRE_HOME" "vampire"
   743                   val vopts = "--mode casc%-t " ^ time  (*what about -m 100000?*)
   744               in
   745                   ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1)
   746               end
   747       	     else if !prover = "E"
   748       	     then
   749 	       let val Eprover = helper_path "E_HOME" "eproof"
   750 	       in
   751 		  ("E", Eprover, 
   752 		     "--tptp-in%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) ::
   753 		   make_atp_list xs (n+1)
   754 	       end
   755 	     else error ("Invalid prover name: " ^ !prover)
   756           end
   757 
   758     val atp_list = make_atp_list sg_terms 1
   759   in
   760     Watcher.callResProvers(childout,atp_list);
   761     Output.debug "Sent commands to watcher!"
   762   end
   763   
   764 fun trace_array fname =
   765   let val path = File.unpack_platform_path fname
   766   in  Array.app (File.append path o (fn s => s ^ "\n"))  end;
   767 
   768 (*Converting a subgoal into negated conjecture clauses*)
   769 fun neg_clauses th n =
   770   let val tacs = [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac]
   771       val st = Seq.hd (EVERY' tacs n th)
   772       val negs = Option.valOf (metahyps_thms n st)
   773   in make_clauses negs |> ResAxioms.assume_abstract_list |> Meson.finish_cnf end;
   774 		                       
   775 (*We write out problem files for each subgoal. Argument probfile generates filenames,
   776   and allows the suppression of the suffix "_1" in problem-generation mode.
   777   FIXME: does not cope with &&, and it isn't easy because one could have multiple
   778   subgoals, each involving &&.*)
   779 fun write_problem_files probfile (ctxt,th)  =
   780   let val goals = Thm.prems_of th
   781       val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
   782       val thy = ProofContext.theory_of ctxt
   783       fun get_neg_subgoals [] _ = []
   784         | get_neg_subgoals (gl::gls) n = neg_clauses th n :: get_neg_subgoals gls (n+1)
   785       val goal_cls = get_neg_subgoals goals 1
   786       val logic = case !linkup_logic_mode of
   787 		Auto => problem_logic_goals (map ((map prop_of)) goal_cls)
   788 	      | Fol => FOL
   789 	      | Hol => HOL
   790       val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
   791       val included_cls = included_thms |> blacklist_filter
   792                                        |> ResAxioms.cnf_rules_pairs |> make_unique 
   793                                        |> restrict_to_logic logic 
   794       val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls))
   795       val white_cls = ResAxioms.cnf_rules_pairs white_thms
   796       (*clauses relevant to goal gl*)
   797       val axcls_list = map (fn gl => get_relevant_clauses thy included_cls white_cls [gl])
   798                            goals
   799       val _ = app (fn axcls => Output.debug ("filtered clauses = " ^ Int.toString(length axcls)))
   800                   axcls_list
   801       val keep_types = if is_fol_logic logic then !ResClause.keep_types 
   802                        else is_typed_hol ()
   803       val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy
   804                              else []
   805       val _ = Output.debug ("classrel clauses = " ^ 
   806                             Int.toString (length classrel_clauses))
   807       val arity_clauses = if keep_types then ResClause.arity_clause_thy thy 
   808                           else []
   809       val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
   810       val writer = if !prover = "spass" then dfg_writer else tptp_writer 
   811       fun write_all [] [] _ = []
   812 	| write_all (ccls::ccls_list) (axcls::axcls_list) k =
   813             let val fname = probfile k
   814                 val axcls = make_unique axcls
   815                 val ccls = subtract_cls ccls axcls
   816                 val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
   817                 val thm_names = Array.fromList clnames
   818                 val _ = if !Output.show_debug_msgs 
   819                         then trace_array (fname ^ "_thm_names") thm_names else ()
   820             in  (thm_names,fname) :: write_all ccls_list axcls_list (k+1)  end
   821       val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
   822   in
   823       (filenames, thm_names_list)
   824   end;
   825 
   826 val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
   827                                     Posix.Process.pid * string list) option);
   828 
   829 fun kill_last_watcher () =
   830     (case !last_watcher_pid of 
   831          NONE => ()
   832        | SOME (_, _, pid, files) => 
   833 	  (Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid);
   834 	   Watcher.killWatcher pid;  
   835 	   ignore (map (try cond_rm_tmp) files)))
   836      handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed";
   837 
   838 (*writes out the current clasimpset to a tptp file;
   839   turns off xsymbol at start of function, restoring it at end    *)
   840 fun isar_atp_body (ctxt, th) =
   841   if Thm.no_prems th then ()
   842   else
   843     let
   844       val _ = kill_last_watcher()
   845       val (files,thm_names_list) = write_problem_files prob_pathname (ctxt,th)
   846       val (childin, childout, pid) = Watcher.createWatcher (th, thm_names_list)
   847     in
   848       last_watcher_pid := SOME (childin, childout, pid, files);
   849       Output.debug ("problem files: " ^ space_implode ", " files); 
   850       Output.debug ("pid: " ^ string_of_pid pid);
   851       watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
   852     end;
   853 
   854 val isar_atp = setmp print_mode [] isar_atp_body;
   855 
   856 (*For ML scripts, and primarily, for debugging*)
   857 fun callatp () = 
   858   let val th = topthm()
   859       val ctxt = ProofContext.init (theory_of_thm th)
   860   in  isar_atp_body (ctxt, th)  end;
   861 
   862 val isar_atp_writeonly = setmp print_mode [] 
   863       (fn (ctxt,th) =>
   864        if Thm.no_prems th then ()
   865        else 
   866          let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix 
   867           	            else prob_pathname
   868          in ignore (write_problem_files probfile (ctxt,th)) end);
   869 
   870 
   871 (** the Isar toplevel hook **)
   872 
   873 fun invoke_atp_ml (ctxt, goal) =
   874   let val thy = ProofContext.theory_of ctxt;
   875   in
   876     Output.debug ("subgoals in isar_atp:\n" ^ 
   877 		  Pretty.string_of (ProofContext.pretty_term ctxt
   878 		    (Logic.mk_conjunction_list (Thm.prems_of goal))));
   879     Output.debug ("current theory: " ^ Context.theory_name thy);
   880     inc hook_count;
   881     Output.debug ("in hook for time: " ^ Int.toString (!hook_count));
   882     ResClause.init thy;
   883     ResHolClause.init thy;
   884     if !time_limit > 0 then isar_atp (ctxt, goal)
   885     else (warning "Writing problem file only"; isar_atp_writeonly (ctxt, goal))
   886   end;
   887 
   888 val invoke_atp = Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep
   889  (fn state =>
   890   let val (ctxt, (_, goal)) = Proof.get_goal (Toplevel.proof_of state)
   891   in  invoke_atp_ml (ctxt, goal)  end);
   892 
   893 val call_atpP =
   894   OuterSyntax.command 
   895     "ProofGeneral.call_atp" 
   896     "call automatic theorem provers" 
   897     OuterKeyword.diag
   898     (Scan.succeed invoke_atp);
   899 
   900 val _ = OuterSyntax.add_parsers [call_atpP];
   901 
   902 end;