1.1 --- a/src/HOL/IsaMakefile	Fri Apr 23 18:06:41 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Apr 23 18:11:41 2010 +0200
     1.3 @@ -283,7 +283,7 @@
     1.4    $(SRC)/Provers/Arith/extract_common_term.ML \
     1.5    $(SRC)/Tools/Metis/metis.ML \
     1.6    Tools/ATP_Manager/atp_manager.ML \
     1.7 -  Tools/ATP_Manager/atp_wrapper.ML \
     1.8 +  Tools/ATP_Manager/atp_systems.ML \
     1.9    Tools/Groebner_Basis/groebner.ML \
    1.10    Tools/Groebner_Basis/misc.ML \
    1.11    Tools/Groebner_Basis/normalizer.ML \

     2.1 --- a/src/HOL/Sledgehammer.thy	Fri Apr 23 18:06:41 2010 +0200
     2.2 +++ b/src/HOL/Sledgehammer.thy	Fri Apr 23 18:11:41 2010 +0200
     2.3 @@ -18,7 +18,7 @@
     2.4    ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
     2.5    ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
     2.6    ("Tools/ATP_Manager/atp_manager.ML")
     2.7 -  ("Tools/ATP_Manager/atp_wrapper.ML")
     2.8 +  ("Tools/ATP_Manager/atp_systems.ML")
     2.9    ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
    2.10    ("Tools/Sledgehammer/sledgehammer_isar.ML")
    2.11    ("Tools/Sledgehammer/meson_tactic.ML")
    2.12 @@ -101,7 +101,7 @@
    2.13  use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
    2.14  use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
    2.15  use "Tools/ATP_Manager/atp_manager.ML"
    2.16 -use "Tools/ATP_Manager/atp_wrapper.ML"
    2.17 +use "Tools/ATP_Manager/atp_systems.ML"
    2.18  setup ATP_Systems.setup
    2.19  use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
    2.20  use "Tools/Sledgehammer/sledgehammer_isar.ML"

     3.1 --- a/src/HOL/Tools/ATP_Manager/SystemOnTPTP	Fri Apr 23 18:06:41 2010 +0200
     3.2 +++ b/src/HOL/Tools/ATP_Manager/SystemOnTPTP	Fri Apr 23 18:11:41 2010 +0200
     3.3 @@ -136,7 +136,7 @@
     3.4    print $Response->content;
     3.5    exit(0);
     3.6  }else {
     3.7 -  print "Remote-script could not extract proof:\n".$Response->content;
     3.8 +  print "Remote script could not extract proof:\n".$Response->content;
     3.9    exit(-1);
    3.10  }
    3.11  

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Apr 23 18:11:41 2010 +0200
     4.3 @@ -0,0 +1,412 @@
     4.4 +(*  Title:      HOL/Tools/ATP_Manager/atp_systems.ML
     4.5 +    Author:     Fabian Immler, TU Muenchen
     4.6 +    Author:     Jasmin Blanchette, TU Muenchen
     4.7 +
     4.8 +Setup for supported ATPs.
     4.9 +*)
    4.10 +
    4.11 +signature ATP_SYSTEMS =
    4.12 +sig
    4.13 +  type prover = ATP_Manager.prover
    4.14 +
    4.15 +  (* hooks for problem files *)
    4.16 +  val dest_dir : string Config.T
    4.17 +  val problem_prefix : string Config.T
    4.18 +  val measure_runtime : bool Config.T
    4.19 +
    4.20 +  val refresh_systems_on_tptp : unit -> unit
    4.21 +  val default_atps_param_value : unit -> string
    4.22 +  val setup : theory -> theory
    4.23 +end;
    4.24 +
    4.25 +structure ATP_Systems : ATP_SYSTEMS =
    4.26 +struct
    4.27 +
    4.28 +open Sledgehammer_Util
    4.29 +open Sledgehammer_Fact_Preprocessor
    4.30 +open Sledgehammer_HOL_Clause
    4.31 +open Sledgehammer_Fact_Filter
    4.32 +open Sledgehammer_Proof_Reconstruct
    4.33 +open ATP_Manager
    4.34 +
    4.35 +(** generic ATP **)
    4.36 +
    4.37 +(* external problem files *)
    4.38 +
    4.39 +val (dest_dir, dest_dir_setup) = Attrib.config_string "atp_dest_dir" (K "");
    4.40 +  (*Empty string means create files in Isabelle's temporary files directory.*)
    4.41 +
    4.42 +val (problem_prefix, problem_prefix_setup) =
    4.43 +  Attrib.config_string "atp_problem_prefix" (K "prob");
    4.44 +
    4.45 +val (measure_runtime, measure_runtime_setup) =
    4.46 +  Attrib.config_bool "atp_measure_runtime" (K false);
    4.47 +
    4.48 +
    4.49 +(* prover configuration *)
    4.50 +
    4.51 +type prover_config =
    4.52 +  {home: string,
    4.53 +   executable: string,
    4.54 +   arguments: Time.time -> string,
    4.55 +   proof_delims: (string * string) list,
    4.56 +   known_failures: (failure * string) list,
    4.57 +   max_new_clauses: int,
    4.58 +   prefers_theory_relevant: bool};
    4.59 +
    4.60 +
    4.61 +(* basic template *)
    4.62 +
    4.63 +val remotify = prefix "remote_"
    4.64 +
    4.65 +fun with_path cleanup after f path =
    4.66 +  Exn.capture f path
    4.67 +  |> tap (fn _ => cleanup path)
    4.68 +  |> Exn.release
    4.69 +  |> tap (after path)
    4.70 +
    4.71 +(* Splits by the first possible of a list of delimiters. *)
    4.72 +fun extract_proof delims output =
    4.73 +  case pairself (find_first (fn s => String.isSubstring s output))
    4.74 +                (ListPair.unzip delims) of
    4.75 +    (SOME begin_delim, SOME end_delim) =>
    4.76 +    output |> first_field begin_delim |> the |> snd
    4.77 +           |> first_field end_delim |> the |> fst
    4.78 +  | _ => ""
    4.79 +
    4.80 +fun extract_proof_and_outcome res_code proof_delims known_failures output =
    4.81 +  case map_filter (fn (failure, pattern) =>
    4.82 +                      if String.isSubstring pattern output then SOME failure
    4.83 +                      else NONE) known_failures of
    4.84 +    [] => (case extract_proof proof_delims output of
    4.85 +             "" => ("", SOME UnknownError)
    4.86 +           | proof => if res_code = 0 then (proof, NONE)
    4.87 +                      else ("", SOME UnknownError))
    4.88 +  | (failure :: _) => ("", SOME failure)
    4.89 +
    4.90 +fun string_for_failure Unprovable = "The ATP problem is unprovable."
    4.91 +  | string_for_failure TimedOut = "Timed out."
    4.92 +  | string_for_failure OutOfResources = "The ATP ran out of resources."
    4.93 +  | string_for_failure OldSpass =
    4.94 +    "Warning: Sledgehammer requires a more recent version of SPASS with \
    4.95 +    \support for the TPTP syntax. To install it, download and untar the \
    4.96 +    \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \
    4.97 +    \\"spass-3.7\" directory's full path to \"" ^
    4.98 +    Path.implode (Path.expand (Path.appends
    4.99 +        (Path.variable "ISABELLE_HOME_USER" ::
   4.100 +         map Path.basic ["etc", "components"]))) ^
   4.101 +    "\" on a line of its own."
   4.102 +  | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
   4.103 +  | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
   4.104 +
   4.105 +fun generic_prover overlord get_facts prepare write_file home executable args
   4.106 +        proof_delims known_failures name
   4.107 +        ({debug, full_types, explicit_apply, isar_proof, modulus, sorts, ...}
   4.108 +         : params) minimize_command
   4.109 +        ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
   4.110 +         : problem) =
   4.111 +  let
   4.112 +    (* get clauses and prepare them for writing *)
   4.113 +    val (ctxt, (chain_ths, th)) = goal;
   4.114 +    val thy = ProofContext.theory_of ctxt;
   4.115 +    val chain_ths = map (Thm.put_name_hint chained_hint) chain_ths;
   4.116 +    val goal_cls = #1 (neg_conjecture_clauses ctxt th subgoal);
   4.117 +    val the_filtered_clauses =
   4.118 +      (case filtered_clauses of
   4.119 +        NONE => get_facts relevance_override goal goal_cls
   4.120 +      | SOME fcls => fcls);
   4.121 +    val the_axiom_clauses =
   4.122 +      (case axiom_clauses of
   4.123 +        NONE => the_filtered_clauses
   4.124 +      | SOME axcls => axcls);
   4.125 +    val (internal_thm_names, clauses) =
   4.126 +      prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy;
   4.127 +
   4.128 +    (* path to unique problem file *)
   4.129 +    val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
   4.130 +                       else Config.get ctxt dest_dir;
   4.131 +    val the_problem_prefix = Config.get ctxt problem_prefix;
   4.132 +    fun prob_pathname nr =
   4.133 +      let
   4.134 +        val probfile =
   4.135 +          Path.basic (the_problem_prefix ^
   4.136 +                      (if overlord then "_" ^ name else serial_string ())
   4.137 +                      ^ "_" ^ string_of_int nr)
   4.138 +      in
   4.139 +        if the_dest_dir = "" then File.tmp_path probfile
   4.140 +        else if File.exists (Path.explode the_dest_dir)
   4.141 +        then Path.append (Path.explode the_dest_dir) probfile
   4.142 +        else error ("No such directory: " ^ the_dest_dir ^ ".")
   4.143 +      end;
   4.144 +
   4.145 +    val command = Path.explode (home ^ "/" ^ executable)
   4.146 +    (* write out problem file and call prover *)
   4.147 +    fun command_line probfile =
   4.148 +      (if Config.get ctxt measure_runtime then
   4.149 +         "TIMEFORMAT='%3U'; { time " ^
   4.150 +         space_implode " " [File.shell_path command, args,
   4.151 +                            File.shell_path probfile] ^ " ; } 2>&1"
   4.152 +       else
   4.153 +         space_implode " " ["exec", File.shell_path command, args,
   4.154 +                            File.shell_path probfile, "2>&1"]) ^
   4.155 +      (if overlord then
   4.156 +         " | sed 's/,/, /g' \
   4.157 +         \| sed 's/\\([^!=]\\)\\([=|]\\)\\([^=]\\)/\\1 \\2 \\3/g' \
   4.158 +         \| sed 's/! =/ !=/g' \
   4.159 +         \| sed 's/  / /g' | sed 's/| |/||/g' \
   4.160 +         \| sed 's/ = = =/===/g' \
   4.161 +         \| sed 's/= = /== /g'"
   4.162 +       else
   4.163 +         "")
   4.164 +    fun split_time s =
   4.165 +      let
   4.166 +        val split = String.tokens (fn c => str c = "\n");
   4.167 +        val (output, t) = s |> split |> split_last |> apfst cat_lines;
   4.168 +        fun as_num f = f >> (fst o read_int);
   4.169 +        val num = as_num (Scan.many1 Symbol.is_ascii_digit);
   4.170 +        val digit = Scan.one Symbol.is_ascii_digit;
   4.171 +        val num3 = as_num (digit ::: digit ::: (digit >> single));
   4.172 +        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
   4.173 +        val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
   4.174 +      in (output, as_time t) end;
   4.175 +    fun split_time' s =
   4.176 +      if Config.get ctxt measure_runtime then split_time s else (s, 0)
   4.177 +    fun run_on probfile =
   4.178 +      if File.exists command then
   4.179 +        write_file full_types explicit_apply probfile clauses
   4.180 +        |> pair (apfst split_time' (bash_output (command_line probfile)))
   4.181 +      else error ("Bad executable: " ^ Path.implode command ^ ".");
   4.182 +
   4.183 +    (* If the problem file has not been exported, remove it; otherwise, export
   4.184 +       the proof file too. *)
   4.185 +    fun cleanup probfile =
   4.186 +      if the_dest_dir = "" then try File.rm probfile else NONE
   4.187 +    fun export probfile (((output, _), _), _) =
   4.188 +      if the_dest_dir = "" then
   4.189 +        ()
   4.190 +      else
   4.191 +        File.write (Path.explode (Path.implode probfile ^ "_proof"))
   4.192 +                   ((if overlord then
   4.193 +                       "% " ^ command_line probfile ^ "\n% " ^ timestamp () ^
   4.194 +                       "\n"
   4.195 +                     else
   4.196 +                        "") ^ output)
   4.197 +
   4.198 +    val (((output, atp_run_time_in_msecs), res_code), _) =
   4.199 +      with_path cleanup export run_on (prob_pathname subgoal);
   4.200 +
   4.201 +    (* Check for success and print out some information on failure. *)
   4.202 +    val (proof, outcome) =
   4.203 +      extract_proof_and_outcome res_code proof_delims known_failures output
   4.204 +    val (message, relevant_thm_names) =
   4.205 +      case outcome of
   4.206 +        NONE => proof_text isar_proof debug modulus sorts ctxt
   4.207 +                           (minimize_command, proof, internal_thm_names, th,
   4.208 +                            subgoal)
   4.209 +      | SOME failure => (string_for_failure failure ^ "\n", [])
   4.210 +  in
   4.211 +    {outcome = outcome, message = message,
   4.212 +     relevant_thm_names = relevant_thm_names,
   4.213 +     atp_run_time_in_msecs = atp_run_time_in_msecs, output = output,
   4.214 +     proof = proof, internal_thm_names = internal_thm_names,
   4.215 +     filtered_clauses = the_filtered_clauses}
   4.216 +  end;
   4.217 +
   4.218 +
   4.219 +(* generic TPTP-based provers *)
   4.220 +
   4.221 +fun generic_tptp_prover
   4.222 +        (name, {home, executable, arguments, proof_delims, known_failures,
   4.223 +                max_new_clauses, prefers_theory_relevant})
   4.224 +        (params as {debug, overlord, respect_no_atp, relevance_threshold,
   4.225 +                    convergence, theory_relevant, higher_order, follow_defs,
   4.226 +                    isar_proof, ...})
   4.227 +        minimize_command timeout =
   4.228 +  generic_prover overlord
   4.229 +      (get_relevant_facts respect_no_atp relevance_threshold convergence
   4.230 +                          higher_order follow_defs max_new_clauses
   4.231 +                          (the_default prefers_theory_relevant theory_relevant))
   4.232 +      (prepare_clauses higher_order false)
   4.233 +      (write_tptp_file (debug andalso overlord andalso not isar_proof)) home
   4.234 +      executable (arguments timeout) proof_delims known_failures name params
   4.235 +      minimize_command
   4.236 +
   4.237 +fun tptp_prover name p = (name, generic_tptp_prover (name, p));
   4.238 +
   4.239 +
   4.240 +(** common provers **)
   4.241 +
   4.242 +fun generous_to_secs time = (Time.toMilliseconds time + 999) div 1000
   4.243 +
   4.244 +(* Vampire *)
   4.245 +
   4.246 +(* Vampire requires an explicit time limit. *)
   4.247 +
   4.248 +val vampire_config : prover_config =
   4.249 +  {home = getenv "VAMPIRE_HOME",
   4.250 +   executable = "vampire",
   4.251 +   arguments = (fn timeout => "--output_syntax tptp --mode casc -t " ^
   4.252 +                              string_of_int (generous_to_secs timeout)),
   4.253 +   proof_delims = [("=========== Refutation ==========",
   4.254 +                    "======= End of refutation =======")],
   4.255 +   known_failures =
   4.256 +     [(Unprovable, "Satisfiability detected"),
   4.257 +      (OutOfResources, "CANNOT PROVE"),
   4.258 +      (OutOfResources, "Refutation not found")],
   4.259 +   max_new_clauses = 60,
   4.260 +   prefers_theory_relevant = false}
   4.261 +val vampire = tptp_prover "vampire" vampire_config
   4.262 +
   4.263 +
   4.264 +(* E prover *)
   4.265 +
   4.266 +val tstp_proof_delims =
   4.267 +  ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
   4.268 +
   4.269 +val e_config : prover_config =
   4.270 +  {home = getenv "E_HOME",
   4.271 +   executable = "eproof",
   4.272 +   arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev \
   4.273 +                              \-tAutoDev --silent --cpu-limit=" ^
   4.274 +                              string_of_int (generous_to_secs timeout)),
   4.275 +   proof_delims = [tstp_proof_delims],
   4.276 +   known_failures =
   4.277 +     [(Unprovable, "SZS status: Satisfiable"),
   4.278 +      (Unprovable, "SZS status Satisfiable"),
   4.279 +      (TimedOut, "Failure: Resource limit exceeded (time)"),
   4.280 +      (TimedOut, "time limit exceeded"),
   4.281 +      (OutOfResources,
   4.282 +       "# Cannot determine problem status within resource limit"),
   4.283 +      (OutOfResources, "SZS status: ResourceOut"),
   4.284 +      (OutOfResources, "SZS status ResourceOut")],
   4.285 +   max_new_clauses = 100,
   4.286 +   prefers_theory_relevant = false}
   4.287 +val e = tptp_prover "e" e_config
   4.288 +
   4.289 +
   4.290 +(* SPASS *)
   4.291 +
   4.292 +fun generic_dfg_prover
   4.293 +        (name, {home, executable, arguments, proof_delims, known_failures,
   4.294 +                max_new_clauses, prefers_theory_relevant})
   4.295 +        (params as {overlord, respect_no_atp, relevance_threshold, convergence,
   4.296 +                    theory_relevant, higher_order, follow_defs, ...})
   4.297 +        minimize_command timeout =
   4.298 +  generic_prover overlord
   4.299 +      (get_relevant_facts respect_no_atp relevance_threshold convergence
   4.300 +                          higher_order follow_defs max_new_clauses
   4.301 +                          (the_default prefers_theory_relevant theory_relevant))
   4.302 +      (prepare_clauses higher_order true) write_dfg_file home executable
   4.303 +      (arguments timeout) proof_delims known_failures name params
   4.304 +      minimize_command
   4.305 +
   4.306 +fun dfg_prover name p = (name, generic_dfg_prover (name, p))
   4.307 +
   4.308 +(* The "-VarWeight=3" option helps the higher-order problems, probably by
   4.309 +   counteracting the presence of "hAPP". *)
   4.310 +val spass_config : prover_config =
   4.311 +  {home = getenv "SPASS_HOME",
   4.312 +   executable = "SPASS",
   4.313 +   arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
   4.314 +     " -FullRed=0 -DocProof -VarWeight=3 -TimeLimit=" ^
   4.315 +     string_of_int (generous_to_secs timeout)),
   4.316 +   proof_delims = [("Here is a proof", "Formulae used in the proof")],
   4.317 +   known_failures =
   4.318 +     [(Unprovable, "SPASS beiseite: Completion found"),
   4.319 +      (TimedOut, "SPASS beiseite: Ran out of time"),
   4.320 +      (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded")],
   4.321 +   max_new_clauses = 40,
   4.322 +   prefers_theory_relevant = true}
   4.323 +val spass = dfg_prover "spass" spass_config
   4.324 +
   4.325 +(* SPASS 3.7 supports both the DFG and the TPTP syntax, whereas SPASS 3.0
   4.326 +   supports only the DFG syntax. As soon as all Isabelle repository/snapshot
   4.327 +   users have upgraded to 3.7, we can kill "spass" (and all DFG support in
   4.328 +   Sledgehammer) and rename "spass_tptp" "spass". *)
   4.329 +
   4.330 +(* FIXME: Change the error message below to point to the Isabelle download
   4.331 +   page once the package is there (around the Isabelle2010 release). *)
   4.332 +
   4.333 +val spass_tptp_config =
   4.334 +  {home = #home spass_config,
   4.335 +   executable = #executable spass_config,
   4.336 +   arguments = prefix "-TPTP " o #arguments spass_config,
   4.337 +   proof_delims = #proof_delims spass_config,
   4.338 +   known_failures =
   4.339 +     #known_failures spass_config @
   4.340 +     [(OldSpass, "unrecognized option `-TPTP'"),
   4.341 +      (OldSpass, "Unrecognized option TPTP")],
   4.342 +   max_new_clauses = #max_new_clauses spass_config,
   4.343 +   prefers_theory_relevant = #prefers_theory_relevant spass_config}
   4.344 +val spass_tptp = tptp_prover "spass_tptp" spass_tptp_config
   4.345 +
   4.346 +(* remote prover invocation via SystemOnTPTP *)
   4.347 +
   4.348 +val systems = Synchronized.var "atp_systems" ([]: string list);
   4.349 +
   4.350 +fun get_systems () =
   4.351 +  case bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" of
   4.352 +    (answer, 0) => split_lines answer
   4.353 +  | (answer, _) =>
   4.354 +    error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer)
   4.355 +
   4.356 +fun refresh_systems_on_tptp () =
   4.357 +  Synchronized.change systems (fn _ => get_systems ());
   4.358 +
   4.359 +fun get_system prefix = Synchronized.change_result systems (fn systems =>
   4.360 +  (if null systems then get_systems () else systems)
   4.361 +  |> `(find_first (String.isPrefix prefix)));
   4.362 +
   4.363 +fun the_system prefix =
   4.364 +  (case get_system prefix of
   4.365 +    NONE => error ("System " ^ quote prefix ^
   4.366 +                   " not available at SystemOnTPTP.")
   4.367 +  | SOME sys => sys);
   4.368 +
   4.369 +val remote_known_failures =
   4.370 +  [(TimedOut, "says Timeout"),
   4.371 +   (MalformedOutput, "Remote script could not extract proof")]
   4.372 +
   4.373 +fun remote_prover_config prover_prefix args
   4.374 +        ({proof_delims, known_failures, max_new_clauses,
   4.375 +          prefers_theory_relevant, ...} : prover_config) : prover_config =
   4.376 +  {home = getenv "ISABELLE_ATP_MANAGER",
   4.377 +   executable = "SystemOnTPTP",
   4.378 +   arguments = (fn timeout =>
   4.379 +     args ^ " -t " ^ string_of_int (generous_to_secs timeout) ^ " -s " ^
   4.380 +     the_system prover_prefix),
   4.381 +   proof_delims = insert (op =) tstp_proof_delims proof_delims,
   4.382 +   known_failures = remote_known_failures @ known_failures,
   4.383 +   max_new_clauses = max_new_clauses,
   4.384 +   prefers_theory_relevant = prefers_theory_relevant}
   4.385 +
   4.386 +val remote_vampire =
   4.387 +  tptp_prover (remotify (fst vampire))
   4.388 +              (remote_prover_config "Vampire---9" "" vampire_config)
   4.389 +
   4.390 +val remote_e =
   4.391 +  tptp_prover (remotify (fst e))
   4.392 +              (remote_prover_config "EP---" "" e_config)
   4.393 +
   4.394 +val remote_spass =
   4.395 +  tptp_prover (remotify (fst spass))
   4.396 +              (remote_prover_config "SPASS---" "-x" spass_config)
   4.397 +
   4.398 +fun maybe_remote (name, _) ({home, ...} : prover_config) =
   4.399 +  name |> home = "" ? remotify
   4.400 +
   4.401 +fun default_atps_param_value () =
   4.402 +  space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
   4.403 +                     remotify (fst vampire)]
   4.404 +
   4.405 +val provers =
   4.406 +  [spass, spass_tptp, vampire, e, remote_vampire, remote_spass, remote_e]
   4.407 +val prover_setup = fold add_prover provers
   4.408 +
   4.409 +val setup =
   4.410 +  dest_dir_setup
   4.411 +  #> problem_prefix_setup
   4.412 +  #> measure_runtime_setup
   4.413 +  #> prover_setup
   4.414 +
   4.415 +end;

     5.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Apr 23 18:06:41 2010 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,412 +0,0 @@
     5.4 -(*  Title:      HOL/Tools/ATP_Manager/atp_systems.ML
     5.5 -    Author:     Fabian Immler, TU Muenchen
     5.6 -    Author:     Jasmin Blanchette, TU Muenchen
     5.7 -
     5.8 -Setup for supported ATPs.
     5.9 -*)
    5.10 -
    5.11 -signature ATP_SYSTEMS =
    5.12 -sig
    5.13 -  type prover = ATP_Manager.prover
    5.14 -
    5.15 -  (* hooks for problem files *)
    5.16 -  val dest_dir : string Config.T
    5.17 -  val problem_prefix : string Config.T
    5.18 -  val measure_runtime : bool Config.T
    5.19 -
    5.20 -  val refresh_systems_on_tptp : unit -> unit
    5.21 -  val default_atps_param_value : unit -> string
    5.22 -  val setup : theory -> theory
    5.23 -end;
    5.24 -
    5.25 -structure ATP_Systems : ATP_SYSTEMS =
    5.26 -struct
    5.27 -
    5.28 -open Sledgehammer_Util
    5.29 -open Sledgehammer_Fact_Preprocessor
    5.30 -open Sledgehammer_HOL_Clause
    5.31 -open Sledgehammer_Fact_Filter
    5.32 -open Sledgehammer_Proof_Reconstruct
    5.33 -open ATP_Manager
    5.34 -
    5.35 -(** generic ATP **)
    5.36 -
    5.37 -(* external problem files *)
    5.38 -
    5.39 -val (dest_dir, dest_dir_setup) = Attrib.config_string "atp_dest_dir" (K "");
    5.40 -  (*Empty string means create files in Isabelle's temporary files directory.*)
    5.41 -
    5.42 -val (problem_prefix, problem_prefix_setup) =
    5.43 -  Attrib.config_string "atp_problem_prefix" (K "prob");
    5.44 -
    5.45 -val (measure_runtime, measure_runtime_setup) =
    5.46 -  Attrib.config_bool "atp_measure_runtime" (K false);
    5.47 -
    5.48 -
    5.49 -(* prover configuration *)
    5.50 -
    5.51 -type prover_config =
    5.52 -  {home: string,
    5.53 -   executable: string,
    5.54 -   arguments: Time.time -> string,
    5.55 -   proof_delims: (string * string) list,
    5.56 -   known_failures: (failure * string) list,
    5.57 -   max_new_clauses: int,
    5.58 -   prefers_theory_relevant: bool};
    5.59 -
    5.60 -
    5.61 -(* basic template *)
    5.62 -
    5.63 -val remotify = prefix "remote_"
    5.64 -
    5.65 -fun with_path cleanup after f path =
    5.66 -  Exn.capture f path
    5.67 -  |> tap (fn _ => cleanup path)
    5.68 -  |> Exn.release
    5.69 -  |> tap (after path)
    5.70 -
    5.71 -(* Splits by the first possible of a list of delimiters. *)
    5.72 -fun extract_proof delims output =
    5.73 -  case pairself (find_first (fn s => String.isSubstring s output))
    5.74 -                (ListPair.unzip delims) of
    5.75 -    (SOME begin_delim, SOME end_delim) =>
    5.76 -    output |> first_field begin_delim |> the |> snd
    5.77 -           |> first_field end_delim |> the |> fst
    5.78 -  | _ => ""
    5.79 -
    5.80 -fun extract_proof_and_outcome res_code proof_delims known_failures output =
    5.81 -  case map_filter (fn (failure, pattern) =>
    5.82 -                      if String.isSubstring pattern output then SOME failure
    5.83 -                      else NONE) known_failures of
    5.84 -    [] => (case extract_proof proof_delims output of
    5.85 -             "" => ("", SOME UnknownError)
    5.86 -           | proof => if res_code = 0 then (proof, NONE)
    5.87 -                      else ("", SOME UnknownError))
    5.88 -  | (failure :: _) => ("", SOME failure)
    5.89 -
    5.90 -fun string_for_failure Unprovable = "The ATP problem is unprovable."
    5.91 -  | string_for_failure TimedOut = "Timed out."
    5.92 -  | string_for_failure OutOfResources = "The ATP ran out of resources."
    5.93 -  | string_for_failure OldSpass =
    5.94 -    "Warning: Sledgehammer requires a more recent version of SPASS with \
    5.95 -    \support for the TPTP syntax. To install it, download and untar the \
    5.96 -    \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \
    5.97 -    \\"spass-3.7\" directory's full path to \"" ^
    5.98 -    Path.implode (Path.expand (Path.appends
    5.99 -        (Path.variable "ISABELLE_HOME_USER" ::
   5.100 -         map Path.basic ["etc", "components"]))) ^
   5.101 -    "\" on a line of its own."
   5.102 -  | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
   5.103 -  | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
   5.104 -
   5.105 -fun generic_prover overlord get_facts prepare write_file home executable args
   5.106 -        proof_delims known_failures name
   5.107 -        ({debug, full_types, explicit_apply, isar_proof, modulus, sorts, ...}
   5.108 -         : params) minimize_command
   5.109 -        ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
   5.110 -         : problem) =
   5.111 -  let
   5.112 -    (* get clauses and prepare them for writing *)
   5.113 -    val (ctxt, (chain_ths, th)) = goal;
   5.114 -    val thy = ProofContext.theory_of ctxt;
   5.115 -    val chain_ths = map (Thm.put_name_hint chained_hint) chain_ths;
   5.116 -    val goal_cls = #1 (neg_conjecture_clauses ctxt th subgoal);
   5.117 -    val the_filtered_clauses =
   5.118 -      (case filtered_clauses of
   5.119 -        NONE => get_facts relevance_override goal goal_cls
   5.120 -      | SOME fcls => fcls);
   5.121 -    val the_axiom_clauses =
   5.122 -      (case axiom_clauses of
   5.123 -        NONE => the_filtered_clauses
   5.124 -      | SOME axcls => axcls);
   5.125 -    val (internal_thm_names, clauses) =
   5.126 -      prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy;
   5.127 -
   5.128 -    (* path to unique problem file *)
   5.129 -    val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
   5.130 -                       else Config.get ctxt dest_dir;
   5.131 -    val the_problem_prefix = Config.get ctxt problem_prefix;
   5.132 -    fun prob_pathname nr =
   5.133 -      let
   5.134 -        val probfile =
   5.135 -          Path.basic (the_problem_prefix ^
   5.136 -                      (if overlord then "_" ^ name else serial_string ())
   5.137 -                      ^ "_" ^ string_of_int nr)
   5.138 -      in
   5.139 -        if the_dest_dir = "" then File.tmp_path probfile
   5.140 -        else if File.exists (Path.explode the_dest_dir)
   5.141 -        then Path.append (Path.explode the_dest_dir) probfile
   5.142 -        else error ("No such directory: " ^ the_dest_dir ^ ".")
   5.143 -      end;
   5.144 -
   5.145 -    val command = Path.explode (home ^ "/" ^ executable)
   5.146 -    (* write out problem file and call prover *)
   5.147 -    fun command_line probfile =
   5.148 -      (if Config.get ctxt measure_runtime then
   5.149 -         "TIMEFORMAT='%3U'; { time " ^
   5.150 -         space_implode " " [File.shell_path command, args,
   5.151 -                            File.shell_path probfile] ^ " ; } 2>&1"
   5.152 -       else
   5.153 -         space_implode " " ["exec", File.shell_path command, args,
   5.154 -                            File.shell_path probfile, "2>&1"]) ^
   5.155 -      (if overlord then
   5.156 -         " | sed 's/,/, /g' \
   5.157 -         \| sed 's/\\([^!=]\\)\\([=|]\\)\\([^=]\\)/\\1 \\2 \\3/g' \
   5.158 -         \| sed 's/! =/ !=/g' \
   5.159 -         \| sed 's/  / /g' | sed 's/| |/||/g' \
   5.160 -         \| sed 's/ = = =/===/g' \
   5.161 -         \| sed 's/= = /== /g'"
   5.162 -       else
   5.163 -         "")
   5.164 -    fun split_time s =
   5.165 -      let
   5.166 -        val split = String.tokens (fn c => str c = "\n");
   5.167 -        val (output, t) = s |> split |> split_last |> apfst cat_lines;
   5.168 -        fun as_num f = f >> (fst o read_int);
   5.169 -        val num = as_num (Scan.many1 Symbol.is_ascii_digit);
   5.170 -        val digit = Scan.one Symbol.is_ascii_digit;
   5.171 -        val num3 = as_num (digit ::: digit ::: (digit >> single));
   5.172 -        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
   5.173 -        val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
   5.174 -      in (output, as_time t) end;
   5.175 -    fun split_time' s =
   5.176 -      if Config.get ctxt measure_runtime then split_time s else (s, 0)
   5.177 -    fun run_on probfile =
   5.178 -      if File.exists command then
   5.179 -        write_file full_types explicit_apply probfile clauses
   5.180 -        |> pair (apfst split_time' (bash_output (command_line probfile)))
   5.181 -      else error ("Bad executable: " ^ Path.implode command ^ ".");
   5.182 -
   5.183 -    (* If the problem file has not been exported, remove it; otherwise, export
   5.184 -       the proof file too. *)
   5.185 -    fun cleanup probfile =
   5.186 -      if the_dest_dir = "" then try File.rm probfile else NONE
   5.187 -    fun export probfile (((output, _), _), _) =
   5.188 -      if the_dest_dir = "" then
   5.189 -        ()
   5.190 -      else
   5.191 -        File.write (Path.explode (Path.implode probfile ^ "_proof"))
   5.192 -                   ((if overlord then
   5.193 -                       "% " ^ command_line probfile ^ "\n% " ^ timestamp () ^
   5.194 -                       "\n"
   5.195 -                     else
   5.196 -                        "") ^ output)
   5.197 -
   5.198 -    val (((output, atp_run_time_in_msecs), res_code), _) =
   5.199 -      with_path cleanup export run_on (prob_pathname subgoal);
   5.200 -
   5.201 -    (* Check for success and print out some information on failure. *)
   5.202 -    val (proof, outcome) =
   5.203 -      extract_proof_and_outcome res_code proof_delims known_failures output
   5.204 -    val (message, relevant_thm_names) =
   5.205 -      case outcome of
   5.206 -        NONE => proof_text isar_proof debug modulus sorts ctxt
   5.207 -                           (minimize_command, proof, internal_thm_names, th,
   5.208 -                            subgoal)
   5.209 -      | SOME failure => (string_for_failure failure ^ "\n", [])
   5.210 -  in
   5.211 -    {outcome = outcome, message = message,
   5.212 -     relevant_thm_names = relevant_thm_names,
   5.213 -     atp_run_time_in_msecs = atp_run_time_in_msecs, output = output,
   5.214 -     proof = proof, internal_thm_names = internal_thm_names,
   5.215 -     filtered_clauses = the_filtered_clauses}
   5.216 -  end;
   5.217 -
   5.218 -
   5.219 -(* generic TPTP-based provers *)
   5.220 -
   5.221 -fun generic_tptp_prover
   5.222 -        (name, {home, executable, arguments, proof_delims, known_failures,
   5.223 -                max_new_clauses, prefers_theory_relevant})
   5.224 -        (params as {debug, overlord, respect_no_atp, relevance_threshold,
   5.225 -                    convergence, theory_relevant, higher_order, follow_defs,
   5.226 -                    isar_proof, ...})
   5.227 -        minimize_command timeout =
   5.228 -  generic_prover overlord
   5.229 -      (get_relevant_facts respect_no_atp relevance_threshold convergence
   5.230 -                          higher_order follow_defs max_new_clauses
   5.231 -                          (the_default prefers_theory_relevant theory_relevant))
   5.232 -      (prepare_clauses higher_order false)
   5.233 -      (write_tptp_file (debug andalso overlord andalso not isar_proof)) home
   5.234 -      executable (arguments timeout) proof_delims known_failures name params
   5.235 -      minimize_command
   5.236 -
   5.237 -fun tptp_prover name p = (name, generic_tptp_prover (name, p));
   5.238 -
   5.239 -
   5.240 -(** common provers **)
   5.241 -
   5.242 -fun generous_to_secs time = (Time.toMilliseconds time + 999) div 1000
   5.243 -
   5.244 -(* Vampire *)
   5.245 -
   5.246 -(* Vampire requires an explicit time limit. *)
   5.247 -
   5.248 -val vampire_config : prover_config =
   5.249 -  {home = getenv "VAMPIRE_HOME",
   5.250 -   executable = "vampire",
   5.251 -   arguments = (fn timeout => "--output_syntax tptp --mode casc -t " ^
   5.252 -                              string_of_int (generous_to_secs timeout)),
   5.253 -   proof_delims = [("=========== Refutation ==========",
   5.254 -                    "======= End of refutation =======")],
   5.255 -   known_failures =
   5.256 -     [(Unprovable, "Satisfiability detected"),
   5.257 -      (OutOfResources, "CANNOT PROVE"),
   5.258 -      (OutOfResources, "Refutation not found")],
   5.259 -   max_new_clauses = 60,
   5.260 -   prefers_theory_relevant = false}
   5.261 -val vampire = tptp_prover "vampire" vampire_config
   5.262 -
   5.263 -
   5.264 -(* E prover *)
   5.265 -
   5.266 -val tstp_proof_delims =
   5.267 -  ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
   5.268 -
   5.269 -val e_config : prover_config =
   5.270 -  {home = getenv "E_HOME",
   5.271 -   executable = "eproof",
   5.272 -   arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev \
   5.273 -                              \-tAutoDev --silent --cpu-limit=" ^
   5.274 -                              string_of_int (generous_to_secs timeout)),
   5.275 -   proof_delims = [tstp_proof_delims],
   5.276 -   known_failures =
   5.277 -     [(Unprovable, "SZS status: Satisfiable"),
   5.278 -      (Unprovable, "SZS status Satisfiable"),
   5.279 -      (TimedOut, "Failure: Resource limit exceeded (time)"),
   5.280 -      (TimedOut, "time limit exceeded"),
   5.281 -      (OutOfResources,
   5.282 -       "# Cannot determine problem status within resource limit"),
   5.283 -      (OutOfResources, "SZS status: ResourceOut"),
   5.284 -      (OutOfResources, "SZS status ResourceOut")],
   5.285 -   max_new_clauses = 100,
   5.286 -   prefers_theory_relevant = false}
   5.287 -val e = tptp_prover "e" e_config
   5.288 -
   5.289 -
   5.290 -(* SPASS *)
   5.291 -
   5.292 -fun generic_dfg_prover
   5.293 -        (name, {home, executable, arguments, proof_delims, known_failures,
   5.294 -                max_new_clauses, prefers_theory_relevant})
   5.295 -        (params as {overlord, respect_no_atp, relevance_threshold, convergence,
   5.296 -                    theory_relevant, higher_order, follow_defs, ...})
   5.297 -        minimize_command timeout =
   5.298 -  generic_prover overlord
   5.299 -      (get_relevant_facts respect_no_atp relevance_threshold convergence
   5.300 -                          higher_order follow_defs max_new_clauses
   5.301 -                          (the_default prefers_theory_relevant theory_relevant))
   5.302 -      (prepare_clauses higher_order true) write_dfg_file home executable
   5.303 -      (arguments timeout) proof_delims known_failures name params
   5.304 -      minimize_command
   5.305 -
   5.306 -fun dfg_prover name p = (name, generic_dfg_prover (name, p))
   5.307 -
   5.308 -(* The "-VarWeight=3" option helps the higher-order problems, probably by
   5.309 -   counteracting the presence of "hAPP". *)
   5.310 -val spass_config : prover_config =
   5.311 -  {home = getenv "SPASS_HOME",
   5.312 -   executable = "SPASS",
   5.313 -   arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
   5.314 -     " -FullRed=0 -DocProof -VarWeight=3 -TimeLimit=" ^
   5.315 -     string_of_int (generous_to_secs timeout)),
   5.316 -   proof_delims = [("Here is a proof", "Formulae used in the proof")],
   5.317 -   known_failures =
   5.318 -     [(Unprovable, "SPASS beiseite: Completion found"),
   5.319 -      (TimedOut, "SPASS beiseite: Ran out of time"),
   5.320 -      (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded")],
   5.321 -   max_new_clauses = 40,
   5.322 -   prefers_theory_relevant = true}
   5.323 -val spass = dfg_prover "spass" spass_config
   5.324 -
   5.325 -(* SPASS 3.7 supports both the DFG and the TPTP syntax, whereas SPASS 3.0
   5.326 -   supports only the DFG syntax. As soon as all Isabelle repository/snapshot
   5.327 -   users have upgraded to 3.7, we can kill "spass" (and all DFG support in
   5.328 -   Sledgehammer) and rename "spass_tptp" "spass". *)
   5.329 -
   5.330 -(* FIXME: Change the error message below to point to the Isabelle download
   5.331 -   page once the package is there (around the Isabelle2010 release). *)
   5.332 -
   5.333 -val spass_tptp_config =
   5.334 -  {home = #home spass_config,
   5.335 -   executable = #executable spass_config,
   5.336 -   arguments = prefix "-TPTP " o #arguments spass_config,
   5.337 -   proof_delims = #proof_delims spass_config,
   5.338 -   known_failures =
   5.339 -     #known_failures spass_config @
   5.340 -     [(OldSpass, "unrecognized option `-TPTP'"),
   5.341 -      (OldSpass, "Unrecognized option TPTP")],
   5.342 -   max_new_clauses = #max_new_clauses spass_config,
   5.343 -   prefers_theory_relevant = #prefers_theory_relevant spass_config}
   5.344 -val spass_tptp = tptp_prover "spass_tptp" spass_tptp_config
   5.345 -
   5.346 -(* remote prover invocation via SystemOnTPTP *)
   5.347 -
   5.348 -val systems = Synchronized.var "atp_systems" ([]: string list);
   5.349 -
   5.350 -fun get_systems () =
   5.351 -  case bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" of
   5.352 -    (answer, 0) => split_lines answer
   5.353 -  | (answer, _) =>
   5.354 -    error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer)
   5.355 -
   5.356 -fun refresh_systems_on_tptp () =
   5.357 -  Synchronized.change systems (fn _ => get_systems ());
   5.358 -
   5.359 -fun get_system prefix = Synchronized.change_result systems (fn systems =>
   5.360 -  (if null systems then get_systems () else systems)
   5.361 -  |> `(find_first (String.isPrefix prefix)));
   5.362 -
   5.363 -fun the_system prefix =
   5.364 -  (case get_system prefix of
   5.365 -    NONE => error ("System " ^ quote prefix ^
   5.366 -                   " not available at SystemOnTPTP.")
   5.367 -  | SOME sys => sys);
   5.368 -
   5.369 -val remote_known_failures =
   5.370 -  [(TimedOut, "says Timeout"),
   5.371 -   (MalformedOutput, "Remote-script could not extract proof")]
   5.372 -
   5.373 -fun remote_prover_config prover_prefix args
   5.374 -        ({proof_delims, known_failures, max_new_clauses,
   5.375 -          prefers_theory_relevant, ...} : prover_config) : prover_config =
   5.376 -  {home = getenv "ISABELLE_ATP_MANAGER",
   5.377 -   executable = "SystemOnTPTP",
   5.378 -   arguments = (fn timeout =>
   5.379 -     args ^ " -t " ^ string_of_int (generous_to_secs timeout) ^ " -s " ^
   5.380 -     the_system prover_prefix),
   5.381 -   proof_delims = insert (op =) tstp_proof_delims proof_delims,
   5.382 -   known_failures = remote_known_failures @ known_failures,
   5.383 -   max_new_clauses = max_new_clauses,
   5.384 -   prefers_theory_relevant = prefers_theory_relevant}
   5.385 -
   5.386 -val remote_vampire =
   5.387 -  tptp_prover (remotify (fst vampire))
   5.388 -              (remote_prover_config "Vampire---9" "" vampire_config)
   5.389 -
   5.390 -val remote_e =
   5.391 -  tptp_prover (remotify (fst e))
   5.392 -              (remote_prover_config "EP---" "" e_config)
   5.393 -
   5.394 -val remote_spass =
   5.395 -  tptp_prover (remotify (fst spass))
   5.396 -              (remote_prover_config "SPASS---" "-x" spass_config)
   5.397 -
   5.398 -fun maybe_remote (name, _) ({home, ...} : prover_config) =
   5.399 -  name |> home = "" ? remotify
   5.400 -
   5.401 -fun default_atps_param_value () =
   5.402 -  space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
   5.403 -                     remotify (fst vampire)]
   5.404 -
   5.405 -val provers =
   5.406 -  [spass, spass_tptp, vampire, e, remote_vampire, remote_spass, remote_e]
   5.407 -val prover_setup = fold add_prover provers
   5.408 -
   5.409 -val setup =
   5.410 -  dest_dir_setup
   5.411 -  #> problem_prefix_setup
   5.412 -  #> measure_runtime_setup
   5.413 -  #> prover_setup
   5.414 -
   5.415 -end;