# HG changeset patch # User blanchet # Date 1277285763 -7200 # Node ID b147d01b8ebc53564272d7ede7ab0cced99a102d # Parent 4dca51ef0285e0f6c792232b88ffc5b3958d5f6a if SPASS fails at finding a proof with the SOS option turned on, turn it off and try again diff -r 4dca51ef0285 -r b147d01b8ebc src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Wed Jun 23 10:20:54 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Wed Jun 23 11:36:03 2010 +0200 @@ -49,7 +49,7 @@ type prover_config = {home_var: string, executable: string, - arguments: Time.time -> string, + arguments: bool -> Time.time -> string, proof_delims: (string * string) list, known_failures: (failure * string) list, max_axiom_clauses: int, @@ -77,7 +77,8 @@ handle Option.Option => "") | _ => "" -fun extract_proof_and_outcome res_code proof_delims known_failures output = +fun extract_proof_and_outcome complete res_code proof_delims known_failures + output = case map_filter (fn (failure, pattern) => if String.isSubstring pattern output then SOME failure else NONE) known_failures of @@ -85,7 +86,11 @@ "" => ("", SOME UnknownError) | proof => if res_code = 0 then (proof, NONE) else ("", SOME UnknownError)) - | (failure :: _) => ("", SOME failure) + | (failure :: _) => + ("", SOME (if failure = IncompleteUnprovable andalso complete then + Unprovable + else + failure)) fun string_for_failure Unprovable = "The ATP problem is unprovable." | string_for_failure IncompleteUnprovable = @@ -165,22 +170,24 @@ val home = getenv home_var val command = Path.explode (home ^ "/" ^ executable) (* write out problem file and call prover *) - fun command_line probfile = - (if Config.get ctxt measure_runtime then - "TIMEFORMAT='%3U'; { time " ^ - space_implode " " [File.shell_path command, arguments timeout, - File.shell_path probfile] ^ " ; } 2>&1" - else - space_implode " " ["exec", File.shell_path command, arguments timeout, - File.shell_path probfile, "2>&1"]) ^ - (if overlord then - " | sed 's/,/, /g' \ - \| sed 's/\\([^!=<]\\)\\([=|]\\)\\([^=>]\\)/\\1 \\2 \\3/g' \ - \| sed 's/ / /g' | sed 's/| |/||/g' \ - \| sed 's/ = = =/===/g' \ - \| sed 's/= = /== /g'" - else - "") + fun command_line complete probfile = + let + val core = File.shell_path command ^ " " ^ arguments complete timeout ^ + " " ^ File.shell_path probfile + in + (if Config.get ctxt measure_runtime then + "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }" + else + "exec " ^ core) ^ " 2>&1" ^ + (if overlord then + " | sed 's/,/, /g' \ + \| sed 's/\\([^!=<]\\)\\([=|]\\)\\([^=>]\\)/\\1 \\2 \\3/g' \ + \| sed 's/ / /g' | sed 's/| |/||/g' \ + \| sed 's/ = = =/===/g' \ + \| sed 's/= = /== /g'" + else + "") + end fun split_time s = let val split = String.tokens (fn c => str c = "\n"); @@ -192,13 +199,36 @@ val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b); val as_time = the_default 0 o Scan.read Symbol.stopper time o explode; in (output, as_time t) end; - val split_time' = - if Config.get ctxt measure_runtime then split_time else rpair 0 fun run_on probfile = if File.exists command then - write_tptp_file (debug andalso overlord) full_types explicit_apply - probfile clauses - |> pair (apfst split_time' (bash_output (command_line probfile))) + let + fun do_run complete = + let + val command = command_line complete probfile + val ((output, msecs), res_code) = + bash_output command + |>> (if overlord then + prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") + else + I) + |>> (if Config.get ctxt measure_runtime then split_time + else rpair 0) + val (proof, outcome) = + extract_proof_and_outcome complete res_code proof_delims + known_failures output + in (output, msecs, proof, outcome) end + val (pool, conjecture_offset) = + write_tptp_file (debug andalso overlord) full_types explicit_apply + probfile clauses + val conjecture_shape = shape_of_clauses (conjecture_offset + 1) goal_clss + val result = + do_run false + |> (fn (_, msecs0, _, SOME IncompleteUnprovable) => + do_run true + |> (fn (output, msecs, proof, outcome) => + (output, msecs0 + msecs, proof, outcome)) + | result => result) + in ((pool, conjecture_shape), result) end else if home = "" then error ("The environment variable " ^ quote home_var ^ " is not set.") else @@ -208,24 +238,15 @@ the proof file too. *) fun cleanup probfile = if the_dest_dir = "" then try File.rm probfile else NONE - fun export probfile (((output, _), _), _) = + fun export probfile (_, (output, _, _, _)) = if the_dest_dir = "" then () else - File.write (Path.explode (Path.implode probfile ^ "_proof")) - ((if overlord then - "% " ^ command_line probfile ^ "\n% " ^ timestamp () ^ - "\n" - else - "") ^ output) + File.write (Path.explode (Path.implode probfile ^ "_proof")) output - val (((output, atp_run_time_in_msecs), res_code), - (pool, conjecture_offset)) = - with_path cleanup export run_on (prob_pathname subgoal); - val conjecture_shape = shape_of_clauses (conjecture_offset + 1) goal_clss - (* Check for success and print out some information on failure. *) - val (proof, outcome) = - extract_proof_and_outcome res_code proof_delims known_failures output + val ((pool, conjecture_shape), (output, msecs, proof, outcome)) = + with_path cleanup export run_on (prob_pathname subgoal) + val (message, relevant_thm_names) = case outcome of NONE => @@ -236,9 +257,8 @@ | SOME failure => (string_for_failure failure ^ "\n", []) in {outcome = outcome, message = message, pool = pool, - relevant_thm_names = relevant_thm_names, - atp_run_time_in_msecs = atp_run_time_in_msecs, output = output, - proof = proof, internal_thm_names = internal_thm_names, + relevant_thm_names = relevant_thm_names, atp_run_time_in_msecs = msecs, + output = output, proof = proof, internal_thm_names = internal_thm_names, conjecture_shape = conjecture_shape, filtered_clauses = the_filtered_clauses} end @@ -255,7 +275,7 @@ val e_config : prover_config = {home_var = "E_HOME", executable = "eproof", - arguments = fn timeout => + arguments = fn _ => fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_generous_secs timeout), proof_delims = [tstp_proof_delims], @@ -278,9 +298,10 @@ val spass_config : prover_config = {home_var = "SPASS_HOME", executable = "SPASS", - arguments = fn timeout => - "-TPTP -Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ - \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout), + arguments = fn complete => fn timeout => + ("-TPTP -Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ + \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout)) + |> not complete ? prefix "-SOS=1 ", proof_delims = [("Here is a proof", "Formulae used in the proof")], known_failures = [(IncompleteUnprovable, "SPASS beiseite: Completion found"), @@ -299,7 +320,7 @@ val vampire_config : prover_config = {home_var = "VAMPIRE_HOME", executable = "vampire", - arguments = fn timeout => + arguments = fn _ => fn timeout => "--output_syntax tptp --mode casc -t " ^ string_of_int (to_generous_secs timeout), proof_delims = @@ -346,7 +367,7 @@ prefers_theory_relevant, ...} : prover_config) : prover_config = {home_var = "ISABELLE_ATP_MANAGER", executable = "SystemOnTPTP", - arguments = fn timeout => + arguments = fn _ => fn timeout => args ^ " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^ the_system atp_prefix, proof_delims = insert (op =) tstp_proof_delims proof_delims,