1.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Fri Apr 27 22:36:27 2012 +0200
     1.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Apr 27 22:36:27 2012 +0200
     1.3 @@ -69,7 +69,6 @@
     1.4      val params =
     1.5        [("card", "1\<emdash>100"),
     1.6         ("box", "false"),
     1.7 -       ("sat_solver", "smart"),
     1.8         ("max_threads", "1"),
     1.9         ("batch_size", "5"),
    1.10         ("falsify", if null conjs then "false" else "true"),
    1.11 @@ -134,6 +133,39 @@
    1.12      | SOME st' => (Output.urgent_message ("SUCCESS: " ^ name); Seq.single st')
    1.13    end
    1.14  
    1.15 +fun nitpick_finite_oracle_tac ctxt timeout i th =
    1.16 +  let
    1.17 +    fun is_safe (Type (@{type_name fun}, Ts)) = forall is_safe Ts
    1.18 +      | is_safe @{typ prop} = true
    1.19 +      | is_safe @{typ bool} = true
    1.20 +      | is_safe _ = false
    1.21 +    val conj = Thm.term_of (Thm.cprem_of th i)
    1.22 +  in
    1.23 +    if exists_type (not o is_safe) conj then
    1.24 +      Seq.empty
    1.25 +    else
    1.26 +      let
    1.27 +        val thy = Proof_Context.theory_of ctxt
    1.28 +        val state = Proof.init ctxt
    1.29 +        val params =
    1.30 +          [("box", "false"),
    1.31 +           ("max_threads", "1"),
    1.32 +           ("verbose", "true"),
    1.33 +           ("debug", if debug then "true" else "false"),
    1.34 +           ("overlord", if overlord then "true" else "false"),
    1.35 +           ("max_potential", "0"),
    1.36 +           ("timeout", string_of_int timeout)]
    1.37 +          |> Nitpick_Isar.default_params thy
    1.38 +        val i = 1
    1.39 +        val n = 1
    1.40 +        val step = 0
    1.41 +        val subst = []
    1.42 +        val (outcome, _) =
    1.43 +          Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst
    1.44 +                                    [] [] conj
    1.45 +      in if outcome = "none" then Skip_Proof.cheat_tac thy th else Seq.empty end
    1.46 +  end
    1.47 +
    1.48  fun atp_tac ctxt override_params timeout prover =
    1.49    Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
    1.50        ([("debug", if debug then "true" else "false"),
    1.51 @@ -157,17 +189,20 @@
    1.52    end
    1.53  
    1.54  fun auto_etc_tac ctxt timeout i =
    1.55 -  SOLVE_TIMEOUT (timeout div 10) "simp" (asm_full_simp_tac (simpset_of ctxt) i)
    1.56 +  SOLVE_TIMEOUT (timeout div 20) "nitpick"
    1.57 +      (nitpick_finite_oracle_tac ctxt (timeout div 20) i)
    1.58 +  ORELSE SOLVE_TIMEOUT (timeout div 10) "simp"
    1.59 +      (asm_full_simp_tac (simpset_of ctxt) i)
    1.60    ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i)
    1.61    ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
    1.62        (auto_tac ctxt
    1.63         THEN ALLGOALS (atp_tac ctxt [] (timeout div 5) ATP_Systems.spassN))
    1.64    ORELSE SOLVE_TIMEOUT (timeout div 5) "smt" (SMT_Solver.smt_tac ctxt [] i)
    1.65 -  ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac ctxt i)
    1.66 -  ORELSE SOLVE_TIMEOUT (timeout div 10) "best" (best_tac ctxt i)
    1.67 +  ORELSE SOLVE_TIMEOUT (timeout div 20) "fast" (fast_tac ctxt i)
    1.68 +  ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac ctxt i)
    1.69    ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac ctxt i)
    1.70 -  ORELSE SOLVE_TIMEOUT (timeout div 10) "arith" (Arith_Data.arith_tac ctxt i)
    1.71 -  ORELSE SOLVE_TIMEOUT timeout "fastforce" (fast_force_tac ctxt i)
    1.72 +  ORELSE SOLVE_TIMEOUT (timeout div 20) "arith" (Arith_Data.arith_tac ctxt i)
    1.73 +  ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac ctxt i)
    1.74  
    1.75  fun problem_const_prefix thy = Context.theory_name thy ^ Long_Name.separator
    1.76