src/HOL/Tools/ATP_Manager/atp_systems.ML
author blanchet
Tue Jul 27 17:43:11 2010 +0200 (2010-07-27)
changeset 38019 e207a64e1e0b
parent 38017 3ad3e3ca2451
child 38021 e024504943d1
permissions -rw-r--r--
complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
     1 (*  Title:      HOL/Tools/ATP_Manager/atp_systems.ML
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 Setup for supported ATPs.
     6 *)
     7 
     8 signature ATP_SYSTEMS =
     9 sig
    10   val trace : bool Unsynchronized.ref
    11   val dest_dir : string Config.T
    12   val problem_prefix : string Config.T
    13   val measure_runtime : bool Config.T
    14   val refresh_systems_on_tptp : unit -> unit
    15   val default_atps_param_value : unit -> string
    16   val setup : theory -> theory
    17 end;
    18 
    19 structure ATP_Systems : ATP_SYSTEMS =
    20 struct
    21 
    22 open Metis_Clauses
    23 open Sledgehammer_Util
    24 open Sledgehammer_Fact_Filter
    25 open ATP_Problem
    26 open Sledgehammer_Proof_Reconstruct
    27 open ATP_Manager
    28 
    29 val trace = Unsynchronized.ref false
    30 fun trace_msg msg = if !trace then tracing (msg ()) else ()
    31 
    32 (** generic ATP **)
    33 
    34 (* external problem files *)
    35 
    36 val (dest_dir, dest_dir_setup) = Attrib.config_string "atp_dest_dir" (K "");
    37   (*Empty string means create files in Isabelle's temporary files directory.*)
    38 
    39 val (problem_prefix, problem_prefix_setup) =
    40   Attrib.config_string "atp_problem_prefix" (K "prob");
    41 
    42 val (measure_runtime, measure_runtime_setup) =
    43   Attrib.config_bool "atp_measure_runtime" (K false);
    44 
    45 
    46 (* prover configuration *)
    47 
    48 type prover_config =
    49   {home_var: string,
    50    executable: string,
    51    arguments: bool -> Time.time -> string,
    52    proof_delims: (string * string) list,
    53    known_failures: (failure * string) list,
    54    max_new_relevant_facts_per_iter: int,
    55    prefers_theory_relevant: bool,
    56    explicit_forall: bool}
    57 
    58 
    59 (* basic template *)
    60 
    61 val remotify = prefix "remote_"
    62 
    63 fun with_path cleanup after f path =
    64   Exn.capture f path
    65   |> tap (fn _ => cleanup path)
    66   |> Exn.release
    67   |> tap (after path)
    68 
    69 (* Splits by the first possible of a list of delimiters. *)
    70 fun extract_proof delims output =
    71   case pairself (find_first (fn s => String.isSubstring s output))
    72                 (ListPair.unzip delims) of
    73     (SOME begin_delim, SOME end_delim) =>
    74     (output |> first_field begin_delim |> the |> snd
    75             |> first_field end_delim |> the |> fst
    76             |> first_field "\n" |> the |> snd
    77      handle Option.Option => "")
    78   | _ => ""
    79 
    80 fun extract_proof_and_outcome complete res_code proof_delims known_failures
    81                               output =
    82   case map_filter (fn (failure, pattern) =>
    83                       if String.isSubstring pattern output then SOME failure
    84                       else NONE) known_failures of
    85     [] => (case extract_proof proof_delims output of
    86              "" => ("", SOME UnknownError)
    87            | proof => if res_code = 0 then (proof, NONE)
    88                       else ("", SOME UnknownError))
    89   | (failure :: _) =>
    90     ("", SOME (if failure = IncompleteUnprovable andalso complete then
    91                  Unprovable
    92                else
    93                  failure))
    94 
    95 fun string_for_failure Unprovable = "The ATP problem is unprovable."
    96   | string_for_failure IncompleteUnprovable =
    97     "The ATP cannot prove the problem."
    98   | string_for_failure CantConnect = "Can't connect to remote ATP."
    99   | string_for_failure TimedOut = "Timed out."
   100   | string_for_failure OutOfResources = "The ATP ran out of resources."
   101   | string_for_failure OldSpass =
   102     (* FIXME: Change the error message below to point to the Isabelle download
   103        page once the package is there. *)
   104     "Warning: Sledgehammer requires a more recent version of SPASS with \
   105     \support for the TPTP syntax. To install it, download and untar the \
   106     \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \
   107     \\"spass-3.7\" directory's full path to \"" ^
   108     Path.implode (Path.expand (Path.appends
   109         (Path.variable "ISABELLE_HOME_USER" ::
   110          map Path.basic ["etc", "components"]))) ^
   111     "\" on a line of its own."
   112   | string_for_failure MalformedInput =
   113     "Internal Sledgehammer error: The ATP problem is malformed. Please report \
   114     \this to the Isabelle developers."
   115   | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
   116   | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
   117 
   118 
   119 (* Clause preparation *)
   120 
   121 datatype fol_formula =
   122   FOLFormula of {formula_name: string,
   123                  kind: kind,
   124                  combformula: (name, combterm) formula,
   125                  ctypes_sorts: typ list}
   126 
   127 fun mk_anot phi = AConn (ANot, [phi])
   128 fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
   129 fun mk_ahorn [] phi = phi
   130   | mk_ahorn (phi :: phis) psi =
   131     AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
   132 
   133 (* ### FIXME: reintroduce
   134 fun make_clause_table xs =
   135   fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty
   136 (* Remove existing axiom clauses from the conjecture clauses, as this can
   137    dramatically boost an ATP's performance (for some reason). *)
   138 fun subtract_cls ax_clauses =
   139   filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
   140 *)
   141 
   142 fun combformula_for_prop thy =
   143   let
   144     val do_term = combterm_from_term thy
   145     fun do_quant bs q s T t' =
   146       do_formula ((s, T) :: bs) t'
   147       #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
   148     and do_conn bs c t1 t2 =
   149       do_formula bs t1 ##>> do_formula bs t2
   150       #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
   151     and do_formula bs t =
   152       case t of
   153         @{const Not} $ t1 =>
   154         do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
   155       | Const (@{const_name All}, _) $ Abs (s, T, t') =>
   156         do_quant bs AForall s T t'
   157       | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
   158         do_quant bs AExists s T t'
   159       | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
   160       | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
   161       | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2
   162       | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
   163         do_conn bs AIff t1 t2
   164       | _ => (fn ts => do_term bs (Envir.eta_contract t)
   165                        |>> APred ||> union (op =) ts)
   166   in do_formula [] end
   167 
   168 (* Converts an elim-rule into an equivalent theorem that does not have the
   169    predicate variable. Leaves other theorems unchanged. We simply instantiate
   170    the conclusion variable to False. (Cf. "transform_elim_term" in
   171    "ATP_Systems".) *)
   172 (* FIXME: test! *)
   173 fun transform_elim_term t =
   174   case Logic.strip_imp_concl t of
   175     @{const Trueprop} $ Var (z, @{typ bool}) =>
   176     subst_Vars [(z, @{const True})] t
   177   | Var (z, @{typ prop}) => subst_Vars [(z, @{prop True})] t
   178   | _ => t
   179 
   180 (* Removes the lambdas from an equation of the form "t = (%x. u)".
   181    (Cf. "extensionalize_theorem" in "Clausifier".) *)
   182 fun extensionalize_term t =
   183   let
   184     fun aux j (Const (@{const_name "op ="}, Type (_, [Type (_, [_, T']), _]))
   185                $ t2 $ Abs (s, var_T, t')) =
   186         let val var_t = Var (("x", j), var_T) in
   187           Const (@{const_name "op ="}, T' --> T' --> HOLogic.boolT)
   188             $ betapply (t2, var_t) $ subst_bound (var_t, t')
   189           |> aux (j + 1)
   190         end
   191       | aux _ t = t
   192   in aux (maxidx_of_term t + 1) t end
   193 
   194 (* FIXME: Guarantee freshness *)
   195 fun concealed_bound_name j = "Sledgehammer" ^ Int.toString j
   196 fun conceal_bounds Ts t =
   197   subst_bounds (map (Free o apfst concealed_bound_name)
   198                     (length Ts - 1 downto 0 ~~ rev Ts), t)
   199 fun reveal_bounds Ts =
   200   subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
   201                     (0 upto length Ts - 1 ~~ Ts))
   202 
   203 fun introduce_combinators_in_term ctxt kind t =
   204   let
   205     val thy = ProofContext.theory_of ctxt
   206     fun aux Ts t =
   207       case t of
   208         @{const Not} $ t1 => @{const Not} $ aux Ts t1
   209       | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
   210         t0 $ Abs (s, T, aux (T :: Ts) t')
   211       | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
   212         t0 $ Abs (s, T, aux (T :: Ts) t')
   213       | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   214       | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   215       | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   216       | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
   217           $ t1 $ t2 =>
   218         t0 $ aux Ts t1 $ aux Ts t2
   219       | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
   220                t
   221              else
   222                let
   223                  val t = t |> conceal_bounds Ts
   224                            |> Envir.eta_contract
   225                  val ([t], ctxt') = Variable.import_terms true [t] ctxt
   226                in
   227                  t |> cterm_of thy
   228                    |> Clausifier.introduce_combinators_in_cterm
   229                    |> singleton (Variable.export ctxt' ctxt)
   230                    |> prop_of |> Logic.dest_equals |> snd
   231                    |> reveal_bounds Ts
   232                end
   233   in t |> not (Meson.is_fol_term thy t) ? aux [] end
   234   handle THM _ =>
   235          (* A type variable of sort "{}" will make abstraction fail. *)
   236          case kind of
   237            Axiom => HOLogic.true_const
   238          | Conjecture => HOLogic.false_const
   239 
   240 (* making axiom and conjecture clauses *)
   241 fun make_clause ctxt (formula_name, kind, t) =
   242   let
   243     val thy = ProofContext.theory_of ctxt
   244     (* ### FIXME: perform other transformations previously done by
   245        "Clausifier.to_nnf", e.g. "HOL.If" *)
   246     val t = t |> transform_elim_term
   247               |> Object_Logic.atomize_term thy
   248               |> extensionalize_term
   249               |> introduce_combinators_in_term ctxt kind
   250     val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   251   in
   252     FOLFormula {formula_name = formula_name, combformula = combformula,
   253                 kind = kind, ctypes_sorts = ctypes_sorts}
   254   end
   255 
   256 fun make_axiom_clause ctxt (name, th) =
   257   (name, make_clause ctxt (name, Axiom, prop_of th))
   258 fun make_conjecture_clauses ctxt ts =
   259   map2 (fn j => fn t => make_clause ctxt (Int.toString j, Conjecture, t))
   260        (0 upto length ts - 1) ts
   261 
   262 (** Helper clauses **)
   263 
   264 fun count_combterm (CombConst ((s, _), _, _)) =
   265     Symtab.map_entry s (Integer.add 1)
   266   | count_combterm (CombVar _) = I
   267   | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
   268 fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
   269   | count_combformula (AConn (_, phis)) = fold count_combformula phis
   270   | count_combformula (APred tm) = count_combterm tm
   271 fun count_fol_formula (FOLFormula {combformula, ...}) =
   272   count_combformula combformula
   273 
   274 val optional_helpers =
   275   [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}),
   276    (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),
   277    (["c_COMBS"], @{thms COMBS_def})]
   278 val optional_typed_helpers =
   279   [(["c_True", "c_False"], @{thms True_or_False}),
   280    (["c_If"], @{thms if_True if_False True_or_False})]
   281 val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
   282 
   283 val init_counters =
   284   Symtab.make (maps (maps (map (rpair 0) o fst))
   285                     [optional_helpers, optional_typed_helpers])
   286 
   287 fun get_helper_clauses ctxt is_FO full_types conjectures axclauses =
   288   let
   289     val ct = fold (fold count_fol_formula) [conjectures, axclauses]
   290                   init_counters
   291     fun is_needed c = the (Symtab.lookup ct c) > 0
   292     val cnfs =
   293       (optional_helpers
   294        |> full_types ? append optional_typed_helpers
   295        |> maps (fn (ss, ths) =>
   296                    if exists is_needed ss then map (`Thm.get_name_hint) ths
   297                    else [])) @
   298       (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
   299   in map (snd o make_axiom_clause ctxt) cnfs end
   300 
   301 fun s_not (@{const Not} $ t) = t
   302   | s_not t = @{const Not} $ t
   303 
   304 (* prepare for passing to writer,
   305    create additional clauses based on the information from extra_cls *)
   306 fun prepare_clauses ctxt full_types hyp_ts concl_t axcls extra_cls =
   307   let
   308     val thy = ProofContext.theory_of ctxt
   309     val goal_t = Logic.list_implies (hyp_ts, concl_t)
   310     val is_FO = Meson.is_fol_term thy goal_t
   311     val _ = trace_msg (fn _ => Syntax.string_of_term ctxt goal_t)
   312     val axtms = map (prop_of o snd) extra_cls
   313     val subs = tfree_classes_of_terms [goal_t]
   314     val supers = tvar_classes_of_terms axtms
   315     val tycons = type_consts_of_terms thy (goal_t :: axtms)
   316     (* TFrees in conjecture clauses; TVars in axiom clauses *)
   317     val conjectures =
   318       map (s_not o HOLogic.dest_Trueprop) hyp_ts @
   319         [HOLogic.dest_Trueprop concl_t]
   320       |> make_conjecture_clauses ctxt
   321     val extra_clauses = map (snd o make_axiom_clause ctxt) extra_cls
   322     val (clnames, axiom_clauses) =
   323       ListPair.unzip (map (make_axiom_clause ctxt) axcls)
   324     (* FIXME: Should it read "extra_clauses" or "axiom_clauses" in the
   325        "get_helper_clauses" call? *)
   326     val helper_clauses =
   327       get_helper_clauses ctxt is_FO full_types conjectures extra_clauses
   328     val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   329     val class_rel_clauses = make_class_rel_clauses thy subs supers'
   330   in
   331     (Vector.fromList clnames,
   332       (conjectures, axiom_clauses, extra_clauses, helper_clauses,
   333        class_rel_clauses, arity_clauses))
   334   end
   335 
   336 val axiom_prefix = "ax_"
   337 val conjecture_prefix = "conj_"
   338 val arity_clause_prefix = "clsarity_"
   339 val tfrees_name = "tfrees"
   340 
   341 fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
   342 
   343 fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
   344   | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
   345   | fo_term_for_combtyp (CombType (name, tys)) =
   346     ATerm (name, map fo_term_for_combtyp tys)
   347 
   348 fun fo_literal_for_type_literal (TyLitVar (class, name)) =
   349     (true, ATerm (class, [ATerm (name, [])]))
   350   | fo_literal_for_type_literal (TyLitFree (class, name)) =
   351     (true, ATerm (class, [ATerm (name, [])]))
   352 
   353 fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot
   354 
   355 fun fo_term_for_combterm full_types =
   356   let
   357     fun aux top_level u =
   358       let
   359         val (head, args) = strip_combterm_comb u
   360         val (x, ty_args) =
   361           case head of
   362             CombConst (name, _, ty_args) =>
   363             if fst name = "equal" then
   364               (if top_level andalso length args = 2 then name
   365                else ("c_fequal", @{const_name fequal}), [])
   366             else
   367               (name, if full_types then [] else ty_args)
   368           | CombVar (name, _) => (name, [])
   369           | CombApp _ => raise Fail "impossible \"CombApp\""
   370         val t = ATerm (x, map fo_term_for_combtyp ty_args @
   371                           map (aux false) args)
   372     in
   373       if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
   374     end
   375   in aux true end
   376 
   377 fun formula_for_combformula full_types =
   378   let
   379     fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   380       | aux (AConn (c, phis)) = AConn (c, map aux phis)
   381       | aux (APred tm) = APred (fo_term_for_combterm full_types tm)
   382   in aux end
   383 
   384 fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
   385   mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
   386                 (type_literals_for_types ctypes_sorts))
   387            (formula_for_combformula full_types combformula)
   388 
   389 fun problem_line_for_axiom full_types
   390         (formula as FOLFormula {formula_name, kind, ...}) =
   391   Fof (axiom_prefix ^ ascii_of formula_name, kind,
   392        formula_for_axiom full_types formula)
   393 
   394 fun problem_line_for_class_rel_clause
   395         (ClassRelClause {axiom_name, subclass, superclass, ...}) =
   396   let val ty_arg = ATerm (("T", "T"), []) in
   397     Fof (ascii_of axiom_name, Axiom,
   398          AConn (AImplies, [APred (ATerm (subclass, [ty_arg])),
   399                            APred (ATerm (superclass, [ty_arg]))]))
   400   end
   401 
   402 fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
   403     (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
   404   | fo_literal_for_arity_literal (TVarLit (c, sort)) =
   405     (false, ATerm (c, [ATerm (sort, [])]))
   406 
   407 fun problem_line_for_arity_clause
   408         (ArityClause {axiom_name, conclLit, premLits, ...}) =
   409   Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
   410        mk_ahorn (map (formula_for_fo_literal o apfst not
   411                       o fo_literal_for_arity_literal) premLits)
   412                 (formula_for_fo_literal
   413                      (fo_literal_for_arity_literal conclLit)))
   414 
   415 fun problem_line_for_conjecture full_types
   416         (FOLFormula {formula_name, kind, combformula, ...}) =
   417   Fof (conjecture_prefix ^ formula_name, kind,
   418        formula_for_combformula full_types combformula)
   419 
   420 fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
   421   map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
   422 
   423 fun problem_line_for_free_type lit =
   424   Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit))
   425 fun problem_lines_for_free_types conjectures =
   426   let
   427     val litss = map free_type_literals_for_conjecture conjectures
   428     val lits = fold (union (op =)) litss []
   429   in map problem_line_for_free_type lits end
   430 
   431 (** "hBOOL" and "hAPP" **)
   432 
   433 type const_info = {min_arity: int, max_arity: int, sub_level: bool}
   434 
   435 fun consider_term top_level (ATerm ((s, _), ts)) =
   436   (if is_tptp_variable s then
   437      I
   438    else
   439      let val n = length ts in
   440        Symtab.map_default
   441            (s, {min_arity = n, max_arity = 0, sub_level = false})
   442            (fn {min_arity, max_arity, sub_level} =>
   443                {min_arity = Int.min (n, min_arity),
   444                 max_arity = Int.max (n, max_arity),
   445                 sub_level = sub_level orelse not top_level})
   446      end)
   447   #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
   448 fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
   449   | consider_formula (AConn (_, phis)) = fold consider_formula phis
   450   | consider_formula (APred tm) = consider_term true tm
   451 
   452 fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
   453 fun consider_problem problem = fold (fold consider_problem_line o snd) problem
   454 
   455 fun const_table_for_problem explicit_apply problem =
   456   if explicit_apply then NONE
   457   else SOME (Symtab.empty |> consider_problem problem)
   458 
   459 val tc_fun = make_fixed_type_const @{type_name fun}
   460 
   461 fun min_arity_of thy full_types NONE s =
   462     (if s = "equal" orelse s = type_wrapper_name orelse
   463         String.isPrefix type_const_prefix s orelse
   464         String.isPrefix class_prefix s then
   465        16383 (* large number *)
   466      else if full_types then
   467        0
   468      else case strip_prefix_and_undo_ascii const_prefix s of
   469        SOME s' => num_type_args thy (invert_const s')
   470      | NONE => 0)
   471   | min_arity_of _ _ (SOME the_const_tab) s =
   472     case Symtab.lookup the_const_tab s of
   473       SOME ({min_arity, ...} : const_info) => min_arity
   474     | NONE => 0
   475 
   476 fun full_type_of (ATerm ((s, _), [ty, _])) =
   477     if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
   478   | full_type_of _ = raise Fail "expected type wrapper"
   479 
   480 fun list_hAPP_rev _ t1 [] = t1
   481   | list_hAPP_rev NONE t1 (t2 :: ts2) =
   482     ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
   483   | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
   484     let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
   485                          [full_type_of t2, ty]) in
   486       ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
   487     end
   488 
   489 fun repair_applications_in_term thy full_types const_tab =
   490   let
   491     fun aux opt_ty (ATerm (name as (s, _), ts)) =
   492       if s = type_wrapper_name then
   493         case ts of
   494           [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
   495         | _ => raise Fail "malformed type wrapper"
   496       else
   497         let
   498           val ts = map (aux NONE) ts
   499           val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
   500         in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
   501   in aux NONE end
   502 
   503 fun boolify t = ATerm (`I "hBOOL", [t])
   504 
   505 (* True if the constant ever appears outside of the top-level position in
   506    literals, or if it appears with different arities (e.g., because of different
   507    type instantiations). If false, the constant always receives all of its
   508    arguments and is used as a predicate. *)
   509 fun is_predicate NONE s =
   510     s = "equal" orelse String.isPrefix type_const_prefix s orelse
   511     String.isPrefix class_prefix s
   512   | is_predicate (SOME the_const_tab) s =
   513     case Symtab.lookup the_const_tab s of
   514       SOME {min_arity, max_arity, sub_level} =>
   515       not sub_level andalso min_arity = max_arity
   516     | NONE => false
   517 
   518 fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
   519   if s = type_wrapper_name then
   520     case ts of
   521       [_, t' as ATerm ((s', _), _)] =>
   522       if is_predicate const_tab s' then t' else boolify t
   523     | _ => raise Fail "malformed type wrapper"
   524   else
   525     t |> not (is_predicate const_tab s) ? boolify
   526 
   527 fun close_universally phi =
   528   let
   529     fun term_vars bounds (ATerm (name as (s, _), tms)) =
   530         (is_tptp_variable s andalso not (member (op =) bounds name))
   531           ? insert (op =) name
   532         #> fold (term_vars bounds) tms
   533     fun formula_vars bounds (AQuant (q, xs, phi)) =
   534         formula_vars (xs @ bounds) phi
   535       | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
   536       | formula_vars bounds (APred tm) = term_vars bounds tm
   537   in
   538     case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
   539   end
   540 
   541 fun repair_formula thy explicit_forall full_types const_tab =
   542   let
   543     fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   544       | aux (AConn (c, phis)) = AConn (c, map aux phis)
   545       | aux (APred tm) =
   546         APred (tm |> repair_applications_in_term thy full_types const_tab
   547                   |> repair_predicates_in_term const_tab)
   548   in aux #> explicit_forall ? close_universally end
   549 
   550 fun repair_problem_line thy explicit_forall full_types const_tab
   551                         (Fof (ident, kind, phi)) =
   552   Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
   553 fun repair_problem_with_const_table thy =
   554   map o apsnd o map ooo repair_problem_line thy
   555 
   556 fun repair_problem thy explicit_forall full_types explicit_apply problem =
   557   repair_problem_with_const_table thy explicit_forall full_types
   558       (const_table_for_problem explicit_apply problem) problem
   559 
   560 fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply
   561                     file (conjectures, axiom_clauses, extra_clauses,
   562                           helper_clauses, class_rel_clauses, arity_clauses) =
   563   let
   564     val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
   565     val class_rel_lines =
   566       map problem_line_for_class_rel_clause class_rel_clauses
   567     val arity_lines = map problem_line_for_arity_clause arity_clauses
   568     val helper_lines = map (problem_line_for_axiom full_types) helper_clauses
   569     val conjecture_lines =
   570       map (problem_line_for_conjecture full_types) conjectures
   571     val tfree_lines = problem_lines_for_free_types conjectures
   572     (* Reordering these might or might not confuse the proof reconstruction
   573        code or the SPASS Flotter hack. *)
   574     val problem =
   575       [("Relevant facts", axiom_lines),
   576        ("Class relationships", class_rel_lines),
   577        ("Arity declarations", arity_lines),
   578        ("Helper facts", helper_lines),
   579        ("Conjectures", conjecture_lines),
   580        ("Type variables", tfree_lines)]
   581       |> repair_problem thy explicit_forall full_types explicit_apply
   582     val (problem, pool) = nice_tptp_problem readable_names problem
   583     val conjecture_offset =
   584       length axiom_lines + length class_rel_lines + length arity_lines
   585       + length helper_lines
   586     val _ = File.write_list file (strings_for_tptp_problem problem)
   587   in
   588     (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
   589      conjecture_offset)
   590   end
   591 
   592 fun extract_clause_sequence output =
   593   let
   594     val tokens_of = String.tokens (not o Char.isAlphaNum)
   595     fun extract_num ("clause" :: (ss as _ :: _)) =
   596     Int.fromString (List.last ss)
   597       | extract_num _ = NONE
   598   in output |> split_lines |> map_filter (extract_num o tokens_of) end
   599 
   600 val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
   601 
   602 val parse_clause_formula_pair =
   603   $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")"
   604   --| Scan.option ($$ ",")
   605 val parse_clause_formula_relation =
   606   Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
   607   |-- Scan.repeat parse_clause_formula_pair
   608 val extract_clause_formula_relation =
   609   Substring.full
   610   #> Substring.position set_ClauseFormulaRelationN
   611   #> snd #> Substring.string #> strip_spaces #> explode
   612   #> parse_clause_formula_relation #> fst
   613 
   614 fun repair_conjecture_shape_and_theorem_names output conjecture_shape
   615                                               thm_names =
   616   if String.isSubstring set_ClauseFormulaRelationN output then
   617     (* This is a hack required for keeping track of axioms after they have been
   618        clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part
   619        of this hack. *)
   620     let
   621       val j0 = hd conjecture_shape
   622       val seq = extract_clause_sequence output
   623       val name_map = extract_clause_formula_relation output
   624       fun renumber_conjecture j =
   625         AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0))
   626         |> the_single
   627         |> (fn s => find_index (curry (op =) s) seq + 1)
   628     in
   629       (conjecture_shape |> map renumber_conjecture,
   630        seq |> map (the o AList.lookup (op =) name_map)
   631            |> map (fn s => case try (unprefix axiom_prefix) s of
   632                              SOME s' => undo_ascii_of s'
   633                            | NONE => "")
   634            |> Vector.fromList)
   635     end
   636   else
   637     (conjecture_shape, thm_names)
   638 
   639 
   640 (* generic TPTP-based provers *)
   641 
   642 fun generic_tptp_prover
   643         (name, {home_var, executable, arguments, proof_delims, known_failures,
   644                 max_new_relevant_facts_per_iter, prefers_theory_relevant,
   645                 explicit_forall})
   646         ({debug, overlord, full_types, explicit_apply, relevance_threshold,
   647           relevance_convergence, theory_relevant, defs_relevant, isar_proof,
   648           isar_shrink_factor, ...} : params)
   649         minimize_command timeout
   650         ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
   651          : problem) =
   652   let
   653     (* get clauses and prepare them for writing *)
   654     val (ctxt, (_, th)) = goal;
   655     val thy = ProofContext.theory_of ctxt
   656     (* ### FIXME: (1) preprocessing for "if" etc. *)
   657     val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
   658     val the_filtered_clauses =
   659       case filtered_clauses of
   660         SOME fcls => fcls
   661       | NONE => relevant_facts full_types relevance_threshold
   662                     relevance_convergence defs_relevant
   663                     max_new_relevant_facts_per_iter
   664                     (the_default prefers_theory_relevant theory_relevant)
   665                     relevance_override goal hyp_ts concl_t
   666     val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
   667     val (internal_thm_names, clauses) =
   668       prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses
   669                       the_filtered_clauses
   670 
   671     (* path to unique problem file *)
   672     val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
   673                        else Config.get ctxt dest_dir;
   674     val the_problem_prefix = Config.get ctxt problem_prefix;
   675     fun prob_pathname nr =
   676       let
   677         val probfile =
   678           Path.basic ((if overlord then "prob_" ^ name
   679                        else the_problem_prefix ^ serial_string ())
   680                       ^ "_" ^ string_of_int nr)
   681       in
   682         if the_dest_dir = "" then File.tmp_path probfile
   683         else if File.exists (Path.explode the_dest_dir)
   684         then Path.append (Path.explode the_dest_dir) probfile
   685         else error ("No such directory: " ^ the_dest_dir ^ ".")
   686       end;
   687 
   688     val home = getenv home_var
   689     val command = Path.explode (home ^ "/" ^ executable)
   690     (* write out problem file and call prover *)
   691     fun command_line complete probfile =
   692       let
   693         val core = File.shell_path command ^ " " ^ arguments complete timeout ^
   694                    " " ^ File.shell_path probfile
   695       in
   696         (if Config.get ctxt measure_runtime then
   697            "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
   698          else
   699            "exec " ^ core) ^ " 2>&1"
   700       end
   701     fun split_time s =
   702       let
   703         val split = String.tokens (fn c => str c = "\n");
   704         val (output, t) = s |> split |> split_last |> apfst cat_lines;
   705         fun as_num f = f >> (fst o read_int);
   706         val num = as_num (Scan.many1 Symbol.is_ascii_digit);
   707         val digit = Scan.one Symbol.is_ascii_digit;
   708         val num3 = as_num (digit ::: digit ::: (digit >> single));
   709         val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
   710         val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
   711       in (output, as_time t) end;
   712     fun run_on probfile =
   713       if home = "" then
   714         error ("The environment variable " ^ quote home_var ^ " is not set.")
   715       else if File.exists command then
   716         let
   717           fun do_run complete =
   718             let
   719               val command = command_line complete probfile
   720               val ((output, msecs), res_code) =
   721                 bash_output command
   722                 |>> (if overlord then
   723                        prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
   724                      else
   725                        I)
   726                 |>> (if Config.get ctxt measure_runtime then split_time
   727                      else rpair 0)
   728               val (proof, outcome) =
   729                 extract_proof_and_outcome complete res_code proof_delims
   730                                           known_failures output
   731             in (output, msecs, proof, outcome) end
   732           val readable_names = debug andalso overlord
   733           val (pool, conjecture_offset) =
   734             write_tptp_file thy readable_names explicit_forall full_types
   735                             explicit_apply probfile clauses
   736           val conjecture_shape =
   737             conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
   738           val result =
   739             do_run false
   740             |> (fn (_, msecs0, _, SOME _) =>
   741                    do_run true
   742                    |> (fn (output, msecs, proof, outcome) =>
   743                           (output, msecs0 + msecs, proof, outcome))
   744                  | result => result)
   745         in ((pool, conjecture_shape), result) end
   746       else
   747         error ("Bad executable: " ^ Path.implode command ^ ".");
   748 
   749     (* If the problem file has not been exported, remove it; otherwise, export
   750        the proof file too. *)
   751     fun cleanup probfile =
   752       if the_dest_dir = "" then try File.rm probfile else NONE
   753     fun export probfile (_, (output, _, _, _)) =
   754       if the_dest_dir = "" then
   755         ()
   756       else
   757         File.write (Path.explode (Path.implode probfile ^ "_proof")) output
   758 
   759     val ((pool, conjecture_shape), (output, msecs, proof, outcome)) =
   760       with_path cleanup export run_on (prob_pathname subgoal)
   761     val (conjecture_shape, internal_thm_names) =
   762       repair_conjecture_shape_and_theorem_names output conjecture_shape
   763                                                 internal_thm_names
   764 
   765     val (message, used_thm_names) =
   766       case outcome of
   767         NONE =>
   768         proof_text isar_proof
   769             (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   770             (full_types, minimize_command, proof, internal_thm_names, th,
   771              subgoal)
   772       | SOME failure => (string_for_failure failure ^ "\n", [])
   773   in
   774     {outcome = outcome, message = message, pool = pool,
   775      used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,
   776      output = output, proof = proof, internal_thm_names = internal_thm_names,
   777      conjecture_shape = conjecture_shape,
   778      filtered_clauses = the_filtered_clauses}
   779   end
   780 
   781 fun tptp_prover name p = (name, generic_tptp_prover (name, p));
   782 
   783 fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000
   784 
   785 (* E prover *)
   786 
   787 val tstp_proof_delims =
   788   ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
   789 
   790 val e_config : prover_config =
   791   {home_var = "E_HOME",
   792    executable = "eproof",
   793    arguments = fn _ => fn timeout =>
   794      "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^
   795      string_of_int (to_generous_secs timeout),
   796    proof_delims = [tstp_proof_delims],
   797    known_failures =
   798      [(Unprovable, "SZS status: CounterSatisfiable"),
   799       (Unprovable, "SZS status CounterSatisfiable"),
   800       (TimedOut, "Failure: Resource limit exceeded (time)"),
   801       (TimedOut, "time limit exceeded"),
   802       (OutOfResources,
   803        "# Cannot determine problem status within resource limit"),
   804       (OutOfResources, "SZS status: ResourceOut"),
   805       (OutOfResources, "SZS status ResourceOut")],
   806    max_new_relevant_facts_per_iter = 80 (* FIXME *),
   807    prefers_theory_relevant = false,
   808    explicit_forall = false}
   809 val e = tptp_prover "e" e_config
   810 
   811 
   812 (* The "-VarWeight=3" option helps the higher-order problems, probably by
   813    counteracting the presence of "hAPP". *)
   814 val spass_config : prover_config =
   815   {home_var = "ISABELLE_ATP_MANAGER",
   816    executable = "SPASS_TPTP",
   817    (* "div 2" accounts for the fact that SPASS is often run twice. *)
   818    arguments = fn complete => fn timeout =>
   819      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
   820       \-VarWeight=3 -TimeLimit=" ^
   821       string_of_int (to_generous_secs timeout div 2))
   822      |> not complete ? prefix "-SOS=1 ",
   823    proof_delims = [("Here is a proof", "Formulae used in the proof")],
   824    known_failures =
   825      [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
   826       (TimedOut, "SPASS beiseite: Ran out of time"),
   827       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
   828       (MalformedInput, "Undefined symbol"),
   829       (MalformedInput, "Free Variable"),
   830       (OldSpass, "tptp2dfg")],
   831    max_new_relevant_facts_per_iter = 26 (* FIXME *),
   832    prefers_theory_relevant = true,
   833    explicit_forall = true}
   834 val spass = tptp_prover "spass" spass_config
   835 
   836 (* Vampire *)
   837 
   838 val vampire_config : prover_config =
   839   {home_var = "VAMPIRE_HOME",
   840    executable = "vampire",
   841    arguments = fn _ => fn timeout =>
   842      "--output_syntax tptp --mode casc -t " ^
   843      string_of_int (to_generous_secs timeout),
   844    proof_delims =
   845      [("=========== Refutation ==========",
   846        "======= End of refutation ======="),
   847       ("% SZS output start Refutation", "% SZS output end Refutation")],
   848    known_failures =
   849      [(Unprovable, "UNPROVABLE"),
   850       (IncompleteUnprovable, "CANNOT PROVE"),
   851       (Unprovable, "Satisfiability detected"),
   852       (OutOfResources, "Refutation not found")],
   853    max_new_relevant_facts_per_iter = 40 (* FIXME *),
   854    prefers_theory_relevant = false,
   855    explicit_forall = false}
   856 val vampire = tptp_prover "vampire" vampire_config
   857 
   858 (* Remote prover invocation via SystemOnTPTP *)
   859 
   860 val systems = Synchronized.var "atp_systems" ([]: string list);
   861 
   862 fun get_systems () =
   863   case bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" of
   864     (answer, 0) => split_lines answer
   865   | (answer, _) =>
   866     error ("Failed to get available systems at SystemOnTPTP:\n" ^
   867            perhaps (try (unsuffix "\n")) answer)
   868 
   869 fun refresh_systems_on_tptp () =
   870   Synchronized.change systems (fn _ => get_systems ())
   871 
   872 fun get_system prefix = Synchronized.change_result systems (fn systems =>
   873   (if null systems then get_systems () else systems)
   874   |> `(find_first (String.isPrefix prefix)));
   875 
   876 fun the_system prefix =
   877   (case get_system prefix of
   878     NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP.")
   879   | SOME sys => sys);
   880 
   881 val remote_known_failures =
   882   [(CantConnect, "HTTP-Error"),
   883    (TimedOut, "says Timeout"),
   884    (MalformedOutput, "Remote script could not extract proof")]
   885 
   886 fun remote_config atp_prefix args
   887         ({proof_delims, known_failures, max_new_relevant_facts_per_iter,
   888           prefers_theory_relevant, explicit_forall, ...} : prover_config)
   889         : prover_config =
   890   {home_var = "ISABELLE_ATP_MANAGER",
   891    executable = "SystemOnTPTP",
   892    arguments = fn _ => fn timeout =>
   893      args ^ " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
   894      the_system atp_prefix,
   895    proof_delims = insert (op =) tstp_proof_delims proof_delims,
   896    known_failures = remote_known_failures @ known_failures,
   897    max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter,
   898    prefers_theory_relevant = prefers_theory_relevant,
   899    explicit_forall = explicit_forall}
   900 
   901 fun remote_tptp_prover prover atp_prefix args config =
   902   tptp_prover (remotify (fst prover)) (remote_config atp_prefix args config)
   903 
   904 val remote_e = remote_tptp_prover e "EP---" "" e_config
   905 val remote_spass = remote_tptp_prover spass "SPASS---" "-x" spass_config
   906 val remote_vampire = remote_tptp_prover vampire "Vampire---9" "" vampire_config
   907 
   908 fun maybe_remote (name, _) ({home_var, ...} : prover_config) =
   909   name |> getenv home_var = "" ? remotify
   910 
   911 fun default_atps_param_value () =
   912   space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
   913                      remotify (fst vampire)]
   914 
   915 val provers = [e, spass, vampire, remote_e, remote_spass, remote_vampire]
   916 val prover_setup = fold add_prover provers
   917 
   918 val setup =
   919   dest_dir_setup
   920   #> problem_prefix_setup
   921   #> measure_runtime_setup
   922   #> prover_setup
   923 
   924 end;