author blanchet Tue Aug 30 16:07:34 2011 +0200 (2011-08-30) changeset 44589 0a1dfc6365e9 parent 44588 e74aa9d9162b child 44590 3a8a31be92d2
first step towards polymorphic TFF + changed defaults for Vampire
 src/HOL/Tools/ATP/atp_problem.ML file | annotate | diff | revisions src/HOL/Tools/ATP/atp_systems.ML file | annotate | diff | revisions src/HOL/Tools/ATP/atp_translate.ML file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Aug 30 16:04:23 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Aug 30 16:07:34 2011 +0200
1.3 @@ -19,14 +19,15 @@
1.4
1.5    datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
1.6
1.7 -  datatype tff_flavor = Implicit | Explicit
1.8 -  datatype thf_flavor = Without_Choice | With_Choice
1.9 +  datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
1.10 +  datatype tff_explicitness = TFF_Implicit | TFF_Explicit
1.11 +  datatype thf_flavor = THF_Without_Choice | THF_With_Choice
1.12    datatype format =
1.13      CNF |
1.14      CNF_UEQ |
1.15      FOF |
1.16 -    TFF of tff_flavor |
1.17 -    THF of thf_flavor
1.18 +    TFF of tff_polymorphism * tff_explicitness |
1.19 +    THF0 of thf_flavor
1.20
1.21    datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
1.22    datatype 'a problem_line =
1.23 @@ -119,15 +120,16 @@
1.24
1.25  datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
1.26
1.27 -datatype tff_flavor = Implicit | Explicit
1.28 -datatype thf_flavor = Without_Choice | With_Choice
1.29 +datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
1.30 +datatype tff_explicitness = TFF_Implicit | TFF_Explicit
1.31 +datatype thf_flavor = THF_Without_Choice | THF_With_Choice
1.32
1.33  datatype format =
1.34    CNF |
1.35    CNF_UEQ |
1.36    FOF |
1.37 -  TFF of tff_flavor |
1.38 -  THF of thf_flavor
1.39 +  TFF of tff_polymorphism * tff_explicitness |
1.40 +  THF0 of thf_flavor
1.41
1.42  datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
1.43  datatype 'a problem_line =
1.44 @@ -211,10 +213,10 @@
1.45    | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
1.46    | formula_map f (AAtom tm) = AAtom (f tm)
1.47
1.48 -fun is_format_thf (THF _) = true
1.49 +fun is_format_thf (THF0 _) = true
1.50    | is_format_thf _ = false
1.51  fun is_format_typed (TFF _) = true
1.52 -  | is_format_typed (THF _) = true
1.53 +  | is_format_typed (THF0 _) = true
1.54    | is_format_typed _ = false
1.55
1.56  fun string_for_kind Axiom = "axiom"
1.57 @@ -228,7 +230,7 @@
1.58      raise Fail "unexpected higher-order type in first-order format"
1.59    | strip_tff_type (AType s) = ([], s)
1.60
1.61 -fun string_for_type (THF _) ty =
1.62 +fun string_for_type (THF0 _) ty =
1.63      let
1.64        fun aux _ (AType s) = s
1.65          | aux rhs (AFun (ty1, ty2)) =
1.66 @@ -270,7 +272,7 @@
1.67        |> is_format_thf format ? enclose "(" ")"
1.68      else
1.69        (case (s = tptp_ho_forall orelse s = tptp_ho_exists,
1.70 -             s = tptp_choice andalso format = THF With_Choice, ts) of
1.71 +             s = tptp_choice andalso format = THF0 THF_With_Choice, ts) of
1.72           (true, _, [AAbs ((s', ty), tm)]) =>
1.73           (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
1.74              possible, to work around LEO-II 1.2.8 parser limitation. *)
1.75 @@ -291,7 +293,7 @@
1.76             else
1.77               s ^ "(" ^ commas ss ^ ")"
1.78           end)
1.79 -  | string_for_term (format as THF _) (AAbs ((s, ty), tm)) =
1.80 +  | string_for_term (format as THF0 _) (AAbs ((s, ty), tm)) =
1.81      "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "] : " ^
1.82      string_for_term format tm ^ ")"
1.83    | string_for_term _ _ = raise Fail "unexpected term in first-order format"
1.84 @@ -324,7 +326,7 @@
1.85    | string_for_format CNF_UEQ = tptp_cnf
1.86    | string_for_format FOF = tptp_fof
1.87    | string_for_format (TFF _) = tptp_tff
1.88 -  | string_for_format (THF _) = tptp_thf
1.89 +  | string_for_format (THF0 _) = tptp_thf
1.90
1.91  fun string_for_problem_line format (Decl (ident, sym, ty)) =
1.92      string_for_format format ^ "(" ^ ident ^ ", type,\n    " ^ sym ^ " : " ^
```
```     2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 30 16:04:23 2011 +0200
2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 30 16:07:34 2011 +0200
2.3 @@ -241,8 +241,8 @@
2.4     prem_kind = Hypothesis,
2.5     best_slices = fn ctxt =>
2.6       (* FUDGE *)
2.7 -     [(0.667, (false, (150, THF Without_Choice, "simple_higher", sosN))),
2.8 -      (0.333, (true, (50, THF Without_Choice, "simple_higher", no_sosN)))]
2.9 +     [(0.667, (false, (150, THF0 THF_Without_Choice, "simple_higher", sosN))),
2.10 +      (0.333, (true, (50, THF0 THF_Without_Choice, "simple_higher", no_sosN)))]
2.11       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
2.12           else I)}
2.13
2.14 @@ -262,7 +262,8 @@
2.15     conj_sym_kind = Axiom,
2.16     prem_kind = Hypothesis,
2.17     best_slices =
2.18 -     K [(1.0, (true, (100, THF With_Choice, "simple_higher", "")))] (* FUDGE *)}
2.19 +     K [(1.0, (true, (100, THF0 THF_With_Choice, "simple_higher", "")))]
2.20 +     (* FUDGE *)}
2.21
2.22  val satallax = (satallaxN, satallax_config)
2.23
2.24 @@ -309,6 +310,8 @@
2.25  fun is_old_vampire_version () =
2.26    string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER
2.27
2.28 +val vampire_tff = TFF (TFF_Monomorphic, TFF_Implicit)
2.29 +
2.30  val vampire_config : atp_config =
2.31    {exec = ("VAMPIRE_HOME", "vampire"),
2.32     required_execs = [],
2.33 @@ -340,9 +343,9 @@
2.34           (0.333, (false, (500, FOF, "mono_tags?", sosN))),
2.35           (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))]
2.36        else
2.37 -        [(0.333, (false, (150, TFF Implicit, "poly_guards", sosN))),
2.38 -         (0.333, (false, (500, TFF Implicit, "simple", sosN))),
2.39 -         (0.334, (true, (50, TFF Implicit, "simple", no_sosN)))])
2.40 +        [(0.333, (false, (150, vampire_tff, "poly_guards", sosN))),
2.41 +         (0.333, (false, (500, vampire_tff, "simple", sosN))),
2.42 +         (0.334, (true, (50, vampire_tff, "simple", no_sosN)))])
2.43       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
2.44           else I)}
2.45
2.46 @@ -351,6 +354,8 @@
2.47
2.48  (* Z3 with TPTP syntax *)
2.49
2.50 +val z3_tff = TFF (TFF_Monomorphic, TFF_Implicit)
2.51 +
2.52  val z3_tptp_config : atp_config =
2.53    {exec = ("Z3_HOME", "z3"),
2.54     required_execs = [],
2.55 @@ -368,10 +373,10 @@
2.56     prem_kind = Hypothesis,
2.57     best_slices =
2.58       (* FUDGE *)
2.59 -     K [(0.5, (false, (250, FOF, "mono_guards?", ""))),
2.60 -        (0.25, (false, (125, FOF, "mono_guards?", ""))),
2.61 -        (0.125, (false, (62, TFF Implicit, "simple", ""))),
2.62 -        (0.125, (false, (31, TFF Implicit, "simple", "")))]}
2.63 +     K [(0.5, (false, (250, z3_tff, "simple", ""))),
2.64 +        (0.25, (false, (125, z3_tff, "simple", ""))),
2.65 +        (0.125, (false, (62, z3_tff, "simple", ""))),
2.66 +        (0.125, (false, (31, z3_tff, "simple", "")))]}
2.67
2.68  val z3_tptp = (z3_tptpN, z3_tptp_config)
2.69
2.70 @@ -381,7 +386,8 @@
2.71  val systems = Synchronized.var "atp_systems" ([] : string list)
2.72
2.73  fun get_systems () =
2.74 -  case Isabelle_System.bash_output "\"\$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
2.75 +  case Isabelle_System.bash_output
2.76 +           "\"\$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
2.77      (output, 0) => split_lines output
2.78    | (output, _) =>
2.79      error (case extract_known_failure known_perl_failures output of
2.80 @@ -449,31 +455,32 @@
2.81    (remote_prefix ^ name,
2.82     remotify_config system_name system_versions best_slice config)
2.83
2.84 +val dumb_tff = TFF (TFF_Monomorphic, TFF_Explicit)
2.85 +
2.86  val remote_e =
2.87    remotify_atp e "EP" ["1.0", "1.1", "1.2"]
2.88                 (K (750, FOF, "mono_tags?") (* FUDGE *))
2.89  val remote_leo2 =
2.90    remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
2.91 -               (K (100, THF Without_Choice, "simple_higher") (* FUDGE *))
2.92 +               (K (100, THF0 THF_Without_Choice, "simple_higher") (* FUDGE *))
2.93  val remote_satallax =
2.94    remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
2.95 -               (K (100, THF With_Choice, "simple_higher") (* FUDGE *))
2.96 +               (K (100, THF0 THF_With_Choice, "simple_higher") (* FUDGE *))
2.97  val remote_vampire =
2.98    remotify_atp vampire "Vampire" ["1.8"]
2.99 -               (K (250, TFF Implicit, "simple") (* FUDGE *))
2.100 +               (K (250, FOF, "mono_guards?") (* FUDGE *))
2.101  val remote_z3_tptp =
2.102 -  remotify_atp z3_tptp "Z3" ["3.0"]
2.103 -                       (K (250, TFF Implicit, "simple") (* FUDGE *))
2.104 +  remotify_atp z3_tptp "Z3" ["3.0"] (K (250, z3_tff, "simple") (* FUDGE *))
2.105  val remote_e_sine =
2.106    remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
2.107               Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
2.108  val remote_snark =
2.109    remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
2.110               [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
2.111 -             (K (100, TFF Explicit, "simple") (* FUDGE *))
2.112 +             (K (100, dumb_tff, "simple") (* FUDGE *))
2.113  val remote_e_tofof =
2.114 -  remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config)
2.115 -             Axiom Hypothesis (K (150, TFF Explicit, "simple") (* FUDGE *))
2.116 +  remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
2.117 +             Hypothesis (K (150, dumb_tff, "simple") (* FUDGE *))
2.118  val remote_waldmeister =
2.119    remote_atp waldmeisterN "Waldmeister" ["710"]
2.120               [("#START OF PROOF", "Proved Goals:")]
```
```     3.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 16:04:23 2011 +0200
3.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 16:07:34 2011 +0200
3.3 @@ -320,7 +320,7 @@
3.4    fun default c = const_prefix ^ lookup_const c
3.5  in
3.6    fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
3.7 -    | make_fixed_const (SOME (THF With_Choice)) c =
3.8 +    | make_fixed_const (SOME (THF0 THF_With_Choice)) c =
3.9          if c = choice_const then tptp_choice else default c
3.10      | make_fixed_const _ c = default c
3.11  end
3.12 @@ -625,7 +625,7 @@
3.13    | is_type_level_monotonicity_based Fin_Nonmono_Types = true
3.14    | is_type_level_monotonicity_based _ = false
3.15
3.16 -fun adjust_type_enc (THF _) type_enc = type_enc
3.17 +fun adjust_type_enc (THF0 _) type_enc = type_enc
3.18    | adjust_type_enc (TFF _) (Simple_Types (_, level)) =
3.19      Simple_Types (First_Order, level)
3.20    | adjust_type_enc format (Simple_Types (_, level)) =
3.21 @@ -889,16 +889,17 @@
3.22                 if is_tptp_equal s andalso length args = 2 then
3.23                   IConst (`I tptp_equal, T, [])
3.24                 else
3.25 -                 (* Use a proxy even for partially applied THF equality, because
3.26 -                    the LEO-II and Satallax parsers complain about not being
3.27 -                    able to infer the type of "=". *)
3.28 +                 (* Use a proxy even for partially applied THF0 equality,
3.29 +                    because the LEO-II and Satallax parsers complain about not
3.30 +                    being able to infer the type of "=". *)
3.31                   IConst (proxy_base |>> prefix const_prefix, T, T_args)
3.32               | _ => IConst (name, T, [])
3.33             else
3.34               IConst (proxy_base |>> prefix const_prefix, T, T_args)
3.35            | NONE => if s = tptp_choice then
3.36                        tweak_ho_quant tptp_choice T args
3.37 -                    else IConst (name, T, T_args))
3.38 +                    else
3.39 +                      IConst (name, T, T_args))
3.40        | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
3.41        | intro _ _ tm = tm
3.42    in intro true [] end
3.43 @@ -2177,12 +2178,10 @@
3.44        |> (case format of
3.45              CNF => ensure_cnf_problem
3.46            | CNF_UEQ => filter_cnf_ueq_problem
3.47 -          | _ => I)
3.48 -      |> (if is_format_typed format andalso format <> TFF Implicit then
3.49 -            declare_undeclared_syms_in_atp_problem type_decl_prefix
3.50 -                                                   implicit_declsN
3.51 -          else
3.52 -            I)
3.53 +          | FOF => I
3.54 +          | TFF (_, TFF_Implicit) => I
3.55 +          | _ => declare_undeclared_syms_in_atp_problem type_decl_prefix
3.56 +                                                        implicit_declsN)
3.57      val (problem, pool) = problem |> nice_atp_problem readable_names
3.58      val helpers_offset = offset_of_heading_in_problem helpersN problem 0
3.59      val typed_helpers =
```