--- 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 =
--- 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
--- 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)
--- 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 =
--- 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
--- 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;
--- 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
--- 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 =