<commit_before>(*  Title:      HOL/ex/CASC_Setup.thy
    Author:     <NAME>
    Copyright   2011

Setup for Isabelle, Nitpick, and Refute for participating at CASC in the THF and
TNT divisions. This theory file should be loaded by the Isabelle theory files
generated by <NAME>'s TPTP2X tool from the original THF0 files.
*)

theory CASC_Setup
imports Main
uses "sledgehammer_tactics.ML"
begin

declare mem_def [simp add]

declare [[smt_oracle]]

refute_params [maxtime = 10000, no_assms, expect = genuine]
nitpick_params [timeout = none, card = 1-50, verbose, dont_box, no_assms,
                batch_size = 1, expect = genuine]

ML {* Proofterm.proofs := 0 *}

ML {*
fun SOLVE_TIMEOUT seconds name tac st =
  let
    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'))
  end
*}

ML {*
fun isabellep_tac ctxt cs ss css max_secs =
   SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt []))
   ORELSE
   SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
       (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
   ORELSE
   SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac ss))
   ORELSE
   SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac cs))
   ORELSE
   SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac css
       THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
   ORELSE
   SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac ctxt []))
   ORELSE
   SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac cs))
   ORELSE
   SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac cs))
   ORELSE
   SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac css))
   ORELSE
   SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac css))
*}

end<commit_msg>just one universal Proof.context -- discontinued claset/clasimpset;<commit_after>(*  Title:      HOL/ex/CASC_Setup.thy
    Author:     <NAME>
    Copyright   2011

Setup for Isabelle, Nitpick, and Refute for participating at CASC in the THF and
TNT divisions. This theory file should be loaded by the Isabelle theory files
generated by Ge<NAME>'s TPTP2X tool from the original THF0 files.
*)

theory CASC_Setup
imports Main
uses "sledgehammer_tactics.ML"
begin

declare mem_def [simp add]

declare [[smt_oracle]]

refute_params [maxtime = 10000, no_assms, expect = genuine]
nitpick_params [timeout = none, card = 1-50, verbose, dont_box, no_assms,
                batch_size = 1, expect = genuine]

ML {* Proofterm.proofs := 0 *}

ML {*
fun SOLVE_TIMEOUT seconds name tac st =
  let
    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'))
  end
*}

ML {*
fun isabellep_tac ctxt max_secs =
   SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt []))
   ORELSE
   SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
       (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
   ORELSE
   SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt)))
   ORELSE
   SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt))
   ORELSE
   SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt
       THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
   ORELSE
   SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac ctxt []))
   ORELSE
   SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt))
   ORELSE
   SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac ctxt))
   ORELSE
   SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac ctxt))
   ORELSE
   SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac ctxt))
*}

end
{'fraction_non_alphanumeric': 0.09851390220517738, 'fraction_numerical': 0.015819750719079578, 'mean_word_length': 3.758266818700114, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 17, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6312442', 'n_tokens_mistral': 1726, 'n_tokens_neox': 1603, 'n_words': 436}