--- a/src/HOL/Tools/SMT/smt_solver.ML Tue Jun 04 20:49:33 2019 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Fri Jun 07 11:08:29 2019 +0200
@@ -7,7 +7,7 @@
signature SMT_SOLVER =
sig
(*configuration*)
- datatype outcome = Unsat | Sat | Unknown
+ datatype outcome = Unsat | Sat | Unknown | Time_Out
type parsed_proof =
{outcome: SMT_Failure.failure option,
@@ -138,7 +138,7 @@
(* configuration *)
-datatype outcome = Unsat | Sat | Unknown
+datatype outcome = Unsat | Sat | Unknown | Time_Out
type parsed_proof =
{outcome: SMT_Failure.failure option,
@@ -198,6 +198,7 @@
(case parse_proof0 of
SOME pp => pp outer_ctxt replay_data xfacts prems concl lines
| NONE => {outcome = NONE, fact_ids = NONE, atp_proof = K []})
+ | (Time_Out, _) => raise SMT_Failure.SMT (SMT_Failure.Time_Out)
| (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat)))
fun replay outcome replay0 oracle outer_ctxt
@@ -211,6 +212,7 @@
SOME replay => replay outer_ctxt replay_data lines
| NONE => error "No proof reconstruction for solver -- \
\declare [[smt_oracle]] to allow oracle")
+ | (Time_Out, _) => raise SMT_Failure.SMT (SMT_Failure.Time_Out)
| (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat)))
val cfalse = Thm.cterm_of \<^context> \<^prop>\<open>False\<close>
--- a/src/HOL/Tools/SMT/smt_systems.ML Tue Jun 04 20:49:33 2019 +0200
+++ b/src/HOL/Tools/SMT/smt_systems.ML Fri Jun 07 11:08:29 2019 +0200
@@ -19,10 +19,11 @@
fun make_command name () = [getenv (name ^ "_SOLVER")]
-fun outcome_of unsat sat unknown solver_name line =
+fun outcome_of unsat sat unknown timeout solver_name line =
if String.isPrefix unsat line then SMT_Solver.Unsat
else if String.isPrefix sat line then SMT_Solver.Sat
else if String.isPrefix unknown line then SMT_Solver.Unknown
+ else if String.isPrefix timeout line then SMT_Solver.Time_Out
else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^ quote solver_name ^
" failed -- enable tracing using the " ^ quote (Config.name_of SMT_Config.trace) ^
" option for details"))
@@ -56,7 +57,7 @@
options = cvc3_options,
smt_options = [],
default_max_relevant = 400 (* FUDGE *),
- outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
+ outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
parse_proof = NONE,
replay = NONE }
@@ -96,7 +97,7 @@
options = cvc4_options,
smt_options = [(":produce-unsat-cores", "true")],
default_max_relevant = 400 (* FUDGE *),
- outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
+ outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
parse_proof = SOME (K CVC4_Proof_Parse.parse_proof),
replay = NONE }
@@ -127,7 +128,7 @@
"--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]),
smt_options = [(":produce-proofs", "true")],
default_max_relevant = 200 (* FUDGE *),
- outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown"),
+ outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "timeout"),
parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
replay = SOME Verit_Replay.replay }
@@ -157,7 +158,7 @@
options = z3_options,
smt_options = [(":produce-proofs", "true")],
default_max_relevant = 350 (* FUDGE *),
- outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
+ outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
parse_proof = SOME Z3_Replay.parse_proof,
replay = SOME Z3_Replay.replay }