src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
changeset 37498 b426cbdb5a23
parent 37496 9ae78e12e126
child 37500 7587b6e63454
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 22 13:17:59 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 22 14:28:22 2010 +0200
     1.3 @@ -32,19 +32,17 @@
     1.4    val conceal_skolem_somes :
     1.5      int -> (string * term) list -> term -> (string * term) list * term
     1.6    exception TRIVIAL
     1.7 -  val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list
     1.8 -  val make_axiom_clauses : bool -> theory ->
     1.9 -       (thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list
    1.10 +  val make_conjecture_clauses : theory -> thm list -> hol_clause list
    1.11 +  val make_axiom_clauses :
    1.12 +    theory -> (thm * (axiom_name * hol_clause_id)) list
    1.13 +    -> (axiom_name * hol_clause) list
    1.14    val type_wrapper_name : string
    1.15    val get_helper_clauses :
    1.16 -    bool -> theory -> bool -> bool -> hol_clause list
    1.17 -      -> (thm * (axiom_name * hol_clause_id)) list -> hol_clause list
    1.18 +    theory -> bool -> bool -> hol_clause list
    1.19 +    -> (thm * (axiom_name * hol_clause_id)) list -> hol_clause list
    1.20    val write_tptp_file : bool -> bool -> bool -> Path.T ->
    1.21      hol_clause list * hol_clause list * hol_clause list * hol_clause list *
    1.22      classrel_clause list * arity_clause list -> name_pool option * int
    1.23 -  val write_dfg_file : bool -> bool -> Path.T ->
    1.24 -    hol_clause list * hol_clause list * hol_clause list * hol_clause list *
    1.25 -    classrel_clause list * arity_clause list -> name_pool option * int
    1.26  end
    1.27  
    1.28  structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
    1.29 @@ -98,65 +96,66 @@
    1.30  
    1.31  fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
    1.32  
    1.33 -fun type_of dfg (Type (a, Ts)) =
    1.34 -    let val (folTypes,ts) = types_of dfg Ts in
    1.35 -      (TyConstr (`(make_fixed_type_const dfg) a, folTypes), ts)
    1.36 +fun type_of (Type (a, Ts)) =
    1.37 +    let val (folTypes,ts) = types_of Ts in
    1.38 +      (TyConstr (`make_fixed_type_const a, folTypes), ts)
    1.39      end
    1.40 -  | type_of _ (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
    1.41 -  | type_of _ (tp as TVar (x, _)) =
    1.42 +  | type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
    1.43 +  | type_of (tp as TVar (x, _)) =
    1.44      (TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
    1.45 -and types_of dfg Ts =
    1.46 -      let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
    1.47 -      in  (folTyps, union_all ts)  end;
    1.48 +and types_of Ts =
    1.49 +    let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
    1.50 +      (folTyps, union_all ts)
    1.51 +    end
    1.52  
    1.53  (* same as above, but no gathering of sort information *)
    1.54 -fun simp_type_of dfg (Type (a, Ts)) =
    1.55 -      TyConstr (`(make_fixed_type_const dfg) a, map (simp_type_of dfg) Ts)
    1.56 -  | simp_type_of _ (TFree (a, _)) = TyFree (`make_fixed_type_var a)
    1.57 -  | simp_type_of _ (TVar (x, _)) =
    1.58 -    TyVar (make_schematic_type_var x, string_of_indexname x);
    1.59 +fun simp_type_of (Type (a, Ts)) =
    1.60 +      TyConstr (`make_fixed_type_const a, map simp_type_of Ts)
    1.61 +  | simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a)
    1.62 +  | simp_type_of (TVar (x, _)) =
    1.63 +    TyVar (make_schematic_type_var x, string_of_indexname x)
    1.64  
    1.65  
    1.66  (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
    1.67 -fun combterm_of dfg thy (Const (c, T)) =
    1.68 +fun combterm_of thy (Const (c, T)) =
    1.69        let
    1.70 -        val (tp, ts) = type_of dfg T
    1.71 +        val (tp, ts) = type_of T
    1.72          val tvar_list =
    1.73            (if String.isPrefix skolem_theory_name c then
    1.74               [] |> Term.add_tvarsT T |> map TVar
    1.75             else
    1.76               (c, T) |> Sign.const_typargs thy)
    1.77 -          |> map (simp_type_of dfg)
    1.78 -        val c' = CombConst (`(make_fixed_const dfg) c, tp, tvar_list)
    1.79 +          |> map simp_type_of
    1.80 +        val c' = CombConst (`make_fixed_const c, tp, tvar_list)
    1.81        in  (c',ts)  end
    1.82 -  | combterm_of dfg _ (Free(v, T)) =
    1.83 -      let val (tp,ts) = type_of dfg T
    1.84 +  | combterm_of _ (Free(v, T)) =
    1.85 +      let val (tp,ts) = type_of T
    1.86            val v' = CombConst (`make_fixed_var v, tp, [])
    1.87        in  (v',ts)  end
    1.88 -  | combterm_of dfg _ (Var(v, T)) =
    1.89 -      let val (tp,ts) = type_of dfg T
    1.90 +  | combterm_of _ (Var(v, T)) =
    1.91 +      let val (tp,ts) = type_of T
    1.92            val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
    1.93        in  (v',ts)  end
    1.94 -  | combterm_of dfg thy (P $ Q) =
    1.95 -      let val (P',tsP) = combterm_of dfg thy P
    1.96 -          val (Q',tsQ) = combterm_of dfg thy Q
    1.97 -      in  (CombApp(P',Q'), union (op =) tsP tsQ)  end
    1.98 -  | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL clause", t);
    1.99 -
   1.100 -fun predicate_of dfg thy ((@{const Not} $ P), polarity) = predicate_of dfg thy (P, not polarity)
   1.101 -  | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity);
   1.102 +  | combterm_of thy (P $ Q) =
   1.103 +      let val (P', tsP) = combterm_of thy P
   1.104 +          val (Q', tsQ) = combterm_of thy Q
   1.105 +      in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
   1.106 +  | combterm_of _ (t as Abs _) = raise CLAUSE ("HOL clause", t)
   1.107  
   1.108 -fun literals_of_term1 dfg thy args (@{const Trueprop} $ P) = literals_of_term1 dfg thy args P
   1.109 -  | literals_of_term1 dfg thy args (@{const "op |"} $ P $ Q) =
   1.110 -      literals_of_term1 dfg thy (literals_of_term1 dfg thy args P) Q
   1.111 -  | literals_of_term1 dfg thy (lits,ts) P =
   1.112 -      let val ((pred,ts'),pol) = predicate_of dfg thy (P,true)
   1.113 -      in
   1.114 -          (Literal(pol,pred)::lits, union (op =) ts ts')
   1.115 -      end;
   1.116 +fun predicate_of thy ((@{const Not} $ P), polarity) =
   1.117 +    predicate_of thy (P, not polarity)
   1.118 +  | predicate_of thy (t, polarity) =
   1.119 +    (combterm_of thy (Envir.eta_contract t), polarity)
   1.120  
   1.121 -fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
   1.122 -val literals_of_term = literals_of_term_dfg false;
   1.123 +fun literals_of_term1 args thy (@{const Trueprop} $ P) =
   1.124 +    literals_of_term1 args thy P
   1.125 +  | literals_of_term1 args thy (@{const "op |"} $ P $ Q) =
   1.126 +    literals_of_term1 (literals_of_term1 args thy P) thy Q
   1.127 +  | literals_of_term1 (lits, ts) thy P =
   1.128 +    let val ((pred, ts'), pol) = predicate_of thy (P, true) in
   1.129 +      (Literal (pol, pred) :: lits, union (op =) ts ts')
   1.130 +    end
   1.131 +val literals_of_term = literals_of_term1 ([], [])
   1.132  
   1.133  fun skolem_name i j num_T_args =
   1.134    skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
   1.135 @@ -199,11 +198,11 @@
   1.136  exception TRIVIAL;
   1.137  
   1.138  (* making axiom and conjecture clauses *)
   1.139 -fun make_clause dfg thy (clause_id, axiom_name, kind, th) skolem_somes =
   1.140 +fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes =
   1.141    let
   1.142      val (skolem_somes, t) =
   1.143        th |> prop_of |> conceal_skolem_somes clause_id skolem_somes
   1.144 -    val (lits, ctypes_sorts) = literals_of_term_dfg dfg thy t
   1.145 +    val (lits, ctypes_sorts) = literals_of_term thy t
   1.146    in
   1.147      if forall isFalse lits then
   1.148        raise TRIVIAL
   1.149 @@ -213,29 +212,26 @@
   1.150                    kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
   1.151    end
   1.152  
   1.153 -fun add_axiom_clause dfg thy (th, (name, id)) (skolem_somes, clss) =
   1.154 +fun add_axiom_clause thy (th, (name, id)) (skolem_somes, clss) =
   1.155    let
   1.156 -    val (skolem_somes, cls) =
   1.157 -      make_clause dfg thy (id, name, Axiom, th) skolem_somes
   1.158 +    val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes
   1.159    in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
   1.160  
   1.161 -fun make_axiom_clauses dfg thy clauses =
   1.162 -  ([], []) |> fold (add_axiom_clause dfg thy) clauses |> snd
   1.163 +fun make_axiom_clauses thy clauses =
   1.164 +  ([], []) |> fold (add_axiom_clause thy) clauses |> snd
   1.165  
   1.166 -fun make_conjecture_clauses dfg thy =
   1.167 +fun make_conjecture_clauses thy =
   1.168    let
   1.169      fun aux _ _ [] = []
   1.170        | aux n skolem_somes (th :: ths) =
   1.171          let
   1.172            val (skolem_somes, cls) =
   1.173 -            make_clause dfg thy (n, "conjecture", Conjecture, th) skolem_somes
   1.174 +            make_clause thy (n, "conjecture", Conjecture, th) skolem_somes
   1.175          in cls :: aux (n + 1) skolem_somes ths end
   1.176    in aux 0 [] end
   1.177  
   1.178  (**********************************************************************)
   1.179 -(* convert clause into ATP specific formats:                          *)
   1.180 -(* TPTP used by Vampire and E                                         *)
   1.181 -(* DFG used by SPASS                                                  *)
   1.182 +(* convert clause into TPTP format                                    *)
   1.183  (**********************************************************************)
   1.184  
   1.185  (*Result of a function type; no need to check that the argument type matches.*)
   1.186 @@ -315,17 +311,11 @@
   1.187    string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single
   1.188  
   1.189  fun string_of_predicate (params as (_, explicit_apply, _, cnh)) t =
   1.190 -  case t of
   1.191 -    (CombApp (CombApp (CombConst (("equal", _), _, _), t1), t2)) =>
   1.192 -    (* DFG only: new TPTP prefers infix equality *)
   1.193 -    pool_map (string_of_combterm params) [t1, t2]
   1.194 -    #>> prefix "equal" o paren_pack
   1.195 -  | _ =>
   1.196 -    case #1 (strip_combterm_comb t) of
   1.197 -      CombConst ((s, _), _, _) =>
   1.198 -      (if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm)
   1.199 -          params t
   1.200 -    | _ => boolify params t
   1.201 +  case #1 (strip_combterm_comb t) of
   1.202 +    CombConst ((s, _), _, _) =>
   1.203 +    (if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm)
   1.204 +        params t
   1.205 +  | _ => boolify params t
   1.206  
   1.207  
   1.208  (*** TPTP format ***)
   1.209 @@ -353,7 +343,7 @@
   1.210  
   1.211  fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
   1.212                  pool =
   1.213 -let
   1.214 +  let
   1.215      val ((lits, tylits), pool) =
   1.216        tptp_type_literals params (kind = Conjecture) cls pool
   1.217    in
   1.218 @@ -361,94 +351,6 @@
   1.219    end
   1.220  
   1.221  
   1.222 -(*** DFG format ***)
   1.223 -
   1.224 -fun dfg_literal params (Literal (pos, pred)) =
   1.225 -  string_of_predicate params pred #>> dfg_sign pos
   1.226 -
   1.227 -fun dfg_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) =
   1.228 -  pool_map (dfg_literal params) literals
   1.229 -  #>> rpair (map (dfg_of_type_literal pos)
   1.230 -                 (type_literals_for_types ctypes_sorts))
   1.231 -
   1.232 -fun get_uvars (CombConst _) vars pool = (vars, pool)
   1.233 -  | get_uvars (CombVar (name, _)) vars pool =
   1.234 -    nice_name name pool |>> (fn var => var :: vars)
   1.235 -  | get_uvars (CombApp (P, Q)) vars pool =
   1.236 -    let val (vars, pool) = get_uvars P vars pool in get_uvars Q vars pool end
   1.237 -
   1.238 -fun get_uvars_l (Literal (_, c)) = get_uvars c [];
   1.239 -
   1.240 -fun dfg_vars (HOLClause {literals, ...}) =
   1.241 -  pool_map get_uvars_l literals #>> union_all
   1.242 -
   1.243 -fun dfg_clause params (cls as HOLClause {axiom_name, clause_id, kind,
   1.244 -                                         ctypes_sorts, ...}) pool =
   1.245 -  let
   1.246 -    val ((lits, tylits), pool) =
   1.247 -      dfg_type_literals params (kind = Conjecture) cls pool
   1.248 -    val (vars, pool) = dfg_vars cls pool
   1.249 -    val tvars = get_tvar_strs ctypes_sorts
   1.250 -  in
   1.251 -    ((gen_dfg_cls (clause_id, axiom_name, kind, lits, tylits, tvars @ vars),
   1.252 -      tylits), pool)
   1.253 -  end
   1.254 -
   1.255 -
   1.256 -(** For DFG format: accumulate function and predicate declarations **)
   1.257 -
   1.258 -fun add_types tvars = fold add_fol_type_funcs tvars
   1.259 -
   1.260 -fun add_decls (full_types, explicit_apply, cma, cnh)
   1.261 -              (CombConst ((c, _), ctp, tvars)) (funcs, preds) =
   1.262 -      (if c = "equal" then
   1.263 -         (add_types tvars funcs, preds)
   1.264 -       else
   1.265 -         let val arity = min_arity_of cma c
   1.266 -             val ntys = if not full_types then length tvars else 0
   1.267 -             val addit = Symtab.update(c, arity + ntys)
   1.268 -         in
   1.269 -             if needs_hBOOL explicit_apply cnh c then
   1.270 -               (add_types tvars (addit funcs), preds)
   1.271 -             else
   1.272 -               (add_types tvars funcs, addit preds)
   1.273 -         end) |>> full_types ? add_fol_type_funcs ctp
   1.274 -  | add_decls _ (CombVar (_, ctp)) (funcs, preds) =
   1.275 -      (add_fol_type_funcs ctp funcs, preds)
   1.276 -  | add_decls params (CombApp (P, Q)) decls =
   1.277 -      decls |> add_decls params P |> add_decls params Q
   1.278 -
   1.279 -fun add_literal_decls params (Literal (_, c)) = add_decls params c
   1.280 -
   1.281 -fun add_clause_decls params (HOLClause {literals, ...}) decls =
   1.282 -    fold (add_literal_decls params) literals decls
   1.283 -    handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
   1.284 -
   1.285 -fun decls_of_clauses (params as (full_types, explicit_apply, _, _)) clauses
   1.286 -                     arity_clauses =
   1.287 -  let
   1.288 -    val functab =
   1.289 -      init_functab
   1.290 -      |> fold Symtab.update [(type_wrapper_name, 2), ("hAPP", 2),
   1.291 -                             ("tc_bool", 0)]
   1.292 -      val predtab = Symtab.empty |> Symtab.update ("hBOOL", 1)
   1.293 -      val (functab, predtab) =
   1.294 -        (functab, predtab) |> fold (add_clause_decls params) clauses
   1.295 -                           |>> fold add_arity_clause_funcs arity_clauses
   1.296 -  in (Symtab.dest functab, Symtab.dest predtab) end
   1.297 -
   1.298 -fun add_clause_preds (HOLClause {ctypes_sorts, ...}) preds =
   1.299 -  fold add_type_sort_preds ctypes_sorts preds
   1.300 -  handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities")
   1.301 -
   1.302 -(*Higher-order clauses have only the predicates hBOOL and type classes.*)
   1.303 -fun preds_of_clauses clauses clsrel_clauses arity_clauses =
   1.304 -  Symtab.empty
   1.305 -  |> fold add_clause_preds clauses
   1.306 -  |> fold add_arity_clause_preds arity_clauses
   1.307 -  |> fold add_classrel_clause_preds clsrel_clauses
   1.308 -  |> Symtab.dest
   1.309 -
   1.310  (**********************************************************************)
   1.311  (* write clauses to files                                             *)
   1.312  (**********************************************************************)
   1.313 @@ -480,9 +382,9 @@
   1.314    Symtab.make (maps (maps (map (rpair 0) o fst))
   1.315                      [optional_helpers, optional_typed_helpers])
   1.316  
   1.317 -fun get_helper_clauses dfg thy is_FO full_types conjectures axcls =
   1.318 +fun get_helper_clauses thy is_FO full_types conjectures axcls =
   1.319    let
   1.320 -    val axclauses = map snd (make_axiom_clauses dfg thy axcls)
   1.321 +    val axclauses = map snd (make_axiom_clauses thy axcls)
   1.322      val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
   1.323      fun is_needed c = the (Symtab.lookup ct c) > 0
   1.324      val cnfs =
   1.325 @@ -492,7 +394,7 @@
   1.326                     if exists is_needed ss then cnf_helper_thms thy raw ths
   1.327                     else []))
   1.328        @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
   1.329 -  in map snd (make_axiom_clauses dfg thy cnfs) end
   1.330 +  in map snd (make_axiom_clauses thy cnfs) end
   1.331  
   1.332  (*Find the minimal arity of each function mentioned in the term. Also, note which uses
   1.333    are not at top level, to see if hBOOL is needed.*)
   1.334 @@ -521,7 +423,7 @@
   1.335                             (const_min_arity, const_needs_hBOOL) =
   1.336    fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
   1.337  
   1.338 -fun display_arity explicit_apply const_needs_hBOOL (c,n) =
   1.339 +fun display_arity explicit_apply const_needs_hBOOL (c, n) =
   1.340    trace_msg (fn () => "Constant: " ^ c ^
   1.341                  " arity:\t" ^ Int.toString n ^
   1.342                  (if needs_hBOOL explicit_apply const_needs_hBOOL c then
   1.343 @@ -541,10 +443,6 @@
   1.344       in (const_min_arity, const_needs_hBOOL) end
   1.345    else (Symtab.empty, Symtab.empty);
   1.346  
   1.347 -fun header () =
   1.348 -  "% This file was generated by Isabelle (most likely Sledgehammer)\n" ^
   1.349 -  "% " ^ timestamp () ^ "\n"
   1.350 -
   1.351  (* TPTP format *)
   1.352  
   1.353  fun write_tptp_file readable_names full_types explicit_apply file clauses =
   1.354 @@ -572,7 +470,8 @@
   1.355        + length helper_clss
   1.356      val _ =
   1.357        File.write_list file
   1.358 -          (header () ::
   1.359 +          ("% This file was generated by Isabelle (most likely Sledgehammer)\n\
   1.360 +           \% " ^ timestamp () ^ "\n" ::
   1.361             section "Relevant fact" ax_clss @
   1.362             section "Class relationship" classrel_clss @
   1.363             section "Arity declaration" arity_clss @
   1.364 @@ -581,53 +480,4 @@
   1.365             section "Type variable" tfree_clss)
   1.366    in (pool, conjecture_offset) end
   1.367  
   1.368 -(* DFG format *)
   1.369 -
   1.370 -fun dfg_tfree_predicate s = (first_field "(" s |> the |> fst, 1)
   1.371 -
   1.372 -fun write_dfg_file full_types explicit_apply file clauses =
   1.373 -  let
   1.374 -    (* Some of the helper functions below are not name-pool-aware. However,
   1.375 -       there's no point in adding name pool support if the DFG format is on its
   1.376 -       way out anyway. *)
   1.377 -    val pool = NONE
   1.378 -    val (conjectures, axclauses, _, helper_clauses,
   1.379 -      classrel_clauses, arity_clauses) = clauses
   1.380 -    val (cma, cnh) = count_constants explicit_apply clauses
   1.381 -    val params = (full_types, explicit_apply, cma, cnh)
   1.382 -    val ((conjecture_clss, tfree_litss), pool) =
   1.383 -      pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip
   1.384 -    val tfree_lits = union_all tfree_litss
   1.385 -    val problem_name = Path.implode (Path.base file)
   1.386 -    val (axstrs, pool) = pool_map (apfst fst oo dfg_clause params) axclauses pool
   1.387 -    val tfree_clss = map dfg_tfree_clause tfree_lits
   1.388 -    val tfree_preds = map dfg_tfree_predicate tfree_lits
   1.389 -    val (helper_clauses_strs, pool) =
   1.390 -      pool_map (apfst fst oo dfg_clause params) helper_clauses pool
   1.391 -    val (funcs, cl_preds) =
   1.392 -      decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
   1.393 -    val ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
   1.394 -    val preds = tfree_preds @ cl_preds @ ty_preds
   1.395 -    val conjecture_offset =
   1.396 -      length axclauses + length classrel_clauses + length arity_clauses
   1.397 -      + length helper_clauses
   1.398 -    val _ =
   1.399 -      File.write_list file
   1.400 -          (header () ::
   1.401 -           string_of_start problem_name ::
   1.402 -           string_of_descrip problem_name ::
   1.403 -           string_of_symbols (string_of_funcs funcs)
   1.404 -                             (string_of_preds preds) ::
   1.405 -           "list_of_clauses(axioms, cnf).\n" ::
   1.406 -           axstrs @
   1.407 -           map dfg_classrel_clause classrel_clauses @
   1.408 -           map dfg_arity_clause arity_clauses @
   1.409 -           helper_clauses_strs @
   1.410 -           ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @
   1.411 -           conjecture_clss @
   1.412 -           tfree_clss @
   1.413 -           ["end_of_list.\n\n",
   1.414 -            "end_problem.\n"])
   1.415 -  in (pool, conjecture_offset) end
   1.416 -
   1.417  end;