# HG changeset patch # User blanchet # Date 1335392886 -7200 # Node ID ba321ce6f344eaccae10b065ebdba22ba7fe87fe # Parent 53e30966b4b6dc4440d4bdc1acbc76ecae20a49b tuning; no need for relevance filter diff -r 53e30966b4b6 -r ba321ce6f344 src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML Wed Apr 25 23:39:19 2012 +0200 +++ b/src/HOL/TPTP/atp_problem_import.ML Thu Apr 26 00:28:06 2012 +0200 @@ -22,7 +22,7 @@ open ATP_Proof -(** TPTP parsing based on ML-Yacc-generated "TPTP_Parser" **) +(** TPTP parsing **) (* cf. "close_form" in "refute.ML" *) fun close_form t = @@ -46,9 +46,10 @@ ||> List.partition (has_role TPTP_Syntax.Role_Definition) in (map get_prop conjs, pairself (map get_prop) defs_and_nondefs, - Theory.checkpoint thy) + thy |> Theory.checkpoint |> Proof_Context.init_global) end + (** Nitpick (alias Nitrox) **) fun aptrueprop f ((t0 as @{const Trueprop}) $ t1) = t0 $ f t1 @@ -56,8 +57,8 @@ fun nitpick_tptp_file timeout file_name = let - val (conjs, (defs, nondefs), thy) = read_tptp_file @{theory} file_name - val ctxt = Proof_Context.init_global thy + val (conjs, (defs, nondefs), ctxt) = read_tptp_file @{theory} file_name + val thy = Proof_Context.theory_of ctxt val defs = defs |> map (ATP_Util.extensionalize_term ctxt #> aptrueprop (open_form I)) val state = Proof.init ctxt @@ -101,8 +102,7 @@ else "Unknown") |> writeln - val (conjs, (defs, nondefs), thy) = read_tptp_file @{theory} file_name - val ctxt = Proof_Context.init_global thy + val (conjs, (defs, nondefs), ctxt) = read_tptp_file @{theory} file_name val params = [("maxtime", string_of_int timeout), ("maxvars", "100000")] @@ -115,6 +115,12 @@ (** Sledgehammer and Isabelle (combination of provers) **) +val cvc3N = "cvc3" +val z3N = "z3" + +fun can_tac ctxt tactic conj = + can (Goal.prove ctxt [] [] conj) (K tactic) + fun SOLVE_TIMEOUT seconds name tac st = let val result = @@ -128,20 +134,7 @@ | 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 - 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 i = 1 fun atp_tac ctxt timeout prover = Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt @@ -152,15 +145,12 @@ *) ("provers", prover), ("timeout", string_of_int timeout)] - Sledgehammer_Filter.no_relevance_override - -val cvc3N = "cvc3" -val z3N = "z3" + {add = [], del = [], only = true} i fun sledgehammer_tac ctxt timeout = let fun slice timeout prover = - SOLVE_TIMEOUT timeout prover (ALLGOALS (atp_tac ctxt timeout prover)) + SOLVE_TIMEOUT timeout prover (atp_tac ctxt timeout prover) in slice (timeout div 10) ATP_Systems.spassN ORELSE @@ -177,37 +167,54 @@ slice timeout ATP_Systems.satallaxN end -val sledgehammer_tptp_file = apply_tactic_to_tptp_file sledgehammer_tac - -(** Isabelle (combination of provers) **) - -fun isabelle_tac ctxt timeout = - sledgehammer_tac ctxt (timeout div 2) +fun auto_etc_tac ctxt timeout = + SOLVE_TIMEOUT (timeout div 10) "simp" (asm_full_simp_tac (simpset_of ctxt) i) 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)) + SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i) ORELSE SOLVE_TIMEOUT (timeout div 20) "auto+spass" - (auto_tac ctxt - THEN ALLGOALS (atp_tac ctxt (timeout div 20) ATP_Systems.spassN)) + (auto_tac ctxt THEN atp_tac ctxt (timeout div 20) ATP_Systems.spassN) + ORELSE + SOLVE_TIMEOUT (timeout div 20) "fast" (fast_tac ctxt i) ORELSE - SOLVE_TIMEOUT (timeout div 20) "fast" (ALLGOALS (fast_tac ctxt)) + SOLVE_TIMEOUT (timeout div 20) "best" (best_tac ctxt i) ORELSE - SOLVE_TIMEOUT (timeout div 20) "best" (ALLGOALS (best_tac ctxt)) + SOLVE_TIMEOUT (timeout div 20) "force" (force_tac ctxt i) ORELSE - SOLVE_TIMEOUT (timeout div 20) "force" (ALLGOALS (force_tac ctxt)) + SOLVE_TIMEOUT (timeout div 20) "arith" (Arith_Data.arith_tac ctxt i) 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)) + SOLVE_TIMEOUT timeout "fastforce" (fast_force_tac ctxt i) + +fun make_conj assms conjs = + (rev assms, case conjs of conj :: _ => conj | [] => @{prop False}) + |> Logic.list_implies + +fun print_szs_from_success conjs success = + writeln ("% SZS status " ^ + (if success then + if null conjs then "Unsatisfiable" else "Theorem" + else + "% SZS status Unknown")) -val isabelle_tptp_file = apply_tactic_to_tptp_file isabelle_tac +fun sledgehammer_tptp_file timeout file_name = + let + val (conjs, (defs, nondefs), ctxt) = read_tptp_file @{theory} file_name + val conj = make_conj (defs @ nondefs) conjs + in + can_tac ctxt (sledgehammer_tac ctxt timeout) conj + |> print_szs_from_success conjs + end +fun isabelle_tptp_file timeout file_name = + let + val (conjs, (defs, nondefs), ctxt) = read_tptp_file @{theory} file_name + val conj = make_conj (defs @ nondefs) conjs + in + (can_tac ctxt (sledgehammer_tac ctxt (timeout div 2)) conj orelse + can_tac ctxt (auto_etc_tac ctxt (timeout div 2)) conj orelse + can_tac ctxt (atp_tac ctxt timeout ATP_Systems.satallaxN) conj) + |> print_szs_from_success conjs + end (** Translator between TPTP(-like) file formats **)