src/HOL/Tools/ATP/reduce_axiomsN.ML
changeset 19321 30b5bb35dd33
parent 19315 b218cc3d1bb4
child 19334 96ca738055a6
     1.1 --- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Thu Mar 23 06:18:38 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Thu Mar 23 10:05:03 2006 +0100
     1.3 @@ -89,6 +89,7 @@
     1.4  
     1.5  (**** Constant / Type Frequencies ****)
     1.6  
     1.7 +
     1.8  local
     1.9  
    1.10  fun cons_nr CTVar = 0
    1.11 @@ -187,30 +188,49 @@
    1.12  fun showax ((_,cname), (_,w)) = 
    1.13      Output.debug ("Axiom " ^ show_cname cname ^ " has weight " ^ Real.toString w)
    1.14  	      
    1.15 +exception ConstFree;
    1.16 +fun dest_ConstFree (Const aT) = aT
    1.17 +  | dest_ConstFree (Free aT) = aT
    1.18 +  | dest_ConstFree _ = raise ConstFree;
    1.19 +
    1.20 +(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
    1.21 +fun defines thy (tm,(name,n)) gctypes =
    1.22 +  let fun defs hs =
    1.23 +        let val (rator,args) = strip_comb hs
    1.24 +            val ct = const_with_typ thy (dest_ConstFree rator)
    1.25 +        in  forall is_Var args andalso uni_mem ct gctypes  end
    1.26 +        handle ConstFree => false
    1.27 +  in    
    1.28 +    case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ _) => 
    1.29 +          defs lhs andalso
    1.30 +          (Output.debug ("Definition found: " ^ name ^ "_" ^ Int.toString n); true)
    1.31 +      | _ => false
    1.32 +  end
    1.33 +
    1.34  fun relevance_filter_aux thy axioms goals = 
    1.35    let val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms
    1.36        val goals_consts_typs = get_goal_consts_typs thy goals
    1.37 -      fun relevant [] (ax,r) = (ax,r)
    1.38 -	| relevant ((clstm,consts_typs)::y) (ax,r) =
    1.39 +      fun relevant [] (rels,nonrels) = (rels,nonrels)
    1.40 +	| relevant ((clstm,consts_typs)::axs) (rels,nonrels) =
    1.41  	    let val weight = clause_weight const_tab goals_consts_typs consts_typs
    1.42  		val ccc = (clstm, (consts_typs,weight))
    1.43  	    in
    1.44 -	      if !pass_mark <= weight 
    1.45 -	      then relevant y (ccc::ax, r)
    1.46 -	      else relevant y (ax, ccc::r)
    1.47 +	      if !pass_mark <= weight orelse defines thy clstm goals_consts_typs
    1.48 +	      then relevant axs (ccc::rels, nonrels)
    1.49 +	      else relevant axs (rels, ccc::nonrels)
    1.50  	    end
    1.51        val (rel_clauses,nrel_clauses) =
    1.52  	  relevant (map (pair_consts_typs_axiom thy) axioms) ([],[]) 
    1.53 -      val (ax,r) = relevant_clauses const_tab rel_clauses nrel_clauses ([],[]) []
    1.54 -      val max_filtered = floor (!reduction_factor * real (length ax))
    1.55 -      val ax' = Library.take(max_filtered, Library.sort axiom_ord ax)
    1.56 +      val (rels,nonrels) = relevant_clauses const_tab rel_clauses nrel_clauses ([],[]) []
    1.57 +      val max_filtered = floor (!reduction_factor * real (length rels))
    1.58 +      val rels' = Library.take(max_filtered, Library.sort axiom_ord rels)
    1.59    in
    1.60        if !Output.show_debug_msgs then
    1.61  	   (List.app showconst (Symtab.dest const_tab);
    1.62 -	    List.app showax ax)
    1.63 +	    List.app showax rels)
    1.64        else ();
    1.65 -      if !add_unit then (filter good_unit_clause r) @ ax'
    1.66 -      else ax'
    1.67 +      if !add_unit then (filter good_unit_clause nonrels) @ rels'
    1.68 +      else rels'
    1.69    end;
    1.70  
    1.71  fun relevance_filter thy axioms goals =