more work on TPTP Isabelle and Sledgehammer tactics
authorblanchet
Wed Apr 25 22:00:33 2012 +0200 (2012-04-25)
changeset 477669f7cdd5fff7c
parent 47765 18f37b7aa6a6
child 47767 857b20f4a4b6
more work on TPTP Isabelle and Sledgehammer tactics
src/HOL/TPTP/ATP_Problem_Import.thy
src/HOL/TPTP/atp_problem_import.ML
src/HOL/ex/sledgehammer_tactics.ML
     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;