author blanchet Fri Apr 27 22:36:27 2012 +0200 (2012-04-27) changeset 47812 bb477988edb4 parent 47811 1e8eb643540d child 47817 5d2d63f4363e
use Nitpick as an oracle for finite problems
```     1.1 --- a/src/HOL/TPTP/ATP_Problem_Import.thy	Fri Apr 27 22:36:27 2012 +0200
1.2 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Fri Apr 27 22:36:27 2012 +0200
1.3 @@ -3,6 +3,7 @@
1.4  *)
1.5
1.6  header {* ATP Problem Importer *}
1.7 +
1.8  theory ATP_Problem_Import
1.9  imports Complex_Main TPTP_Interpret
1.10  uses "sledgehammer_tactics.ML"
```
```     2.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Fri Apr 27 22:36:27 2012 +0200
2.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Apr 27 22:36:27 2012 +0200
2.3 @@ -69,7 +69,6 @@
2.4      val params =
2.5        [("card", "1\<emdash>100"),
2.6         ("box", "false"),
2.7 -       ("sat_solver", "smart"),
2.9         ("batch_size", "5"),
2.10         ("falsify", if null conjs then "false" else "true"),
2.11 @@ -134,6 +133,39 @@
2.12      | SOME st' => (Output.urgent_message ("SUCCESS: " ^ name); Seq.single st')
2.13    end
2.14
2.15 +fun nitpick_finite_oracle_tac ctxt timeout i th =
2.16 +  let
2.17 +    fun is_safe (Type (@{type_name fun}, Ts)) = forall is_safe Ts
2.18 +      | is_safe @{typ prop} = true
2.19 +      | is_safe @{typ bool} = true
2.20 +      | is_safe _ = false
2.21 +    val conj = Thm.term_of (Thm.cprem_of th i)
2.22 +  in
2.23 +    if exists_type (not o is_safe) conj then
2.24 +      Seq.empty
2.25 +    else
2.26 +      let
2.27 +        val thy = Proof_Context.theory_of ctxt
2.28 +        val state = Proof.init ctxt
2.29 +        val params =
2.30 +          [("box", "false"),
2.32 +           ("verbose", "true"),
2.33 +           ("debug", if debug then "true" else "false"),
2.34 +           ("overlord", if overlord then "true" else "false"),
2.35 +           ("max_potential", "0"),
2.36 +           ("timeout", string_of_int timeout)]
2.37 +          |> Nitpick_Isar.default_params thy
2.38 +        val i = 1
2.39 +        val n = 1
2.40 +        val step = 0
2.41 +        val subst = []
2.42 +        val (outcome, _) =
2.43 +          Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst
2.44 +                                    [] [] conj
2.45 +      in if outcome = "none" then Skip_Proof.cheat_tac thy th else Seq.empty end
2.46 +  end
2.47 +
2.48  fun atp_tac ctxt override_params timeout prover =
2.49    Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
2.50        ([("debug", if debug then "true" else "false"),
2.51 @@ -157,17 +189,20 @@
2.52    end
2.53
2.54  fun auto_etc_tac ctxt timeout i =
2.55 -  SOLVE_TIMEOUT (timeout div 10) "simp" (asm_full_simp_tac (simpset_of ctxt) i)
2.56 +  SOLVE_TIMEOUT (timeout div 20) "nitpick"
2.57 +      (nitpick_finite_oracle_tac ctxt (timeout div 20) i)
2.58 +  ORELSE SOLVE_TIMEOUT (timeout div 10) "simp"
2.59 +      (asm_full_simp_tac (simpset_of ctxt) i)
2.60    ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i)
2.61    ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
2.62        (auto_tac ctxt
2.63         THEN ALLGOALS (atp_tac ctxt [] (timeout div 5) ATP_Systems.spassN))
2.64    ORELSE SOLVE_TIMEOUT (timeout div 5) "smt" (SMT_Solver.smt_tac ctxt [] i)
2.65 -  ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac ctxt i)
2.66 -  ORELSE SOLVE_TIMEOUT (timeout div 10) "best" (best_tac ctxt i)
2.67 +  ORELSE SOLVE_TIMEOUT (timeout div 20) "fast" (fast_tac ctxt i)
2.68 +  ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac ctxt i)
2.69    ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac ctxt i)
2.70 -  ORELSE SOLVE_TIMEOUT (timeout div 10) "arith" (Arith_Data.arith_tac ctxt i)
2.71 -  ORELSE SOLVE_TIMEOUT timeout "fastforce" (fast_force_tac ctxt i)
2.72 +  ORELSE SOLVE_TIMEOUT (timeout div 20) "arith" (Arith_Data.arith_tac ctxt i)
2.73 +  ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac ctxt i)
2.74
2.75  fun problem_const_prefix thy = Context.theory_name thy ^ Long_Name.separator
2.76
```