# HG changeset patch
# User boehmes
# Date 1297676443 -3600
# Node ID 2dc75bae522657a0b730289ca71e61134940d728
# Parent  bf49b7a8593600e3ecfb599baf09d4cf22c9924d
more explicit errors to inform users about problems related to SMT solvers;
fall back to remote SMT solver (if local version does not exist);
extend the Z3 proof parser to accommodate for slight changes introduced by Z3 2.18

diff -r bf49b7a85936 -r 2dc75bae5226 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Sun Feb 13 17:45:21 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Mon Feb 14 10:40:43 2011 +0100
@@ -23,6 +23,7 @@
   (*options*)
   val oracle: bool Config.T
   val datatypes: bool Config.T
+  val timeoutN: string
   val timeout: real Config.T
   val random_seed: int Config.T
   val fixed: bool Config.T
diff -r bf49b7a85936 -r 2dc75bae5226 src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Sun Feb 13 17:45:21 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Mon Feb 14 10:40:43 2011 +0100
@@ -20,14 +20,17 @@
 fun make_local_avail name () = getenv (name ^ "_INSTALLED") = "yes"
 fun make_remote_avail name () = getenv (name ^ "_REMOTE_SOLVER") <> ""
 fun make_avail is_remote name =
-  if is_remote then make_remote_avail name else make_local_avail name
+  if is_remote then make_remote_avail name
+  else make_local_avail name orf make_remote_avail name
 
 fun make_local_command name () = [getenv (name ^ "_SOLVER")]
 fun make_remote_command name () =
   [getenv "ISABELLE_SMT_REMOTE", getenv (name ^ "_REMOTE_SOLVER")]
 fun make_command is_remote name =
   if is_remote then make_remote_command name
-  else make_local_command name
+  else (fn () =>
+    if make_local_avail name () then make_local_command name ()
+    else make_remote_command name ())
 
 fun outcome_of unsat sat unknown solver_name line =
   if String.isPrefix unsat line then SMT_Solver.Unsat
diff -r bf49b7a85936 -r 2dc75bae5226 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Sun Feb 13 17:45:21 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon Feb 14 10:40:43 2011 +0100
@@ -343,8 +343,11 @@
     handle
       SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) =>
         (SMT_Config.verbose_msg ctxt (str_of ctxt) fail; NONE)
-    | SMT_Failure.SMT fail =>
-        (SMT_Config.trace_msg ctxt (str_of ctxt) fail; NONE)
+    | SMT_Failure.SMT (fail as SMT_Failure.Time_Out) =>
+        error ("SMT: Solver " ^ quote (SMT_Config.solver_of ctxt) ^ ": " ^
+          SMT_Failure.string_of_failure ctxt fail ^ " (setting the " ^
+          "configuration option " ^ SMT_Config.timeoutN ^ " might help)")
+    | SMT_Failure.SMT fail => error (str_of ctxt fail)
 
   fun tag_rules thms = map_index (apsnd (pair NONE)) thms
   fun tag_prems thms = map (pair ~1 o pair NONE) thms
diff -r bf49b7a85936 -r 2dc75bae5226 src/HOL/Tools/SMT/z3_interface.ML
--- a/src/HOL/Tools/SMT/z3_interface.ML	Sun Feb 13 17:45:21 2011 +0100
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Mon Feb 14 10:40:43 2011 +0100
@@ -203,7 +203,8 @@
   | (Sym ("iff", _), [ct, cu]) => SOME (mk_iff ct cu)
   | (Sym ("~", _), [ct, cu]) => SOME (mk_iff ct cu)
   | (Sym ("xor", _), [ct, cu]) => SOME (mk_not (mk_iff ct cu))
-  | (Sym ("ite", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3)
+  | (Sym ("if", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3)
+  | (Sym ("ite", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3) (* FIXME: remove *)
   | (Sym ("=", _), [ct, cu]) => SOME (mk_eq ct cu)
   | (Sym ("distinct", _), _) => SOME (mk_distinct cts)
   | (Sym ("select", _), [ca, ck]) => SOME (Thm.capply (mk_access ca) ck)