# HG changeset patch # User boehmes # Date 1289856248 -3600 # Node ID bbcb7aa90afc7530392be2d69afb7dc883571f67 # Parent 0125cbb5d3c7828a9e23e1a1499ca8407cc5a0f4# Parent 9597b93a8c00ae77dd1936434b755d1b0e5eb420 merged diff -r 9597b93a8c00 -r bbcb7aa90afc src/HOL/Tools/SMT/smt_failure.ML --- a/src/HOL/Tools/SMT/smt_failure.ML Mon Nov 15 22:08:01 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_failure.ML Mon Nov 15 22:24:08 2010 +0100 @@ -10,7 +10,7 @@ Counterexample of bool * term list | Time_Out | Out_Of_Memory | - Solver_Crashed of int | + Abnormal_Termination of int | Other_Failure of string val string_of_failure: Proof.context -> failure -> string exception SMT of failure @@ -23,7 +23,7 @@ Counterexample of bool * term list | Time_Out | Out_Of_Memory | - Solver_Crashed of int | + Abnormal_Termination of int | Other_Failure of string fun string_of_failure ctxt (Counterexample (real, ex)) = @@ -38,8 +38,8 @@ end | string_of_failure _ Time_Out = "Timed out" | string_of_failure _ Out_Of_Memory = "Ran out of memory" - | string_of_failure _ (Solver_Crashed err) = - "Solver crashed with error code " ^ string_of_int err + | string_of_failure _ (Abnormal_Termination err) = + "Solver terminated abnormally with error code " ^ string_of_int err | string_of_failure _ (Other_Failure msg) = msg exception SMT of failure diff -r 9597b93a8c00 -r bbcb7aa90afc src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Mon Nov 15 22:08:01 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_solver.ML Mon Nov 15 22:24:08 2010 +0100 @@ -138,7 +138,7 @@ val _ = C.trace_msg ctxt (pretty "Result:") ls val _ = null ls andalso return_code <> 0 andalso - raise SMT_Failure.SMT (SMT_Failure.Solver_Crashed return_code) + raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code) in ls end end @@ -308,7 +308,7 @@ val ctxt = Proof.context_of st |> Config.put C.oracle false - |> Config.put C.timeout (Real.fromInt (Time.toSeconds time_limit)) + |> Config.put C.timeout (Time.toReal time_limit) |> Config.put C.drop_bad_facts true |> Config.put C.filter_only_facts true val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal diff -r 9597b93a8c00 -r bbcb7aa90afc src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Nov 15 22:08:01 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Nov 15 22:24:08 2010 +0100 @@ -409,14 +409,14 @@ run_time_in_msecs = msecs} end -(* "SMT_Failure.Solver_Crashed" is a misnomer; it should really be called - "Abnormal_Termination". Return codes 1 to 127 are application-specific, - whereas (at least on Unix) 128 to 255 are reserved for signals (e.g., - SIGSEGV) and other system codes. *) +(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. + Return codes 1 to 127 are application-specific, whereas (at least on + Unix) 128 to 255 are reserved for signals (e.g., SIGSEGV) and other + system codes. *) fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut - | failure_from_smt_failure (SMT_Failure.Solver_Crashed code) = + | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) = if code >= 128 then Crashed else IncompleteUnprovable | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources | failure_from_smt_failure _ = UnknownError @@ -469,7 +469,7 @@ NONE => false | SOME (SMT_Failure.Counterexample _) => false | SOME SMT_Failure.Time_Out => iter_timeout <> timeout - | SOME (SMT_Failure.Solver_Crashed code) => + | SOME (SMT_Failure.Abnormal_Termination code) => (if verbose then "The SMT solver invoked with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " terminated abnormally with \ @@ -512,7 +512,7 @@ command_call smtN (map fst used_facts)) ^ minimize_line minimize_command (map fst used_facts) | SOME SMT_Failure.Time_Out => "Timed out." - | SOME (SMT_Failure.Solver_Crashed code) => + | SOME (SMT_Failure.Abnormal_Termination code) => "The SMT solver terminated abnormally with exit code " ^ string_of_int code ^ "." | SOME (SMT_Failure.Counterexample _) => "The SMT problem is unprovable."