--- a/src/HOL/TPTP/atp_problem_import.ML Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Thu Aug 07 12:17:41 2014 +0200
@@ -45,20 +45,18 @@
fun read_tptp_file thy postproc file_name =
let
fun has_role role (_, role', _, _) = (role' = role)
- fun get_prop (name, role, P, info) =
- let val P' = P |> Logic.varify_global |> close_form in
- (name, P') |> postproc
- end
+ fun get_prop f (name, _, P, _) = P |> f |> close_form |> pair name |> postproc
+
val path = exploded_absolute_path file_name
val ((_, _, problem), thy) =
- TPTP_Interpret.interpret_file true [Path.dir path, Path.explode "$TPTP"]
- path [] [] thy
- val (conjs, defs_and_nondefs) =
- problem |> List.partition (has_role TPTP_Syntax.Role_Conjecture)
- ||> List.partition (has_role TPTP_Syntax.Role_Definition)
+ TPTP_Interpret.interpret_file true [Path.dir path, Path.explode "$TPTP"] path [] [] thy
+ val (conjs, defs_and_nondefs) = problem
+ |> List.partition (has_role TPTP_Syntax.Role_Conjecture)
+ ||> List.partition (has_role TPTP_Syntax.Role_Definition)
in
- (map get_prop conjs, pairself (map get_prop) defs_and_nondefs,
- thy |> Proof_Context.init_global)
+ (map (get_prop I) conjs,
+ pairself (map (get_prop Logic.varify_global)) defs_and_nondefs,
+ Proof_Context.init_global thy)
end
@@ -76,12 +74,10 @@
let
val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name
val thy = Proof_Context.theory_of ctxt
- val (defs, pseudo_defs) =
- defs |> map (ATP_Util.abs_extensionalize_term ctxt
- #> aptrueprop (hol_open_form I))
- |> List.partition (is_legitimate_tptp_def
- o perhaps (try HOLogic.dest_Trueprop)
- o ATP_Util.unextensionalize_def)
+ val (defs, pseudo_defs) = defs
+ |> map (ATP_Util.abs_extensionalize_term ctxt #> aptrueprop (hol_open_form I))
+ |> List.partition (is_legitimate_tptp_def o perhaps (try HOLogic.dest_Trueprop)
+ o ATP_Util.unextensionalize_def)
val nondefs = pseudo_defs @ nondefs
val state = Proof.init ctxt
val params =
@@ -104,8 +100,8 @@
val step = 0
val subst = []
in
- Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst
- defs nondefs (case conjs of conj :: _ => conj | [] => @{prop True});
+ Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst defs nondefs
+ (case conjs of conj :: _ => conj | [] => @{prop True});
()
end
@@ -127,7 +123,7 @@
("maxvars", "100000")]
in
Refute.refute_term ctxt params (defs @ nondefs)
- (case conjs of conj :: _ => conj | [] => @{prop True})
+ (case conjs of conj :: _ => conj | [] => @{prop True})
|> print_szs_of_outcome (not (null conjs))
end
@@ -138,17 +134,16 @@
fun SOLVE_TIMEOUT seconds name tac st =
let
- val _ = Output.urgent_message ("running " ^ name ^ " for " ^
- string_of_int seconds ^ " s")
+ val _ = Output.urgent_message ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s")
val result =
- TimeLimit.timeLimit (Time.fromSeconds seconds)
- (fn () => SINGLE (SOLVE tac) st) ()
- handle TimeLimit.TimeOut => NONE
- | ERROR _ => NONE
+ TimeLimit.timeLimit (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) ()
+ handle
+ TimeLimit.TimeOut => NONE
+ | ERROR _ => NONE
in
- case result of
+ (case result of
NONE => (Output.urgent_message ("FAILURE: " ^ name); Seq.empty)
- | SOME st' => (Output.urgent_message ("SUCCESS: " ^ name); Seq.single st')
+ | SOME st' => (Output.urgent_message ("SUCCESS: " ^ name); Seq.single st'))
end
fun nitpick_finite_oracle_tac ctxt timeout i th =
@@ -157,6 +152,7 @@
| is_safe @{typ prop} = true
| is_safe @{typ bool} = true
| is_safe _ = false
+
val conj = Thm.term_of (Thm.cprem_of th i)
in
if exists_type (not o is_safe) conj then
@@ -179,29 +175,28 @@
val step = 0
val subst = []
val (outcome, _) =
- Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst
- [] [] conj
- in if outcome = "none" then ALLGOALS Skip_Proof.cheat_tac th else Seq.empty end
+ Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst [] [] conj
+ in
+ if outcome = "none" then ALLGOALS Skip_Proof.cheat_tac th else Seq.empty
+ end
end
fun atp_tac ctxt completeness override_params timeout prover =
let
- val ctxt =
- ctxt |> Config.put Sledgehammer_Prover_ATP.atp_completish (completeness > 0)
+ val ctxt = ctxt |> Config.put Sledgehammer_Prover_ATP.atp_completish (completeness > 0)
fun ref_of th = (Facts.named (Thm.derivation_name th), [])
in
Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
- ([("debug", if debug then "true" else "false"),
- ("overlord", if overlord then "true" else "false"),
- ("provers", prover),
- ("timeout", string_of_int timeout)] @
- (if completeness > 0 then
- [("type_enc",
- if completeness = 1 then "mono_native" else "poly_tags")]
- else
- []) @
- override_params)
- {add = map ref_of [ext, @{thm someI}], del = [], only = true}
+ ([("debug", if debug then "true" else "false"),
+ ("overlord", if overlord then "true" else "false"),
+ ("provers", prover),
+ ("timeout", string_of_int timeout)] @
+ (if completeness > 0 then
+ [("type_enc", if completeness = 1 then "mono_native" else "poly_tags")]
+ else
+ []) @
+ override_params)
+ {add = map ref_of [ext, @{thm someI}], del = [], only = true}
end
fun sledgehammer_tac demo ctxt timeout i =
@@ -209,10 +204,8 @@
val frac = if demo then 16 else 12
fun slice mult completeness prover =
SOLVE_TIMEOUT (mult * timeout div frac)
- (prover ^
- (if completeness > 0 then "(" ^ string_of_int completeness ^ ")"
- else ""))
- (atp_tac ctxt completeness [] (mult * timeout div frac) prover i)
+ (prover ^ (if completeness > 0 then "(" ^ string_of_int completeness ^ ")" else ""))
+ (atp_tac ctxt completeness [] (mult * timeout div frac) prover i)
in
slice 2 0 ATP_Proof.spassN
ORELSE slice 2 0 ATP_Proof.vampireN
@@ -236,14 +229,11 @@
in SMT_Solver.smt_tac ctxt [] end
fun auto_etc_tac ctxt timeout i =
- SOLVE_TIMEOUT (timeout div 20) "nitpick"
- (nitpick_finite_oracle_tac ctxt (timeout div 20) i)
- ORELSE SOLVE_TIMEOUT (timeout div 10) "simp"
- (asm_full_simp_tac ctxt i)
+ SOLVE_TIMEOUT (timeout div 20) "nitpick" (nitpick_finite_oracle_tac ctxt (timeout div 20) i)
+ ORELSE SOLVE_TIMEOUT (timeout div 10) "simp" (asm_full_simp_tac ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
- (auto_tac ctxt
- THEN ALLGOALS (atp_tac ctxt 0 [] (timeout div 5) ATP_Proof.spassN))
+ (auto_tac ctxt THEN ALLGOALS (atp_tac ctxt 0 [] (timeout div 5) ATP_Proof.spassN))
ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc3" (smt_solver_tac "cvc3" ctxt i)
@@ -258,27 +248,24 @@
unfold "definitions" of free variables than of constants (cf. PUZ107^5). *)
fun freeze_problem_consts thy =
let val is_problem_const = String.isPrefix (problem_const_prefix thy) in
- map_aterms (fn t as Const (s, T) =>
- if is_problem_const s then Free (Long_Name.base_name s, T)
- else t
- | t => t)
+ map_aterms
+ (fn t as Const (s, T) => if is_problem_const s then Free (Long_Name.base_name s, T) else t
+ | t => t)
end
fun make_conj (defs, nondefs) conjs =
- Logic.list_implies (rev defs @ rev nondefs,
- case conjs of conj :: _ => conj | [] => @{prop False})
+ Logic.list_implies (rev defs @ rev nondefs, case conjs of conj :: _ => conj | [] => @{prop False})
fun print_szs_of_success conjs success =
Output.urgent_message ("% SZS status " ^
- (if success then
- if null conjs then "Unsatisfiable" else "Theorem"
- else
- "Unknown"))
+ (if success then
+ if null conjs then "Unsatisfiable" else "Theorem"
+ else
+ "Unknown"))
fun sledgehammer_tptp_file thy timeout file_name =
let
- val (conjs, assms, ctxt) =
- read_tptp_file thy (freeze_problem_consts thy o snd) file_name
+ val (conjs, assms, ctxt) = read_tptp_file thy (freeze_problem_consts thy o snd) file_name
val conj = make_conj assms conjs
in
can_tac ctxt (sledgehammer_tac true ctxt timeout 1) conj
@@ -287,8 +274,7 @@
fun generic_isabelle_tptp_file demo thy timeout file_name =
let
- val (conjs, assms, ctxt) =
- read_tptp_file thy (freeze_problem_consts thy o snd) file_name
+ val (conjs, assms, ctxt) = read_tptp_file thy (freeze_problem_consts thy o snd) file_name
val conj = make_conj assms conjs
val (last_hope_atp, last_hope_completeness) =
if demo then (ATP_Proof.satallaxN, 0) else (ATP_Proof.vampireN, 2)
@@ -296,7 +282,7 @@
(can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) 1) conj orelse
can_tac ctxt (SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
- (atp_tac ctxt last_hope_completeness [] timeout last_hope_atp 1)) conj)
+ (atp_tac ctxt last_hope_completeness [] timeout last_hope_atp 1)) conj)
|> print_szs_of_success conjs
end
@@ -322,7 +308,8 @@
val uncurried_aliases = false
val readable_names = true
val presimp = true
- val facts = map (apfst (rpair (Global, Non_Rec_Def))) defs @
+ val facts =
+ map (apfst (rpair (Global, Non_Rec_Def))) defs @
map (apfst (rpair (Global, General))) nondefs
val (atp_problem, _, _, _) =
generate_atp_problem ctxt format Hypothesis (type_enc_of_string Strict type_enc) Translator