1.1 --- a/src/HOL/TPTP/atp_export.ML Sat Oct 29 13:15:58 2011 +0200
1.2 +++ b/src/HOL/TPTP/atp_export.ML Sat Oct 29 13:15:58 2011 +0200
1.3 @@ -115,8 +115,7 @@
1.4 val prob_file = File.tmp_path (Path.explode "prob.tptp")
1.5 val {exec, arguments, proof_delims, known_failures, ...} =
1.6 get_atp thy spassN
1.7 - val _ = problem |> tptp_lines_for_atp_problem FOF
1.8 - |> File.write_list prob_file
1.9 + val _ = problem |> lines_for_atp_problem FOF |> File.write_list prob_file
1.10 val command =
1.11 File.shell_path (Path.explode (getenv (fst exec) ^ "/" ^ snd exec)) ^
1.12 " " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^
1.13 @@ -189,7 +188,7 @@
1.14 val atp_problem =
1.15 atp_problem |> add_inferences_to_problem infers
1.16 |> order_problem_facts name_ord
1.17 - val ss = tptp_lines_for_atp_problem FOF atp_problem
1.18 + val ss = lines_for_atp_problem FOF atp_problem
1.19 val _ = app (File.append path) ss
1.20 in () end
1.21
2.1 --- a/src/HOL/Tools/ATP/atp_problem.ML Sat Oct 29 13:15:58 2011 +0200
2.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML Sat Oct 29 13:15:58 2011 +0200
2.3 @@ -25,12 +25,14 @@
2.4 datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic
2.5 datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
2.6 datatype thf_flavor = THF_Without_Choice | THF_With_Choice
2.7 - datatype tptp_format =
2.8 +
2.9 + datatype atp_format =
2.10 CNF |
2.11 CNF_UEQ |
2.12 FOF |
2.13 TFF of tptp_polymorphism * tptp_explicitness |
2.14 - THF of tptp_polymorphism * tptp_explicitness * thf_flavor
2.15 + THF of tptp_polymorphism * tptp_explicitness * thf_flavor |
2.16 + DFG_Sorted
2.17
2.18 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
2.19 datatype 'a problem_line =
2.20 @@ -41,6 +43,11 @@
2.21 * (string, string ho_type) ho_term option
2.22 type 'a problem = (string * 'a problem_line list) list
2.23
2.24 + val isabelle_info_prefix : string
2.25 + val isabelle_info : atp_format -> string -> (string, 'a) ho_term option
2.26 + val introN : string
2.27 + val elimN : string
2.28 + val simpN : string
2.29 val tptp_cnf : string
2.30 val tptp_fof : string
2.31 val tptp_tff : string
2.32 @@ -92,9 +99,9 @@
2.33 bool option -> (bool option -> 'c -> 'd -> 'd) -> ('a, 'b, 'c) formula
2.34 -> 'd -> 'd
2.35 val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
2.36 - val is_format_thf : tptp_format -> bool
2.37 - val is_format_typed : tptp_format -> bool
2.38 - val tptp_lines_for_atp_problem : tptp_format -> string problem -> string list
2.39 + val is_format_thf : atp_format -> bool
2.40 + val is_format_typed : atp_format -> bool
2.41 + val lines_for_atp_problem : atp_format -> string problem -> string list
2.42 val ensure_cnf_problem :
2.43 (string * string) problem -> (string * string) problem
2.44 val filter_cnf_ueq_problem :
2.45 @@ -134,12 +141,13 @@
2.46 datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
2.47 datatype thf_flavor = THF_Without_Choice | THF_With_Choice
2.48
2.49 -datatype tptp_format =
2.50 +datatype atp_format =
2.51 CNF |
2.52 CNF_UEQ |
2.53 FOF |
2.54 TFF of tptp_polymorphism * tptp_explicitness |
2.55 - THF of tptp_polymorphism * tptp_explicitness * thf_flavor
2.56 + THF of tptp_polymorphism * tptp_explicitness * thf_flavor |
2.57 + DFG_Sorted
2.58
2.59 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
2.60 datatype 'a problem_line =
2.61 @@ -148,6 +156,21 @@
2.62 * (string, string ho_type) ho_term option * (string, string ho_type) ho_term option
2.63 type 'a problem = (string * 'a problem_line list) list
2.64
2.65 +val isabelle_info_prefix = "isabelle_"
2.66 +
2.67 +(* Currently, only SPASS supports Isabelle metainformation. *)
2.68 +fun isabelle_info DFG_Sorted s =
2.69 + SOME (ATerm ("[]", [ATerm (isabelle_info_prefix ^ s, [])]))
2.70 + | isabelle_info _ _ = NONE
2.71 +
2.72 +val introN = "intro"
2.73 +val elimN = "elim"
2.74 +val simpN = "simp"
2.75 +
2.76 +fun is_isabelle_info suffix (SOME (ATerm ("[]", [ATerm (s, [])]))) =
2.77 + s = isabelle_info_prefix ^ suffix
2.78 + | is_isabelle_info _ _ = false
2.79 +
2.80 (* official TPTP syntax *)
2.81 val tptp_cnf = "cnf"
2.82 val tptp_fof = "fof"
2.83 @@ -186,6 +209,10 @@
2.84 fun is_tptp_variable s = Char.isUpper (String.sub (s, 0))
2.85 val is_tptp_user_symbol = not o (is_tptp_variable orf is_built_in_tptp_symbol)
2.86
2.87 +val atype_of_types = AType (`I tptp_type_of_types, [])
2.88 +val bool_atype = AType (`I tptp_bool_type, [])
2.89 +val individual_atype = AType (`I tptp_individual_type, [])
2.90 +
2.91 fun raw_polarities_of_conn ANot = (SOME false, NONE)
2.92 | raw_polarities_of_conn AAnd = (SOME true, SOME true)
2.93 | raw_polarities_of_conn AOr = (SOME true, SOME true)
2.94 @@ -228,15 +255,16 @@
2.95 | is_format_thf _ = false
2.96 fun is_format_typed (TFF _) = true
2.97 | is_format_typed (THF _) = true
2.98 + | is_format_typed (DFG_Sorted) = true
2.99 | is_format_typed _ = false
2.100
2.101 -fun string_for_kind Axiom = "axiom"
2.102 - | string_for_kind Definition = "definition"
2.103 - | string_for_kind Lemma = "lemma"
2.104 - | string_for_kind Hypothesis = "hypothesis"
2.105 - | string_for_kind Conjecture = "conjecture"
2.106 +fun tptp_string_for_kind Axiom = "axiom"
2.107 + | tptp_string_for_kind Definition = "definition"
2.108 + | tptp_string_for_kind Lemma = "lemma"
2.109 + | tptp_string_for_kind Hypothesis = "hypothesis"
2.110 + | tptp_string_for_kind Conjecture = "conjecture"
2.111
2.112 -fun string_for_app format func args =
2.113 +fun tptp_string_for_app format func args =
2.114 if is_format_thf format then
2.115 "(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")"
2.116 else
2.117 @@ -255,17 +283,21 @@
2.118
2.119 fun str_for_type format ty =
2.120 let
2.121 - fun str _ (AType (s, [])) = s
2.122 + val dfg = (format = DFG_Sorted)
2.123 + fun str _ (AType (s, [])) =
2.124 + if dfg andalso s = tptp_individual_type then "Top" else s
2.125 | str _ (AType (s, tys)) =
2.126 let val ss = tys |> map (str false) in
2.127 if s = tptp_product_type then
2.128 - ss |> space_implode (" " ^ tptp_product_type ^ " ")
2.129 - |> length ss > 1 ? enclose "(" ")"
2.130 + ss |> space_implode
2.131 + (if dfg then ", " else " " ^ tptp_product_type ^ " ")
2.132 + |> (not dfg andalso length ss > 1) ? enclose "(" ")"
2.133 else
2.134 - string_for_app format s ss
2.135 + tptp_string_for_app format s ss
2.136 end
2.137 | str rhs (AFun (ty1, ty2)) =
2.138 - str false ty1 ^ " " ^ tptp_fun_type ^ " " ^ str true ty2
2.139 + (str false ty1 |> dfg ? enclose "(" ")") ^ " " ^
2.140 + (if dfg then "" else tptp_fun_type ^ " ") ^ str true ty2
2.141 |> not rhs ? enclose "(" ")"
2.142 | str _ (ATyAbs (ss, ty)) =
2.143 tptp_pi_binder ^ "[" ^
2.144 @@ -274,17 +306,16 @@
2.145 in str true ty end
2.146
2.147 fun string_for_type (format as THF _) ty = str_for_type format ty
2.148 - | string_for_type (format as TFF _) ty = str_for_type format (flatten_type ty)
2.149 - | string_for_type _ _ = raise Fail "unexpected type in untyped format"
2.150 + | string_for_type format ty = str_for_type format (flatten_type ty)
2.151
2.152 -fun string_for_quantifier AForall = tptp_forall
2.153 - | string_for_quantifier AExists = tptp_exists
2.154 +fun tptp_string_for_quantifier AForall = tptp_forall
2.155 + | tptp_string_for_quantifier AExists = tptp_exists
2.156
2.157 -fun string_for_connective ANot = tptp_not
2.158 - | string_for_connective AAnd = tptp_and
2.159 - | string_for_connective AOr = tptp_or
2.160 - | string_for_connective AImplies = tptp_implies
2.161 - | string_for_connective AIff = tptp_iff
2.162 +fun tptp_string_for_connective ANot = tptp_not
2.163 + | tptp_string_for_connective AAnd = tptp_and
2.164 + | tptp_string_for_connective AOr = tptp_or
2.165 + | tptp_string_for_connective AImplies = tptp_implies
2.166 + | tptp_string_for_connective AIff = tptp_iff
2.167
2.168 fun string_for_bound_var format (s, ty) =
2.169 s ^
2.170 @@ -298,84 +329,193 @@
2.171 fun is_format_with_choice (THF (_, _, THF_With_Choice)) = true
2.172 | is_format_with_choice _ = false
2.173
2.174 -fun string_for_term _ (ATerm (s, [])) = s
2.175 - | string_for_term format (ATerm (s, ts)) =
2.176 +fun tptp_string_for_term _ (ATerm (s, [])) = s
2.177 + | tptp_string_for_term format (ATerm (s, ts)) =
2.178 (if s = tptp_empty_list then
2.179 (* used for lists in the optional "source" field of a derivation *)
2.180 - "[" ^ commas (map (string_for_term format) ts) ^ "]"
2.181 + "[" ^ commas (map (tptp_string_for_term format) ts) ^ "]"
2.182 else if is_tptp_equal s then
2.183 - space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts)
2.184 + space_implode (" " ^ tptp_equal ^ " ")
2.185 + (map (tptp_string_for_term format) ts)
2.186 |> is_format_thf format ? enclose "(" ")"
2.187 else case (s = tptp_ho_forall orelse s = tptp_ho_exists,
2.188 s = tptp_choice andalso is_format_with_choice format, ts) of
2.189 (true, _, [AAbs ((s', ty), tm)]) =>
2.190 (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
2.191 possible, to work around LEO-II 1.2.8 parser limitation. *)
2.192 - string_for_formula format
2.193 + tptp_string_for_formula format
2.194 (AQuant (if s = tptp_ho_forall then AForall else AExists,
2.195 [(s', SOME ty)], AAtom tm))
2.196 | (_, true, [AAbs ((s', ty), tm)]) =>
2.197 (* There is code in "ATP_Translate" to ensure that "Eps" is always
2.198 applied to an abstraction. *)
2.199 tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
2.200 - string_for_term format tm ^ ""
2.201 + tptp_string_for_term format tm ^ ""
2.202 |> enclose "(" ")"
2.203 - | _ => string_for_app format s (map (string_for_term format) ts))
2.204 - | string_for_term (format as THF _) (AAbs ((s, ty), tm)) =
2.205 + | _ => tptp_string_for_app format s (map (tptp_string_for_term format) ts))
2.206 + | tptp_string_for_term (format as THF _) (AAbs ((s, ty), tm)) =
2.207 "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^
2.208 - string_for_term format tm ^ ")"
2.209 - | string_for_term _ _ = raise Fail "unexpected term in first-order format"
2.210 -and string_for_formula format (AQuant (q, xs, phi)) =
2.211 - string_for_quantifier q ^
2.212 + tptp_string_for_term format tm ^ ")"
2.213 + | tptp_string_for_term _ _ =
2.214 + raise Fail "unexpected term in first-order format"
2.215 +and tptp_string_for_formula format (AQuant (q, xs, phi)) =
2.216 + tptp_string_for_quantifier q ^
2.217 "[" ^ commas (map (string_for_bound_var format) xs) ^ "]: " ^
2.218 - string_for_formula format phi
2.219 + tptp_string_for_formula format phi
2.220 |> enclose "(" ")"
2.221 - | string_for_formula format
2.222 + | tptp_string_for_formula format
2.223 (AConn (ANot, [AAtom (ATerm ("=" (* tptp_equal *), ts))])) =
2.224 space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ")
2.225 - (map (string_for_term format) ts)
2.226 + (map (tptp_string_for_term format) ts)
2.227 |> is_format_thf format ? enclose "(" ")"
2.228 - | string_for_formula format (AConn (c, [phi])) =
2.229 - string_for_connective c ^ " " ^
2.230 - (string_for_formula format phi |> is_format_thf format ? enclose "(" ")")
2.231 + | tptp_string_for_formula format (AConn (c, [phi])) =
2.232 + tptp_string_for_connective c ^ " " ^
2.233 + (tptp_string_for_formula format phi
2.234 + |> is_format_thf format ? enclose "(" ")")
2.235 |> enclose "(" ")"
2.236 - | string_for_formula format (AConn (c, phis)) =
2.237 - space_implode (" " ^ string_for_connective c ^ " ")
2.238 - (map (string_for_formula format) phis)
2.239 + | tptp_string_for_formula format (AConn (c, phis)) =
2.240 + space_implode (" " ^ tptp_string_for_connective c ^ " ")
2.241 + (map (tptp_string_for_formula format) phis)
2.242 |> enclose "(" ")"
2.243 - | string_for_formula format (AAtom tm) = string_for_term format tm
2.244 + | tptp_string_for_formula format (AAtom tm) = tptp_string_for_term format tm
2.245
2.246 fun the_source (SOME source) = source
2.247 | the_source NONE =
2.248 ATerm ("inference",
2.249 ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", [])))
2.250
2.251 -fun string_for_format CNF = tptp_cnf
2.252 - | string_for_format CNF_UEQ = tptp_cnf
2.253 - | string_for_format FOF = tptp_fof
2.254 - | string_for_format (TFF _) = tptp_tff
2.255 - | string_for_format (THF _) = tptp_thf
2.256 +fun tptp_string_for_format CNF = tptp_cnf
2.257 + | tptp_string_for_format CNF_UEQ = tptp_cnf
2.258 + | tptp_string_for_format FOF = tptp_fof
2.259 + | tptp_string_for_format (TFF _) = tptp_tff
2.260 + | tptp_string_for_format (THF _) = tptp_thf
2.261 + | tptp_string_for_format DFG_Sorted = raise Fail "non-TPTP format"
2.262
2.263 -fun string_for_problem_line format (Decl (ident, sym, ty)) =
2.264 - string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^
2.265 - string_for_type format ty ^ ").\n"
2.266 - | string_for_problem_line format (Formula (ident, kind, phi, source, info)) =
2.267 - string_for_format format ^ "(" ^ ident ^ ", " ^ string_for_kind kind ^
2.268 - ",\n (" ^ string_for_formula format phi ^ ")" ^
2.269 +fun tptp_string_for_problem_line format (Decl (ident, sym, ty)) =
2.270 + tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^
2.271 + " : " ^ string_for_type format ty ^ ").\n"
2.272 + | tptp_string_for_problem_line format
2.273 + (Formula (ident, kind, phi, source, info)) =
2.274 + tptp_string_for_format format ^ "(" ^ ident ^ ", " ^
2.275 + tptp_string_for_kind kind ^ ",\n (" ^
2.276 + tptp_string_for_formula format phi ^ ")" ^
2.277 (case (source, info) of
2.278 (NONE, NONE) => ""
2.279 - | (SOME tm, NONE) => ", " ^ string_for_term format tm
2.280 + | (SOME tm, NONE) => ", " ^ tptp_string_for_term format tm
2.281 | (_, SOME tm) =>
2.282 - ", " ^ string_for_term format (the_source source) ^
2.283 - ", " ^ string_for_term format tm) ^ ").\n"
2.284 -fun tptp_lines_for_atp_problem format problem =
2.285 - "% This file was generated by Isabelle (most likely Sledgehammer)\n\
2.286 - \% " ^ timestamp () ^ "\n" ::
2.287 + ", " ^ tptp_string_for_term format (the_source source) ^
2.288 + ", " ^ tptp_string_for_term format tm) ^ ").\n"
2.289 +
2.290 +fun tptp_lines format =
2.291 maps (fn (_, []) => []
2.292 | (heading, lines) =>
2.293 "\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" ::
2.294 - map (string_for_problem_line format) lines)
2.295 - problem
2.296 + map (tptp_string_for_problem_line format) lines)
2.297 +
2.298 +fun arity_of_type (AFun (_, ty)) = 1 + arity_of_type ty
2.299 + | arity_of_type _ = 0
2.300 +
2.301 +fun binder_atypes (AFun (ty1, ty2)) = ty1 :: binder_atypes ty2
2.302 + | binder_atypes _ = []
2.303 +
2.304 +fun is_function_type (AFun (_, ty)) = is_function_type ty
2.305 + | is_function_type (AType (s, _)) =
2.306 + s <> tptp_type_of_types andalso s <> tptp_bool_type
2.307 + | is_function_type _ = false
2.308 +
2.309 +fun is_predicate_type (AFun (_, ty)) = is_predicate_type ty
2.310 + | is_predicate_type (AType (s, _)) = (s = tptp_bool_type)
2.311 + | is_predicate_type _ = false
2.312 +
2.313 +fun dfg_string_for_formula info =
2.314 + let
2.315 + fun str_for_term simp (ATerm (s, tms)) =
2.316 + (if is_tptp_equal s then "equal" |> simp ? suffix ":lr"
2.317 + else if s = tptp_true then "true"
2.318 + else if s = tptp_false then "false"
2.319 + else s) ^
2.320 + (if null tms then ""
2.321 + else "(" ^ commas (map (str_for_term false) tms) ^ ")")
2.322 + | str_for_term _ _ = raise Fail "unexpected term in first-order format"
2.323 + fun str_for_quant AForall = "forall"
2.324 + | str_for_quant AExists = "exists"
2.325 + fun str_for_conn _ ANot = "not"
2.326 + | str_for_conn _ AAnd = "and"
2.327 + | str_for_conn _ AOr = "or"
2.328 + | str_for_conn _ AImplies = "implies"
2.329 + | str_for_conn simp AIff = "equiv" |> simp ? suffix ":lr"
2.330 + fun str_for_formula simp (AQuant (q, xs, phi)) =
2.331 + str_for_quant q ^ "(" ^ "[" ^
2.332 + commas (map (string_for_bound_var DFG_Sorted) xs) ^ "], " ^
2.333 + str_for_formula simp phi ^ ")"
2.334 + | str_for_formula simp (AConn (c, phis)) =
2.335 + str_for_conn simp c ^ "(" ^
2.336 + commas (map (str_for_formula false) phis) ^ ")"
2.337 + | str_for_formula simp (AAtom tm) = str_for_term simp tm
2.338 + in str_for_formula (is_isabelle_info simpN info) end
2.339 +
2.340 +fun dfg_lines problem =
2.341 + let
2.342 + fun ary sym ty =
2.343 + "(" ^ sym ^ ", " ^ string_of_int (arity_of_type ty) ^ ")"
2.344 + fun fun_typ sym ty =
2.345 + "function(" ^ sym ^ ", " ^ string_for_type DFG_Sorted ty ^ ")."
2.346 + fun pred_typ sym ty =
2.347 + "predicate(" ^
2.348 + commas (sym :: map (string_for_type DFG_Sorted) (binder_atypes ty)) ^ ")."
2.349 + fun formula pred (Formula (ident, kind, phi, _, info)) =
2.350 + if pred kind then
2.351 + SOME ("formula(" ^ dfg_string_for_formula info phi ^ ", " ^ ident ^
2.352 + ").")
2.353 + else
2.354 + NONE
2.355 + | formula _ _ = NONE
2.356 + fun filt f = problem |> map (map_filter f o snd) |> flat
2.357 + val func_aries =
2.358 + filt (fn Decl (_, sym, ty) =>
2.359 + if is_function_type ty then SOME (ary sym ty) else NONE
2.360 + | _ => NONE)
2.361 + |> commas |> enclose "functions [" "]."
2.362 + val pred_aries =
2.363 + filt (fn Decl (_, sym, ty) =>
2.364 + if is_predicate_type ty then SOME (ary sym ty) else NONE
2.365 + | _ => NONE)
2.366 + |> commas |> enclose "predicates [" "]."
2.367 + val sorts =
2.368 + filt (fn Decl (_, sym, AType (s, [])) =>
2.369 + if s = tptp_type_of_types then SOME sym else NONE
2.370 + | _ => NONE)
2.371 + |> commas |> enclose "sorts [" "]."
2.372 + val func_sigs =
2.373 + filt (fn Decl (_, sym, ty) =>
2.374 + if is_function_type ty then SOME (fun_typ sym ty) else NONE
2.375 + | _ => NONE)
2.376 + val pred_sigs =
2.377 + filt (fn Decl (_, sym, ty) =>
2.378 + if is_predicate_type ty then SOME (pred_typ sym ty) else NONE
2.379 + | _ => NONE)
2.380 + val axioms = filt (formula (curry (op <>) Conjecture))
2.381 + val conjs = filt (formula (curry (op =) Conjecture))
2.382 + fun list_of _ [] = []
2.383 + | list_of heading ss =
2.384 + "list_of_" ^ heading ^ ".\n" :: map (suffix "\n") ss @
2.385 + ["end_of_list.\n\n"]
2.386 + in
2.387 + "\nbegin_problem(isabelle).\n\n" ::
2.388 + list_of "descriptions"
2.389 + ["name({**}).", "author({**}).", "status(unknown).",
2.390 + "description({**})."] @
2.391 + list_of "symbols" [func_aries, pred_aries, sorts] @
2.392 + list_of "declarations" (func_sigs @ pred_sigs) @
2.393 + list_of "formulae(axioms)" axioms @
2.394 + list_of "formulae(conjectures)" conjs @
2.395 + ["end_problem.\n"]
2.396 + end
2.397 +
2.398 +fun lines_for_atp_problem format problem =
2.399 + "% This file was generated by Isabelle (most likely Sledgehammer)\n\
2.400 + \% " ^ timestamp () ^ "\n" ::
2.401 + (if format = DFG_Sorted then dfg_lines else tptp_lines format) problem
2.402
2.403
2.404 (** CNF (Metis) and CNF UEQ (Waldmeister) **)
2.405 @@ -467,11 +607,6 @@
2.406 (* TFF allows implicit declarations of types, function symbols, and predicate
2.407 symbols (with "$i" as the type of individuals), but some provers (e.g.,
2.408 SNARK) require explicit declarations. The situation is similar for THF. *)
2.409 -
2.410 -val atype_of_types = AType (`I tptp_type_of_types, [])
2.411 -val bool_atype = AType (`I tptp_bool_type, [])
2.412 -val individual_atype = AType (`I tptp_individual_type, [])
2.413 -
2.414 fun default_type pred_sym =
2.415 let
2.416 fun typ 0 = if pred_sym then bool_atype else individual_atype
2.417 @@ -548,7 +683,12 @@
2.418 unreadable "op_1", "op_2", etc., in the problem files. "eq" is reserved to
2.419 ensure that "HOL.eq" is correctly mapped to equality (not clear whether this
2.420 is still necessary). *)
2.421 -val reserved_nice_names = [tptp_old_equal, "op", "eq"]
2.422 +val spass_reserved_nice_names =
2.423 + ["forall", "exists", "le", "ls", "ge", "gs", "plus", "minus", "mult", "fract",
2.424 + "equal", "true", "false", "or", "and", "not", "implies", "implied", "equiv",
2.425 + "lr", "def"]
2.426 +val reserved_nice_names =
2.427 + [tptp_old_equal, "op", "eq"] @ spass_reserved_nice_names
2.428
2.429 fun readable_name full_name s =
2.430 if s = full_name then
3.1 --- a/src/HOL/Tools/ATP/atp_proof.ML Sat Oct 29 13:15:58 2011 +0200
3.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML Sat Oct 29 13:15:58 2011 +0200
3.3 @@ -24,8 +24,6 @@
3.4 TimedOut |
3.5 Inappropriate |
3.6 OutOfResources |
3.7 - SpassTooOld |
3.8 - VampireTooOld |
3.9 NoPerl |
3.10 NoLibwwwPerl |
3.11 MalformedInput |
3.12 @@ -81,8 +79,6 @@
3.13 TimedOut |
3.14 Inappropriate |
3.15 OutOfResources |
3.16 - SpassTooOld |
3.17 - VampireTooOld |
3.18 NoPerl |
3.19 NoLibwwwPerl |
3.20 MalformedInput |
3.21 @@ -134,17 +130,6 @@
3.22 | string_for_failure Inappropriate =
3.23 "The problem lies outside the prover's scope."
3.24 | string_for_failure OutOfResources = "The prover ran out of resources."
3.25 - | string_for_failure SpassTooOld =
3.26 - "Isabelle requires a more recent version of SPASS with support for the \
3.27 - \TPTP syntax. To install it, download and extract the package \
3.28 - \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
3.29 - \\"spass-3.7\" directory's absolute path to " ^
3.30 - Path.print (Path.expand (Path.explode "$ISABELLE_HOME_USER/etc/components")) ^
3.31 - " on a line of its own."
3.32 - | string_for_failure VampireTooOld =
3.33 - "Isabelle requires a more recent version of Vampire. To install it, follow \
3.34 - \the instructions from the Sledgehammer manual (\"isabelle doc\
3.35 - \ sledgehammer\")."
3.36 | string_for_failure NoPerl = "Perl" ^ missing_message_tail
3.37 | string_for_failure NoLibwwwPerl =
3.38 "The Perl module \"libwww-perl\"" ^ missing_message_tail
4.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Sat Oct 29 13:15:58 2011 +0200
4.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sat Oct 29 13:15:58 2011 +0200
4.3 @@ -7,7 +7,7 @@
4.4
4.5 signature ATP_SYSTEMS =
4.6 sig
4.7 - type tptp_format = ATP_Problem.tptp_format
4.8 + type atp_format = ATP_Problem.atp_format
4.9 type formula_kind = ATP_Problem.formula_kind
4.10 type failure = ATP_Proof.failure
4.11
4.12 @@ -23,7 +23,7 @@
4.13 prem_kind : formula_kind,
4.14 best_slices :
4.15 Proof.context
4.16 - -> (real * (bool * (int * tptp_format * string * string))) list}
4.17 + -> (real * (bool * (int * atp_format * string * string))) list}
4.18
4.19 val force_sos : bool Config.T
4.20 val e_smartN : string
4.21 @@ -46,6 +46,7 @@
4.22 val satallaxN : string
4.23 val snarkN : string
4.24 val spassN : string
4.25 + val spass_newN : string
4.26 val vampireN : string
4.27 val waldmeisterN : string
4.28 val z3_tptpN : string
4.29 @@ -53,7 +54,7 @@
4.30 val remote_atp :
4.31 string -> string -> string list -> (string * string) list
4.32 -> (failure * string) list -> formula_kind -> formula_kind
4.33 - -> (Proof.context -> int * tptp_format * string) -> string * atp_config
4.34 + -> (Proof.context -> int * atp_format * string) -> string * atp_config
4.35 val add_atp : string * atp_config -> theory -> theory
4.36 val get_atp : theory -> string -> atp_config
4.37 val supported_atps : theory -> string list
4.38 @@ -82,7 +83,7 @@
4.39 prem_kind : formula_kind,
4.40 best_slices :
4.41 Proof.context
4.42 - -> (real * (bool * (int * tptp_format * string * string))) list}
4.43 + -> (real * (bool * (int * atp_format * string * string))) list}
4.44
4.45 (* "best_slices" must be found empirically, taking a wholistic approach since
4.46 the ATPs are run in parallel. The "real" components give the faction of the
4.47 @@ -130,6 +131,7 @@
4.48 val satallaxN = "satallax"
4.49 val snarkN = "snark"
4.50 val spassN = "spass"
4.51 +val spass_newN = "spass_new"
4.52 val vampireN = "vampire"
4.53 val waldmeisterN = "waldmeister"
4.54 val z3_tptpN = "z3_tptp"
4.55 @@ -315,7 +317,6 @@
4.56 (MalformedInput, "Undefined symbol"),
4.57 (MalformedInput, "Free Variable"),
4.58 (Unprovable, "No formulae and clauses found in input file"),
4.59 - (SpassTooOld, "tptp2dfg"),
4.60 (InternalError, "Please report this error")],
4.61 conj_sym_kind = Hypothesis,
4.62 prem_kind = Conjecture,
4.63 @@ -329,6 +330,25 @@
4.64
4.65 val spass = (spassN, spass_config)
4.66
4.67 +(* Experimental *)
4.68 +val spass_new_config : atp_config =
4.69 + {exec = ("SPASS_HOME", "SPASS"),
4.70 + required_execs = [],
4.71 + arguments = #arguments spass_config,
4.72 + proof_delims = #proof_delims spass_config,
4.73 + known_failures = #known_failures spass_config,
4.74 + conj_sym_kind = #conj_sym_kind spass_config,
4.75 + prem_kind = #prem_kind spass_config,
4.76 + best_slices = fn ctxt =>
4.77 + (* FUDGE *)
4.78 + [(0.333, (false, (150, DFG_Sorted, "mono_simple", sosN))) (*,
4.79 + (0.333, (false, (300, DFG_Sorted, "poly_tags??", sosN))),
4.80 + (0.334, (true, (50, DFG_Sorted, "mono_simple", no_sosN)))*)]
4.81 + |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
4.82 + else I)}
4.83 +
4.84 +val spass_new = (spass_newN, spass_new_config)
4.85 +
4.86
4.87 (* Vampire *)
4.88
4.89 @@ -359,7 +379,6 @@
4.90 (GaveUp, "CANNOT PROVE"),
4.91 (Unprovable, "Satisfiability detected"),
4.92 (Unprovable, "Termination reason: Satisfiable"),
4.93 - (VampireTooOld, "not a valid option"),
4.94 (Interrupted, "Aborted by signal SIGINT")],
4.95 conj_sym_kind = Conjecture,
4.96 prem_kind = Conjecture,
4.97 @@ -545,9 +564,9 @@
4.98 Synchronized.change systems (fn _ => get_systems ())
4.99
4.100 val atps =
4.101 - [e, leo2, pff, phf, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
4.102 - remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine, remote_snark,
4.103 - remote_e_tofof, remote_waldmeister]
4.104 + [e, leo2, pff, phf, satallax, spass, spass_new, vampire, z3_tptp, remote_e,
4.105 + remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine,
4.106 + remote_snark, remote_e_tofof, remote_waldmeister]
4.107 val setup = fold add_atp atps
4.108
4.109 end;
5.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Sat Oct 29 13:15:58 2011 +0200
5.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Sat Oct 29 13:15:58 2011 +0200
5.3 @@ -11,7 +11,7 @@
5.4 type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
5.5 type connective = ATP_Problem.connective
5.6 type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
5.7 - type tptp_format = ATP_Problem.tptp_format
5.8 + type atp_format = ATP_Problem.atp_format
5.9 type formula_kind = ATP_Problem.formula_kind
5.10 type 'a problem = 'a ATP_Problem.problem
5.11
5.12 @@ -86,7 +86,7 @@
5.13 val is_type_enc_quasi_sound : type_enc -> bool
5.14 val is_type_enc_fairly_sound : type_enc -> bool
5.15 val type_enc_from_string : soundness -> string -> type_enc
5.16 - val adjust_type_enc : tptp_format -> type_enc -> type_enc
5.17 + val adjust_type_enc : atp_format -> type_enc -> type_enc
5.18 val mk_aconns :
5.19 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
5.20 val unmangled_const : string -> string * (string, 'b) ho_term list
5.21 @@ -94,7 +94,7 @@
5.22 val helper_table : ((string * bool) * thm list) list
5.23 val factsN : string
5.24 val prepare_atp_problem :
5.25 - Proof.context -> tptp_format -> formula_kind -> formula_kind -> type_enc
5.26 + Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc
5.27 -> bool -> string -> bool -> bool -> term list -> term
5.28 -> ((string * locality) * term) list
5.29 -> string problem * string Symtab.table * int * int
5.30 @@ -123,20 +123,10 @@
5.31 val lambdasN = "lambdas"
5.32 val smartN = "smart"
5.33
5.34 -val generate_info = false (* experimental *)
5.35 -
5.36 -fun isabelle_info s =
5.37 - if generate_info then SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
5.38 - else NONE
5.39 -
5.40 -val introN = "intro"
5.41 -val elimN = "elim"
5.42 -val simpN = "simp"
5.43 -
5.44 (* TFF1 is still in development, and it is still unclear whether symbols will be
5.45 allowed to have types like "$tType > $o" (i.e., "![A : $tType] : $o"), with
5.46 - "dummy" type variables. *)
5.47 -val avoid_first_order_dummy_type_vars = true
5.48 + ghost type variables. *)
5.49 +val avoid_first_order_ghost_type_vars = true
5.50
5.51 val bound_var_prefix = "B_"
5.52 val all_bound_var_prefix = "BA_"
5.53 @@ -313,7 +303,7 @@
5.54 tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
5.55 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
5.56
5.57 -(* "HOL.eq" and Choice are mapped to the ATP's equivalents *)
5.58 +(* "HOL.eq" and choice are mapped to the ATP's equivalents *)
5.59 local
5.60 val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT
5.61 fun default c = const_prefix ^ lookup_const c
5.62 @@ -650,6 +640,8 @@
5.63 | adjust_type_enc (THF _) type_enc = type_enc
5.64 | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =
5.65 Simple_Types (First_Order, Mangled_Monomorphic, level)
5.66 + | adjust_type_enc DFG_Sorted (Simple_Types (_, _, level)) =
5.67 + Simple_Types (First_Order, Mangled_Monomorphic, level)
5.68 | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
5.69 Simple_Types (First_Order, poly, level)
5.70 | adjust_type_enc format (Simple_Types (_, poly, level)) =
5.71 @@ -755,7 +747,7 @@
5.72 AAtom (ATerm (class, arg ::
5.73 (case type_enc of
5.74 Simple_Types (First_Order, Polymorphic, _) =>
5.75 - if avoid_first_order_dummy_type_vars then [ATerm (TYPE_name, [arg])]
5.76 + if avoid_first_order_ghost_type_vars then [ATerm (TYPE_name, [arg])]
5.77 else []
5.78 | _ => [])))
5.79 fun formulas_for_types type_enc add_sorts_on_typ Ts =
5.80 @@ -1545,7 +1537,7 @@
5.81
5.82 val type_tag = `(make_fixed_const NONE) type_tag_name
5.83
5.84 -fun type_tag_idempotence_fact type_enc =
5.85 +fun type_tag_idempotence_fact format type_enc =
5.86 let
5.87 fun var s = ATerm (`I s, [])
5.88 fun tag tm = ATerm (type_tag, [var "A", tm])
5.89 @@ -1553,7 +1545,7 @@
5.90 in
5.91 Formula (type_tag_idempotence_helper_name, Axiom,
5.92 eq_formula type_enc [] false (tag tagged_var) tagged_var,
5.93 - isabelle_info simpN, NONE)
5.94 + isabelle_info format simpN, NONE)
5.95 end
5.96
5.97 fun should_specialize_helper type_enc t =
5.98 @@ -1833,32 +1825,34 @@
5.99 |> close_formula_universally type_enc,
5.100 NONE,
5.101 case locality of
5.102 - Intro => isabelle_info introN
5.103 - | Elim => isabelle_info elimN
5.104 - | Simp => isabelle_info simpN
5.105 + Intro => isabelle_info format introN
5.106 + | Elim => isabelle_info format elimN
5.107 + | Simp => isabelle_info format simpN
5.108 | _ => NONE)
5.109 |> Formula
5.110
5.111 -fun formula_line_for_class_rel_clause type_enc
5.112 +fun formula_line_for_class_rel_clause format type_enc
5.113 ({name, subclass, superclass, ...} : class_rel_clause) =
5.114 let val ty_arg = ATerm (tvar_a_name, []) in
5.115 Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
5.116 AConn (AImplies,
5.117 [type_class_formula type_enc subclass ty_arg,
5.118 type_class_formula type_enc superclass ty_arg])
5.119 - |> close_formula_universally type_enc, isabelle_info introN, NONE)
5.120 + |> close_formula_universally type_enc,
5.121 + isabelle_info format introN, NONE)
5.122 end
5.123
5.124 fun formula_from_arity_atom type_enc (class, t, args) =
5.125 ATerm (t, map (fn arg => ATerm (arg, [])) args)
5.126 |> type_class_formula type_enc class
5.127
5.128 -fun formula_line_for_arity_clause type_enc
5.129 +fun formula_line_for_arity_clause format type_enc
5.130 ({name, prem_atoms, concl_atom, ...} : arity_clause) =
5.131 Formula (arity_clause_prefix ^ name, Axiom,
5.132 mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms)
5.133 (formula_from_arity_atom type_enc concl_atom)
5.134 - |> close_formula_universally type_enc, isabelle_info introN, NONE)
5.135 + |> close_formula_universally type_enc,
5.136 + isabelle_info format introN, NONE)
5.137
5.138 fun formula_line_for_conjecture ctxt format mono type_enc
5.139 ({name, kind, iformula, atomic_types, ...} : translated_formula) =
5.140 @@ -1883,7 +1877,7 @@
5.141 fun decl_line_for_class order s =
5.142 let val name as (s, _) = `make_type_class s in
5.143 Decl (sym_decl_prefix ^ s, name,
5.144 - if order = First_Order andalso avoid_first_order_dummy_type_vars then
5.145 + if order = First_Order andalso avoid_first_order_ghost_type_vars then
5.146 ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype))
5.147 else
5.148 AFun (atype_of_types, bool_atype))
5.149 @@ -2059,7 +2053,7 @@
5.150 (K (K (K (K (K (K true)))))) (SOME true)
5.151 |> bound_tvars type_enc (atyps_of T)
5.152 |> close_formula_universally type_enc,
5.153 - isabelle_info introN, NONE)
5.154 + isabelle_info format introN, NONE)
5.155
5.156 fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
5.157 let val x_var = ATerm (`make_bound_var "X", []) in
5.158 @@ -2069,7 +2063,7 @@
5.159 eq_formula type_enc (atyps_of T) false
5.160 (tag_with_type ctxt format mono type_enc NONE T x_var)
5.161 x_var,
5.162 - isabelle_info simpN, NONE)
5.163 + isabelle_info format simpN, NONE)
5.164 end
5.165
5.166 fun problem_lines_for_mono_types ctxt format mono type_enc Ts =
5.167 @@ -2143,7 +2137,7 @@
5.168 |> n > 1 ? bound_tvars type_enc (atyps_of T)
5.169 |> close_formula_universally type_enc
5.170 |> maybe_negate,
5.171 - isabelle_info introN, NONE)
5.172 + isabelle_info format introN, NONE)
5.173 end
5.174
5.175 fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s
5.176 @@ -2179,7 +2173,7 @@
5.177 in
5.178 cons (Formula (ident_base ^ "_res", kind,
5.179 eq (tag_with res_T (cst bounds)) (cst tagged_bounds),
5.180 - isabelle_info simpN, NONE))
5.181 + isabelle_info format simpN, NONE))
5.182 end
5.183 else
5.184 I
5.185 @@ -2191,7 +2185,7 @@
5.186 cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
5.187 eq (cst (bounds1 @ tag_with arg_T bound :: bounds2))
5.188 (cst bounds),
5.189 - isabelle_info simpN, NONE))
5.190 + isabelle_info format simpN, NONE))
5.191 | _ => raise Fail "expected nonempty tail"
5.192 else
5.193 I
5.194 @@ -2343,7 +2337,7 @@
5.195 |> map (formula_line_for_fact ctxt format helper_prefix I false true mono
5.196 type_enc)
5.197 |> (if needs_type_tag_idempotence ctxt type_enc then
5.198 - cons (type_tag_idempotence_fact type_enc)
5.199 + cons (type_tag_idempotence_fact format type_enc)
5.200 else
5.201 I)
5.202 (* Reordering these might confuse the proof reconstruction code or the SPASS
5.203 @@ -2355,8 +2349,10 @@
5.204 (not exporter) (not exporter) mono type_enc)
5.205 (0 upto length facts - 1 ~~ facts)),
5.206 (class_relsN,
5.207 - map (formula_line_for_class_rel_clause type_enc) class_rel_clauses),
5.208 - (aritiesN, map (formula_line_for_arity_clause type_enc) arity_clauses),
5.209 + map (formula_line_for_class_rel_clause format type_enc)
5.210 + class_rel_clauses),
5.211 + (aritiesN,
5.212 + map (formula_line_for_arity_clause format type_enc) arity_clauses),
5.213 (helpersN, helper_lines),
5.214 (conjsN,
5.215 map (formula_line_for_conjecture ctxt format mono type_enc) conjs),
6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sat Oct 29 13:15:58 2011 +0200
6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sat Oct 29 13:15:58 2011 +0200
6.3 @@ -799,28 +799,28 @@
6.4 is_that_fact thm
6.5 end)
6.6
6.7 -fun meta_equify (@{const Trueprop}
6.8 - $ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2)) =
6.9 - Const (@{const_name "=="}, T --> T --> @{typ prop}) $ t1 $ t2
6.10 - | meta_equify t = t
6.11 -
6.12 -val normalize_simp_prop =
6.13 - meta_equify
6.14 - #> map_aterms (fn Var ((s, _), T) => Var ((s, 0), T) | t => t)
6.15 +val crude_zero_vars =
6.16 + map_aterms (fn Var ((s, _), T) => Var ((s, 0), T) | t => t)
6.17 #> map_types (map_type_tvar (fn ((s, _), S) => TVar ((s, 0), S)))
6.18
6.19 fun clasimpset_rule_table_of ctxt =
6.20 let
6.21 - fun add loc g f = fold (Termtab.update o rpair loc o g o prop_of o f)
6.22 - val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt |> claset_of |> Classical.rep_cs
6.23 + val thy = Proof_Context.theory_of ctxt
6.24 + val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
6.25 + fun add loc g f =
6.26 + fold (Termtab.update o rpair loc o g o crude_zero_vars o prop_of o f)
6.27 + val {safeIs, safeEs, hazIs, hazEs, ...} =
6.28 + ctxt |> claset_of |> Classical.rep_cs
6.29 val intros = Item_Net.content safeIs @ Item_Net.content hazIs
6.30 - val elims = map Classical.classical_rule (Item_Net.content safeEs @ Item_Net.content hazEs)
6.31 + val elims =
6.32 + Item_Net.content safeEs @ Item_Net.content hazEs
6.33 + |> map Classical.classical_rule
6.34 val simps = ctxt |> simpset_of |> dest_ss |> #simps
6.35 in
6.36 Termtab.empty |> add Intro I I intros
6.37 |> add Elim I I elims
6.38 |> add Simp I snd simps
6.39 - |> add Simp normalize_simp_prop snd simps
6.40 + |> add Simp atomize snd simps
6.41 end
6.42
6.43 fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths =
6.44 @@ -833,17 +833,20 @@
6.45 fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms
6.46 val is_chained = member Thm.eq_thm_prop chained_ths
6.47 val clasimpset_table = clasimpset_rule_table_of ctxt
6.48 - fun locality_of_theorem global (name: string) th =
6.49 - if String.isSubstring ".induct" name orelse(*FIXME: use structured name*)
6.50 + fun locality_of_theorem global name th =
6.51 + if String.isSubstring ".induct" name orelse (*FIXME: use structured name*)
6.52 String.isSubstring ".inducts" name then
6.53 - Induction
6.54 + Induction
6.55 else if is_chained th then
6.56 Chained
6.57 else if global then
6.58 case Termtab.lookup clasimpset_table (prop_of th) of
6.59 SOME loc => loc
6.60 | NONE => General
6.61 - else if is_assum th then Assum else Local
6.62 + else if is_assum th then
6.63 + Assum
6.64 + else
6.65 + Local
6.66 fun is_good_unnamed_local th =
6.67 not (Thm.has_name_hint th) andalso
6.68 forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Oct 29 13:15:58 2011 +0200
7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Oct 29 13:15:58 2011 +0200
7.3 @@ -659,11 +659,9 @@
7.4 arguments ctxt full_proof extra slice_timeout weights ^ " " ^
7.5 File.shell_path prob_file
7.6 val command = "TIMEFORMAT='%3R'; { time " ^ core ^ " ; } 2>&1"
7.7 - val _ =
7.8 - atp_problem
7.9 - |> tptp_lines_for_atp_problem format
7.10 - |> cons ("% " ^ command ^ "\n")
7.11 - |> File.write_list prob_file
7.12 + val _ = atp_problem |> lines_for_atp_problem format
7.13 + |> cons ("% " ^ command ^ "\n")
7.14 + |> File.write_list prob_file
7.15 val conjecture_shape =
7.16 conjecture_offset + 1
7.17 upto conjecture_offset + length hyp_ts + 1