# HG changeset patch
# User boehmes
# Date 1257256315 -3600
# Node ID 1312e8337ce5b758ff7b97ec19c7cae6af7581c8
# Parent  ab2f6574a2a6cfb01f90f1bf64a338d44b0f76c9
added a specific SMT exception captured by smt_tac (prevents the SMT method from failing with an exception),
replaced unspecific 'error' invocations with raising of specific SMT exceptions,
added annotations to traced SMT problem and solver output

diff -r ab2f6574a2a6 -r 1312e8337ce5 src/HOL/SMT/Tools/cvc3_solver.ML
--- a/src/HOL/SMT/Tools/cvc3_solver.ML	Tue Nov 03 14:07:38 2009 +0100
+++ b/src/HOL/SMT/Tools/cvc3_solver.ML	Tue Nov 03 14:51:55 2009 +0100
@@ -21,10 +21,7 @@
 val is_unsat = String.isPrefix "Unsatisfiable."
 val is_unknown = String.isPrefix "Unknown."
 
-fun cex_kind true = "Counterexample"
-  | cex_kind false = "Possible counterexample"
-
-fun raise_cex real = error (cex_kind real ^ " found.")
+fun raise_cex real = raise SMT_Solver.SMT_COUNTEREXAMPLE (real, [])
 
 fun core_oracle ({context, output, recon, ...} : SMT_Solver.proof_data) =
   let
@@ -35,7 +32,7 @@
     if is_unsat l then @{cprop False}
     else if is_sat l then raise_cex true
     else if is_unknown l then raise_cex false
-    else error (solver_name ^ " failed")
+    else raise SMT_Solver.SMT (solver_name ^ " failed")
   end
 
 fun smtlib_solver oracle _ = {
diff -r ab2f6574a2a6 -r 1312e8337ce5 src/HOL/SMT/Tools/smt_solver.ML
--- a/src/HOL/SMT/Tools/smt_solver.ML	Tue Nov 03 14:07:38 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Tue Nov 03 14:51:55 2009 +0100
@@ -6,6 +6,7 @@
 
 signature SMT_SOLVER =
 sig
+  exception SMT of string
   exception SMT_COUNTEREXAMPLE of bool * term list
 
   type interface = {
@@ -53,6 +54,7 @@
 structure SMT_Solver: SMT_SOLVER =
 struct
 
+exception SMT of string
 exception SMT_COUNTEREXAMPLE of bool * term list
 
 
@@ -79,7 +81,7 @@
 
 fun with_timeout ctxt f x =
   TimeLimit.timeLimit (Time.fromSeconds (Config.get ctxt timeout)) f x
-  handle TimeLimit.TimeOut => error ("SMT: timeout")
+  handle TimeLimit.TimeOut => raise SMT "timeout"
 
 val (trace, setup_trace) = Attrib.config_bool "smt_trace" false
 
@@ -112,13 +114,17 @@
 
 fun run in_path out_path (ctxt, cmd, output) =
   let
+    fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
+      (map Pretty.str ls))
+
     val x = File.open_output output in_path
-    val _ = trace_msg ctxt File.read in_path
+    val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines o File.read)
+      in_path
 
     val _ = with_timeout ctxt system_out (cmd in_path out_path)
     fun lines_of path = the_default [] (try (File.fold_lines cons out_path) [])
     val ls = rev (dropwhile (equal "") (lines_of out_path))
-    val _ = trace_msg ctxt cat_lines ls
+    val _ = trace_msg ctxt (pretty "SMT result:") ls
   in (x, ls) end
 
 in
@@ -206,28 +212,34 @@
 
 (* SMT tactic *)
 
-fun smt_unsat_tac solver ctxt rules =
+local
+  fun pretty_cex ctxt (real, ex) =
+    let
+      val msg = if real then "SMT: counterexample found"
+        else "SMT: potential counterexample found"
+    in
+      if null ex then msg ^ "."
+      else Pretty.string_of (Pretty.big_list (msg ^ ":")
+        (map (Syntax.pretty_term ctxt) ex))
+    end
+
+  fun fail_tac ctxt msg st = (trace_msg ctxt I msg; Tactical.no_tac st)
+
+  fun SAFE pass_exns tac ctxt i st =
+    if pass_exns then tac ctxt i st
+    else (tac ctxt i st
+      handle SMT msg => fail_tac ctxt ("SMT: " ^ msg) st
+           | SMT_COUNTEREXAMPLE cex => fail_tac ctxt (pretty_cex ctxt cex) st)
+
+  fun smt_solver rules ctxt = solver_of (Context.Proof ctxt) ctxt rules
+in
+fun smt_tac' pass_exns ctxt rules =
   Tactic.rtac @{thm ccontr} THEN'
   SUBPROOF (fn {context, prems, ...} =>
-    Tactic.rtac (solver context (rules @ prems)) 1) ctxt
-
-fun pretty_counterex ctxt (real, ex) =
-  let
-    val msg = if real then "SMT: counterexample found:"
-      else "SMT: potential counterexample found:"
-    val cex = if null ex then [Pretty.str "(no assignments)"]
-      else map (Syntax.pretty_term ctxt) ex
-  in Pretty.string_of (Pretty.big_list msg cex) end
-
-fun smt_tac' pass_smt_exns ctxt =
-  let
-    val solver = solver_of (Context.Proof ctxt)
-    fun safe_solver ctxt thms = solver ctxt thms
-      handle SMT_COUNTEREXAMPLE cex => error (pretty_counterex ctxt cex)
-    val solver' = if pass_smt_exns then solver else safe_solver
-  in smt_unsat_tac solver' ctxt end
+    SAFE pass_exns (Tactic.rtac o smt_solver (rules @ prems)) context 1) ctxt
 
 val smt_tac = smt_tac' false
