src/HOL/Tools/res_atp.ML
changeset 21224 f86b8463af37
parent 21132 88d1daae0319
child 21243 afffe1f72143
equal deleted inserted replaced
21223:b3bdc1abc7d3 21224:f86b8463af37
    12   val custom_spass: string list ref
    12   val custom_spass: string list ref
    13   val destdir: string ref
    13   val destdir: string ref
    14   val helper_path: string -> string -> string
    14   val helper_path: string -> string -> string
    15   val problem_name: string ref
    15   val problem_name: string ref
    16   val time_limit: int ref
    16   val time_limit: int ref
       
    17   val set_prover: string -> unit
    17    
    18    
    18   datatype mode = Auto | Fol | Hol
    19   datatype mode = Auto | Fol | Hol
    19   val linkup_logic_mode : mode ref
    20   val linkup_logic_mode : mode ref
    20   val write_subgoal_file: bool -> mode -> Proof.context -> thm list -> thm list -> int -> string
    21   val write_subgoal_file: bool -> mode -> Proof.context -> thm list -> thm list -> int -> string
    21   val vampire_time: int ref
    22   val vampire_time: int ref
    63 (********************************************************************)
    64 (********************************************************************)
    64 
    65 
    65 (*** background linkup ***)
    66 (*** background linkup ***)
    66 val call_atp = ref false; 
    67 val call_atp = ref false; 
    67 val hook_count = ref 0;
    68 val hook_count = ref 0;
    68 val time_limit = ref 80;
    69 val time_limit = ref 60;
    69 val prover = ref "E";   (* use E as the default prover *)
    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 
    70 val custom_spass =   (*specialized options for SPASS*)
    90 val custom_spass =   (*specialized options for SPASS*)
    71       ref ["-Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub"];
    91       ref ["-Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub"];
    72 val destdir = ref "";   (*Empty means write files to /tmp*)
    92 val destdir = ref "";   (*Empty means write files to /tmp*)
    73 val problem_name = ref "prob";
    93 val problem_name = ref "prob";
    74 
    94 
   301   FIXME: this blacklist needs to be maintained using theory data and added to using
   321   FIXME: this blacklist needs to be maintained using theory data and added to using
   302   an attribute.*)
   322   an attribute.*)
   303 val blacklist = ref
   323 val blacklist = ref
   304   ["Datatype.prod.size",
   324   ["Datatype.prod.size",
   305    "Datatype.unit.exhaust", (*"unit" thms cause unsound proofs; unit.nchotomy is caught automatically*)
   325    "Datatype.unit.exhaust", (*"unit" thms cause unsound proofs; unit.nchotomy is caught automatically*)
   306    "Datatype.unit.induct", (*"unit" thms cause unsound proofs; unit.nchotomy is caught automatically*)
   326    "Datatype.unit.induct", 
   307    "Datatype.unit.inducts",
   327    "Datatype.unit.inducts",
   308    "Datatype.unit.split_asm", 
   328    "Datatype.unit.split_asm", 
   309    "Datatype.unit.split",
   329    "Datatype.unit.split",
   310    "Datatype.unit.splits",
   330    "Datatype.unit.splits",
   311    "Divides.dvd_0_left_iff",
   331    "Divides.dvd_0_left_iff",
   518   | get_literals (Const("op |",_)$P$Q) lits = get_literals Q (get_literals P lits)
   538   | get_literals (Const("op |",_)$P$Q) lits = get_literals Q (get_literals P lits)
   519   | get_literals lit lits = (lit::lits);
   539   | get_literals lit lits = (lit::lits);
   520 
   540 
   521 fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t [])));
   541 fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t [])));
   522 
   542 
   523 (*Versions ONLY for "faking" a theorem name. Here we take variable names into account
       
   524   so that similar theorems don't collide.  FIXME: this entire business of "faking" 
       
   525   theorem names must end!*)
       
   526 fun hashw_typ (TVar ((a,i), _), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w))
       
   527   | hashw_typ (TFree (a,_), w) = Polyhash.hashw_string (a,w)
       
   528   | hashw_typ (Type (a, Ts), w) = Polyhash.hashw_string (a, List.foldl hashw_typ w Ts);
       
   529 
       
   530 fun full_hashw_term ((Const(c,T)), w) = Polyhash.hashw_string (c, hashw_typ(T,w))
       
   531   | full_hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w)
       
   532   | full_hashw_term ((Var((a,i),_)), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w))
       
   533   | full_hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w)
       
   534   | full_hashw_term ((Abs(_,T,t)), w) = full_hashw_term (t, hashw_typ(T,w))
       
   535   | full_hashw_term ((P$Q), w) = full_hashw_term (Q, (full_hashw_term (P, w)));
       
   536 
       
   537 fun full_hashw_thm (th,w) = 
       
   538   let val {prop,hyps,...} = rep_thm th
       
   539   in List.foldl full_hashw_term w (prop::hyps) end
       
   540 
       
   541 fun full_hash_thm th = full_hashw_thm (th,0w0);
       
   542 
       
   543 fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
   543 fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
   544 
   544 
   545 (*Create a hash table for clauses, of the given size*)
   545 (*Create a hash table for clauses, of the given size*)
   546 fun mk_clause_table n =
   546 fun mk_clause_table n =
   547       Polyhash.mkTable (hash_term o prop_of, equal_thm)
   547       Polyhash.mkTable (hash_term o prop_of, equal_thm)
   570 (*Filter axiom clauses, but keep supplied clauses and clauses in whitelist. 
   570 (*Filter axiom clauses, but keep supplied clauses and clauses in whitelist. 
   571   Duplicates are removed later.*)
   571   Duplicates are removed later.*)
   572 fun get_relevant_clauses thy cls_thms white_cls goals =
   572 fun get_relevant_clauses thy cls_thms white_cls goals =
   573   white_cls @ (ReduceAxiomsN.relevance_filter thy cls_thms goals);
   573   white_cls @ (ReduceAxiomsN.relevance_filter thy cls_thms goals);
   574 
   574 
   575 (*This name is cryptic but short. Unlike gensym, we get the same name each time.*)
       
   576 fun fake_thm_name th = 
       
   577     Context.theory_name (theory_of_thm th) ^ "." ^ Word.toString (full_hash_thm th);
       
   578 
       
   579 fun put_name_pair ("",th) = (fake_thm_name th, th)
       
   580   | put_name_pair (a,th)  = (a,th);
       
   581 
       
   582 fun display_thms [] = ()
   575 fun display_thms [] = ()
   583   | display_thms ((name,thm)::nthms) = 
   576   | display_thms ((name,thm)::nthms) = 
   584       let val nthm = name ^ ": " ^ (string_of_thm thm)
   577       let val nthm = name ^ ": " ^ (string_of_thm thm)
   585       in Output.debug nthm; display_thms nthms  end;
   578       in Output.debug nthm; display_thms nthms  end;
   586  
   579  
   587 fun all_facts_of ctxt =
   580 fun all_valid_thms ctxt =
   588   FactIndex.find (ProofContext.fact_index_of ctxt) ([], [])
   581   PureThy.thms_containing (ProofContext.theory_of ctxt) ([], []) @
   589   |> maps #2 |> map (`Thm.name_of_thm);
   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;
   590 
   596 
   591 (* get lemmas from claset, simpset, atpset and extra supplied rules *)
   597 (* get lemmas from claset, simpset, atpset and extra supplied rules *)
   592 fun get_clasimp_atp_lemmas ctxt user_thms = 
   598 fun get_clasimp_atp_lemmas ctxt user_thms = 
   593   let val included_thms =
   599   let val included_thms =
   594 	if !include_all 
   600 	if !include_all 
   595 	then (tap (fn ths => Output.debug
   601 	then (tap (fn ths => Output.debug
   596 	             ("Including all " ^ Int.toString (length ths) ^ " theorems")) 
   602 	             ("Including all " ^ Int.toString (length ths) ^ " theorems")) 
   597 	          (all_facts_of ctxt @ PureThy.all_thms_of (ProofContext.theory_of ctxt)))
   603 	          (name_thm_pairs ctxt))
   598 	else 
   604 	else 
   599 	let val claset_thms =
   605 	let val claset_thms =
   600 		if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt
   606 		if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt
   601 		else []
   607 		else []
   602 	    val simpset_thms = 
   608 	    val simpset_thms = 
   607 		else []
   613 		else []
   608 	    val _ = if !Output.show_debug_msgs 
   614 	    val _ = if !Output.show_debug_msgs 
   609 		    then (Output.debug "ATP theorems: "; display_thms atpset_thms) 
   615 		    then (Output.debug "ATP theorems: "; display_thms atpset_thms) 
   610 		    else ()		 
   616 		    else ()		 
   611 	in  claset_thms @ simpset_thms @ atpset_thms  end
   617 	in  claset_thms @ simpset_thms @ atpset_thms  end
   612       val user_rules = map (put_name_pair o ResAxioms.pairname)
   618       val user_rules = filter check_named 
   613 			   (if null user_thms then !whitelist else user_thms)
   619                          (map (ResAxioms.pairname)
       
   620 			   (if null user_thms then !whitelist else user_thms))
   614   in
   621   in
   615       (map put_name_pair included_thms, user_rules)
   622       (filter check_named included_thms, user_rules)
   616   end;
   623   end;
   617 
   624 
   618 (*Remove lemmas that are banned from the backlist. Also remove duplicates. *)
   625 (*Remove lemmas that are banned from the backlist. Also remove duplicates. *)
   619 fun blacklist_filter thms = 
   626 fun blacklist_filter thms = 
   620   if !run_blacklist_filter then 
   627   if !run_blacklist_filter then 
   740       	     else if !prover = "E"
   747       	     else if !prover = "E"
   741       	     then
   748       	     then
   742 	       let val Eprover = helper_path "E_HOME" "eproof"
   749 	       let val Eprover = helper_path "E_HOME" "eproof"
   743 	       in
   750 	       in
   744 		  ("E", Eprover, 
   751 		  ("E", Eprover, 
   745 		     "--tptp-in%-l5%-xAuto%-tAuto%--silent%--cpu-limit=" ^ time, probfile) ::
   752 		     "--tptp-in%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) ::
   746 		   make_atp_list xs (n+1)
   753 		   make_atp_list xs (n+1)
   747 	       end
   754 	       end
   748 	     else error ("Invalid prover name: " ^ !prover)
   755 	     else error ("Invalid prover name: " ^ !prover)
   749           end
   756           end
   750 
   757