more tweaking of TPTP/CASC setup
authorblanchet
Fri Apr 27 12:16:10 2012 +0200 (2012-04-27)
changeset 47785d27bb852c430
parent 47784 fe43977e434f
child 47786 034cc7cc8b4a
more tweaking of TPTP/CASC setup
src/HOL/TPTP/ATP_Problem_Import.thy
src/HOL/TPTP/atp_problem_import.ML
     1.1 --- a/src/HOL/TPTP/ATP_Problem_Import.thy	Thu Apr 26 21:58:16 2012 +0200
     1.2 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Fri Apr 27 12:16:10 2012 +0200
     1.3 @@ -15,4 +15,8 @@
     1.4  declare [[show_consts]] (* for Refute *)
     1.5  declare [[smt_oracle]]
     1.6  
     1.7 +(*
     1.8 +ML {* ATP_Problem_Import.isabelle_tptp_file 100 "$TPTP/Problems/PUZ/PUZ107^5.p" *}
     1.9 +*)
    1.10 +
    1.11  end
     2.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Thu Apr 26 21:58:16 2012 +0200
     2.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Apr 27 12:16:10 2012 +0200
     2.3 @@ -33,10 +33,11 @@
     2.4             Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t')))
     2.5         (Term.add_vars t []) t
     2.6  
     2.7 -fun read_tptp_file thy file_name =
     2.8 +fun read_tptp_file thy postproc file_name =
     2.9    let
    2.10      fun has_role role (_, role', _, _) = (role' = role)
    2.11 -    fun get_prop (_, _, P, _) = P |> Logic.varify_global |> close_form
    2.12 +    fun get_prop (_, _, P, _) =
    2.13 +      P |> Logic.varify_global |> close_form |> postproc
    2.14      val path =
    2.15        Path.explode file_name
    2.16        |> (fn path =>
    2.17 @@ -60,7 +61,7 @@
    2.18  
    2.19  fun nitpick_tptp_file timeout file_name =
    2.20    let
    2.21 -    val (conjs, (defs, nondefs), ctxt) = read_tptp_file @{theory} file_name
    2.22 +    val (conjs, (defs, nondefs), ctxt) = read_tptp_file @{theory} I file_name
    2.23      val thy = Proof_Context.theory_of ctxt
    2.24      val defs = defs |> map (ATP_Util.extensionalize_term ctxt
    2.25                              #> aptrueprop (open_form I))
    2.26 @@ -103,7 +104,7 @@
    2.27         else
    2.28           "Unknown")
    2.29        |> writeln
    2.30 -    val (conjs, (defs, nondefs), ctxt) = read_tptp_file @{theory} file_name
    2.31 +    val (conjs, (defs, nondefs), ctxt) = read_tptp_file @{theory} I file_name
    2.32      val params =
    2.33        [("maxtime", string_of_int timeout),
    2.34         ("maxvars", "100000")]
    2.35 @@ -119,38 +120,36 @@
    2.36  val cvc3N = "cvc3"
    2.37  val z3N = "z3"
    2.38  
    2.39 -fun can_tac ctxt tactic conj =
    2.40 -  can (Goal.prove ctxt [] [] conj) (K tactic)
    2.41 +fun can_tac ctxt tactic conj = can (Goal.prove ctxt [] [] conj) (K tactic)
    2.42  
    2.43  fun SOLVE_TIMEOUT seconds name tac st =
    2.44    let
    2.45 +    val _ = writeln ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s")
    2.46      val result =
    2.47        TimeLimit.timeLimit (Time.fromSeconds seconds)
    2.48          (fn () => SINGLE (SOLVE tac) st) ()
    2.49        handle TimeLimit.TimeOut => NONE
    2.50          | ERROR _ => NONE
    2.51    in
    2.52 -    (case result of
    2.53 -      NONE => (warning ("FAILURE: " ^ name); Seq.empty)
    2.54 -    | SOME st' => (warning ("SUCCESS: " ^ name); Seq.single st'))
    2.55 +    case result of
    2.56 +      NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
    2.57 +    | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st')
    2.58    end
    2.59  
    2.60 -val i = 1
    2.61 -
    2.62  fun atp_tac ctxt timeout prover =
    2.63    Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
    2.64        [("debug", if debug then "true" else "false"),
    2.65         ("overlord", if overlord then "true" else "false"),
    2.66         ("provers", prover),
    2.67         ("timeout", string_of_int timeout)]
    2.68 -      {add = [], del = [], only = true} i
    2.69 +      {add = [], del = [], only = true}
    2.70  
    2.71 -fun sledgehammer_tac ctxt timeout =
    2.72 +fun sledgehammer_tac ctxt timeout i =
    2.73    let
    2.74      fun slice timeout prover =
    2.75 -      SOLVE_TIMEOUT timeout prover (atp_tac ctxt timeout prover)
    2.76 +      SOLVE_TIMEOUT timeout prover (atp_tac ctxt timeout prover i)
    2.77    in
    2.78 -    slice timeout ATP_Systems.satallaxN
    2.79 +    slice (timeout div 10) ATP_Systems.satallaxN
    2.80      ORELSE
    2.81      slice (timeout div 10) ATP_Systems.spassN
    2.82      ORELSE
    2.83 @@ -165,13 +164,14 @@
    2.84      slice (timeout div 10) ATP_Systems.leo2N
    2.85    end
    2.86  
    2.87 -fun auto_etc_tac ctxt timeout =
    2.88 +fun auto_etc_tac ctxt timeout i =
    2.89    SOLVE_TIMEOUT (timeout div 10) "simp" (asm_full_simp_tac (simpset_of ctxt) i)
    2.90    ORELSE
    2.91    SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i)
    2.92    ORELSE
    2.93    SOLVE_TIMEOUT (timeout div 20) "auto+spass"
    2.94 -      (auto_tac ctxt THEN atp_tac ctxt (timeout div 20) ATP_Systems.spassN)
    2.95 +      (auto_tac ctxt
    2.96 +       THEN ALLGOALS (atp_tac ctxt (timeout div 20) ATP_Systems.spassN))
    2.97    ORELSE
    2.98    SOLVE_TIMEOUT (timeout div 20) "fast" (fast_tac ctxt i)
    2.99    ORELSE
   2.100 @@ -183,6 +183,18 @@
   2.101    ORELSE
   2.102    SOLVE_TIMEOUT timeout "fastforce" (fast_force_tac ctxt i)
   2.103  
   2.104 +val problem_const_prefix = Context.theory_name @{theory} ^ Long_Name.separator
   2.105 +
   2.106 +(* Isabelle's standard automatic tactics ("auto", etc.) are more eager to
   2.107 +   unfold "definitions" of free variables than of constants (cf. PUZ107^5). *)
   2.108 +val freeze_problem_consts =
   2.109 +  map_aterms (fn t as Const (s, T) =>
   2.110 +                 if String.isPrefix problem_const_prefix s then
   2.111 +                   Free (Long_Name.base_name s, T)
   2.112 +                 else
   2.113 +                   t
   2.114 +               | t => t)
   2.115 +
   2.116  fun make_conj (defs, nondefs) conjs =
   2.117    Logic.list_implies (rev defs @ rev nondefs,
   2.118                        case conjs of conj :: _ => conj | [] => @{prop False})
   2.119 @@ -196,21 +208,23 @@
   2.120  
   2.121  fun sledgehammer_tptp_file timeout file_name =
   2.122    let
   2.123 -    val (conjs, assms, ctxt) = read_tptp_file @{theory} file_name
   2.124 +    val (conjs, assms, ctxt) =
   2.125 +      read_tptp_file @{theory} freeze_problem_consts file_name
   2.126      val conj = make_conj assms conjs
   2.127    in
   2.128 -    can_tac ctxt (sledgehammer_tac ctxt timeout) conj
   2.129 +    can_tac ctxt (sledgehammer_tac ctxt timeout 1) conj
   2.130      |> print_szs_from_success conjs
   2.131    end
   2.132  
   2.133  fun isabelle_tptp_file timeout file_name =
   2.134    let
   2.135 -    val (conjs, assms, ctxt) = read_tptp_file @{theory} file_name
   2.136 +    val (conjs, assms, ctxt) =
   2.137 +      read_tptp_file @{theory} freeze_problem_consts file_name
   2.138      val conj = make_conj assms conjs
   2.139    in
   2.140 -    (can_tac ctxt (sledgehammer_tac ctxt (timeout div 2)) conj orelse
   2.141 -     can_tac ctxt (auto_etc_tac ctxt (timeout div 2)) conj orelse
   2.142 -     can_tac ctxt (atp_tac ctxt timeout ATP_Systems.satallaxN) conj)
   2.143 +    (can_tac ctxt (sledgehammer_tac ctxt (timeout div 2) 1) conj orelse
   2.144 +     can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
   2.145 +     can_tac ctxt (atp_tac ctxt timeout ATP_Systems.satallaxN 1) conj)
   2.146      |> print_szs_from_success conjs
   2.147    end
   2.148