+end
 
 val smt_method =
   Scan.optional Attrib.thms [] >>
diff -r ab2f6574a2a6 -r 1312e8337ce5 src/HOL/SMT/Tools/smtlib_interface.ML
--- a/src/HOL/SMT/Tools/smtlib_interface.ML	Tue Nov 03 14:07:38 2009 +0100
+++ b/src/HOL/SMT/Tools/smtlib_interface.ML	Tue Nov 03 14:51:55 2009 +0100
@@ -87,7 +87,7 @@
         SOME (loc', t') => wr_expr loc' env t'
       | NONE => wrn (wr_expr loc env) n ts)
   | T.SLet ((v, _), t1, t2) =>
-      if loc then raise TERM ("SMTLIB: let expression in term", [])
+      if loc then raise SMT_Solver.SMT "SMTLIB: let expression in term"
       else
         let
           val (loc', t1') = the (dest_marker t1)
diff -r ab2f6574a2a6 -r 1312e8337ce5 src/HOL/SMT/Tools/yices_solver.ML
--- a/src/HOL/SMT/Tools/yices_solver.ML	Tue Nov 03 14:07:38 2009 +0100
+++ b/src/HOL/SMT/Tools/yices_solver.ML	Tue Nov 03 14:51:55 2009 +0100
@@ -17,12 +17,7 @@
 
 val options = ["--smtlib"]
 
-fun cex_kind true = "Counterexample"
-  | cex_kind false = "Possible counterexample"
-
-fun raise_cex real = error (cex_kind real ^ " found.")
-
-structure S = SMT_Solver
+fun raise_cex real = raise SMT_Solver.SMT_COUNTEREXAMPLE (real, [])
 
 fun core_oracle ({context, output, recon, ...} : SMT_Solver.proof_data) =
   let
@@ -33,7 +28,7 @@
     if String.isPrefix "unsat" l then @{cprop False}
     else if String.isPrefix "sat" l then raise_cex true
     else if String.isPrefix "unknown" l then raise_cex false
-    else error (solver_name ^ " failed")
+    else raise SMT_Solver.SMT (solver_name ^ " failed")
   end
 
 fun smtlib_solver oracle _ = {
diff -r ab2f6574a2a6 -r 1312e8337ce5 src/HOL/SMT/Tools/z3_proof.ML
--- a/src/HOL/SMT/Tools/z3_proof.ML	Tue Nov 03 14:07:38 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_proof.ML	Tue Nov 03 14:51:55 2009 +0100
@@ -16,7 +16,7 @@
 structure T = Z3_Proof_Terms
 structure R = Z3_Proof_Rules
 
-fun z3_exn msg = error ("Z3 proof reconstruction: " ^ msg)
+fun z3_exn msg = raise SMT_Solver.SMT ("Z3 proof reconstruction: " ^ msg)
 
 
 fun lift f (x, y) = apsnd (pair x) (f y)
@@ -223,10 +223,11 @@
   def :|-- (fn k => expr thy k #> pair NONE || rule thy k #>> K NONE) ||
   rule thy ~1 #>> SOME
 
-fun parse_error line_no ((_, xs), _) =
-  "parse error at line " ^ string_of_int line_no ^ ": " ^ quote (implode xs)
-
-fun handle_errors ln scan = Scan.error (Scan.!! (parse_error ln) scan)
+fun handle_errors line_no scan (st as (_, xs)) =
+  (case try scan st of
+    SOME y => y
+  | NONE => z3_exn ("parse error at line " ^ string_of_int line_no ^ ": " ^
+      quote (implode xs)))
 
 fun parse_line thy l (st as (stop, line_no, cx)) =
   if is_some stop then st
diff -r ab2f6574a2a6 -r 1312e8337ce5 src/HOL/SMT/Tools/z3_proof_rules.ML
--- a/src/HOL/SMT/Tools/z3_proof_rules.ML	Tue Nov 03 14:07:38 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_proof_rules.ML	Tue Nov 03 14:51:55 2009 +0100
@@ -26,7 +26,7 @@
 
 structure T = Z3_Proof_Terms
 
-fun z3_exn msg = error ("Z3 proof reconstruction: " ^ msg)
+fun z3_exn msg = raise SMT_Solver.SMT ("Z3 proof reconstruction: " ^ msg)
 
 
 (* proof rule names *)
diff -r ab2f6574a2a6 -r 1312e8337ce5 src/HOL/SMT/Tools/z3_solver.ML
--- a/src/HOL/SMT/Tools/z3_solver.ML	Tue Nov 03 14:07:38 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_solver.ML	Tue Nov 03 14:51:55 2009 +0100
@@ -52,7 +52,7 @@
     if String.isPrefix "unsat" l then ls
     else if String.isPrefix "sat" l then raise_cex true recon ls
     else if String.isPrefix "unknown" l then raise_cex false recon ls
-    else error (solver_name ^ " failed")
+    else raise SMT_Solver.SMT (solver_name ^ " failed")
   end
 
 fun core_oracle ({output, recon, ...} : SMT_Solver.proof_data) =