# HG changeset patch # User blanchet # Date 1279890289 -7200 # Node ID 6a48c85a211ad36ccf488d1ee9b7d13a8c587739 # Parent e557d511c791fcffc1b0a180ff310ff2cbbc2f28 first step in using "fof" rather than "cnf" in TPTP problems diff -r e557d511c791 -r 6a48c85a211a src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Jul 23 14:07:35 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Jul 23 15:04:49 2010 +0200 @@ -529,14 +529,14 @@ (** EXTRACTING LEMMAS **) (* A list consisting of the first number in each line is returned. - TSTP: Interesting lines have the form "cnf(108, axiom, ...)", where the + TSTP: Interesting lines have the form "fof(108, axiom, ...)", where the number (108) is extracted. SPASS: Lines have the form "108[0:Inp] ...", where the first number (108) is extracted. *) -fun extract_clause_numbers_in_atp_proof atp_proof = +fun extract_formula_numbers_in_atp_proof atp_proof = let val tokens_of = String.tokens (not o is_ident_char) - fun extract_num ("cnf" :: num :: "axiom" :: _) = Int.fromString num + fun extract_num ("fof" :: num :: "axiom" :: _) = Int.fromString num | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num | extract_num _ = NONE in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end @@ -579,7 +579,7 @@ i) = let val raw_lemmas = - atp_proof |> extract_clause_numbers_in_atp_proof + atp_proof |> extract_formula_numbers_in_atp_proof |> filter (is_axiom_clause_number thm_names) |> map (fn i => Vector.sub (thm_names, i - 1)) val (chained_lemmas, other_lemmas) = diff -r e557d511c791 -r 6a48c85a211a src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Fri Jul 23 14:07:35 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Fri Jul 23 15:04:49 2010 +0200 @@ -27,23 +27,44 @@ (** ATP problem **) -datatype 'a atp_term = ATerm of 'a * 'a atp_term list -type 'a atp_literal = bool * 'a atp_term -datatype 'a problem_line = Cnf of string * kind * 'a atp_literal list +datatype 'a fo_term = ATerm of 'a * 'a fo_term list +datatype quantifier = AForall | AExists +datatype connective = ANot | AAnd | AOr | AImplies | AIff +datatype 'a formula = + AQuant of quantifier * 'a list * 'a formula | + AConn of connective * 'a formula list | + APred of 'a fo_term + +fun mk_anot phi = AConn (ANot, [phi]) + +datatype 'a problem_line = Fof of string * kind * 'a formula type 'a problem = (string * 'a problem_line list) list -fun string_for_atp_term (ATerm (s, [])) = s - | string_for_atp_term (ATerm (s, ts)) = - s ^ "(" ^ commas (map string_for_atp_term ts) ^ ")" -fun string_for_atp_literal (pos, ATerm ("equal", [t1, t2])) = - string_for_atp_term t1 ^ " " ^ (if pos then "=" else "!=") ^ " " ^ - string_for_atp_term t2 - | string_for_atp_literal (pos, t) = - (if pos then "" else "~ ") ^ string_for_atp_term t -fun string_for_problem_line (Cnf (ident, kind, lits)) = - "cnf(" ^ ident ^ ", " ^ - (case kind of Axiom => "axiom" | Conjecture => "negated_conjecture") ^ ",\n" ^ - " (" ^ space_implode " | " (map string_for_atp_literal lits) ^ ")).\n" +fun string_for_term (ATerm (s, [])) = s + | string_for_term (ATerm (s, ts)) = + if s = "equal" then space_implode " = " (map string_for_term ts) + else s ^ "(" ^ commas (map string_for_term ts) ^ ")" +fun string_for_quantifier AForall = "!" + | string_for_quantifier AExists = "?" +fun string_for_connective ANot = "~" + | string_for_connective AAnd = "&" + | string_for_connective AOr = "|" + | string_for_connective AImplies = "=>" + | string_for_connective AIff = "<=>" +fun string_for_formula (AQuant (q, xs, phi)) = + string_for_quantifier q ^ " [" ^ commas xs ^ "] : " ^ + string_for_formula phi + | string_for_formula (AConn (c, [phi])) = + string_for_connective c ^ " " ^ string_for_formula phi + | string_for_formula (AConn (c, phis)) = + "(" ^ space_implode (" " ^ string_for_connective c ^ " ") + (map string_for_formula phis) ^ ")" + | string_for_formula (APred tm) = string_for_term tm + +fun string_for_problem_line (Fof (ident, kind, phi)) = + "fof(" ^ ident ^ ", " ^ + (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^ + " (" ^ string_for_formula phi ^ ")).\n" fun strings_for_problem problem = "% This file was generated by Isabelle (most likely Sledgehammer)\n\ \% " ^ timestamp () ^ "\n" :: @@ -97,11 +118,17 @@ end in add 0 |> apsnd SOME end -fun nice_atp_term (ATerm (name, ts)) = - nice_name name ##>> pool_map nice_atp_term ts #>> ATerm -fun nice_atp_literal (pos, t) = nice_atp_term t #>> pair pos -fun nice_problem_line (Cnf (ident, kind, lits)) = - pool_map nice_atp_literal lits #>> (fn lits => Cnf (ident, kind, lits)) + +fun nice_term (ATerm (name, ts)) = + nice_name name ##>> pool_map nice_term ts #>> ATerm +fun nice_formula (AQuant (q, xs, phi)) = + pool_map nice_name xs ##>> nice_formula phi + #>> (fn (xs, phi) => AQuant (q, xs, phi)) + | nice_formula (AConn (c, phis)) = + pool_map nice_formula phis #>> curry AConn c + | nice_formula (APred tm) = nice_term tm #>> APred +fun nice_problem_line (Fof (ident, kind, phi)) = + nice_formula phi #>> (fn phi => Fof (ident, kind, phi)) fun nice_problem problem = pool_map (fn (heading, lines) => pool_map nice_problem_line lines #>> pair heading) problem @@ -117,12 +144,12 @@ fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) -fun atp_term_for_combtyp (CombTVar name) = ATerm (name, []) - | atp_term_for_combtyp (CombTFree name) = ATerm (name, []) - | atp_term_for_combtyp (CombType (name, tys)) = - ATerm (name, map atp_term_for_combtyp tys) +fun fo_term_for_combtyp (CombTVar name) = ATerm (name, []) + | fo_term_for_combtyp (CombTFree name) = ATerm (name, []) + | fo_term_for_combtyp (CombType (name, tys)) = + ATerm (name, map fo_term_for_combtyp tys) -fun atp_term_for_combterm full_types top_level u = +fun fo_term_for_combterm full_types top_level u = let val (head, args) = strip_combterm_comb u val (x, ty_args) = @@ -135,58 +162,67 @@ (name, if full_types then [] else ty_args) | CombVar (name, _) => (name, []) | CombApp _ => raise Fail "impossible \"CombApp\"" - val t = ATerm (x, map atp_term_for_combtyp ty_args @ - map (atp_term_for_combterm full_types false) args) + val t = ATerm (x, map fo_term_for_combtyp ty_args @ + map (fo_term_for_combterm full_types false) args) in - if full_types then wrap_type (atp_term_for_combtyp (type_of_combterm u)) t + if full_types then wrap_type (fo_term_for_combtyp (type_of_combterm u)) t else t end -fun atp_literal_for_literal full_types (FOLLiteral (pos, t)) = - (pos, atp_term_for_combterm full_types true t) +fun fo_literal_for_literal full_types (FOLLiteral (pos, t)) = + (pos, fo_term_for_combterm full_types true t) -fun atp_literal_for_type_literal pos (TyLitVar (class, name)) = +fun fo_literal_for_type_literal pos (TyLitVar (class, name)) = (pos, ATerm (class, [ATerm (name, [])])) - | atp_literal_for_type_literal pos (TyLitFree (class, name)) = + | fo_literal_for_type_literal pos (TyLitFree (class, name)) = (pos, ATerm (class, [ATerm (name, [])])) -fun atp_literals_for_axiom full_types - (FOLClause {literals, ctypes_sorts, ...}) = - map (atp_literal_for_literal full_types) literals @ - map (atp_literal_for_type_literal false) +fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot +fun formula_for_fo_literals [] = APred (ATerm (("$false", "$false"), [])) + | formula_for_fo_literals (lit :: lits) = + AConn (AOr, [formula_for_fo_literal lit, formula_for_fo_literals lits]) + +fun formula_for_axiom full_types (FOLClause {literals, ctypes_sorts, ...}) = + map (fo_literal_for_literal full_types) literals @ + map (fo_literal_for_type_literal false) (type_literals_for_types ctypes_sorts) + |> formula_for_fo_literals fun problem_line_for_axiom full_types (clause as FOLClause {axiom_name, clause_id, kind, ...}) = - Cnf (hol_ident axiom_name clause_id, kind, - atp_literals_for_axiom full_types clause) + Fof (hol_ident axiom_name clause_id, kind, + formula_for_axiom full_types clause) fun problem_line_for_class_rel_clause (ClassRelClause {axiom_name, subclass, superclass, ...}) = let val ty_arg = ATerm (("T", "T"), []) in - Cnf (ascii_of axiom_name, Axiom, [(false, ATerm (subclass, [ty_arg])), - (true, ATerm (superclass, [ty_arg]))]) + Fof (ascii_of axiom_name, Axiom, + AConn (AImplies, [APred (ATerm (subclass, [ty_arg])), + APred (ATerm (superclass, [ty_arg]))])) end -fun atp_literal_for_arity_literal (TConsLit (c, t, args)) = +fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) - | atp_literal_for_arity_literal (TVarLit (c, sort)) = + | fo_literal_for_arity_literal (TVarLit (c, sort)) = (false, ATerm (c, [ATerm (sort, [])])) fun problem_line_for_arity_clause (ArityClause {axiom_name, conclLit, premLits, ...}) = - Cnf (arity_clause_prefix ^ ascii_of axiom_name, Axiom, - map atp_literal_for_arity_literal (conclLit :: premLits)) + Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom, + map fo_literal_for_arity_literal (conclLit :: premLits) + |> formula_for_fo_literals) fun problem_line_for_conjecture full_types (clause as FOLClause {axiom_name, clause_id, kind, literals, ...}) = - Cnf (hol_ident axiom_name clause_id, kind, - map (atp_literal_for_literal full_types) literals) + Fof (hol_ident axiom_name clause_id, kind, + map (fo_literal_for_literal full_types) literals + |> formula_for_fo_literals |> mk_anot) fun atp_free_type_literals_for_conjecture (FOLClause {ctypes_sorts, ...}) = - map (atp_literal_for_type_literal true) (type_literals_for_types ctypes_sorts) + map (fo_literal_for_type_literal true) (type_literals_for_types ctypes_sorts) -fun problem_line_for_free_type lit = Cnf ("tfree_tcs", Conjecture, [lit]) +fun problem_line_for_free_type lit = + Fof ("tfree_tcs", Conjecture, formula_for_fo_literal lit) fun problem_lines_for_free_types conjectures = let val litss = map atp_free_type_literals_for_conjecture conjectures @@ -197,10 +233,10 @@ type const_info = {min_arity: int, max_arity: int, sub_level: bool} -fun is_atp_variable s = Char.isUpper (String.sub (s, 0)) +fun is_variable s = Char.isUpper (String.sub (s, 0)) fun consider_term top_level (ATerm ((s, _), ts)) = - (if is_atp_variable s then + (if is_variable s then I else let val n = length ts in @@ -212,8 +248,11 @@ sub_level = sub_level orelse not top_level}) end) #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts -fun consider_literal (_, t) = consider_term true t -fun consider_problem_line (Cnf (_, _, lits)) = fold consider_literal lits +fun consider_formula (AQuant (_, _, phi)) = consider_formula phi + | consider_formula (AConn (_, phis)) = fold consider_formula phis + | consider_formula (APred tm) = consider_term true tm + +fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi fun consider_problem problem = fold (fold consider_problem_line o snd) problem fun const_table_for_problem explicit_apply problem = @@ -288,21 +327,43 @@ else t |> not (is_predicate const_tab s) ? boolify -fun repair_literal thy full_types const_tab (pos, t) = - (pos, t |> repair_applications_in_term thy full_types const_tab - |> repair_predicates_in_term const_tab) -fun repair_problem_line thy full_types const_tab (Cnf (ident, kind, lits)) = - Cnf (ident, kind, map (repair_literal thy full_types const_tab) lits) -fun repair_problem_with_const_table thy full_types const_tab problem = - map (apsnd (map (repair_problem_line thy full_types const_tab))) problem -fun repair_problem thy full_types explicit_apply problem = - repair_problem_with_const_table thy full_types +fun close_universally phi = + let + fun term_vars bounds (ATerm (name as (s, _), tms)) = + (is_variable s andalso not (member (op =) bounds name)) + ? insert (op =) name + #> fold (term_vars bounds) tms + fun formula_vars bounds (AQuant (q, xs, phi)) = + formula_vars (xs @ bounds) phi + | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis + | formula_vars bounds (APred tm) = term_vars bounds tm + in + case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi) + end + +fun repair_formula thy explicit_forall full_types const_tab = + let + fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) + | aux (AConn (c, phis)) = AConn (c, map aux phis) + | aux (APred tm) = + APred (tm |> repair_applications_in_term thy full_types const_tab + |> repair_predicates_in_term const_tab) + in aux #> explicit_forall ? close_universally end + +fun repair_problem_line thy explicit_forall full_types const_tab + (Fof (ident, kind, phi)) = + Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi) +val repair_problem_with_const_table = map o apsnd o map oooo repair_problem_line + +fun repair_problem thy explicit_forall full_types explicit_apply problem = + repair_problem_with_const_table thy explicit_forall full_types (const_table_for_problem explicit_apply problem) problem fun write_tptp_file thy readable_names full_types explicit_apply file (conjectures, axiom_clauses, extra_clauses, helper_clauses, class_rel_clauses, arity_clauses) = let + val explicit_forall = true (* FIXME *) val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses val class_rel_lines = map problem_line_for_class_rel_clause class_rel_clauses @@ -311,13 +372,14 @@ val conjecture_lines = map (problem_line_for_conjecture full_types) conjectures val tfree_lines = problem_lines_for_free_types conjectures - val problem = [("Relevant facts", axiom_lines), - ("Class relationships", class_rel_lines), - ("Arity declarations", arity_lines), - ("Helper facts", helper_lines), - ("Conjectures", conjecture_lines), - ("Type variables", tfree_lines)] - |> repair_problem thy full_types explicit_apply + val problem = + [("Relevant facts", axiom_lines), + ("Class relationships", class_rel_lines), + ("Arity declarations", arity_lines), + ("Helper facts", helper_lines), + ("Conjectures", conjecture_lines), + ("Type variables", tfree_lines)] + |> repair_problem thy explicit_forall full_types explicit_apply val (problem, pool) = nice_problem problem (empty_name_pool readable_names) val conjecture_offset = length axiom_lines + length class_rel_lines + length arity_lines