# HG changeset patch # User blanchet # Date 1335521770 -7200 # Node ID d27bb852c430ae99062ce63a1148b128a3f50979 # Parent fe43977e434f8e3e01e452faa568744f5c600172 more tweaking of TPTP/CASC setup diff -r fe43977e434f -r d27bb852c430 src/HOL/TPTP/ATP_Problem_Import.thy --- a/src/HOL/TPTP/ATP_Problem_Import.thy Thu Apr 26 21:58:16 2012 +0200 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy Fri Apr 27 12:16:10 2012 +0200 @@ -15,4 +15,8 @@ declare [[show_consts]] (* for Refute *) declare [[smt_oracle]] +(* +ML {* ATP_Problem_Import.isabelle_tptp_file 100 "$TPTP/Problems/PUZ/PUZ107^5.p" *} +*) + end diff -r fe43977e434f -r d27bb852c430 src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML Thu Apr 26 21:58:16 2012 +0200 +++ b/src/HOL/TPTP/atp_problem_import.ML Fri Apr 27 12:16:10 2012 +0200 @@ -33,10 +33,11 @@ Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t'))) (Term.add_vars t []) t -fun read_tptp_file thy file_name = +fun read_tptp_file thy postproc file_name = let fun has_role role (_, role', _, _) = (role' = role) - fun get_prop (_, _, P, _) = P |> Logic.varify_global |> close_form + fun get_prop (_, _, P, _) = + P |> Logic.varify_global |> close_form |> postproc val path = Path.explode file_name |> (fn path => @@ -60,7 +61,7 @@ fun nitpick_tptp_file timeout file_name = let - val (conjs, (defs, nondefs), ctxt) = read_tptp_file @{theory} file_name + val (conjs, (defs, nondefs), ctxt) = read_tptp_file @{theory} I file_name val thy = Proof_Context.theory_of ctxt val defs = defs |> map (ATP_Util.extensionalize_term ctxt #> aptrueprop (open_form I)) @@ -103,7 +104,7 @@ else "Unknown") |> writeln - val (conjs, (defs, nondefs), ctxt) = read_tptp_file @{theory} file_name + val (conjs, (defs, nondefs), ctxt) = read_tptp_file @{theory} I file_name val params = [("maxtime", string_of_int timeout), ("maxvars", "100000")] @@ -119,38 +120,36 @@ val cvc3N = "cvc3" val z3N = "z3" -fun can_tac ctxt tactic conj = - can (Goal.prove ctxt [] [] conj) (K tactic) +fun can_tac ctxt tactic conj = can (Goal.prove ctxt [] [] conj) (K tactic) fun SOLVE_TIMEOUT seconds name tac st = let + val _ = writeln ("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 in - (case result of - NONE => (warning ("FAILURE: " ^ name); Seq.empty) - | SOME st' => (warning ("SUCCESS: " ^ name); Seq.single st')) + case result of + NONE => (writeln ("FAILURE: " ^ name); Seq.empty) + | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st') end -val i = 1 - fun atp_tac ctxt timeout prover = 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)] - {add = [], del = [], only = true} i + {add = [], del = [], only = true} -fun sledgehammer_tac ctxt timeout = +fun sledgehammer_tac ctxt timeout i = let fun slice timeout prover = - SOLVE_TIMEOUT timeout prover (atp_tac ctxt timeout prover) + SOLVE_TIMEOUT timeout prover (atp_tac ctxt timeout prover i) in - slice timeout ATP_Systems.satallaxN + slice (timeout div 10) ATP_Systems.satallaxN ORELSE slice (timeout div 10) ATP_Systems.spassN ORELSE @@ -165,13 +164,14 @@ slice (timeout div 10) ATP_Systems.leo2N end -fun auto_etc_tac ctxt timeout = +fun auto_etc_tac ctxt timeout i = SOLVE_TIMEOUT (timeout div 10) "simp" (asm_full_simp_tac (simpset_of ctxt) i) ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i) ORELSE SOLVE_TIMEOUT (timeout div 20) "auto+spass" - (auto_tac ctxt THEN atp_tac ctxt (timeout div 20) ATP_Systems.spassN) + (auto_tac ctxt + THEN ALLGOALS (atp_tac ctxt (timeout div 20) ATP_Systems.spassN)) ORELSE SOLVE_TIMEOUT (timeout div 20) "fast" (fast_tac ctxt i) ORELSE @@ -183,6 +183,18 @@ ORELSE SOLVE_TIMEOUT timeout "fastforce" (fast_force_tac ctxt i) +val problem_const_prefix = Context.theory_name @{theory} ^ Long_Name.separator + +(* Isabelle's standard automatic tactics ("auto", etc.) are more eager to + unfold "definitions" of free variables than of constants (cf. PUZ107^5). *) +val freeze_problem_consts = + map_aterms (fn t as Const (s, T) => + if String.isPrefix problem_const_prefix s then + Free (Long_Name.base_name s, T) + else + t + | t => t) + fun make_conj (defs, nondefs) conjs = Logic.list_implies (rev defs @ rev nondefs, case conjs of conj :: _ => conj | [] => @{prop False}) @@ -196,21 +208,23 @@ fun sledgehammer_tptp_file timeout file_name = let - val (conjs, assms, ctxt) = read_tptp_file @{theory} file_name + val (conjs, assms, ctxt) = + read_tptp_file @{theory} freeze_problem_consts file_name val conj = make_conj assms conjs in - can_tac ctxt (sledgehammer_tac ctxt timeout) conj + can_tac ctxt (sledgehammer_tac ctxt timeout 1) conj |> print_szs_from_success conjs end fun isabelle_tptp_file timeout file_name = let - val (conjs, assms, ctxt) = read_tptp_file @{theory} file_name + val (conjs, assms, ctxt) = + read_tptp_file @{theory} freeze_problem_consts file_name val conj = make_conj assms 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) + (can_tac ctxt (sledgehammer_tac ctxt (timeout div 2) 1) conj orelse + can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse + can_tac ctxt (atp_tac ctxt timeout ATP_Systems.satallaxN 1) conj) |> print_szs_from_success conjs end