# HG changeset patch # User boehmes # Date 1288086576 -7200 # Node ID b1780e551273ae34c4996142ad34fc94d2d23ed2 # Parent 57f5db2a48a3d6c73e006f2d607bb396a3564a5f tuned diff -r 57f5db2a48a3 -r b1780e551273 src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Tue Oct 26 11:49:23 2010 +0200 +++ b/src/HOL/Tools/SMT/smt_solver.ML Tue Oct 26 11:49:36 2010 +0200 @@ -76,8 +76,7 @@ fun string_of_failure ctxt (Counterexample (real, ex)) = let - val msg = if real then "Counterexample found" - else "Potential counterexample found" + val msg = (if real then "C" else "Potential c") ^ "ounterexample found" in if null ex then msg ^ "." else Pretty.string_of (Pretty.big_list (msg ^ ":") @@ -419,26 +418,21 @@ (* SMT tactic *) -local - fun fail_tac f msg st = (f 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 fail => fail_tac - (trace_msg ctxt (prefix "SMT: ") o string_of_failure ctxt) fail st) -in - fun smt_tac' pass_exns ctxt rules = CONVERSION (SMT_Normalize.atomize_conv ctxt) THEN' Tactic.rtac @{thm ccontr} THEN' SUBPROOF (fn {context, prems, ...} => - let fun solve cx = snd (smt_solver cx (map (pair ~1) (rules @ prems))) - in SAFE pass_exns (Tactic.rtac o solve) context 1 end) ctxt + let + fun solve cx = snd (smt_solver cx (map (pair ~1) (rules @ prems))) + fun trace cx f = trace_msg cx (prefix "SMT: " o string_of_failure cx) f + in + (if pass_exns then SOME (solve cx) + else (SOME (solve cx) handle SMT fail => (trace cx fail; NONE))) + |> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac) + end val smt_tac = smt_tac' false -end - val smt_method = Scan.optional Attrib.thms [] >> (fn thms => fn ctxt => METHOD (fn facts =>