src/HOL/Tools/res_atp.ML
author webertj
Thu Aug 31 14:36:48 2006 +0200 (2006-08-31)
changeset 20446 7e616709bca2
parent 20444 6c5e38a73db0
child 20457 85414caac94a
permissions -rw-r--r--
String.concatWith (not available in PolyML) replaced by space_implode
     1 (*  Author: Jia Meng, Cambridge University Computer Laboratory, NICTA
     2     ID: $Id$
     3     Copyright 2004 University of Cambridge
     4 
     5 ATPs with TPTP format input.
     6 *)
     7 
     8 signature RES_ATP =
     9 sig
    10   val prover: string ref
    11   val custom_spass: string list ref
    12   val destdir: string ref
    13   val helper_path: string -> string -> string
    14   val problem_name: string ref
    15   val time_limit: int ref
    16    
    17   datatype mode = Auto | Fol | Hol
    18   val linkup_logic_mode : mode ref
    19   val write_subgoal_file: bool -> mode -> Proof.context -> thm list -> thm list -> int -> string
    20   val vampire_time: int ref
    21   val eprover_time: int ref
    22   val spass_time: int ref
    23   val run_vampire: int -> unit
    24   val run_eprover: int -> unit
    25   val run_spass: int -> unit
    26   val vampireLimit: unit -> int
    27   val eproverLimit: unit -> int
    28   val spassLimit: unit -> int
    29   val atp_method: (Proof.context -> thm list -> int -> tactic) ->
    30     Method.src -> Proof.context -> Proof.method
    31   val cond_rm_tmp: string -> unit
    32   val keep_atp_input: bool ref
    33   val fol_keep_types: bool ref
    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 end;
    54 
    55 structure ResAtp : RES_ATP =
    56 struct
    57 
    58 (********************************************************************)
    59 (* some settings for both background automatic ATP calling procedure*)
    60 (* and also explicit ATP invocation methods                         *)
    61 (********************************************************************)
    62 
    63 (*** background linkup ***)
    64 val call_atp = ref false; 
    65 val hook_count = ref 0;
    66 val time_limit = ref 80;
    67 val prover = ref "E";   (* use E as the default prover *)
    68 val custom_spass =   (*specialized options for SPASS*)
    69       ref ["-Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub"];
    70 val destdir = ref "";   (*Empty means write files to /tmp*)
    71 val problem_name = ref "prob";
    72 
    73 (*Return the path to a "helper" like SPASS or tptp2X, first checking that
    74   it exists.  FIXME: modify to use Path primitives and move to some central place.*)  
    75 fun helper_path evar base =
    76   case getenv evar of
    77       "" => error  ("Isabelle environment variable " ^ evar ^ " not defined")
    78     | home => 
    79         let val path = home ^ "/" ^ base
    80         in  if File.exists (File.unpack_platform_path path) then path 
    81 	    else error ("Could not find the file " ^ path)
    82 	end;  
    83 
    84 fun probfile_nosuffix _ = 
    85   if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
    86   else if File.exists (File.unpack_platform_path (!destdir))
    87   then !destdir ^ "/" ^ !problem_name
    88   else error ("No such directory: " ^ !destdir);
    89 
    90 fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n;
    91 
    92 
    93 (*** ATP methods ***)
    94 val vampire_time = ref 60;
    95 val eprover_time = ref 60;
    96 val spass_time = ref 60;
    97 
    98 fun run_vampire time =  
    99     if (time >0) then vampire_time:= time
   100     else vampire_time:=60;
   101 
   102 fun run_eprover time = 
   103     if (time > 0) then eprover_time:= time
   104     else eprover_time:=60;
   105 
   106 fun run_spass time = 
   107     if (time > 0) then spass_time:=time
   108     else spass_time:=60;
   109 
   110 
   111 fun vampireLimit () = !vampire_time;
   112 fun eproverLimit () = !eprover_time;
   113 fun spassLimit () = !spass_time;
   114 
   115 val keep_atp_input = ref false;
   116 val fol_keep_types = ResClause.keep_types;
   117 val hol_full_types = ResHolClause.full_types;
   118 val hol_partial_types = ResHolClause.partial_types;
   119 val hol_const_types_only = ResHolClause.const_types_only;
   120 val hol_no_types = ResHolClause.no_types;
   121 fun hol_typ_level () = ResHolClause.find_typ_level ();
   122 fun is_typed_hol () = 
   123     let val tp_level = hol_typ_level()
   124     in
   125 	not (tp_level = ResHolClause.T_NONE)
   126     end;
   127 val include_combS = ResHolClause.include_combS;
   128 val include_min_comb = ResHolClause.include_min_comb;
   129 
   130 fun atp_input_file () =
   131     let val file = !problem_name 
   132     in
   133 	if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file))
   134 	else if File.exists (File.unpack_platform_path (!destdir))
   135 	then !destdir ^ "/" ^ file
   136 	else error ("No such directory: " ^ !destdir)
   137     end;
   138 
   139 val include_all = ref false;
   140 val include_simpset = ref false;
   141 val include_claset = ref false; 
   142 val include_atpset = ref true;
   143 
   144 (*Tests show that follow_defs gives VERY poor results with "include_all"*)
   145 fun add_all() = (include_all:=true; ReduceAxiomsN.follow_defs := false);
   146 fun rm_all() = include_all:=false;
   147 
   148 fun add_simpset() = include_simpset:=true;
   149 fun rm_simpset() = include_simpset:=false;
   150 
   151 fun add_claset() = include_claset:=true;
   152 fun rm_claset() = include_claset:=false;
   153 
   154 fun add_clasimp() = (include_simpset:=true;include_claset:=true);
   155 fun rm_clasimp() = (include_simpset:=false;include_claset:=false);
   156 
   157 fun add_atpset() = include_atpset:=true;
   158 fun rm_atpset() = include_atpset:=false;
   159 
   160 
   161 (**** relevance filter ****)
   162 val run_relevance_filter = ref true;
   163 val run_blacklist_filter = ref true;
   164 
   165 (******************************************************************)
   166 (* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *)
   167 (******************************************************************)
   168 
   169 datatype logic = FOL | HOL | HOLC | HOLCS;
   170 
   171 fun string_of_logic FOL = "FOL"
   172   | string_of_logic HOL = "HOL"
   173   | string_of_logic HOLC = "HOLC"
   174   | string_of_logic HOLCS = "HOLCS";
   175 
   176 
   177 fun is_fol_logic FOL = true
   178   | is_fol_logic  _ = false
   179 
   180 
   181 (*HOLCS will not occur here*)
   182 fun upgrade_lg HOLC _ = HOLC
   183   | upgrade_lg HOL HOLC = HOLC
   184   | upgrade_lg HOL _ = HOL
   185   | upgrade_lg FOL lg = lg; 
   186 
   187 (* check types *)
   188 fun has_bool_hfn (Type("bool",_)) = true
   189   | has_bool_hfn (Type("fun",_)) = true
   190   | has_bool_hfn (Type(_, Ts)) = exists has_bool_hfn Ts
   191   | has_bool_hfn _ = false;
   192 
   193 fun is_hol_fn tp =
   194     let val (targs,tr) = strip_type tp
   195     in
   196 	exists (has_bool_hfn) (tr::targs)
   197     end;
   198 
   199 fun is_hol_pred tp =
   200     let val (targs,tr) = strip_type tp
   201     in
   202 	exists (has_bool_hfn) targs
   203     end;
   204 
   205 exception FN_LG of term;
   206 
   207 fun fn_lg (t as Const(f,tp)) (lg,seen) = 
   208     if is_hol_fn tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
   209   | fn_lg (t as Free(f,tp)) (lg,seen) = 
   210     if is_hol_fn tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
   211   | fn_lg (t as Var(f,tp)) (lg,seen) =
   212     if is_hol_fn tp then (upgrade_lg HOL lg,t ins seen) else (lg,t ins seen)
   213   | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,t ins seen)
   214   | fn_lg f _ = raise FN_LG(f); 
   215 
   216 
   217 fun term_lg [] (lg,seen) = (lg,seen)
   218   | term_lg (tm::tms) (FOL,seen) =
   219     let val (f,args) = strip_comb tm
   220 	val (lg',seen') = if f mem seen then (FOL,seen) 
   221 			  else fn_lg f (FOL,seen)
   222 	val _ =
   223           if is_fol_logic lg' then ()
   224           else Output.debug ("Found a HOL term: " ^ Display.raw_string_of_term f)
   225 	 in
   226 	     term_lg (args@tms) (lg',seen')
   227     end
   228   | term_lg _ (lg,seen) = (lg,seen)
   229 
   230 exception PRED_LG of term;
   231 
   232 fun pred_lg (t as Const(P,tp)) (lg,seen)= 
   233     if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) 
   234   | pred_lg (t as Free(P,tp)) (lg,seen) =
   235     if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
   236   | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen)
   237   | pred_lg P _ = raise PRED_LG(P);
   238 
   239 
   240 fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen)
   241   | lit_lg P (lg,seen) =
   242     let val (pred,args) = strip_comb P
   243 	val (lg',seen') = if pred mem seen then (lg,seen) 
   244 			  else pred_lg pred (lg,seen)
   245 	val _ =
   246           if is_fol_logic lg' then ()
   247           else Output.debug ("Found a HOL predicate: " ^ Display.raw_string_of_term pred)
   248     in
   249 	term_lg args (lg',seen')
   250     end;
   251 
   252 fun lits_lg [] (lg,seen) = (lg,seen)
   253   | lits_lg (lit::lits) (FOL,seen) =
   254     let val (lg,seen') = lit_lg lit (FOL,seen)
   255 	val _ =
   256           if is_fol_logic lg then ()
   257           else Output.debug ("Found a HOL literal: " ^ Display.raw_string_of_term lit)
   258     in
   259 	lits_lg lits (lg,seen')
   260     end
   261   | lits_lg lits (lg,seen) = (lg,seen);
   262 
   263 
   264 fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs = 
   265     dest_disj_aux t (dest_disj_aux t' disjs)
   266   | dest_disj_aux t disjs = t::disjs;
   267 
   268 fun dest_disj t = dest_disj_aux t [];
   269 
   270 fun logic_of_clause tm (lg,seen) =
   271     let val tm' = HOLogic.dest_Trueprop tm
   272 	val disjs = dest_disj tm'
   273     in
   274 	lits_lg disjs (lg,seen)
   275     end;
   276 
   277 fun logic_of_clauses [] (lg,seen) = (lg,seen)
   278   | logic_of_clauses (cls::clss) (FOL,seen) =
   279     let val (lg,seen') = logic_of_clause cls (FOL,seen)
   280 	val _ =
   281           if is_fol_logic lg then ()
   282           else Output.debug ("Found a HOL clause: " ^ Display.raw_string_of_term cls)
   283     in
   284 	logic_of_clauses clss (lg,seen')
   285     end
   286   | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
   287 
   288 fun problem_logic_goals_aux [] (lg,seen) = lg
   289   | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) = 
   290     problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen));
   291     
   292 fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]);
   293 
   294 (***************************************************************)
   295 (* Retrieving and filtering lemmas                             *)
   296 (***************************************************************)
   297 
   298 (*** white list and black list of lemmas ***)
   299 
   300 (*The rule subsetI is frequently omitted by the relevance filter.*)
   301 val whitelist = ref [subsetI]; 
   302 
   303 (*Names of theorems and theorem lists to be banned. The final numeric suffix of
   304   theorem lists is first removed.
   305 
   306   These theorems typically produce clauses that are prolific (match too many equality or
   307   membership literals) and relate to seldom-used facts. Some duplicate other rules.
   308   FIXME: this blacklist needs to be maintained using theory data and added to using
   309   an attribute.*)
   310 val blacklist = ref
   311   ["Datatype.unit.split_asm",         (*These  "unit" thms cause unsound proofs*)
   312                                (*Datatype.unit.nchotomy is caught automatically*)
   313    "Datatype.unit.induct",
   314    "Datatype.unit.inducts",
   315    "Datatype.unit.split",
   316    "Datatype.unit.splits",
   317    "Product_Type.unit_abs_eta_conv",
   318    "Product_Type.unit_induct",
   319 
   320    "Datatype.prod.size",
   321    "Divides.dvd_0_left_iff",
   322    "Finite_Set.card_0_eq",
   323    "Finite_Set.card_infinite",
   324    "Finite_Set.Max_ge",
   325    "Finite_Set.Max_in",
   326    "Finite_Set.Max_le_iff",
   327    "Finite_Set.Max_less_iff",
   328    "Finite_Set.max.f_below_strict_below.below_f_conv", (*duplicates in Orderings.*)
   329    "Finite_Set.max.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
   330    "Finite_Set.Min_ge_iff",
   331    "Finite_Set.Min_gr_iff",
   332    "Finite_Set.Min_in",
   333    "Finite_Set.Min_le",
   334    "Finite_Set.min_max.below_inf_sup_Inf_Sup.inf_Sup_absorb", 
   335    "Finite_Set.min_max.below_inf_sup_Inf_Sup.sup_Inf_absorb", 
   336    "Finite_Set.min.f_below_strict_below.below_f_conv",        (*duplicates in Orderings.*)
   337    "Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
   338    "IntDef.Integ.Abs_Integ_inject",
   339    "IntDef.Integ.Abs_Integ_inverse",
   340    "IntDiv.zdvd_0_left",
   341    "List.append_eq_append_conv",
   342    "List.hd_Cons_tl",   (*Says everything is [] or Cons. Probably prolific.*)
   343    "List.in_listsD",
   344    "List.in_listsI",
   345    "List.lists.Cons",
   346    "List.listsE",
   347    "Nat.less_one", (*not directional? obscure*)
   348    "Nat.not_gr0",
   349    "Nat.one_eq_mult_iff", (*duplicate by symmetry*)
   350    "NatArith.of_nat_0_eq_iff",
   351    "NatArith.of_nat_eq_0_iff",
   352    "NatArith.of_nat_le_0_iff",
   353    "NatSimprocs.divide_le_0_iff_number_of",  (*too many clauses*)
   354    "NatSimprocs.divide_less_0_iff_number_of",
   355    "NatSimprocs.equation_minus_iff_1",  (*not directional*)
   356    "NatSimprocs.equation_minus_iff_number_of", (*not directional*)
   357    "NatSimprocs.le_minus_iff_1", (*not directional*)
   358    "NatSimprocs.le_minus_iff_number_of",  (*not directional*)
   359    "NatSimprocs.less_minus_iff_1", (*not directional*)
   360    "NatSimprocs.less_minus_iff_number_of", (*not directional*)
   361    "NatSimprocs.minus_equation_iff_number_of", (*not directional*)
   362    "NatSimprocs.minus_le_iff_1", (*not directional*)
   363    "NatSimprocs.minus_le_iff_number_of", (*not directional*)
   364    "NatSimprocs.minus_less_iff_1", (*not directional*)
   365    "NatSimprocs.mult_le_cancel_left_number_of", (*excessive case analysis*)
   366    "NatSimprocs.mult_le_cancel_right_number_of", (*excessive case analysis*)
   367    "NatSimprocs.mult_less_cancel_left_number_of", (*excessive case analysis*)
   368    "NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*)
   369    "NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*)
   370    "NatSimprocs.zero_less_divide_iff_number_of",
   371    "OrderedGroup.abs_0_eq", (*duplicate by symmetry*)
   372    "OrderedGroup.diff_eq_0_iff_eq", (*prolific?*)
   373    "OrderedGroup.join_0_eq_0",
   374    "OrderedGroup.meet_0_eq_0",
   375    "OrderedGroup.pprt_eq_0",   (*obscure*)
   376    "OrderedGroup.pprt_eq_id",   (*obscure*)
   377    "OrderedGroup.pprt_mono",   (*obscure*)
   378    "Parity.even_nat_power",   (*obscure, somewhat prolilfic*)
   379    "Parity.power_eq_0_iff_number_of",
   380    "Parity.power_le_zero_eq_number_of",   (*obscure and prolific*)
   381    "Parity.power_less_zero_eq_number_of",
   382    "Parity.zero_le_power_eq_number_of",   (*obscure and prolific*)
   383    "Parity.zero_less_power_eq_number_of",   (*obscure and prolific*)
   384    "Power.zero_less_power_abs_iff",
   385    "Relation.diagI",
   386    "Relation.ImageI",
   387    "Ring_and_Field.divide_cancel_left", (*fields are seldom used & often prolific*)
   388    "Ring_and_Field.divide_cancel_right",
   389    "Ring_and_Field.divide_divide_eq_left",
   390    "Ring_and_Field.divide_divide_eq_right",
   391    "Ring_and_Field.divide_eq_0_iff",
   392    "Ring_and_Field.divide_eq_1_iff",
   393    "Ring_and_Field.divide_eq_eq_1",
   394    "Ring_and_Field.divide_le_0_1_iff",
   395    "Ring_and_Field.divide_le_eq_1_neg",  (*obscure and prolific*)
   396    "Ring_and_Field.divide_le_eq_1_pos",  (*obscure and prolific*)
   397    "Ring_and_Field.divide_less_0_1_iff",
   398    "Ring_and_Field.divide_less_eq_1_neg",  (*obscure and prolific*)
   399    "Ring_and_Field.divide_less_eq_1_pos",  (*obscure and prolific*)
   400    "Ring_and_Field.eq_divide_eq_1", (*duplicate by symmetry*)
   401    "Ring_and_Field.field_mult_cancel_left",
   402    "Ring_and_Field.field_mult_cancel_right",
   403    "Ring_and_Field.inverse_le_iff_le_neg",
   404    "Ring_and_Field.inverse_le_iff_le",
   405    "Ring_and_Field.inverse_less_iff_less_neg",
   406    "Ring_and_Field.inverse_less_iff_less",
   407    "Ring_and_Field.le_divide_eq_1_neg", (*obscure and prolific*)
   408    "Ring_and_Field.le_divide_eq_1_pos", (*obscure and prolific*)
   409    "Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*)
   410    "Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*)
   411    "Ring_and_Field.one_eq_divide_iff",  (*duplicate by symmetry*)
   412    "Set.disjoint_insert",
   413    "Set.insert_disjoint",
   414    "Set.Inter_UNIV_conv",
   415    "Set.ball_simps", "Set.bex_simps",   (*quantifier rewriting: useless*)
   416    "Set.Diff_eq_empty_iff", (*redundant with paramodulation*)
   417    "Set.Diff_insert0",
   418    "Set.empty_Union_conv", (*redundant with paramodulation*)
   419    "Set.Int_UNIV", (*redundant with paramodulation*)
   420    "Set.Inter_iff",              (*We already have InterI, InterE*)
   421    "Set.psubsetE",    (*too prolific and obscure*)
   422    "Set.psubsetI",
   423    "Set.singleton_insert_inj_eq'",
   424    "Set.singleton_insert_inj_eq",
   425    "Set.singletonD",  (*these two duplicate some "insert" lemmas*)
   426    "Set.singletonI",
   427    "Set.Un_empty", (*redundant with paramodulation*)
   428    "Set.Union_empty_conv", (*redundant with paramodulation*)
   429    "Set.Union_iff",              (*We already have UnionI, UnionE*)
   430    "SetInterval.atLeastAtMost_iff", (*obscure and prolific*)
   431    "SetInterval.atLeastLessThan_iff", (*obscure and prolific*)
   432    "SetInterval.greaterThanAtMost_iff", (*obscure and prolific*)
   433    "SetInterval.greaterThanLessThan_iff", (*obscure and prolific*)
   434    "SetInterval.ivl_subset"];  (*excessive case analysis*)
   435 
   436 
   437 (*These might be prolific but are probably OK, and min and max are basic.
   438    "Orderings.max_less_iff_conj", 
   439    "Orderings.min_less_iff_conj",
   440    "Orderings.min_max.below_inf.below_inf_conv",
   441    "Orderings.min_max.below_sup.above_sup_conv",
   442 Very prolific and somewhat obscure:
   443    "Set.InterD",
   444    "Set.UnionI",
   445 *)
   446 
   447 (*** retrieve lemmas from clasimpset and atpset, may filter them ***)
   448 
   449 (*The "name" of a theorem is its statement, if nothing else is available.*)
   450 val plain_string_of_thm =
   451     setmp show_question_marks false 
   452       (setmp print_mode [] 
   453 	(Pretty.setmp_margin 999 string_of_thm));
   454 	
   455 (*Returns the first substring enclosed in quotation marks, typically omitting 
   456   the [.] of meta-level assumptions.*)
   457 val firstquoted = hd o (String.tokens (fn c => c = #"\""))
   458 	
   459 fun fake_thm_name th = 
   460     Context.theory_name (theory_of_thm th) ^ "." ^ firstquoted (plain_string_of_thm th);
   461 
   462 fun put_name_pair ("",th) = (fake_thm_name th, th)
   463   | put_name_pair (a,th)  = (a,th);
   464 
   465 (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
   466 
   467 exception HASH_CLAUSE and HASH_STRING;
   468 
   469 (*Catches (for deletion) theorems automatically generated from other theorems*)
   470 fun insert_suffixed_names ht x = 
   471      (Polyhash.insert ht (x^"_iff1", ()); 
   472       Polyhash.insert ht (x^"_iff2", ()); 
   473       Polyhash.insert ht (x^"_dest", ())); 
   474 
   475 (*Are all characters in this string digits?*)
   476 fun all_numeric s = null (String.tokens Char.isDigit s);
   477 
   478 (*Delete a suffix of the form _\d+*)
   479 fun delete_numeric_suffix s =
   480   case rev (String.fields (fn c => c = #"_") s) of
   481       last::rest => 
   482           if all_numeric last 
   483           then [s, space_implode "_" (rev rest)]
   484           else [s]
   485     | [] => [s];
   486 
   487 fun make_banned_test xs = 
   488   let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
   489                                 (6000, HASH_STRING)
   490       fun banned s = exists (fn s' => isSome (Polyhash.peek ht s')) 
   491                             (delete_numeric_suffix s)
   492   in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
   493       app (insert_suffixed_names ht) (!blacklist @ xs); 
   494       banned
   495   end;
   496 
   497 (** a hash function from Term.term to int, and also a hash table **)
   498 val xor_words = List.foldl Word.xorb 0w0;
   499 
   500 fun hashw_term ((Const(c,_)), w) = Polyhash.hashw_string (c,w)
   501   | hashw_term ((Free(_,_)), w) = w
   502   | hashw_term ((Var(_,_)), w) = w
   503   | hashw_term ((Bound _), w) = w
   504   | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
   505   | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));
   506 
   507 fun hashw_pred (P,w) = 
   508     let val (p,args) = strip_comb P
   509     in
   510 	List.foldl hashw_term w (p::args)
   511     end;
   512 
   513 fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_pred(P,0w0))
   514   | hash_literal P = hashw_pred(P,0w0);
   515 
   516 
   517 fun get_literals (Const("Trueprop",_)$P) lits = get_literals P lits
   518   | get_literals (Const("op |",_)$P$Q) lits = get_literals Q (get_literals P lits)
   519   | get_literals lit lits = (lit::lits);
   520 
   521 
   522 fun hash_term term = Word.toIntX (xor_words (map hash_literal (get_literals term [])));
   523 
   524 fun hash_thm  thm = hash_term (prop_of thm);
   525 
   526 fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
   527 (*Create a hash table for clauses, of the given size*)
   528 fun mk_clause_table n =
   529       Polyhash.mkTable (hash_thm, equal_thm)
   530                        (n, HASH_CLAUSE);
   531 
   532 (*Use a hash table to eliminate duplicates from xs*)
   533 fun make_unique ht xs = 
   534       (app (ignore o Polyhash.peekInsert ht) xs;  Polyhash.listItems ht);
   535 
   536 fun mem_thm th [] = false
   537   | mem_thm th ((th',_)::thms_names) = equal_thm (th,th') orelse mem_thm th thms_names;
   538 
   539 fun insert_thms [] thms_names = thms_names
   540   | insert_thms ((thm,name)::thms_names) thms_names' =
   541       if mem_thm thm thms_names' then insert_thms thms_names thms_names' 
   542       else insert_thms thms_names ((thm,name)::thms_names');
   543 
   544 fun display_thms [] = ()
   545   | display_thms ((name,thm)::nthms) = 
   546       let val nthm = name ^ ": " ^ (string_of_thm thm)
   547       in Output.debug nthm; display_thms nthms  end;
   548  
   549 
   550 fun all_facts_of ctxt =
   551   FactIndex.find (ProofContext.fact_index_of ctxt) ([], [])
   552   |> maps #2 |> map (`Thm.name_of_thm);
   553 
   554 (* get lemmas from claset, simpset, atpset and extra supplied rules *)
   555 fun get_clasimp_atp_lemmas ctxt user_thms = 
   556   let val included_thms =
   557 	if !include_all 
   558 	then (tap (fn ths => Output.debug ("Including all " ^ Int.toString (length ths) ^
   559 	                                   " theorems")) 
   560 	          (all_facts_of ctxt @ PureThy.all_thms_of (ProofContext.theory_of ctxt)))
   561 	else 
   562 	let val claset_thms =
   563 		if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt
   564 		else []
   565 	    val simpset_thms = 
   566 		if !include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt
   567 		else []
   568 	    val atpset_thms =
   569 		if !include_atpset then ResAxioms.atpset_rules_of_ctxt ctxt
   570 		else []
   571 	    val _ = if !Output.show_debug_msgs 
   572 		    then (Output.debug "ATP theorems: "; display_thms atpset_thms) 
   573 		    else ()		 
   574 	in  claset_thms @ simpset_thms @ atpset_thms  end
   575       val user_rules = map (put_name_pair o ResAxioms.pairname)
   576 			   (if null user_thms then !whitelist else user_thms)
   577   in
   578       (map put_name_pair included_thms, user_rules)
   579   end;
   580 
   581 (* remove lemmas that are banned from the backlist *)
   582 fun blacklist_filter thms = 
   583   if !run_blacklist_filter then 
   584       let val banned = make_banned_test (map #1 thms)
   585 	  fun ok (a,_) = not (banned a)
   586       in  filter ok thms  end
   587   else thms;
   588 
   589 (* filter axiom clauses, but keep supplied clauses and clauses in whitelist *)
   590 fun get_relevant_clauses ctxt cls_thms white_cls goals =
   591  let val cls_thms_list = make_unique (mk_clause_table 2200) (List.concat (white_cls@cls_thms))
   592      val relevant_cls_thms_list = 
   593 	 if !run_relevance_filter 
   594 	 then ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_thms_list goals 
   595 	 else cls_thms_list
   596  in
   597      insert_thms (List.concat white_cls) relevant_cls_thms_list 
   598  end;
   599 
   600 (***************************************************************)
   601 (* ATP invocation methods setup                                *)
   602 (***************************************************************)
   603 
   604 
   605 (**** prover-specific format: TPTP ****)
   606 
   607 
   608 fun cnf_hyps_thms ctxt = 
   609     let val ths = Assumption.prems_of ctxt
   610     in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end;
   611 
   612 
   613 (**** write to files ****)
   614 
   615 datatype mode = Auto | Fol | Hol;
   616 
   617 val linkup_logic_mode = ref Auto;
   618 
   619 fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =
   620     if is_fol_logic logic 
   621     then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
   622     else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) user_lemmas;
   623 
   624 fun dfg_writer logic goals filename (axioms,classrels,arities) user_lemmas =
   625     if is_fol_logic logic 
   626     then ResClause.dfg_write_file goals filename (axioms, classrels, arities)
   627     else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities) user_lemmas;
   628 
   629 (*Called by the oracle-based methods declared in res_atp_methods.ML*)
   630 fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
   631     let val conj_cls = make_clauses conjectures 
   632                          |> ResAxioms.assume_abstract_list |> Meson.finish_cnf
   633 	val hyp_cls = cnf_hyps_thms ctxt
   634 	val goal_cls = conj_cls@hyp_cls
   635 	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
   636 	val user_lemmas_names = map #1 user_rules
   637 	val rm_black_cls = blacklist_filter included_thms 
   638 	val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_black_cls
   639 	val user_cls = ResAxioms.cnf_rules_pairs user_rules
   640 	val axclauses = get_relevant_clauses ctxt cla_simp_atp_clauses
   641 	                            user_cls (map prop_of goal_cls)
   642 	val thy = ProofContext.theory_of ctxt
   643 	val prob_logic = case mode of 
   644                             Auto => problem_logic_goals [map prop_of goal_cls]
   645 			  | Fol => FOL
   646 			  | Hol => HOL
   647 	val keep_types = if is_fol_logic prob_logic then !fol_keep_types else is_typed_hol ()
   648 	val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
   649 	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
   650         val writer = if dfg then dfg_writer else tptp_writer 
   651 	val file = atp_input_file()
   652     in
   653 	(writer prob_logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
   654 	 Output.debug ("Writing to " ^ file);
   655 	 file)
   656     end;
   657 
   658 
   659 (**** remove tmp files ****)
   660 fun cond_rm_tmp file = 
   661     if !keep_atp_input then Output.debug "ATP input kept..." 
   662     else if !destdir <> "" then Output.debug ("ATP input kept in directory " ^ (!destdir))
   663     else (Output.debug "deleting ATP inputs..."; OS.FileSys.remove file);
   664 
   665 
   666 (****** setup ATPs as Isabelle methods ******)
   667 fun atp_meth' tac ths ctxt = 
   668     Method.SIMPLE_METHOD' HEADGOAL
   669     (tac ctxt ths);
   670 
   671 fun atp_meth tac ths ctxt = 
   672     let val thy = ProofContext.theory_of ctxt
   673 	val _ = ResClause.init thy
   674 	val _ = ResHolClause.init thy
   675     in
   676 	atp_meth' tac ths ctxt
   677     end;
   678 
   679 fun atp_method tac = Method.thms_ctxt_args (atp_meth tac);
   680 
   681 (***************************************************************)
   682 (* automatic ATP invocation                                    *)
   683 (***************************************************************)
   684 
   685 (* call prover with settings and problem file for the current subgoal *)
   686 fun watcher_call_provers sign sg_terms (childin, childout, pid) =
   687   let
   688     fun make_atp_list [] n = []
   689       | make_atp_list (sg_term::xs) n =
   690           let
   691             val probfile = prob_pathname n
   692             val time = Int.toString (!time_limit)
   693           in
   694             Output.debug ("problem file in watcher_call_provers is " ^ probfile);
   695             (*options are separated by Watcher.setting_sep, currently #"%"*)
   696             if !prover = "spass"
   697             then
   698               let val spass = helper_path "SPASS_HOME" "SPASS"
   699                   val sopts =
   700    "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
   701               in 
   702                   ("spass", spass, sopts, probfile) :: make_atp_list xs (n+1)
   703               end
   704             else if !prover = "vampire"
   705 	    then 
   706               let val vampire = helper_path "VAMPIRE_HOME" "vampire"
   707                   val casc = if !time_limit > 70 then "--mode casc%" else ""
   708                   val vopts = casc ^ "-m 100000%-t " ^ time
   709               in
   710                   ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1)
   711               end
   712       	     else if !prover = "E"
   713       	     then
   714 	       let val Eprover = helper_path "E_HOME" "eproof"
   715 	       in
   716 		  ("E", Eprover, 
   717 		     "--tptp-in%-l5%-xAuto%-tAuto%--silent%--cpu-limit=" ^ time, probfile) ::
   718 		   make_atp_list xs (n+1)
   719 	       end
   720 	     else error ("Invalid prover name: " ^ !prover)
   721           end
   722 
   723     val atp_list = make_atp_list sg_terms 1
   724   in
   725     Watcher.callResProvers(childout,atp_list);
   726     Output.debug "Sent commands to watcher!"
   727   end
   728   
   729 fun trace_array fname =
   730   let val path = File.tmp_path (Path.basic fname)
   731   in  Array.app (File.append path o (fn s => s ^ "\n"))  end;
   732 
   733 (*We write out problem files for each subgoal. Argument probfile generates filenames,
   734   and allows the suppression of the suffix "_1" in problem-generation mode.
   735   FIXME: does not cope with &&, and it isn't easy because one could have multiple
   736   subgoals, each involving &&.*)
   737 fun write_problem_files probfile (ctxt,th)  =
   738   let val goals = Thm.prems_of th
   739       val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
   740       val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
   741       val rm_blacklist_cls = blacklist_filter included_thms
   742       val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_blacklist_cls
   743       val axclauses = get_relevant_clauses ctxt cla_simp_atp_clauses (ResAxioms.cnf_rules_pairs white_thms) goals 
   744       val _ = Output.debug ("total clauses from thms = " ^ Int.toString (length axclauses))
   745       val thy = ProofContext.theory_of ctxt
   746       fun get_neg_subgoals n =
   747 	  if n=0 then []
   748 	  else
   749 	      let val st = Seq.hd (EVERY' [rtac ccontr, ObjectLogic.atomize_tac, 
   750 	                                   skolemize_tac] n th)
   751 		  val negs = Option.valOf (metahyps_thms n st)
   752 		  val negs_clauses = make_clauses negs |> ResAxioms.assume_abstract_list
   753 		                       |> Meson.finish_cnf
   754 	      in
   755 		  negs_clauses :: get_neg_subgoals (n-1)
   756 	      end
   757       val neg_subgoals = get_neg_subgoals (length goals) 
   758       val goals_logic = case !linkup_logic_mode of
   759                             Auto => problem_logic_goals (map (map prop_of) neg_subgoals)
   760 			  | Fol => FOL
   761 			  | Hol => HOL
   762       val keep_types = if is_fol_logic goals_logic then !ResClause.keep_types else is_typed_hol ()
   763       val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
   764       val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
   765       val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
   766       val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
   767       val writer = if !prover = "spass" then dfg_writer else tptp_writer 
   768       fun write_all [] _ = []
   769 	| write_all (sub::subgoals) k =
   770 	   (writer goals_logic sub (probfile k) (axclauses,classrel_clauses,arity_clauses) [],
   771 	    probfile k) :: write_all subgoals (k-1)
   772       val (clnames::_, filenames) = ListPair.unzip (write_all neg_subgoals (length goals))
   773       val thm_names = Array.fromList clnames
   774       val _ = if !Output.show_debug_msgs 
   775               then trace_array "thm_names" thm_names else ()
   776   in
   777       (filenames, thm_names)
   778   end;
   779 
   780 val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
   781                                     Posix.Process.pid * string list) option);
   782 
   783 fun kill_last_watcher () =
   784     (case !last_watcher_pid of 
   785          NONE => ()
   786        | SOME (_, _, pid, files) => 
   787 	  (Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid);
   788 	   Watcher.killWatcher pid;  
   789 	   ignore (map (try OS.FileSys.remove) files)))
   790      handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed";
   791 
   792 (*writes out the current clasimpset to a tptp file;
   793   turns off xsymbol at start of function, restoring it at end    *)
   794 val isar_atp = setmp print_mode [] 
   795  (fn (ctxt, th) =>
   796   if Thm.no_prems th then ()
   797   else
   798     let
   799       val _ = kill_last_watcher()
   800       val (files,thm_names) = write_problem_files prob_pathname (ctxt,th)
   801       val (childin, childout, pid) = Watcher.createWatcher (th, thm_names)
   802     in
   803       last_watcher_pid := SOME (childin, childout, pid, files);
   804       Output.debug ("problem files: " ^ space_implode ", " files); 
   805       Output.debug ("pid: " ^ string_of_pid pid);
   806       watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
   807     end);
   808 
   809 val isar_atp_writeonly = setmp print_mode [] 
   810       (fn (ctxt,th) =>
   811        if Thm.no_prems th then ()
   812        else 
   813          let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix 
   814           	            else prob_pathname
   815          in ignore (write_problem_files probfile (ctxt,th)) end);
   816 
   817 
   818 (** the Isar toplevel hook **)
   819 
   820 fun invoke_atp_ml (ctxt, goal) =
   821   let val thy = ProofContext.theory_of ctxt;
   822   in
   823     Output.debug ("subgoals in isar_atp:\n" ^ 
   824 		  Pretty.string_of (ProofContext.pretty_term ctxt
   825 		    (Logic.mk_conjunction_list (Thm.prems_of goal))));
   826     Output.debug ("current theory: " ^ Context.theory_name thy);
   827     inc hook_count;
   828     Output.debug ("in hook for time: " ^ Int.toString (!hook_count));
   829     ResClause.init thy;
   830     ResHolClause.init thy;
   831     if !destdir = "" andalso !time_limit > 0 then isar_atp (ctxt, goal)
   832     else isar_atp_writeonly (ctxt, goal)
   833   end;
   834 
   835 val invoke_atp = Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep
   836  (fn state =>
   837   let val (ctxt, (_, goal)) = Proof.get_goal (Toplevel.proof_of state)
   838   in  invoke_atp_ml (ctxt, goal)  end);
   839 
   840 val call_atpP =
   841   OuterSyntax.command 
   842     "ProofGeneral.call_atp" 
   843     "call automatic theorem provers" 
   844     OuterKeyword.diag
   845     (Scan.succeed invoke_atp);
   846 
   847 val _ = OuterSyntax.add_parsers [call_atpP];
   848 
   849 end;