equal
deleted
inserted
replaced
1 theory TPTP |
|
2 imports Main |
|
3 uses "~~/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML" |
|
4 begin |
|
5 |
|
6 declare mem_def [simp add] |
|
7 |
|
8 declare [[smt_oracle]] |
|
9 |
|
10 ML {* proofs := 0 *} |
|
11 |
|
12 ML {* |
|
13 fun SOLVE_TIMEOUT seconds name tac st = |
|
14 let |
|
15 val result = |
|
16 TimeLimit.timeLimit (Time.fromSeconds seconds) |
|
17 (fn () => SINGLE (SOLVE tac) st) () |
|
18 handle TimeLimit.TimeOut => NONE |
|
19 | ERROR _ => NONE |
|
20 in |
|
21 (case result of |
|
22 NONE => (writeln ("FAILURE: " ^ name); Seq.empty) |
|
23 | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st')) |
|
24 end |
|
25 *} |
|
26 |
|
27 ML {* |
|
28 fun isabellep_tac max_secs = |
|
29 SOLVE_TIMEOUT (max_secs div 5) "sledgehammer" |
|
30 (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context})) |
|
31 ORELSE |
|
32 SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac @{simpset})) |
|
33 ORELSE |
|
34 SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac @{claset})) |
|
35 ORELSE |
|
36 SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac @{clasimpset} |
|
37 THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context})) |
|
38 ORELSE |
|
39 SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac @{context} [])) |
|
40 ORELSE |
|
41 SOLVE_TIMEOUT (max_secs div 5) "fast" (ALLGOALS (fast_tac @{claset})) |
|
42 ORELSE |
|
43 SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac @{claset})) |
|
44 ORELSE |
|
45 SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac @{clasimpset})) |
|
46 ORELSE |
|
47 SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac @{clasimpset})) |
|
48 *} |
|
49 |
|
50 end |
|