# HG changeset patch # User blanchet # Date 1298028775 -3600 # Node ID eb2e39555f981dd30eaff24f62cb7d79799270d7 # Parent dd2125fb75f96fb600e6be35f77d794b2660e3aa extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs diff -r dd2125fb75f9 -r eb2e39555f98 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Thu Feb 17 12:14:47 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_problem.ML Fri Feb 18 12:32:55 2011 +0100 @@ -16,8 +16,9 @@ AAtom of 'b type 'a uniform_formula = ('a, 'a fo_term) formula - datatype kind = Axiom | Hypothesis | Conjecture - datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula + datatype kind = Axiom | Definition | Lemma | Hypothesis | Conjecture + datatype 'a problem_line = + Fof of string * kind * ('a, 'a fo_term) formula * string fo_term option type 'a problem = (string * 'a problem_line list) list val timestamp : unit -> string @@ -44,19 +45,25 @@ AAtom of 'b type 'a uniform_formula = ('a, 'a fo_term) formula -datatype kind = Axiom | Hypothesis | Conjecture -datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula +datatype kind = Axiom | Definition | Lemma | Hypothesis | Conjecture +datatype 'a problem_line = + Fof of string * kind * ('a, 'a fo_term) formula * string fo_term option type 'a problem = (string * 'a problem_line list) list val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now fun string_for_kind Axiom = "axiom" + | string_for_kind Definition = "definition" + | string_for_kind Lemma = "lemma" | string_for_kind Hypothesis = "hypothesis" | string_for_kind Conjecture = "conjecture" fun string_for_term (ATerm (s, [])) = s | string_for_term (ATerm ("equal", ts)) = space_implode " = " (map string_for_term ts) + | string_for_term (ATerm ("[]", ts)) = + (* used for lists in the optional "source" field of a derivation *) + "[" ^ commas (map string_for_term ts) ^ "]" | string_for_term (ATerm (s, ts)) = s ^ "(" ^ commas (map string_for_term ts) ^ ")" fun string_for_quantifier AForall = "!" @@ -81,7 +88,7 @@ | string_for_formula (AAtom tm) = string_for_term tm fun string_for_problem_line use_conjecture_for_hypotheses - (Fof (ident, kind, phi)) = + (Fof (ident, kind, phi, source)) = let val (kind, phi) = if kind = Hypothesis andalso use_conjecture_for_hypotheses then @@ -90,7 +97,10 @@ (kind, phi) in "fof(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n (" ^ - string_for_formula phi ^ ")).\n" + string_for_formula phi ^ ")" ^ + (case source of + SOME tm => ", " ^ string_for_term tm + | NONE => "") ^ ").\n" end fun tptp_strings_for_atp_problem use_conjecture_for_hypotheses problem = "% This file was generated by Isabelle (most likely Sledgehammer)\n\ @@ -160,8 +170,8 @@ | nice_formula (AConn (c, phis)) = pool_map nice_formula phis #>> curry AConn c | nice_formula (AAtom tm) = nice_term tm #>> AAtom -fun nice_problem_line (Fof (ident, kind, phi)) = - nice_formula phi #>> (fn phi => Fof (ident, kind, phi)) +fun nice_problem_line (Fof (ident, kind, phi, source)) = + nice_formula phi #>> (fn phi => Fof (ident, kind, phi, source)) fun nice_problem problem = pool_map (fn (heading, lines) => pool_map nice_problem_line lines #>> pair heading) problem diff -r dd2125fb75f9 -r eb2e39555f98 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Thu Feb 17 12:14:47 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Feb 18 12:32:55 2011 +0100 @@ -109,10 +109,10 @@ datatype e_weight_method = E_Auto | E_Fun_Weight | E_Sym_Offset_Weight val e_weight_method = Unsynchronized.ref E_Fun_Weight -val e_default_fun_weight = Unsynchronized.ref 0.5 +val e_default_fun_weight = Unsynchronized.ref 20.0 (* ### *) val e_fun_weight_base = Unsynchronized.ref 0.0 val e_fun_weight_factor = Unsynchronized.ref 40.0 -val e_default_sym_offs_weight = Unsynchronized.ref 0.0 +val e_default_sym_offs_weight = Unsynchronized.ref 1.0 (* ### *) val e_sym_offs_weight_base = Unsynchronized.ref ~30.0 val e_sym_offs_weight_factor = Unsynchronized.ref ~30.0 @@ -138,8 +138,8 @@ \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \ \-H'(4*" ^ e_weight_method_case "FunWeight" "SymOffsetWeight" ^ "(SimulateSOS, " ^ - scaled_e_weight (e_weight_method_case (!e_default_fun_weight) - (!e_default_sym_offs_weight)) ^ + (e_weight_method_case (!e_default_fun_weight) (!e_default_sym_offs_weight) + |> Real.ceil |> signed_string_of_int) ^ ",20,1.5,1.5,1" ^ (weights () |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight w) |> implode) ^ diff -r dd2125fb75f9 -r eb2e39555f98 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu Feb 17 12:14:47 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri Feb 18 12:32:55 2011 +0100 @@ -294,7 +294,7 @@ in [Fof (helper_prefix ^ ascii_of "ti_ti", Axiom, AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")])) - |> explicit_forall ? close_universally)] + |> explicit_forall ? close_universally, NONE)] end else []) @@ -440,14 +440,15 @@ (formula_for_combformula ctxt type_sys combformula) fun problem_line_for_fact ctxt prefix type_sys (formula as {name, kind, ...}) = - Fof (prefix ^ ascii_of name, kind, formula_for_fact ctxt type_sys formula) + Fof (prefix ^ ascii_of name, kind, formula_for_fact ctxt type_sys formula, + NONE) fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass, superclass, ...}) = let val ty_arg = ATerm (("T", "T"), []) in Fof (class_rel_clause_prefix ^ ascii_of name, Axiom, AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), - AAtom (ATerm (superclass, [ty_arg]))])) + AAtom (ATerm (superclass, [ty_arg]))]), NONE) end fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = @@ -461,12 +462,12 @@ mk_ahorn (map (formula_for_fo_literal o apfst not o fo_literal_for_arity_literal) premLits) (formula_for_fo_literal - (fo_literal_for_arity_literal conclLit))) + (fo_literal_for_arity_literal conclLit)), NONE) fun problem_line_for_conjecture ctxt type_sys ({name, kind, combformula, ...} : translated_formula) = Fof (conjecture_prefix ^ name, kind, - formula_for_combformula ctxt type_sys combformula) + formula_for_combformula ctxt type_sys combformula, NONE) fun free_type_literals_for_conjecture type_sys ({ctypes_sorts, ...} : translated_formula) = @@ -474,7 +475,8 @@ |> map fo_literal_for_type_literal fun problem_line_for_free_type j lit = - Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit) + Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit, + NONE) fun problem_lines_for_free_types type_sys conjs = let val litss = map (free_type_literals_for_conjecture type_sys) conjs @@ -502,7 +504,7 @@ | consider_formula (AConn (_, phis)) = fold consider_formula phis | consider_formula (AAtom tm) = consider_term true tm -fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi +fun consider_problem_line (Fof (_, _, phi, _)) = consider_formula phi fun consider_problem problem = fold (fold consider_problem_line o snd) problem (* needed for helper facts if the problem otherwise does not involve equality *) @@ -593,8 +595,9 @@ in aux #> explicit_forall ? close_universally end fun repair_problem_line thy explicit_forall type_sys const_tab - (Fof (ident, kind, phi)) = - Fof (ident, kind, repair_formula thy explicit_forall type_sys const_tab phi) + (Fof (ident, kind, phi, source)) = + Fof (ident, kind, repair_formula thy explicit_forall type_sys const_tab phi, + source) fun repair_problem thy = map o apsnd o map ooo repair_problem_line thy fun dest_Fof (Fof z) = z @@ -654,7 +657,7 @@ fun add_term_weights weight (ATerm (s, tms)) = (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight) #> fold (add_term_weights weight) tms -fun add_problem_line_weights weight (Fof (_, _, phi)) = +fun add_problem_line_weights weight (Fof (_, _, phi, _)) = fold_formula (add_term_weights weight) phi fun add_conjectures_weights [] = I