36 | SOME st' => (warning ("SUCCESS: " ^ name); Seq.single st')) |
36 | SOME st' => (warning ("SUCCESS: " ^ name); Seq.single st')) |
37 end |
37 end |
38 *} |
38 *} |
39 |
39 |
40 ML {* |
40 ML {* |
41 fun isabellep_tac ctxt cs ss css max_secs = |
41 fun isabellep_tac ctxt max_secs = |
42 SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt [])) |
42 SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt [])) |
43 ORELSE |
43 ORELSE |
44 SOLVE_TIMEOUT (max_secs div 5) "sledgehammer" |
44 SOLVE_TIMEOUT (max_secs div 5) "sledgehammer" |
45 (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt)) |
45 (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt)) |
46 ORELSE |
46 ORELSE |
47 SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac ss)) |
47 SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt))) |
48 ORELSE |
48 ORELSE |
49 SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac cs)) |
49 SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt)) |
50 ORELSE |
50 ORELSE |
51 SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac css |
51 SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt |
52 THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt)) |
52 THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt)) |
53 ORELSE |
53 ORELSE |
54 SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac ctxt [])) |
54 SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac ctxt [])) |
55 ORELSE |
55 ORELSE |
56 SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac cs)) |
56 SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt)) |
57 ORELSE |
57 ORELSE |
58 SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac cs)) |
58 SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac ctxt)) |
59 ORELSE |
59 ORELSE |
60 SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac css)) |
60 SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac ctxt)) |
61 ORELSE |
61 ORELSE |
62 SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac css)) |
62 SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac ctxt)) |
63 *} |
63 *} |
64 |
64 |
65 end |
65 end |