--- a/src/HOL/Tools/ATP/atp_problem.ML Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue May 31 16:38:36 2011 +0200
@@ -17,7 +17,7 @@
datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
- datatype format = CNF_UEQ | FOF | TFF | THF
+ datatype format = CNF | CNF_UEQ | FOF | TFF | THF
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Decl of string * 'a * 'a ho_type |
@@ -71,6 +71,8 @@
val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
val is_format_typed : format -> bool
val tptp_strings_for_atp_problem : format -> string problem -> string list
+ val ensure_cnf_problem :
+ (string * string) problem -> (string * string) problem
val filter_cnf_ueq_problem :
(string * string) problem -> (string * string) problem
val declare_undeclared_syms_in_atp_problem :
@@ -99,7 +101,7 @@
datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
-datatype format = CNF_UEQ | FOF | TFF | THF
+datatype format = CNF | CNF_UEQ | FOF | TFF | THF
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Decl of string * 'a * 'a ho_type |
@@ -256,7 +258,8 @@
val default_source =
ATerm ("inference", ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", [])))
-fun string_for_format CNF_UEQ = tptp_cnf
+fun string_for_format CNF = tptp_cnf
+ | string_for_format CNF_UEQ = tptp_cnf
| string_for_format FOF = tptp_fof
| string_for_format TFF = tptp_tff
| string_for_format THF = tptp_thf
@@ -306,6 +309,8 @@
Formula (ident, Hypothesis, mk_anot phi, source, info)
| negate_conjecture_line line = line
+fun ensure_cnf_problem problem = problem |> map (apsnd (map open_formula_line))
+
fun filter_cnf_ueq_problem problem =
problem
|> map (apsnd (map open_formula_line
--- a/src/HOL/Tools/ATP/atp_translate.ML Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Tue May 31 16:38:36 2011 +0200
@@ -52,7 +52,6 @@
type translated_formula
- val readable_names : bool Config.T
val type_tag_name : string
val bound_var_prefix : string
val schematic_var_prefix: string
@@ -113,7 +112,7 @@
val type_consts_of_terms : theory -> term list -> string list
val prepare_atp_problem :
Proof.context -> format -> formula_kind -> formula_kind -> type_system
- -> bool option -> term list -> term
+ -> bool option -> bool -> term list -> term
-> (translated_formula option * ((string * 'a) * thm)) list
-> string problem * string Symtab.table * int * int
* (string * 'a) list vector * int list * int Symtab.table
@@ -144,13 +143,6 @@
val elim_info = useful_isabelle_info "elim"
val simp_info = useful_isabelle_info "simp"
-(* Readable names are often much shorter, especially if types are mangled in
- names. Also, the logic for generating legal SNARK sort names is only
- implemented for readable names. Finally, readable names are, well, more
- readable. For these reason, they are enabled by default. *)
-val readable_names =
- Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)
-
val type_tag_name = "ti"
val bound_var_prefix = "B_"
@@ -1734,7 +1726,7 @@
val free_typesN = "Type variables"
fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
- explicit_apply hyp_ts concl_t facts =
+ explicit_apply readable_names hyp_ts concl_t facts =
let
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t facts
@@ -1781,14 +1773,16 @@
formula_lines_for_free_types format type_sys (facts @ conjs))]
val problem =
problem
- |> (if format = CNF_UEQ then filter_cnf_ueq_problem else I)
+ |> (case format of
+ CNF => ensure_cnf_problem
+ | CNF_UEQ => filter_cnf_ueq_problem
+ | _ => I)
|> (if is_format_typed format then
declare_undeclared_syms_in_atp_problem type_decl_prefix
implicit_declsN
else
I)
- val (problem, pool) =
- problem |> nice_atp_problem (Config.get ctxt readable_names)
+ val (problem, pool) = problem |> nice_atp_problem readable_names
val helpers_offset = offset_of_heading_in_problem helpersN problem 0
val typed_helpers =
map_filter (fn (j, {name, ...}) =>
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue May 31 16:38:36 2011 +0200
@@ -401,7 +401,7 @@
fun resolve_inf ctxt mode skolem_params thpairs atm th1 th2 =
let
val thy = Proof_Context.theory_of ctxt
- val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
+ val (i_th1, i_th2) = pairself (lookth thpairs) (th1, th2)
val _ = trace_msg ctxt (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
val _ = trace_msg ctxt (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
in
@@ -521,6 +521,7 @@
| path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
(*if not equality, ignore head to skip the hBOOL predicate*)
| path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*)
+ | path_finder New tm ps t = path_finder HO tm ps t (* ### *)
fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
in (tm, nt $ tm_rslt) end
--- a/src/HOL/Tools/Metis/metis_tactics.ML Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue May 31 16:38:36 2011 +0200
@@ -78,18 +78,14 @@
(Thm.get_name_hint th,
Meson_Clausify.cnf_axiom ctxt new_skolemizer j th))
(0 upto length ths0 - 1) ths0
- val thss = map (snd o snd) th_cls_pairs
+ val ths = maps (snd o snd) th_cls_pairs
val dischargers = map (fst o snd) th_cls_pairs
val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
- val _ = app (app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th))) thss
- val (mode, {axioms, tfrees, old_skolems}) =
- prepare_metis_problem ctxt mode cls thss
- val _ = if null tfrees then ()
- else (trace_msg ctxt (fn () => "TFREE CLAUSES");
- app (fn TyLitFree ((s, _), (s', _)) =>
- trace_msg ctxt (fn () => s ^ "(" ^ s' ^ ")")) tfrees)
+ val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
+ val (mode, {axioms, old_skolems, ...}) =
+ prepare_metis_problem ctxt mode cls ths
val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
val thms = map #1 axioms
val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
--- a/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200
@@ -25,12 +25,13 @@
val reveal_old_skolem_terms : (string * term) list -> term -> term
val string_of_mode : mode -> string
val prepare_metis_problem :
- Proof.context -> mode -> thm list -> thm list list -> mode * metis_problem
+ Proof.context -> mode -> thm list -> thm list -> mode * metis_problem
end
structure Metis_Translate : METIS_TRANSLATE =
struct
+open ATP_Problem
open ATP_Translate
val metis_generated_var_prefix = "_"
@@ -282,21 +283,54 @@
val class_rel_clauses = make_class_rel_clauses thy subs supers'
in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses end
+fun metis_name_from_atp s =
+ if is_tptp_equal s then "="
+ else if s = predicator_name then "{}"
+ else if s = app_op_name then "."
+ else s
+fun metis_term_from_atp (ATerm (s, tms)) =
+ if is_tptp_variable s then Metis_Term.Var s
+ else Metis_Term.Fn (metis_name_from_atp s, map metis_term_from_atp tms)
+fun metis_atom_from_atp (AAtom (ATerm (s, tms))) =
+ (metis_name_from_atp s, map metis_term_from_atp tms)
+ | metis_atom_from_atp _ = raise Fail "not CNF -- expected atom"
+fun metis_literal_from_atp (AConn (ANot, [phi])) =
+ (false, metis_atom_from_atp phi)
+ | metis_literal_from_atp phi = (true, metis_atom_from_atp phi)
+fun metis_literals_from_atp (AConn (AOr, [phi1, phi2])) =
+ uncurry (union (op =)) (pairself metis_literals_from_atp (phi1, phi2))
+ | metis_literals_from_atp phi = [metis_literal_from_atp phi]
+fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) =
+ let val j = ident |> unprefix conjecture_prefix |> Int.fromString |> the in
+ (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList
+ |> Metis_Thm.axiom,
+ Meson.make_meta_clause (nth clauses j))
+ end
+ | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
+
(* Function to generate metis clauses, including comb and type clauses *)
-fun prepare_metis_problem ctxt New conj_clauses fact_clausess =
+fun prepare_metis_problem ctxt New conj_clauses fact_clauses =
let
- val x = 1
- in
- error "Not implemented yet"
- end
- | prepare_metis_problem ctxt mode conj_clauses fact_clausess =
+ val type_sys = Preds (Polymorphic, (* Nonmonotonic_Types FIXME ### *) No_Types, Light)
+ val explicit_apply = NONE
+ val clauses = conj_clauses @ fact_clauses
+ val (atp_problem, pool, _, _, _, _, sym_tab) =
+ prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys
+ explicit_apply false (map prop_of clauses)
+ @{prop False} []
+ (* val _ = tracing (PolyML.makestring atp_problem) FIXME ### *)
+ val axioms =
+ atp_problem
+ |> maps (map_filter (try (metis_axiom_from_atp clauses)) o snd)
+ in (New, {axioms = axioms, tfrees = [], old_skolems = [] (* FIXME ### *)}) end
+ | prepare_metis_problem ctxt mode conj_clauses fact_clauses =
let
val thy = Proof_Context.theory_of ctxt
(* The modes FO and FT are sticky. HO can be downgraded to FO. *)
val mode =
if mode = HO andalso
forall (forall (is_quasi_fol_clause thy))
- (conj_clauses :: fact_clausess) then
+ [conj_clauses, fact_clauses] then
FO
else
mode
@@ -321,7 +355,7 @@
{axioms = [], tfrees = init_tfrees ctxt, old_skolems = []}
|> fold (add_thm true o `Meson.make_meta_clause) conj_clauses
|> add_tfrees
- |> fold (fold (add_thm false o `Meson.make_meta_clause)) fact_clausess
+ |> fold (add_thm false o `Meson.make_meta_clause) fact_clauses
val clause_lists = map (Metis_Thm.clause o #1) (#axioms problem)
fun is_used c =
exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists
@@ -343,8 +377,7 @@
if needs_full_types andalso mode <> FT then []
else map prepare_helper thms)
in problem |> fold (add_thm false) helper_ths end
- val type_ths =
- type_ext thy (maps (map prop_of) (conj_clauses :: fact_clausess))
+ val type_ths = type_ext thy (map prop_of (conj_clauses @ fact_clauses))
in (mode, fold add_type_thm type_ths problem) end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 31 16:38:36 2011 +0200
@@ -63,6 +63,10 @@
type prover =
params -> (string -> minimize_command) -> prover_problem -> prover_result
+ val dest_dir : string Config.T
+ val problem_prefix : string Config.T
+ val measure_run_time : bool Config.T
+ val atp_readable_names : bool Config.T
val smt_triggers : bool Config.T
val smt_weights : bool Config.T
val smt_weight_min_facts : int Config.T
@@ -90,9 +94,6 @@
val atp_relevance_fudge : relevance_fudge
val smt_relevance_fudge : relevance_fudge
val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge
- val dest_dir : string Config.T
- val problem_prefix : string Config.T
- val measure_run_time : bool Config.T
val weight_smt_fact :
Proof.context -> int -> ((string * locality) * thm) * int
-> (string * locality) * (int option * thm)
@@ -335,16 +336,20 @@
(* configuration attributes *)
+(* Empty string means create files in Isabelle's temporary files directory. *)
val dest_dir =
Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
- (* Empty string means create files in Isabelle's temporary files directory. *)
-
val problem_prefix =
Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
-
val measure_run_time =
Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false)
+(* In addition to being easier to read, readable names are often much shorter,
+ especially if types are mangled in names. For these reason, they are enabled
+ by default. *)
+val atp_readable_names =
+ Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)
+
val smt_triggers =
Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
val smt_weights =
@@ -661,7 +666,8 @@
val (atp_problem, pool, conjecture_offset, facts_offset,
fact_names, typed_helpers, sym_tab) =
prepare_atp_problem ctxt format conj_sym_kind prem_kind
- type_sys explicit_apply hyp_ts concl_t facts
+ type_sys explicit_apply
+ (Config.get ctxt atp_readable_names) hyp_ts concl_t facts
fun weights () = atp_problem_weights atp_problem
val core =
File.shell_path command ^ " " ^