# HG changeset patch # User blanchet # Date 1280146464 -7200 # Node ID b04307085a093a0b4cd54325fc781ce1acd0bdfe # Parent bb39190370fe86d3a4ca246ae82e3437936f2869 make TPTP generator accept full first-order formulas diff -r bb39190370fe -r b04307085a09 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jul 26 11:26:47 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jul 26 14:14:24 2010 +0200 @@ -324,8 +324,7 @@ NONE => (message, SH_OK (time_isa, time_atp, relevant_thm_names)) | SOME _ => (message, SH_FAIL (time_isa, time_atp)) end - handle ATP_Manager.TRIVIAL () => ("trivial", SH_OK (0, 0, [])) - | ERROR msg => ("error: " ^ msg, SH_ERROR) + handle ERROR msg => ("error: " ^ msg, SH_ERROR) | TimeLimit.TimeOut => ("timeout", SH_ERROR) fun thms_of_name ctxt name = diff -r bb39190370fe -r b04307085a09 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Jul 26 11:26:47 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Jul 26 14:14:24 2010 +0200 @@ -47,7 +47,6 @@ filtered_clauses: ((string * int) * thm) list} type prover = params -> minimize_command -> Time.time -> problem -> prover_result - exception TRIVIAL of unit val kill_atps: unit -> unit val running_atps: unit -> unit @@ -119,9 +118,6 @@ type prover = params -> minimize_command -> Time.time -> problem -> prover_result -(* Trivial problem, which resolution cannot handle (empty clause) *) -exception TRIVIAL of unit - (* named provers *) structure Data = Theory_Data @@ -168,8 +164,7 @@ filtered_clauses = NONE} in prover params (minimize_command name) timeout problem |> #message - handle TRIVIAL () => metis_line full_types i n [] - | ERROR message => "Error: " ^ message ^ "\n" + handle ERROR message => "Error: " ^ message ^ "\n" end) end diff -r bb39190370fe -r b04307085a09 src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jul 26 11:26:47 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jul 26 14:14:24 2010 +0200 @@ -52,7 +52,8 @@ proof_delims: (string * string) list, known_failures: (failure * string) list, max_axiom_clauses: int, - prefers_theory_relevant: bool}; + prefers_theory_relevant: bool, + explicit_forall: bool} (* basic template *) @@ -132,33 +133,35 @@ fun subtract_cls ax_clauses = filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of) -fun is_false_literal (FOLLiteral (pos, CombConst ((c, _), _, _))) = - c = (if pos then "c_False" else "c_True") - | is_false_literal _ = false -fun is_true_literal (FOLLiteral (pol, CombConst ((c, _), _, _))) = - (pol andalso c = "c_True") orelse - (not pol andalso c = "c_False") - | is_true_literal _ = false; -fun is_tautology (FOLClause {literals,...}) = exists is_true_literal literals +(* FIXME: kill *) +fun mk_anot phi = AConn (ANot, [phi]) +fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) (* making axiom and conjecture clauses *) -fun make_clause thy (clause_id, axiom_name, kind, th) skolems = +fun make_clause thy (formula_id, formula_name, kind, th) skolems = let - val (skolems, t) = th |> prop_of |> conceal_skolem_terms clause_id skolems + val (skolems, t) = th |> prop_of |> conceal_skolem_terms formula_id skolems val (lits, ctypes_sorts) = literals_of_term thy t + (* FIXME: avoid "literals_of_term *) + val combformula = + case lits of + [] => APred (CombConst (("c_False", "False"), CombType (("bool", "bool"), []), [])) + | _ => + let val phis = lits |> map (fn FOLLiteral (pos, tm) => APred tm |> not pos ? mk_anot) in + fold (mk_aconn AOr) (tl phis) (hd phis) + |> kind = Conjecture ? mk_anot + end in - if forall is_false_literal lits then - raise TRIVIAL () - else - (skolems, - FOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th, - kind = kind, literals = lits, ctypes_sorts = ctypes_sorts}) + (skolems, + FOLFormula {formula_name = formula_name, formula_id = formula_id, + combformula = combformula, kind = kind, + ctypes_sorts = ctypes_sorts}) end fun add_axiom_clause thy ((name, k), th) (skolems, clss) = let val (skolems, cls) = make_clause thy (k, name, Axiom, th) skolems - in (skolems, clss |> not (is_tautology cls) ? cons (name, cls)) end + in (skolems, (name, cls) :: clss) end fun make_axiom_clauses thy clauses = ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd @@ -175,12 +178,15 @@ (** Helper clauses **) -fun count_combterm (CombConst ((c, _), _, _)) = - Symtab.map_entry c (Integer.add 1) +fun count_combterm (CombConst ((s, _), _, _)) = + Symtab.map_entry s (Integer.add 1) | count_combterm (CombVar _) = I - | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2 -fun count_literal (FOLLiteral (_, t)) = count_combterm t -fun count_clause (FOLClause {literals, ...}) = fold count_literal literals + | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2] +fun count_combformula (AQuant (_, _, phi)) = count_combformula phi + | count_combformula (AConn (_, phis)) = fold count_combformula phis + | count_combformula (APred tm) = count_combterm tm +fun count_fol_formula (FOLFormula {combformula, ...}) = + count_combformula combformula fun cnf_helper_thms thy raw = map (`Thm.get_name_hint) @@ -202,7 +208,8 @@ fun get_helper_clauses thy is_FO full_types conjectures axcls = let val axclauses = map snd (make_axiom_clauses thy axcls) - val ct = fold (fold count_clause) [conjectures, axclauses] init_counters + val ct = fold (fold count_fol_formula) [conjectures, axclauses] + init_counters fun is_needed c = the (Symtab.lookup ct c) > 0 val cnfs = (optional_helpers @@ -289,7 +296,7 @@ fun generic_tptp_prover (name, {home_var, executable, arguments, proof_delims, known_failures, - max_axiom_clauses, prefers_theory_relevant}) + max_axiom_clauses, prefers_theory_relevant, explicit_forall}) ({debug, overlord, full_types, explicit_apply, relevance_threshold, relevance_convergence, theory_relevant, defs_relevant, isar_proof, isar_shrink_factor, ...} : params) @@ -378,8 +385,8 @@ in (output, msecs, proof, outcome) end val readable_names = debug andalso overlord val (pool, conjecture_offset) = - write_tptp_file thy readable_names full_types explicit_apply - probfile clauses + write_tptp_file thy readable_names explicit_forall full_types + explicit_apply probfile clauses val conjecture_shape = shape_of_clauses (conjecture_offset + 1) goal_clss val result = do_run false @@ -450,7 +457,8 @@ (OutOfResources, "SZS status: ResourceOut"), (OutOfResources, "SZS status ResourceOut")], max_axiom_clauses = 100, - prefers_theory_relevant = false} + prefers_theory_relevant = false, + explicit_forall = false} val e = tptp_prover "e" e_config @@ -474,7 +482,8 @@ (MalformedInput, "Free Variable"), (OldSpass, "tptp2dfg")], max_axiom_clauses = 40, - prefers_theory_relevant = true} + prefers_theory_relevant = true, + explicit_forall = true} val spass = tptp_prover "spass" spass_config (* Vampire *) @@ -495,7 +504,8 @@ (Unprovable, "Satisfiability detected"), (OutOfResources, "Refutation not found")], max_axiom_clauses = 60, - prefers_theory_relevant = false} + prefers_theory_relevant = false, + explicit_forall = false} val vampire = tptp_prover "vampire" vampire_config (* Remote prover invocation via SystemOnTPTP *) @@ -528,7 +538,8 @@ fun remote_config atp_prefix args ({proof_delims, known_failures, max_axiom_clauses, - prefers_theory_relevant, ...} : prover_config) : prover_config = + prefers_theory_relevant, explicit_forall, ...} : prover_config) + : prover_config = {home_var = "ISABELLE_ATP_MANAGER", executable = "SystemOnTPTP", arguments = fn _ => fn timeout => @@ -537,7 +548,8 @@ proof_delims = insert (op =) tstp_proof_delims proof_delims, known_failures = remote_known_failures @ known_failures, max_axiom_clauses = max_axiom_clauses, - prefers_theory_relevant = prefers_theory_relevant} + prefers_theory_relevant = prefers_theory_relevant, + explicit_forall = explicit_forall} fun remote_tptp_prover prover atp_prefix args config = tptp_prover (remotify (fst prover)) (remote_config atp_prefix args config) diff -r bb39190370fe -r b04307085a09 src/HOL/Tools/Sledgehammer/metis_clauses.ML --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Mon Jul 26 11:26:47 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Mon Jul 26 14:14:24 2010 +0200 @@ -61,7 +61,7 @@ val type_literals_for_types : typ list -> type_literal list val make_class_rel_clauses: theory -> class list -> class list -> class_rel_clause list val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list - val type_of_combterm : combterm -> combtyp + val combtyp_of : combterm -> combtyp val strip_combterm_comb : combterm -> combterm * combterm list val literals_of_term : theory -> term -> fol_literal list * typ list val conceal_skolem_terms : @@ -373,9 +373,9 @@ fun result_type (CombType (_, [_, tp2])) = tp2 | result_type _ = raise Fail "non-function type" -fun type_of_combterm (CombConst (_, tp, _)) = tp - | type_of_combterm (CombVar (_, tp)) = tp - | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1) +fun combtyp_of (CombConst (_, tp, _)) = tp + | combtyp_of (CombVar (_, tp)) = tp + | combtyp_of (CombApp (t1, _)) = result_type (combtyp_of t1) (*gets the head of a combinator application, along with the list of arguments*) fun strip_combterm_comb u = diff -r bb39190370fe -r b04307085a09 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Jul 26 11:26:47 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Jul 26 14:14:24 2010 +0200 @@ -100,7 +100,7 @@ wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty) | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) = wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]), - type_of_combterm tm); + combtyp_of tm) fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) = let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm diff -r bb39190370fe -r b04307085a09 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Mon Jul 26 11:26:47 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Mon Jul 26 14:14:24 2010 +0200 @@ -126,8 +126,7 @@ \option (e.g., \"timeout = " ^ string_of_int (10 + msecs div 1000) ^ " s\").") | {message, ...} => (NONE, "ATP error: " ^ message)) - handle TRIVIAL () => (SOME [], metis_line full_types i n []) - | ERROR msg => (NONE, "Error: " ^ msg) + handle ERROR msg => (NONE, "Error: " ^ msg) end end; diff -r bb39190370fe -r b04307085a09 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Jul 26 11:26:47 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Jul 26 14:14:24 2010 +0200 @@ -202,7 +202,7 @@ (**** INTERPRETATION OF TSTP SYNTAX TREES ****) exception FO_TERM of string fo_term list -exception FORMULA of string formula list +exception FORMULA of (string, string fo_term) formula list exception SAME of unit (* Type variables are given the basic sort "HOL.type". Some will later be diff -r bb39190370fe -r b04307085a09 src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Mon Jul 26 11:26:47 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Mon Jul 26 14:14:24 2010 +0200 @@ -7,23 +7,32 @@ signature SLEDGEHAMMER_TPTP_FORMAT = sig + type name = Metis_Clauses.name + type kind = Metis_Clauses.kind + type combterm = Metis_Clauses.combterm type class_rel_clause = Metis_Clauses.class_rel_clause type arity_clause = Metis_Clauses.arity_clause - type fol_clause = Metis_Clauses.fol_clause datatype 'a fo_term = ATerm of 'a * 'a fo_term list datatype quantifier = AForall | AExists datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff - datatype 'a formula = - AQuant of quantifier * 'a list * 'a formula | - AConn of connective * 'a formula list | - APred of 'a fo_term + datatype ('a, 'b) formula = + AQuant of quantifier * 'a list * ('a, 'b) formula | + AConn of connective * ('a, 'b) formula list | + APred of 'b + + datatype fol_formula = + FOLFormula of {formula_name: string, + formula_id: int, + kind: kind, + combformula: (name, combterm) formula, + ctypes_sorts: typ list} val axiom_prefix : string val conjecture_prefix : string val write_tptp_file : theory -> bool -> bool -> bool -> bool -> Path.T - -> fol_clause list * fol_clause list * fol_clause list * fol_clause list + -> fol_formula list * fol_formula list * fol_formula list * fol_formula list * class_rel_clause list * arity_clause list -> string Symtab.table * int end; @@ -40,14 +49,17 @@ datatype 'a fo_term = ATerm of 'a * 'a fo_term list datatype quantifier = AForall | AExists datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff -datatype 'a formula = - AQuant of quantifier * 'a list * 'a formula | - AConn of connective * 'a formula list | - APred of 'a fo_term +datatype ('a, 'b) formula = + AQuant of quantifier * 'a list * ('a, 'b) formula | + AConn of connective * ('a, 'b) formula list | + APred of 'b fun mk_anot phi = AConn (ANot, [phi]) +fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) +fun mk_adisjunction [] = APred (ATerm (("$false", "$false"), [])) + | mk_adisjunction (phi :: phis) = fold (mk_aconn AOr) phis phi -datatype 'a problem_line = Fof of string * kind * 'a formula +datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula type 'a problem = (string * 'a problem_line list) list fun string_for_term (ATerm (s, [])) = s @@ -148,6 +160,13 @@ (** Sledgehammer stuff **) +datatype fol_formula = + FOLFormula of {formula_name: string, + formula_id: int, + kind: kind, + combformula: (name, combterm) formula, + ctypes_sorts: typ list} + val axiom_prefix = "ax_" val conjecture_prefix = "conj_" val arity_clause_prefix = "clsarity_" @@ -159,50 +178,52 @@ | fo_term_for_combtyp (CombType (name, tys)) = ATerm (name, map fo_term_for_combtyp tys) -fun fo_term_for_combterm full_types top_level u = - let - val (head, args) = strip_combterm_comb u - val (x, ty_args) = - case head of - CombConst (name, _, ty_args) => - if fst name = "equal" then - (if top_level andalso length args = 2 then name - else ("c_fequal", @{const_name fequal}), []) - else - (name, if full_types then [] else ty_args) - | CombVar (name, _) => (name, []) - | CombApp _ => raise Fail "impossible \"CombApp\"" - 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 (fo_term_for_combtyp (type_of_combterm u)) t - else t - end - -fun fo_literal_for_literal full_types (FOLLiteral (pos, t)) = - (pos, fo_term_for_combterm full_types true t) - fun fo_literal_for_type_literal pos (TyLitVar (class, name)) = (pos, ATerm (class, [ATerm (name, [])])) | fo_literal_for_type_literal pos (TyLitFree (class, name)) = (pos, ATerm (class, [ATerm (name, [])])) 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] = formula_for_fo_literal lit - | 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) +fun fo_term_for_combterm full_types = + let + fun aux top_level u = + let + val (head, args) = strip_combterm_comb u + val (x, ty_args) = + case head of + CombConst (name, _, ty_args) => + if fst name = "equal" then + (if top_level andalso length args = 2 then name + else ("c_fequal", @{const_name fequal}), []) + else + (name, if full_types then [] else ty_args) + | CombVar (name, _) => (name, []) + | CombApp _ => raise Fail "impossible \"CombApp\"" + val t = ATerm (x, map fo_term_for_combtyp ty_args @ + map (aux false) args) + in + if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t + end + in aux true end + +fun formula_for_combformula full_types = + 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 (fo_term_for_combterm full_types tm) + in aux end + +fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) = + formula_for_combformula full_types combformula :: + map (formula_for_fo_literal o fo_literal_for_type_literal false) (type_literals_for_types ctypes_sorts) - |> formula_for_fo_literals + |> mk_adisjunction fun problem_line_for_axiom full_types - (clause as FOLClause {axiom_name, kind, ...}) = - Fof (axiom_prefix ^ ascii_of axiom_name, kind, - formula_for_axiom full_types clause) + (formula as FOLFormula {formula_name, kind, ...}) = + Fof (axiom_prefix ^ ascii_of formula_name, kind, + formula_for_axiom full_types formula) fun problem_line_for_class_rel_clause (ClassRelClause {axiom_name, subclass, superclass, ...}) = @@ -220,16 +241,16 @@ fun problem_line_for_arity_clause (ArityClause {axiom_name, conclLit, premLits, ...}) = Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom, - map fo_literal_for_arity_literal (conclLit :: premLits) - |> formula_for_fo_literals) + conclLit :: premLits + |> map (formula_for_fo_literal o fo_literal_for_arity_literal) + |> mk_adisjunction) fun problem_line_for_conjecture full_types - (clause as FOLClause {clause_id, kind, literals, ...}) = - Fof (conjecture_prefix ^ Int.toString clause_id, - kind, map (fo_literal_for_literal full_types) literals - |> formula_for_fo_literals |> mk_anot) + (FOLFormula {formula_id, kind, combformula, ...}) = + Fof (conjecture_prefix ^ Int.toString formula_id, kind, + formula_for_combformula full_types combformula) -fun atp_free_type_literals_for_conjecture (FOLClause {ctypes_sorts, ...}) = +fun atp_free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) = map (fo_literal_for_type_literal true) (type_literals_for_types ctypes_sorts) fun problem_line_for_free_type lit =