src/HOL/Tools/res_atp.ML
author paulson
Fri Nov 10 20:58:48 2006 +0100 (2006-11-10)
changeset 21290 33b6bb5d6ab8
parent 21243 afffe1f72143
child 21311 3556301c18cd
permissions -rw-r--r--
Improvement to classrel clauses: now outputs the minimum needed.
Theorem names: trying to minimize the number of multiple theorem names presented
     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 := 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.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 add_multi_names ((a, []), pairs) = pairs
   589   | add_multi_names ((a, [th]), pairs) = (a,th)::pairs
   590   | add_multi_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
   591 
   592 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
   593 
   594 (*The single theorems go BEFORE the multiple ones*)
   595 fun name_thm_pairs ctxt = 
   596   let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
   597   in  foldl add_multi_names (foldl add_multi_names [] mults) singles  end;
   598 
   599 fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false)
   600   | check_named (_,th) = true;
   601 
   602 (* get lemmas from claset, simpset, atpset and extra supplied rules *)
   603 fun get_clasimp_atp_lemmas ctxt user_thms = 
   604   let val included_thms =
   605 	if !include_all 
   606 	then (tap (fn ths => Output.debug
   607 	             ("Including all " ^ Int.toString (length ths) ^ " theorems")) 
   608 	          (name_thm_pairs ctxt))
   609 	else 
   610 	let val claset_thms =
   611 		if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt
   612 		else []
   613 	    val simpset_thms = 
   614 		if !include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt
   615 		else []
   616 	    val atpset_thms =
   617 		if !include_atpset then ResAxioms.atpset_rules_of_ctxt ctxt
   618 		else []
   619 	    val _ = if !Output.show_debug_msgs 
   620 		    then (Output.debug "ATP theorems: "; display_thms atpset_thms) 
   621 		    else ()		 
   622 	in  claset_thms @ simpset_thms @ atpset_thms  end
   623       val user_rules = filter check_named 
   624                          (map (ResAxioms.pairname)
   625 			   (if null user_thms then !whitelist else user_thms))
   626   in
   627       (filter check_named included_thms, user_rules)
   628   end;
   629 
   630 (*Remove lemmas that are banned from the backlist. Also remove duplicates. *)
   631 fun blacklist_filter thms = 
   632   if !run_blacklist_filter then 
   633       let val _ = Output.debug("blacklist filter gets " ^ Int.toString (length thms) ^ " theorems")
   634           val banned = make_banned_test (map #1 thms)
   635 	  fun ok (a,_) = not (banned a)
   636 	  val okthms = filter ok thms
   637           val _ = Output.debug("...and returns " ^ Int.toString (length okthms))
   638       in  okthms end
   639   else thms;
   640 
   641 (***************************************************************)
   642 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
   643 (***************************************************************)
   644 
   645 fun setinsert (x,s) = Symtab.update (x,()) s;
   646 
   647 fun add_classes (sorts, cset) = foldl setinsert cset (List.concat sorts);
   648 
   649 (*Remove this trivial type class*)
   650 fun delete_type cset = Symtab.delete_safe "HOL.type" cset;
   651 
   652 fun tvar_classes_of_terms ts =
   653   let val sorts_list = map (map #2 o term_tvars) ts
   654   in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
   655 
   656 fun tfree_classes_of_terms ts =
   657   let val sorts_list = map (map #2 o term_tfrees) ts
   658   in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
   659 
   660 (***************************************************************)
   661 (* ATP invocation methods setup                                *)
   662 (***************************************************************)
   663 
   664 fun cnf_hyps_thms ctxt = 
   665     let val ths = Assumption.prems_of ctxt
   666     in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end;
   667 
   668 (*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
   669 datatype mode = Auto | Fol | Hol;
   670 
   671 val linkup_logic_mode = ref Auto;
   672 
   673 (*Ensures that no higher-order theorems "leak out"*)
   674 fun restrict_to_logic logic cls =
   675   if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o fst) cls 
   676 	                else cls;
   677 
   678 fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =
   679     if is_fol_logic logic 
   680     then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
   681     else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) user_lemmas;
   682 
   683 fun dfg_writer logic goals filename (axioms,classrels,arities) user_lemmas =
   684     if is_fol_logic logic 
   685     then ResClause.dfg_write_file goals filename (axioms, classrels, arities)
   686     else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities) user_lemmas;
   687 
   688 (*Called by the oracle-based methods declared in res_atp_methods.ML*)
   689 fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
   690     let val conj_cls = make_clauses conjectures 
   691                          |> ResAxioms.assume_abstract_list |> Meson.finish_cnf
   692 	val hyp_cls = cnf_hyps_thms ctxt
   693 	val goal_cls = conj_cls@hyp_cls
   694 	val logic = case mode of 
   695                             Auto => problem_logic_goals [map prop_of goal_cls]
   696 			  | Fol => FOL
   697 			  | Hol => HOL
   698 	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
   699 	val cla_simp_atp_clauses = included_thms |> blacklist_filter
   700 	                             |> ResAxioms.cnf_rules_pairs |> make_unique 
   701                                      |> restrict_to_logic logic 
   702 	val user_cls = ResAxioms.cnf_rules_pairs user_rules
   703 	val thy = ProofContext.theory_of ctxt
   704 	val axclauses = get_relevant_clauses thy cla_simp_atp_clauses
   705 	                            user_cls (map prop_of goal_cls) |> make_unique
   706 	val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
   707         val subs = tfree_classes_of_terms (map prop_of goal_cls)
   708         and supers = tvar_classes_of_terms (map (prop_of o #1) axclauses)
   709         (*TFrees in conjecture clauses; TVars in axiom clauses*)
   710         val classrel_clauses = 
   711               if keep_types then ResClause.make_classrel_clauses thy subs supers
   712               else []
   713 	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
   714         val writer = if dfg then dfg_writer else tptp_writer 
   715 	and file = atp_input_file()
   716 	and user_lemmas_names = map #1 user_rules
   717     in
   718 	writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
   719 	Output.debug ("Writing to " ^ file);
   720 	file
   721     end;
   722 
   723 
   724 (**** remove tmp files ****)
   725 fun cond_rm_tmp file = 
   726     if !Output.show_debug_msgs orelse !destdir <> "" then Output.debug "ATP input kept..." 
   727     else OS.FileSys.remove file;
   728 
   729 
   730 (****** setup ATPs as Isabelle methods ******)
   731 fun atp_meth' tac ths ctxt = 
   732     Method.SIMPLE_METHOD' HEADGOAL
   733     (tac ctxt ths);
   734 
   735 fun atp_meth tac ths ctxt = 
   736     let val thy = ProofContext.theory_of ctxt
   737 	val _ = ResClause.init thy
   738 	val _ = ResHolClause.init thy
   739     in
   740 	atp_meth' tac ths ctxt
   741     end;
   742 
   743 fun atp_method tac = Method.thms_ctxt_args (atp_meth tac);
   744 
   745 (***************************************************************)
   746 (* automatic ATP invocation                                    *)
   747 (***************************************************************)
   748 
   749 (* call prover with settings and problem file for the current subgoal *)
   750 fun watcher_call_provers sign sg_terms (childin, childout, pid) =
   751   let
   752     fun make_atp_list [] n = []
   753       | make_atp_list (sg_term::xs) n =
   754           let
   755             val probfile = prob_pathname n
   756             val time = Int.toString (!time_limit)
   757           in
   758             Output.debug ("problem file in watcher_call_provers is " ^ probfile);
   759             (*options are separated by Watcher.setting_sep, currently #"%"*)
   760             if !prover = "spass"
   761             then
   762               let val spass = helper_path "SPASS_HOME" "SPASS"
   763                   val sopts =
   764    "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
   765               in 
   766                   ("spass", spass, sopts, probfile) :: make_atp_list xs (n+1)
   767               end
   768             else if !prover = "vampire"
   769 	    then 
   770               let val vampire = helper_path "VAMPIRE_HOME" "vampire"
   771                   val vopts = "--mode casc%-t " ^ time  (*what about -m 100000?*)
   772               in
   773                   ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1)
   774               end
   775       	     else if !prover = "E"
   776       	     then
   777 	       let val Eprover = helper_path "E_HOME" "eproof"
   778 	       in
   779 		  ("E", Eprover, 
   780 		     "--tptp-in%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) ::
   781 		   make_atp_list xs (n+1)
   782 	       end
   783 	     else error ("Invalid prover name: " ^ !prover)
   784           end
   785 
   786     val atp_list = make_atp_list sg_terms 1
   787   in
   788     Watcher.callResProvers(childout,atp_list);
   789     Output.debug "Sent commands to watcher!"
   790   end
   791   
   792 fun trace_array fname =
   793   let val path = File.unpack_platform_path fname
   794   in  Array.app (File.append path o (fn s => s ^ "\n"))  end;
   795 
   796 (*Converting a subgoal into negated conjecture clauses*)
   797 fun neg_clauses th n =
   798   let val tacs = [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac]
   799       val st = Seq.hd (EVERY' tacs n th)
   800       val negs = Option.valOf (metahyps_thms n st)
   801   in make_clauses negs |> ResAxioms.assume_abstract_list |> Meson.finish_cnf end;
   802 		                       
   803 (*We write out problem files for each subgoal. Argument probfile generates filenames,
   804   and allows the suppression of the suffix "_1" in problem-generation mode.
   805   FIXME: does not cope with &&, and it isn't easy because one could have multiple
   806   subgoals, each involving &&.*)
   807 fun write_problem_files probfile (ctxt,th)  =
   808   let val goals = Thm.prems_of th
   809       val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
   810       val thy = ProofContext.theory_of ctxt
   811       fun get_neg_subgoals [] _ = []
   812         | get_neg_subgoals (gl::gls) n = neg_clauses th n :: get_neg_subgoals gls (n+1)
   813       val goal_cls = get_neg_subgoals goals 1
   814       val logic = case !linkup_logic_mode of
   815 		Auto => problem_logic_goals (map ((map prop_of)) goal_cls)
   816 	      | Fol => FOL
   817 	      | Hol => HOL
   818       val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
   819       val included_cls = included_thms |> blacklist_filter
   820                                        |> ResAxioms.cnf_rules_pairs |> make_unique 
   821                                        |> restrict_to_logic logic 
   822       val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls))
   823       val white_cls = ResAxioms.cnf_rules_pairs white_thms
   824       (*clauses relevant to goal gl*)
   825       val axcls_list = map (fn gl => get_relevant_clauses thy included_cls white_cls [gl])
   826                            goals
   827       val _ = app (fn axcls => Output.debug ("filtered clauses = " ^ Int.toString(length axcls)))
   828                   axcls_list
   829       val keep_types = if is_fol_logic logic then !ResClause.keep_types 
   830                        else is_typed_hol ()
   831       val arity_clauses = if keep_types then ResClause.arity_clause_thy thy 
   832                           else []
   833       val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
   834       val writer = if !prover = "spass" then dfg_writer else tptp_writer 
   835       fun write_all [] [] _ = []
   836 	| write_all (ccls::ccls_list) (axcls::axcls_list) k =
   837             let val fname = probfile k
   838                 val axcls = make_unique axcls
   839                 val ccls = subtract_cls ccls axcls
   840                 val subs = tfree_classes_of_terms (map prop_of ccls)
   841                 and supers = tvar_classes_of_terms (map (prop_of o #1) axcls)
   842                 (*TFrees in conjecture clauses; TVars in axiom clauses*)
   843                 val classrel_clauses = 
   844                       if keep_types then ResClause.make_classrel_clauses thy subs supers
   845                       else []
   846                 val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
   847                 val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
   848                 val thm_names = Array.fromList clnames
   849                 val _ = if !Output.show_debug_msgs 
   850                         then trace_array (fname ^ "_thm_names") thm_names else ()
   851             in  (thm_names,fname) :: write_all ccls_list axcls_list (k+1)  end
   852       val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
   853   in
   854       (filenames, thm_names_list)
   855   end;
   856 
   857 val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
   858                                     Posix.Process.pid * string list) option);
   859 
   860 fun kill_last_watcher () =
   861     (case !last_watcher_pid of 
   862          NONE => ()
   863        | SOME (_, _, pid, files) => 
   864 	  (Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid);
   865 	   Watcher.killWatcher pid;  
   866 	   ignore (map (try cond_rm_tmp) files)))
   867      handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed";
   868 
   869 (*writes out the current clasimpset to a tptp file;
   870   turns off xsymbol at start of function, restoring it at end    *)
   871 fun isar_atp_body (ctxt, th) =
   872   if Thm.no_prems th then ()
   873   else
   874     let
   875       val _ = kill_last_watcher()
   876       val (files,thm_names_list) = write_problem_files prob_pathname (ctxt,th)
   877       val (childin, childout, pid) = Watcher.createWatcher (th, thm_names_list)
   878     in
   879       last_watcher_pid := SOME (childin, childout, pid, files);
   880       Output.debug ("problem files: " ^ space_implode ", " files); 
   881       Output.debug ("pid: " ^ string_of_pid pid);
   882       watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
   883     end;
   884 
   885 val isar_atp = setmp print_mode [] isar_atp_body;
   886 
   887 (*For ML scripts, and primarily, for debugging*)
   888 fun callatp () = 
   889   let val th = topthm()
   890       val ctxt = ProofContext.init (theory_of_thm th)
   891   in  isar_atp_body (ctxt, th)  end;
   892 
   893 val isar_atp_writeonly = setmp print_mode [] 
   894       (fn (ctxt,th) =>
   895        if Thm.no_prems th then ()
   896        else 
   897          let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix 
   898           	            else prob_pathname
   899          in ignore (write_problem_files probfile (ctxt,th)) end);
   900 
   901 
   902 (** the Isar toplevel hook **)
   903 
   904 fun invoke_atp_ml (ctxt, goal) =
   905   let val thy = ProofContext.theory_of ctxt;
   906   in
   907     Output.debug ("subgoals in isar_atp:\n" ^ 
   908 		  Pretty.string_of (ProofContext.pretty_term ctxt
   909 		    (Logic.mk_conjunction_list (Thm.prems_of goal))));
   910     Output.debug ("current theory: " ^ Context.theory_name thy);
   911     inc hook_count;
   912     Output.debug ("in hook for time: " ^ Int.toString (!hook_count));
   913     ResClause.init thy;
   914     ResHolClause.init thy;
   915     if !time_limit > 0 then isar_atp (ctxt, goal)
   916     else (warning "Writing problem file only"; isar_atp_writeonly (ctxt, goal))
   917   end;
   918 
   919 val invoke_atp = Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep
   920  (fn state =>
   921   let val (ctxt, (_, goal)) = Proof.get_goal (Toplevel.proof_of state)
   922   in  invoke_atp_ml (ctxt, goal)  end);
   923 
   924 val call_atpP =
   925   OuterSyntax.command 
   926     "ProofGeneral.call_atp" 
   927     "call automatic theorem provers" 
   928     OuterKeyword.diag
   929     (Scan.succeed invoke_atp);
   930 
   931 val _ = OuterSyntax.add_parsers [call_atpP];
   932 
   933 end;