author blanchet Wed Apr 25 22:00:33 2012 +0200 (2012-04-25) changeset 47766 9f7cdd5fff7c parent 47765 18f37b7aa6a6 child 47767 857b20f4a4b6
more work on TPTP Isabelle and Sledgehammer tactics
```     1.1 --- a/src/HOL/TPTP/ATP_Problem_Import.thy	Wed Apr 25 22:00:33 2012 +0200
1.2 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Wed Apr 25 22:00:33 2012 +0200
1.3 @@ -6,7 +6,8 @@
1.4
1.5  theory ATP_Problem_Import
1.6  imports Complex_Main TPTP_Interpret
1.7 -uses ("atp_problem_import.ML")
1.8 +uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
1.9 +     ("atp_problem_import.ML")
1.10  begin
1.11
1.12  ML {* Proofterm.proofs := 0 *}
```
```     2.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Wed Apr 25 22:00:33 2012 +0200
2.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Wed Apr 25 22:00:33 2012 +0200
2.3 @@ -85,23 +85,22 @@
2.4      val subst = []
2.5    in
2.6      Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst
2.7 -        defs nondefs (case conjs of conj :: _ => conj | _ => @{prop True});
2.8 +        defs nondefs (case conjs of conj :: _ => conj | [] => @{prop True});
2.9      ()
2.10    end
2.11
2.12
2.13  (** Refute **)
2.14
2.15 -fun print_szs_from_outcome falsify s =
2.16 -  "% SZS status " ^
2.17 -  (if s = "genuine" then
2.18 -     if falsify then "CounterSatisfiable" else "Satisfiable"
2.19 -   else
2.20 -     "Unknown")
2.21 -  |> writeln
2.22 -
2.23  fun refute_tptp_file timeout file_name =
2.24    let
2.25 +    fun print_szs_from_outcome falsify s =
2.26 +      "% SZS status " ^
2.27 +      (if s = "genuine" then
2.28 +         if falsify then "CounterSatisfiable" else "Satisfiable"
2.29 +       else
2.30 +         "Unknown")
2.31 +      |> writeln
2.32      val (conjs, (defs, nondefs), thy) = read_tptp_file @{theory} file_name
2.33      val ctxt = Proof_Context.init_global thy
2.34      val params =
2.35 @@ -109,32 +108,106 @@
2.36         ("maxvars", "100000")]
2.37    in
2.38      Refute.refute_term ctxt params (defs @ nondefs)
2.39 -        (case conjs of conj :: _ => conj | _ => @{prop True})
2.40 +        (case conjs of conj :: _ => conj | [] => @{prop True})
2.41      |> print_szs_from_outcome (not (null conjs))
2.42    end
2.43
2.44
2.45 -(** Sledgehammer **)
2.46 +(** Sledgehammer and Isabelle (combination of provers) **)
2.47 +
2.48 +fun SOLVE_TIMEOUT seconds name tac st =
2.49 +  let
2.50 +    val result =
2.51 +      TimeLimit.timeLimit (Time.fromSeconds seconds)
2.52 +        (fn () => SINGLE (SOLVE tac) st) ()
2.53 +      handle TimeLimit.TimeOut => NONE
2.54 +        | ERROR _ => NONE
2.55 +  in
2.56 +    (case result of
2.57 +      NONE => (warning ("FAILURE: " ^ name); Seq.empty)
2.58 +    | SOME st' => (warning ("SUCCESS: " ^ name); Seq.single st'))
2.59 +  end
2.60
2.61  fun apply_tactic_to_tptp_file tactic timeout file_name =
2.62    let
2.63      val (conjs, (defs, nondefs), thy) = read_tptp_file @{theory} file_name
2.64      val ctxt = Proof_Context.init_global thy
2.65 +    val conj =
2.66 +      Logic.list_implies (defs @ nondefs,
2.67 +                          case conjs of conj :: _ => conj | [] => @{prop False})
2.68    in
2.69 -    Goal.prove ctxt [] (defs @ nondefs) (hd conjs) (fn _ => tactic ctxt
2.70 +    case try (Goal.prove ctxt [] [] conj) (K (tactic ctxt timeout)) of
2.71 +      SOME _ =>
2.72 +      writeln ("% SZS status " ^
2.73 +               (if null conjs then "Unsatisfiable" else "Theorem"))
2.74 +    | NONE => writeln ("% SZS status Unknown")
2.75    end
2.76
2.77 -val sledgehammer_tptp_file =
2.78 -  apply_tactic_to_tptp_file Sledgehammer_Tactics.sledgehammer_as_oracle_tac
2.79 +fun atp_tac ctxt timeout prover =
2.80 +  Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
2.81 +      [
2.82 +(*
2.83 +       ("debug", "true"),
2.84 +       ("overlord", "true"),
2.85 +*)
2.86 +       ("provers", prover),
2.87 +       ("timeout", string_of_int timeout)]
2.88 +      Sledgehammer_Filter.no_relevance_override
2.89 +
2.90 +val cvc3N = "cvc3"
2.91 +val z3N = "z3"
2.92
2.93 +fun sledgehammer_tac ctxt timeout =
2.94 +  let
2.95 +    fun slice timeout prover =
2.96 +      SOLVE_TIMEOUT timeout prover (ALLGOALS (atp_tac ctxt timeout prover))
2.97 +  in
2.98 +    slice (timeout div 10) ATP_Systems.spassN
2.99 +    ORELSE
2.100 +    slice (timeout div 10) z3N
2.101 +    ORELSE
2.102 +    slice (timeout div 10) ATP_Systems.vampireN
2.103 +    ORELSE
2.104 +    slice (timeout div 10) ATP_Systems.eN
2.105 +    ORELSE
2.106 +    slice (timeout div 10) cvc3N
2.107 +    ORELSE
2.108 +    slice (timeout div 10) ATP_Systems.leo2N
2.109 +    ORELSE
2.110 +    slice timeout ATP_Systems.satallaxN
2.111 +  end
2.112 +
2.113 +val sledgehammer_tptp_file = apply_tactic_to_tptp_file sledgehammer_tac
2.114
2.115  (** Isabelle (combination of provers) **)
2.116
2.117 -val isabelle_tac =
2.118 -  ...
2.119 +fun isabelle_tac ctxt timeout =
2.120 +  sledgehammer_tac ctxt (timeout div 2)
2.121 +  ORELSE
2.122 +  SOLVE_TIMEOUT (timeout div 10) "simp"
2.123 +      (ALLGOALS (asm_full_simp_tac (simpset_of ctxt)))
2.124 +  ORELSE
2.125 +  SOLVE_TIMEOUT (timeout div 10) "blast" (ALLGOALS (blast_tac ctxt))
2.126 +  ORELSE
2.127 +  SOLVE_TIMEOUT (timeout div 20) "auto+spass"
2.128 +      (auto_tac ctxt
2.129 +       THEN ALLGOALS (atp_tac ctxt (timeout div 20) ATP_Systems.spassN))
2.130 +  ORELSE
2.131 +  SOLVE_TIMEOUT (timeout div 20) "fast" (ALLGOALS (fast_tac ctxt))
2.132 +  ORELSE
2.133 +  SOLVE_TIMEOUT (timeout div 20) "best" (ALLGOALS (best_tac ctxt))
2.134 +  ORELSE
2.135 +  SOLVE_TIMEOUT (timeout div 20) "force" (ALLGOALS (force_tac ctxt))
2.136 +  ORELSE
2.137 +  SOLVE_TIMEOUT (timeout div 20) "arith" (ALLGOALS (Arith_Data.arith_tac ctxt))
2.138 +  ORELSE
2.139 +  SOLVE_TIMEOUT timeout "fastforce" (ALLGOALS (fast_force_tac ctxt))
2.140 +  ORELSE
2.141 +  SOLVE_TIMEOUT timeout "satallax"
2.142 +      (ALLGOALS (atp_tac ctxt timeout ATP_Systems.satallaxN))
2.143
2.144 -val isabelle_tptp_file =
2.145 -  ...
2.146 +val isabelle_tptp_file = apply_tactic_to_tptp_file isabelle_tac
2.147 +
2.148
2.149  (** Translator between TPTP(-like) file formats **)
2.150
```
```     3.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Wed Apr 25 22:00:33 2012 +0200
3.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Wed Apr 25 22:00:33 2012 +0200
3.3 @@ -68,17 +68,26 @@
3.4    end
3.5
3.6  fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
3.7 -  case run_atp override_params relevance_override i i ctxt th of
3.8 -    SOME facts =>
3.9 -    Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt
3.10 -        (maps (thms_of_name ctxt) facts) i th
3.11 -  | NONE => Seq.empty
3.12 +  let
3.13 +    val override_params =
3.14 +      override_params @
3.15 +      [("preplay_timeout", "0")]
3.16 +  in
3.17 +    case run_atp override_params relevance_override i i ctxt th of
3.18 +      SOME facts =>
3.19 +      Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
3.20 +          (maps (thms_of_name ctxt) facts) i th
3.21 +    | NONE => Seq.empty
3.22 +  end
3.23
3.24  fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =
3.25    let
3.26      val thy = Proof_Context.theory_of ctxt
3.27 -    val xs = run_atp (override_params @ [("sound", "true")]) relevance_override
3.28 -                     i i ctxt th
3.29 +    val override_params =
3.30 +      override_params @
3.31 +      [("preplay_timeout", "0"),
3.32 +       ("minimize", "false")]
3.33 +    val xs = run_atp override_params relevance_override i i ctxt th
3.34    in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
3.35
3.36  end;
```