src/HOL/Tools/res_atp.ML
changeset 20868 724ab9896068
parent 20854 f9cf9e62d11c
child 20870 992bcbff055a
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Oct 06 11:16:40 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Oct 06 11:17:27 2006 +0200
     1.3 @@ -135,7 +135,7 @@
     1.4  	else error ("No such directory: " ^ !destdir)
     1.5      end;
     1.6  
     1.7 -val include_all = ref false;
     1.8 +val include_all = ref true;
     1.9  val include_simpset = ref false;
    1.10  val include_claset = ref false; 
    1.11  val include_atpset = ref true;
    1.12 @@ -554,29 +554,28 @@
    1.13                         (n, HASH_CLAUSE);
    1.14  
    1.15  (*Use a hash table to eliminate duplicates from xs. Argument is a list of
    1.16 -  (name, theorem) pairs, but the theorems are hashed into the table. *)
    1.17 +  (thm * (string * int)) tuples. The theorems are hashed into the table. *)
    1.18  fun make_unique xs = 
    1.19 -  let val ht = mk_clause_table 2200
    1.20 +  let val ht = mk_clause_table 7000
    1.21    in
    1.22 -      (app (ignore o Polyhash.peekInsert ht) (map swap xs);  
    1.23 -       map swap (Polyhash.listItems ht))
    1.24 +      app (ignore o Polyhash.peekInsert ht) xs;  
    1.25 +      Polyhash.listItems ht
    1.26    end;
    1.27  
    1.28 -(*FIXME: SLOW!!!*)
    1.29 -fun mem_thm th [] = false
    1.30 -  | mem_thm th ((th',_)::thms_names) = equal_thm (th,th') orelse mem_thm th thms_names;
    1.31 +(*Remove existing axiom clauses from the conjecture clauses, as this can dramatically
    1.32 +  boost an ATP's performance (for some reason)*)
    1.33 +fun subtract_cls c_clauses ax_clauses = 
    1.34 +  let val ht = mk_clause_table 2200
    1.35 +      fun known x = isSome (Polyhash.peek ht x)
    1.36 +  in
    1.37 +      app (ignore o Polyhash.peekInsert ht) ax_clauses;  
    1.38 +      filter (not o known) c_clauses 
    1.39 +  end;
    1.40  
    1.41 -(*FIXME: SLOW!!! These two functions are called only by get_relevant_clauses.
    1.42 -  It would be faster to compare names, rather than theorems, and to use
    1.43 -  a symbol table or hash table.*)
    1.44 -fun insert_thms [] thms_names = thms_names
    1.45 -  | insert_thms ((thm,name)::thms_names) thms_names' =
    1.46 -      if mem_thm thm thms_names' then insert_thms thms_names thms_names' 
    1.47 -      else insert_thms thms_names ((thm,name)::thms_names');
    1.48 -
    1.49 -(* filter axiom clauses, but keep supplied clauses and clauses in whitelist *)
    1.50 +(*Filter axiom clauses, but keep supplied clauses and clauses in whitelist. 
    1.51 +  Duplicates are removed later.*)
    1.52  fun get_relevant_clauses thy cls_thms white_cls goals =
    1.53 -  insert_thms white_cls (ReduceAxiomsN.relevance_filter thy cls_thms goals);
    1.54 +  white_cls @ (ReduceAxiomsN.relevance_filter thy cls_thms goals);
    1.55  
    1.56  (*This name is cryptic but short. Unlike gensym, we get the same name each time.*)
    1.57  fun fake_thm_name th = 
    1.58 @@ -670,12 +669,12 @@
    1.59  			  | Hol => HOL
    1.60  	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
    1.61  	val cla_simp_atp_clauses = included_thms |> blacklist_filter
    1.62 -	                             |> make_unique |> ResAxioms.cnf_rules_pairs
    1.63 +	                             |> ResAxioms.cnf_rules_pairs |> make_unique 
    1.64                                       |> restrict_to_logic logic 
    1.65  	val user_cls = ResAxioms.cnf_rules_pairs user_rules
    1.66  	val thy = ProofContext.theory_of ctxt
    1.67  	val axclauses = get_relevant_clauses thy cla_simp_atp_clauses
    1.68 -	                            user_cls (map prop_of goal_cls)
    1.69 +	                            user_cls (map prop_of goal_cls) |> make_unique
    1.70  	val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
    1.71  	val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
    1.72  	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
    1.73 @@ -787,7 +786,7 @@
    1.74  	      | Hol => HOL
    1.75        val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
    1.76        val included_cls = included_thms |> blacklist_filter
    1.77 -                                       |> make_unique |> ResAxioms.cnf_rules_pairs 
    1.78 +                                       |> ResAxioms.cnf_rules_pairs |> make_unique 
    1.79                                         |> restrict_to_logic logic 
    1.80        val white_cls = ResAxioms.cnf_rules_pairs white_thms
    1.81        (*clauses relevant to goal gl*)
    1.82 @@ -806,9 +805,11 @@
    1.83        val writer = if !prover = "spass" then dfg_writer else tptp_writer 
    1.84        fun write_all [] [] _ = []
    1.85  	| write_all (ccls::ccls_list) (axcls::axcls_list) k =
    1.86 -	   (writer logic ccls (probfile k) (axcls,classrel_clauses,arity_clauses) [],
    1.87 -	    probfile k) 
    1.88 -	   :: write_all ccls_list axcls_list (k+1)
    1.89 +            let val fname = probfile k
    1.90 +                val axcls = make_unique axcls
    1.91 +                val ccls = subtract_cls ccls axcls
    1.92 +                val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
    1.93 +            in  (clnames,fname) :: write_all ccls_list axcls_list (k+1)  end
    1.94        val (clnames::_, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
    1.95        val thm_names = Array.fromList clnames
    1.96        val _ = if !Output.show_debug_msgs