fixed: count constants with supplementary lemmas
authorimmler@in.tum.de
Tue Jun 30 11:21:02 2009 +0200 (2009-06-30)
changeset 318655e97c4abd18e
parent 31864 90ec13cf7ab0
child 31866 d262a0d46246
fixed: count constants with supplementary lemmas
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue Jun 30 10:59:02 2009 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Jun 30 11:21:02 2009 +0200
     1.3 @@ -11,8 +11,9 @@
     1.4    val prepare_clauses : bool -> thm list -> thm list ->
     1.5      (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list ->
     1.6      (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list -> theory ->
     1.7 -    ResHolClause.axiom_name vector * (ResHolClause.clause list * ResHolClause.clause list *
     1.8 -    ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list)
     1.9 +    ResHolClause.axiom_name vector *
    1.10 +      (ResHolClause.clause list * ResHolClause.clause list * ResHolClause.clause list *
    1.11 +      ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list)
    1.12  end;
    1.13  
    1.14  structure ResAtp: RES_ATP =
    1.15 @@ -550,13 +551,14 @@
    1.16      and tycons = type_consts_of_terms thy (ccltms@axtms)
    1.17      (*TFrees in conjecture clauses; TVars in axiom clauses*)
    1.18      val conjectures = ResHolClause.make_conjecture_clauses dfg thy ccls
    1.19 +    val (_, extra_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy extra_cls)
    1.20      val (clnames,axiom_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy axcls)
    1.21      val helper_clauses = ResHolClause.get_helper_clauses dfg thy isFO (conjectures, extra_cls, [])
    1.22      val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
    1.23      val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
    1.24    in
    1.25      (Vector.fromList clnames,
    1.26 -      (conjectures, axiom_clauses, helper_clauses, classrel_clauses, arity_clauses))
    1.27 +      (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
    1.28    end
    1.29  
    1.30  end;
     2.1 --- a/src/HOL/Tools/res_hol_clause.ML	Tue Jun 30 10:59:02 2009 +0200
     2.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Tue Jun 30 11:21:02 2009 +0200
     2.3 @@ -36,10 +36,12 @@
     2.4         clause list * (thm * (axiom_name * clause_id)) list * string list ->
     2.5         clause list
     2.6    val tptp_write_file: bool -> Path.T ->
     2.7 -    clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list ->
     2.8 +    clause list * clause list * clause list * clause list *
     2.9 +    ResClause.classrelClause list * ResClause.arityClause list ->
    2.10      int * int
    2.11    val dfg_write_file: bool -> Path.T ->
    2.12 -    clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list ->
    2.13 +    clause list * clause list * clause list * clause list *
    2.14 +    ResClause.classrelClause list * ResClause.arityClause list ->
    2.15      int * int
    2.16  end
    2.17  
    2.18 @@ -459,11 +461,11 @@
    2.19    Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
    2.20                  (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
    2.21  
    2.22 -fun count_constants (conjectures, axclauses, helper_clauses, _, _) =
    2.23 +fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
    2.24    if minimize_applies then
    2.25       let val (const_min_arity, const_needs_hBOOL) =
    2.26            fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
    2.27 -       |> fold count_constants_clause axclauses
    2.28 +       |> fold count_constants_clause extra_clauses
    2.29         |> fold count_constants_clause helper_clauses
    2.30       val _ = List.app (display_arity const_needs_hBOOL) (Symtab.dest (const_min_arity))
    2.31       in (const_min_arity, const_needs_hBOOL) end
    2.32 @@ -473,7 +475,8 @@
    2.33  
    2.34  fun tptp_write_file t_full file clauses =
    2.35    let
    2.36 -    val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
    2.37 +    val (conjectures, axclauses, _, helper_clauses,
    2.38 +      classrel_clauses, arity_clauses) = clauses
    2.39      val (cma, cnh) = count_constants clauses
    2.40      val params = (t_full, cma, cnh)
    2.41      val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
    2.42 @@ -494,7 +497,8 @@
    2.43  
    2.44  fun dfg_write_file t_full file clauses =
    2.45    let
    2.46 -    val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
    2.47 +    val (conjectures, axclauses, _, helper_clauses,
    2.48 +      classrel_clauses, arity_clauses) = clauses
    2.49      val (cma, cnh) = count_constants clauses
    2.50      val params = (t_full, cma, cnh)
    2.51      val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)