wneuper/isa: src/HOL/Tools/Sledgehammer/sledgehammer.ML@bd443b426d56

     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer.ML

     2     Author:     Fabian Immler, TU Muenchen

     3     Author:     Makarius

     4     Author:     Jasmin Blanchette, TU Muenchen

     6 Sledgehammer's heart.

     7 *)

     9 signature SLEDGEHAMMER =

    10 sig

    11   type failure = ATP_Systems.failure

    12   type relevance_override = Sledgehammer_Fact_Filter.relevance_override

    13   type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command

    14   type params =

    15     {debug: bool,

    16      verbose: bool,

    17      overlord: bool,

    18      atps: string list,

    19      full_types: bool,

    20      explicit_apply: bool,

    21      relevance_threshold: real,

    22      relevance_convergence: real,

    23      max_relevant_per_iter: int option,

    24      theory_relevant: bool option,

    25      defs_relevant: bool,

    26      isar_proof: bool,

    27      isar_shrink_factor: int,

    28      timeout: Time.time}

    29   type problem =

    30     {subgoal: int,

    31      goal: Proof.context * (thm list * thm),

    32      relevance_override: relevance_override,

    33      axioms: (string * thm) list option}

    34   type prover_result =

    35     {outcome: failure option,

    36      message: string,

    37      pool: string Symtab.table,

    38      used_thm_names: string list,

    39      atp_run_time_in_msecs: int,

    40      output: string,

    41      proof: string,

    42      axiom_names: string Vector.vector,

    43      conjecture_shape: int list list}

    44   type prover = params -> minimize_command -> problem -> prover_result

    46   val dest_dir : string Config.T

    47   val problem_prefix : string Config.T

    48   val measure_runtime : bool Config.T

    49   val kill_atps: unit -> unit

    50   val running_atps: unit -> unit

    51   val messages: int option -> unit

    52   val get_prover_fun : theory -> string -> prover

    53   val run_sledgehammer :

    54     params -> int -> relevance_override -> (string -> minimize_command)

    55     -> Proof.state -> unit

    56   val setup : theory -> theory

    57 end;

    59 structure Sledgehammer : SLEDGEHAMMER =

    60 struct

    62 open ATP_Problem

    63 open ATP_Systems

    64 open Metis_Clauses

    65 open Sledgehammer_Util

    66 open Sledgehammer_Fact_Filter

    67 open Sledgehammer_Translate

    68 open Sledgehammer_Proof_Reconstruct

    71 (** The Sledgehammer **)

    73 (* Identifier to distinguish Sledgehammer from other tools using

    74    "Async_Manager". *)

    75 val das_Tool = "Sledgehammer"

    77 fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs"

    78 fun running_atps () = Async_Manager.running_threads das_Tool "ATPs"

    79 val messages = Async_Manager.thread_messages das_Tool "ATP"

    81 (** problems, results, provers, etc. **)

    83 type params =

    84   {debug: bool,

    85    verbose: bool,

    86    overlord: bool,

    87    atps: string list,

    88    full_types: bool,

    89    explicit_apply: bool,

    90    relevance_threshold: real,

    91    relevance_convergence: real,

    92    max_relevant_per_iter: int option,

    93    theory_relevant: bool option,

    94    defs_relevant: bool,

    95    isar_proof: bool,

    96    isar_shrink_factor: int,

    97    timeout: Time.time}

    99 type problem =

   100   {subgoal: int,

   101    goal: Proof.context * (thm list * thm),

   102    relevance_override: relevance_override,

   103    axioms: (string * thm) list option}

   105 type prover_result =

   106   {outcome: failure option,

   107    message: string,

   108    pool: string Symtab.table,

   109    used_thm_names: string list,

   110    atp_run_time_in_msecs: int,

   111    output: string,

   112    proof: string,

   113    axiom_names: string Vector.vector,

   114    conjecture_shape: int list list}

   116 type prover = params -> minimize_command -> problem -> prover_result

   118 (* configuration attributes *)

   120 val (dest_dir, dest_dir_setup) = Attrib.config_string "atp_dest_dir" (K "");

   121   (*Empty string means create files in Isabelle's temporary files directory.*)

   123 val (problem_prefix, problem_prefix_setup) =

   124   Attrib.config_string "atp_problem_prefix" (K "prob");

   126 val (measure_runtime, measure_runtime_setup) =

   127   Attrib.config_bool "atp_measure_runtime" (K false);

   129 fun with_path cleanup after f path =

   130   Exn.capture f path

   131   |> tap (fn _ => cleanup path)

   132   |> Exn.release

   133   |> tap (after path)

   135 (* Splits by the first possible of a list of delimiters. *)

   136 fun extract_proof delims output =

   137   case pairself (find_first (fn s => String.isSubstring s output))

   138                 (ListPair.unzip delims) of

   139     (SOME begin_delim, SOME end_delim) =>

   140     (output |> first_field begin_delim |> the |> snd

   141             |> first_field end_delim |> the |> fst

   142             |> first_field "\n" |> the |> snd

   143      handle Option.Option => "")

   144   | _ => ""

   146 fun extract_proof_and_outcome complete res_code proof_delims known_failures

   147                               output =

   148   case known_failure_in_output output known_failures of

   149     NONE => (case extract_proof proof_delims output of

   150              "" => ("", SOME MalformedOutput)

   151            | proof => if res_code = 0 then (proof, NONE)

   152                       else ("", SOME UnknownError))

   153   | SOME failure =>

   154     ("", SOME (if failure = IncompleteUnprovable andalso complete then

   155                  Unprovable

   156                else

   157                  failure))

   159 fun extract_clause_sequence output =

   160   let

   161     val tokens_of = String.tokens (not o Char.isAlphaNum)

   162     fun extract_num ("clause" :: (ss as _ :: _)) =

   163     Int.fromString (List.last ss)

   164       | extract_num _ = NONE

   165   in output |> split_lines |> map_filter (extract_num o tokens_of) end

   167 val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"

   169 val parse_clause_formula_pair =

   170   $$ "(" |-- scan_integer --| $$ ","

   171   -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")"

   172   --| Scan.option ($$ ",")

   173 val parse_clause_formula_relation =

   174   Scan.this_string set_ClauseFormulaRelationN |-- $$ "("

   175   |-- Scan.repeat parse_clause_formula_pair

   176 val extract_clause_formula_relation =

   177   Substring.full

   178   #> Substring.position set_ClauseFormulaRelationN

   179   #> snd #> Substring.string #> strip_spaces #> explode

   180   #> parse_clause_formula_relation #> fst

   182 fun repair_conjecture_shape_and_theorem_names output conjecture_shape

   183                                               thm_names =

   184   if String.isSubstring set_ClauseFormulaRelationN output then

   185     (* This is a hack required for keeping track of axioms after they have been

   186        clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also

   187        part of this hack. *)

   188     let

   189       val j0 = hd (hd conjecture_shape)

   190       val seq = extract_clause_sequence output

   191       val name_map = extract_clause_formula_relation output

   192       fun renumber_conjecture j =

   193         conjecture_prefix ^ Int.toString (j - j0)

   194         |> AList.find (fn (s, ss) => member (op =) ss s) name_map

   195         |> map (fn s => find_index (curry (op =) s) seq + 1)

   196     in

   197       (conjecture_shape |> map (maps renumber_conjecture),

   198        seq |> map (AList.lookup (op =) name_map #> these

   199                    #> map_filter (try (unprefix axiom_prefix))

   200                    #> map undo_ascii_of #> space_implode " ")

   201            |> Vector.fromList)

   202     end

   203   else

   204     (conjecture_shape, thm_names)

   207 (* generic TPTP-based provers *)

   209 fun prover_fun atp_name

   210         {exec, required_execs, arguments, proof_delims, known_failures,

   211          default_max_relevant_per_iter, default_theory_relevant,

   212          explicit_forall}

   213         ({debug, verbose, overlord, full_types, explicit_apply,

   214           relevance_threshold, relevance_convergence,

   215           max_relevant_per_iter, theory_relevant,

   216           defs_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)

   217         minimize_command

   218         ({subgoal, goal, relevance_override, axioms} : problem) =

   219   let

   220     val (ctxt, (_, th)) = goal;

   221     val thy = ProofContext.theory_of ctxt

   222     val (params, hyp_ts, concl_t) = strip_subgoal th subgoal

   224     fun print s = (priority s; if debug then tracing s else ())

   225     fun print_v f = () |> verbose ? print o f

   226     fun print_d f = () |> debug ? print o f

   228     val the_axioms =

   229       case axioms of

   230         SOME axioms => axioms

   231       | NONE =>

   232         (print_d (fn () => "Selecting relevant facts for " ^ quote atp_name ^

   233                            ".");

   234          relevant_facts full_types relevance_threshold relevance_convergence

   235                         defs_relevant

   236                         (the_default default_max_relevant_per_iter

   237                                      max_relevant_per_iter)

   238                         (the_default default_theory_relevant theory_relevant)

   239                         relevance_override goal hyp_ts concl_t

   240          |> tap ((fn n => print_v (fn () =>

   241                       "Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^

   242                       " for " ^ quote atp_name ^ ".")) o length))

   244     (* path to unique problem file *)

   245     val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"

   246                        else Config.get ctxt dest_dir;

   247     val the_problem_prefix = Config.get ctxt problem_prefix;

   248     fun prob_pathname nr =

   249       let

   250         val probfile =

   251           Path.basic ((if overlord then "prob_" ^ atp_name

   252                        else the_problem_prefix ^ serial_string ())

   253                       ^ "_" ^ string_of_int nr)

   254       in

   255         if the_dest_dir = "" then File.tmp_path probfile

   256         else if File.exists (Path.explode the_dest_dir)

   257         then Path.append (Path.explode the_dest_dir) probfile

   258         else error ("No such directory: " ^ the_dest_dir ^ ".")

   259       end;

   261     val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)

   262     (* write out problem file and call prover *)

   263     fun command_line complete probfile =

   264       let

   265         val core = File.shell_path command ^ " " ^ arguments complete timeout ^

   266                    " " ^ File.shell_path probfile

   267       in

   268         (if Config.get ctxt measure_runtime then

   269            "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"

   270          else

   271            "exec " ^ core) ^ " 2>&1"

   272       end

   273     fun split_time s =

   274       let

   275         val split = String.tokens (fn c => str c = "\n");

   276         val (output, t) = s |> split |> split_last |> apfst cat_lines;

   277         fun as_num f = f >> (fst o read_int);

   278         val num = as_num (Scan.many1 Symbol.is_ascii_digit);

   279         val digit = Scan.one Symbol.is_ascii_digit;

   280         val num3 = as_num (digit ::: digit ::: (digit >> single));

   281         val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);

   282         val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;

   283       in (output, as_time t) end;

   284     fun run_on probfile =

   285       case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of

   286         (home_var, _) :: _ =>

   287         error ("The environment variable " ^ quote home_var ^ " is not set.")

   288       | [] =>

   289         if File.exists command then

   290           let

   291             fun do_run complete =

   292               let

   293                 val command = command_line complete probfile

   294                 val ((output, msecs), res_code) =

   295                   bash_output command

   296                   |>> (if overlord then

   297                          prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")

   298                        else

   299                          I)

   300                   |>> (if Config.get ctxt measure_runtime then split_time

   301                        else rpair 0)

   302                 val (proof, outcome) =

   303                   extract_proof_and_outcome complete res_code proof_delims

   304                                             known_failures output

   305               in (output, msecs, proof, outcome) end

   306             val _ = print_d (fn () => "Preparing problem for " ^

   307                                       quote atp_name ^ "...")

   308             val readable_names = debug andalso overlord

   309             val (problem, pool, conjecture_offset, axiom_names) =

   310               prepare_problem ctxt readable_names explicit_forall full_types

   311                               explicit_apply hyp_ts concl_t the_axioms

   312             val _ = File.write_list probfile (strings_for_tptp_problem problem)

   313             val conjecture_shape =

   314               conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1

   315               |> map single

   316             val _ = print_d (fn () => "Running " ^ quote atp_name ^ "...")

   317             val result =

   318               do_run false

   319               |> (fn (_, msecs0, _, SOME _) =>

   320                      do_run true

   321                      |> (fn (output, msecs, proof, outcome) =>

   322                             (output, msecs0 + msecs, proof, outcome))

   323                    | result => result)

   324           in ((pool, conjecture_shape, axiom_names), result) end

   325         else

   326           error ("Bad executable: " ^ Path.implode command ^ ".")

   328     (* If the problem file has not been exported, remove it; otherwise, export

   329        the proof file too. *)

   330     fun cleanup probfile =

   331       if the_dest_dir = "" then try File.rm probfile else NONE

   332     fun export probfile (_, (output, _, _, _)) =

   333       if the_dest_dir = "" then

   334         ()

   335       else

   336         File.write (Path.explode (Path.implode probfile ^ "_proof")) output

   338     val ((pool, conjecture_shape, axiom_names),

   339          (output, msecs, proof, outcome)) =

   340       with_path cleanup export run_on (prob_pathname subgoal)

   341     val (conjecture_shape, axiom_names) =

   342       repair_conjecture_shape_and_theorem_names output conjecture_shape

   343                                                 axiom_names

   345     val (message, used_thm_names) =

   346       case outcome of

   347         NONE =>

   348         proof_text isar_proof

   349             (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)

   350             (full_types, minimize_command, proof, axiom_names, th, subgoal)

   351       | SOME failure => (string_for_failure failure ^ "\n", [])

   352   in

   353     {outcome = outcome, message = message, pool = pool,

   354      used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,

   355      output = output, proof = proof, axiom_names = axiom_names,

   356      conjecture_shape = conjecture_shape}

   357   end

   359 fun get_prover_fun thy name = prover_fun name (get_prover thy name)

   361 fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n

   362                         relevance_override minimize_command proof_state

   363                         atp_name =

   364   let

   365     val thy = Proof.theory_of proof_state

   366     val birth_time = Time.now ()

   367     val death_time = Time.+ (birth_time, timeout)

   368     val prover = get_prover_fun thy atp_name

   369     val {context = ctxt, facts, goal} = Proof.goal proof_state;

   370     val desc =

   371       "ATP " ^ quote atp_name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^

   372       Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));

   373   in

   374     Async_Manager.launch das_Tool verbose birth_time death_time desc

   375         (fn () =>

   376             let

   377               val problem =

   378                 {subgoal = i, goal = (ctxt, (facts, goal)),

   379                  relevance_override = relevance_override, axioms = NONE}

   380             in

   381               prover params (minimize_command atp_name) problem |> #message

   382               handle ERROR message => "Error: " ^ message ^ "\n"

   383                    | exn => "Internal error: \n" ^ ML_Compiler.exn_message exn ^

   384                             "\n"

   385             end)

   386   end

   388 fun run_sledgehammer {atps = [], ...} _ _ _ _ = error "No ATP is set."

   389   | run_sledgehammer (params as {atps, ...}) i relevance_override

   390                      minimize_command state =

   391     case subgoal_count state of

   392       0 => priority "No subgoal!"

   393     | n =>

   394       let

   395         val _ = kill_atps ()

   396         val _ = priority "Sledgehammering..."

   397         val _ = app (start_prover_thread params i n relevance_override

   398                                          minimize_command state) atps

   399       in () end

   401 val setup =

   402   dest_dir_setup

   403   #> problem_prefix_setup

   404   #> measure_runtime_setup

   406 end;

author	blanchet
	Wed, 18 Aug 2010 17:16:37 +0200
changeset 38813	bd443b426d56
parent 38812	b03f8fe043ec
child 38820	db482afec7f0
permissions	-rw-r--r--