|
1 (* Title: HOL/ex/CASC_Setup.thy |
|
2 Author: Jasmin Blanchette |
|
3 Copyright 2011 |
|
4 |
|
5 Setup for Isabelle, Nitpick, and Refute for participating at CASC in the THF and |
|
6 TNT divisions. This theory file should be loaded by the Isabelle theory files |
|
7 generated by Geoff Sutcliffe's TPTP2X tool from the original THF0 files. |
|
8 *) |
|
9 |
|
10 theory CASC_Setup |
|
11 imports Main |
|
12 uses "sledgehammer_tactics.ML" |
|
13 begin |
|
14 |
|
15 declare mem_def [simp add] |
|
16 |
|
17 declare [[smt_oracle]] |
|
18 |
|
19 refute_params [maxtime = 10000, no_assms, expect = genuine] |
|
20 nitpick_params [timeout = none, card = 1-50, verbose, dont_box, no_assms, |
|
21 batch_size = 1, expect = genuine] |
|
22 |
|
23 ML {* Proofterm.proofs := 0 *} |
|
24 |
|
25 ML {* |
|
26 fun SOLVE_TIMEOUT seconds name tac st = |
|
27 let |
|
28 val result = |
|
29 TimeLimit.timeLimit (Time.fromSeconds seconds) |
|
30 (fn () => SINGLE (SOLVE tac) st) () |
|
31 handle TimeLimit.TimeOut => NONE |
|
32 | ERROR _ => NONE |
|
33 in |
|
34 (case result of |
|
35 NONE => (warning ("FAILURE: " ^ name); Seq.empty) |
|
36 | SOME st' => (warning ("SUCCESS: " ^ name); Seq.single st')) |
|
37 end |
|
38 *} |
|
39 |
|
40 ML {* |
|
41 fun isabellep_tac ctxt cs ss css max_secs = |
|
42 SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt [])) |
|
43 ORELSE |
|
44 SOLVE_TIMEOUT (max_secs div 5) "sledgehammer" |
|
45 (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt)) |
|
46 ORELSE |
|
47 SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac ss)) |
|
48 ORELSE |
|
49 SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac cs)) |
|
50 ORELSE |
|
51 SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac css |
|
52 THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt)) |
|
53 ORELSE |
|
54 SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac ctxt [])) |
|
55 ORELSE |
|
56 SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac cs)) |
|
57 ORELSE |
|
58 SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac cs)) |
|
59 ORELSE |
|
60 SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac css)) |
|
61 ORELSE |
|
62 SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac css)) |
|
63 *} |
|
64 |
|
65 end |