# HG changeset patch
# User blanchet
# Date 1559898509 -7200
# Node ID c04d4951a155c7fd9044033129ad7f2d70433b8c
# Parent  aa7c49651f4ec93b2f13766993f9b0f2a518d3ef
handle timeouts gracefully in 'smt' proof method (patch due to Mathias Fleury)

diff -r aa7c49651f4e -r c04d4951a155 src/HOL/Tools/SMT/smt_solver.ML
--- 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>
diff -r aa7c49651f4e -r c04d4951a155 src/HOL/Tools/SMT/smt_systems.ML
--- 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 }