use Nitpick as an oracle for finite problems
authorblanchet
Fri Apr 27 22:36:27 2012 +0200 (2012-04-27)
changeset 47812bb477988edb4
parent 47811 1e8eb643540d
child 47817 5d2d63f4363e
use Nitpick as an oracle for finite problems
src/HOL/TPTP/ATP_Problem_Import.thy
src/HOL/TPTP/atp_problem_import.ML
     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.8         ("max_threads", "1"),
     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.31 +           ("max_threads", "1"),
    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