--- a/src/HOL/TPTP/ATP_Problem_Import.thy Wed Apr 25 22:00:33 2012 +0200
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy Wed Apr 25 22:00:33 2012 +0200
@@ -6,7 +6,8 @@
theory ATP_Problem_Import
imports Complex_Main TPTP_Interpret
-uses ("atp_problem_import.ML")
+uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
+ ("atp_problem_import.ML")
begin
ML {* Proofterm.proofs := 0 *}
--- a/src/HOL/TPTP/atp_problem_import.ML Wed Apr 25 22:00:33 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Wed Apr 25 22:00:33 2012 +0200
@@ -85,23 +85,22 @@
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});
+ defs nondefs (case conjs of conj :: _ => conj | [] => @{prop True});
()
end
(** Refute **)
-fun print_szs_from_outcome falsify s =
- "% SZS status " ^
- (if s = "genuine" then
- if falsify then "CounterSatisfiable" else "Satisfiable"
- else
- "Unknown")
- |> writeln
-
fun refute_tptp_file timeout file_name =
let
+ fun print_szs_from_outcome falsify s =
+ "% SZS status " ^
+ (if s = "genuine" then
+ if falsify then "CounterSatisfiable" else "Satisfiable"
+ else
+ "Unknown")
+ |> writeln
val (conjs, (defs, nondefs), thy) = read_tptp_file @{theory} file_name
val ctxt = Proof_Context.init_global thy
val params =
@@ -109,32 +108,106 @@
("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_from_outcome (not (null conjs))
end
-(** Sledgehammer **)
+(** Sledgehammer and Isabelle (combination of provers) **)
+
+fun SOLVE_TIMEOUT seconds name tac st =
+ let
+ val result =
+ TimeLimit.timeLimit (Time.fromSeconds seconds)
+ (fn () => SINGLE (SOLVE tac) st) ()
+ handle TimeLimit.TimeOut => NONE
+ | ERROR _ => NONE
+ in
+ (case result of
+ NONE => (warning ("FAILURE: " ^ name); Seq.empty)
+ | SOME st' => (warning ("SUCCESS: " ^ name); Seq.single st'))
+ end
fun apply_tactic_to_tptp_file tactic timeout file_name =
let
val (conjs, (defs, nondefs), thy) = read_tptp_file @{theory} file_name
val ctxt = Proof_Context.init_global thy
+ val conj =
+ Logic.list_implies (defs @ nondefs,
+ case conjs of conj :: _ => conj | [] => @{prop False})
in
- Goal.prove ctxt [] (defs @ nondefs) (hd conjs) (fn _ => tactic ctxt
+ case try (Goal.prove ctxt [] [] conj) (K (tactic ctxt timeout)) of
+ SOME _ =>
+ writeln ("% SZS status " ^
+ (if null conjs then "Unsatisfiable" else "Theorem"))
+ | NONE => writeln ("% SZS status Unknown")
end
-val sledgehammer_tptp_file =
- apply_tactic_to_tptp_file Sledgehammer_Tactics.sledgehammer_as_oracle_tac
+fun atp_tac ctxt timeout prover =
+ Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
+ [
+(*
+ ("debug", "true"),
+ ("overlord", "true"),
+*)
+ ("provers", prover),
+ ("timeout", string_of_int timeout)]
+ Sledgehammer_Filter.no_relevance_override
+
+val cvc3N = "cvc3"
+val z3N = "z3"
+fun sledgehammer_tac ctxt timeout =
+ let
+ fun slice timeout prover =
+ SOLVE_TIMEOUT timeout prover (ALLGOALS (atp_tac ctxt timeout prover))
+ in
+ slice (timeout div 10) ATP_Systems.spassN
+ ORELSE
+ slice (timeout div 10) z3N
+ ORELSE
+ slice (timeout div 10) ATP_Systems.vampireN
+ ORELSE
+ slice (timeout div 10) ATP_Systems.eN
+ ORELSE
+ slice (timeout div 10) cvc3N
+ ORELSE
+ slice (timeout div 10) ATP_Systems.leo2N
+ ORELSE
+ slice timeout ATP_Systems.satallaxN
+ end
+
+val sledgehammer_tptp_file = apply_tactic_to_tptp_file sledgehammer_tac
(** Isabelle (combination of provers) **)
-val isabelle_tac =
- ...
+fun isabelle_tac ctxt timeout =
+ sledgehammer_tac ctxt (timeout div 2)
+ ORELSE
+ SOLVE_TIMEOUT (timeout div 10) "simp"
+ (ALLGOALS (asm_full_simp_tac (simpset_of ctxt)))
+ ORELSE
+ SOLVE_TIMEOUT (timeout div 10) "blast" (ALLGOALS (blast_tac ctxt))
+ ORELSE
+ SOLVE_TIMEOUT (timeout div 20) "auto+spass"
+ (auto_tac ctxt
+ THEN ALLGOALS (atp_tac ctxt (timeout div 20) ATP_Systems.spassN))
+ ORELSE
+ SOLVE_TIMEOUT (timeout div 20) "fast" (ALLGOALS (fast_tac ctxt))
+ ORELSE
+ SOLVE_TIMEOUT (timeout div 20) "best" (ALLGOALS (best_tac ctxt))
+ ORELSE
+ SOLVE_TIMEOUT (timeout div 20) "force" (ALLGOALS (force_tac ctxt))
+ ORELSE
+ SOLVE_TIMEOUT (timeout div 20) "arith" (ALLGOALS (Arith_Data.arith_tac ctxt))
+ ORELSE
+ SOLVE_TIMEOUT timeout "fastforce" (ALLGOALS (fast_force_tac ctxt))
+ ORELSE
+ SOLVE_TIMEOUT timeout "satallax"
+ (ALLGOALS (atp_tac ctxt timeout ATP_Systems.satallaxN))
-val isabelle_tptp_file =
- ...
+val isabelle_tptp_file = apply_tactic_to_tptp_file isabelle_tac
+
(** Translator between TPTP(-like) file formats **)
--- a/src/HOL/ex/sledgehammer_tactics.ML Wed Apr 25 22:00:33 2012 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML Wed Apr 25 22:00:33 2012 +0200
@@ -68,17 +68,26 @@
end
fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
- case run_atp override_params relevance_override i i ctxt th of
- SOME facts =>
- Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt
- (maps (thms_of_name ctxt) facts) i th
- | NONE => Seq.empty
+ let
+ val override_params =
+ override_params @
+ [("preplay_timeout", "0")]
+ in
+ case run_atp override_params relevance_override i i ctxt th of
+ SOME facts =>
+ Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
+ (maps (thms_of_name ctxt) facts) i th
+ | NONE => Seq.empty
+ end
fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =
let
val thy = Proof_Context.theory_of ctxt
- val xs = run_atp (override_params @ [("sound", "true")]) relevance_override
- i i ctxt th
+ val override_params =
+ override_params @
+ [("preplay_timeout", "0"),
+ ("minimize", "false")]
+ val xs = run_atp override_params relevance_override i i ctxt th
in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
end;