# HG changeset patch
# User huffman
# Date 1289221638 28800
# Node ID 61176a1f9cd3a92ad0f8755fbf9c16968aa791f1
# Parent  6354e21e61fa832e71e3b30d139ca14df362324d# Parent  3d93bd33304dba83196d5e7674c5f446ea2c96d3
merged

diff -r 6354e21e61fa -r 61176a1f9cd3 NEWS
--- a/NEWS	Sat Nov 06 10:01:00 2010 -0700
+++ b/NEWS	Mon Nov 08 05:07:18 2010 -0800
@@ -350,9 +350,10 @@
     z3_trace_assms ~> smt_trace_used_facts
     INCOMPATIBILITY.
   - Added:
+    smt_verbose
+    smt_datatypes
     cvc3_options
     yices_options
-    smt_datatypes
 
 * Removed [split_format ... and ... and ...] version of
 [split_format].  Potential INCOMPATIBILITY.
diff -r 6354e21e61fa -r 61176a1f9cd3 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sat Nov 06 10:01:00 2010 -0700
+++ b/src/HOL/IsaMakefile	Mon Nov 08 05:07:18 2010 -0800
@@ -270,6 +270,7 @@
   Semiring_Normalization.thy \
   SetInterval.thy \
   Sledgehammer.thy \
+  Smallcheck.thy \
   SMT.thy \
   String.thy \
   Typerep.thy \
@@ -336,8 +337,11 @@
   Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML \
   Tools/Sledgehammer/sledgehammer_atp_translate.ML \
   Tools/Sledgehammer/sledgehammer_util.ML \
+  Tools/smallvalue_generators.ML \
   Tools/SMT/smtlib_interface.ML \
   Tools/SMT/smt_builtin.ML \
+  Tools/SMT/smt_config.ML \
+  Tools/SMT/smt_failure.ML \
   Tools/SMT/smt_monomorph.ML \
   Tools/SMT/smt_normalize.ML \
   Tools/SMT/smt_setup_solvers.ML \
diff -r 6354e21e61fa -r 61176a1f9cd3 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Sat Nov 06 10:01:00 2010 -0700
+++ b/src/HOL/Main.thy	Mon Nov 08 05:07:18 2010 -0800
@@ -1,7 +1,7 @@
 header {* Main HOL *}
 
 theory Main
-imports Plain Record Predicate_Compile Nitpick
+imports Plain Record Predicate_Compile Smallcheck Nitpick
 begin
 
 text {*
diff -r 6354e21e61fa -r 61176a1f9cd3 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Nov 06 10:01:00 2010 -0700
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Nov 08 05:07:18 2010 -0800
@@ -7,7 +7,6 @@
 
 val proverK = "prover"
 val prover_timeoutK = "prover_timeout"
-val prover_hard_timeoutK = "prover_hard_timeout"
 val keepK = "keep"
 val full_typesK = "full_types"
 val minimizeK = "minimize"
@@ -16,7 +15,9 @@
 
 fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
 fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
-fun metis_tag id = "#" ^ string_of_int id ^ " metis (sledgehammer): "
+fun metis_tag smt id =
+  "#" ^ string_of_int id ^ " " ^ (if smt then "smt" else "metis") ^
+  " (sledgehammer): "
 
 val separator = "-----"
 
@@ -405,8 +406,7 @@
     val (prover_name, prover) = get_prover (Proof.context_of st) args
     val dir = AList.lookup (op =) args keepK
     val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
-    val hard_timeout = AList.lookup (op =) args prover_hard_timeoutK
-      |> Option.map (fst o read_int o explode)
+    val hard_timeout = SOME timeout (* always use a hard timeout *)
     val (msg, result) = run_sh prover_name prover hard_timeout timeout dir st
   in
     case result of
@@ -438,7 +438,6 @@
 
 fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
   let
-    open Metis_Translate
     val ctxt = Proof.context_of st
     val n0 = length (these (!named_thms))
     val (prover_name, _) = get_prover ctxt args
@@ -466,12 +465,13 @@
   end
 
 
-fun run_metis trivial full m name named_thms id
+fun run_metis smt trivial full m name named_thms id
     ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
   let
     fun metis thms ctxt =
-      if full then Metis_Tactics.metisFT_tac ctxt thms
-      else Metis_Tactics.metis_tac ctxt thms
+      (if smt then SMT_Solver.smt_tac
+       else if full then Metis_Tactics.metisFT_tac
+       else Metis_Tactics.metis_tac) ctxt thms
     fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
 
     fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
@@ -494,7 +494,7 @@
   in
     maps snd named_thms
     |> timed_metis
-    |>> log o prefix (metis_tag id)
+    |>> log o prefix (metis_tag smt id)
     |> snd
   end
 
@@ -508,6 +508,9 @@
     let
       val named_thms =
         Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
+      val ctxt = Proof.context_of pre
+      val (prover_name, _) = get_prover ctxt args
+      val smt = String.isSuffix "smt" prover_name (* hack *)
       val minimize = AList.defined (op =) args minimizeK
       val metis_ft = AList.defined (op =) args metis_ftK
       val trivial = TimeLimit.timeLimit try_outer_timeout
@@ -516,15 +519,15 @@
       fun apply_metis m1 m2 =
         if metis_ft
         then
-          if not (Mirabelle.catch_result metis_tag false
-              (run_metis trivial false m1 name (these (!named_thms))) id st)
+          if not (Mirabelle.catch_result (metis_tag smt) false
+              (run_metis smt trivial false m1 name (these (!named_thms))) id st)
           then
-            (Mirabelle.catch_result metis_tag false
-              (run_metis trivial true m2 name (these (!named_thms))) id st; ())
+            (Mirabelle.catch_result (metis_tag smt) false
+              (run_metis smt trivial true m2 name (these (!named_thms))) id st; ())
           else ()
         else
-          (Mirabelle.catch_result metis_tag false
-            (run_metis trivial false m1 name (these (!named_thms))) id st; ())
+          (Mirabelle.catch_result (metis_tag smt) false
+            (run_metis smt trivial false m1 name (these (!named_thms))) id st; ())
     in 
       change_data id (set_mini minimize);
       Mirabelle.catch sh_tag (run_sledgehammer trivial args named_thms) id st;
diff -r 6354e21e61fa -r 61176a1f9cd3 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Sat Nov 06 10:01:00 2010 -0700
+++ b/src/HOL/SMT.thy	Mon Nov 08 05:07:18 2010 -0800
@@ -8,7 +8,9 @@
 imports List
 uses
   "Tools/Datatype/datatype_selectors.ML"
-  ("Tools/SMT/smt_monomorph.ML")
+  "Tools/SMT/smt_failure.ML"
+  "Tools/SMT/smt_config.ML"
+  "Tools/SMT/smt_monomorph.ML"
   ("Tools/SMT/smt_builtin.ML")
   ("Tools/SMT/smt_normalize.ML")
   ("Tools/SMT/smt_translate.ML")
@@ -126,7 +128,6 @@
 
 subsection {* Setup *}
 
-use "Tools/SMT/smt_monomorph.ML"
 use "Tools/SMT/smt_builtin.ML"
 use "Tools/SMT/smt_normalize.ML"
 use "Tools/SMT/smt_translate.ML"
@@ -141,6 +142,7 @@
 use "Tools/SMT/smt_setup_solvers.ML"
 
 setup {*
+  SMT_Config.setup #>
   SMT_Solver.setup #>
   Z3_Proof_Reconstruction.setup #>
   SMT_Setup_Solvers.setup
@@ -241,6 +243,13 @@
 subsection {* Tracing *}
 
 text {*
+The SMT method, when applied, traces important information.  To
+make it entirely silent, set the following option to @{text false}.
+*}
+
+declare [[ smt_verbose = true ]]
+
+text {*
 For tracing the generated problem file given to the SMT solver as
 well as the returned result of the solver, the option
 @{text smt_trace} should be set to @{text true}.
diff -r 6354e21e61fa -r 61176a1f9cd3 src/HOL/Smallcheck.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Smallcheck.thy	Mon Nov 08 05:07:18 2010 -0800
@@ -0,0 +1,69 @@
+(* Author: Lukas Bulwahn, TU Muenchen *)
+
+header {* Another simple counterexample generator *}
+
+theory Smallcheck
+imports Quickcheck
+uses ("Tools/smallvalue_generators.ML")
+begin
+
+
+section {* small value generator type classes *}
+
+class small = term_of +
+fixes small :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
+
+instantiation unit :: small
+begin
+
+definition "find_first f d = f ()"
+
+instance ..
+
+end
+
+instantiation int :: small
+begin
+
+function small' :: "(int => term list option) => int => int => term list option"
+where "small' f d i = (if d < i then None else (case f i of Some t => Some t | None => small' f d (i + 1)))"
+by pat_completeness auto
+
+termination 
+  by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
+
+definition "small f d = small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
+
+instance ..
+
+end
+
+instantiation prod :: (small, small) small
+begin
+
+definition
+  "small f d = small (%x. small (%y. f (x, y)) d) d"
+
+instance ..
+
+end
+
+section {* Defining combinators for any first-order data type *}
+
+definition catch_match :: "term list option => term list option => term list option"
+where
+  [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
+
+code_const catch_match 
+  (SML "(_) handle Match => _")
+
+use "Tools/smallvalue_generators.ML"
+
+(* We do not activate smallcheck yet. 
+setup {* Smallvalue_Generators.setup *}
+*)
+
+hide_fact catch_match_def
+hide_const (open) catch_match
+
+end
\ No newline at end of file
diff -r 6354e21e61fa -r 61176a1f9cd3 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Sat Nov 06 10:01:00 2010 -0700
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Nov 08 05:07:18 2010 -0800
@@ -166,6 +166,7 @@
      [(Unprovable, "UNPROVABLE"),
       (IncompleteUnprovable, "CANNOT PROVE"),
       (TimedOut, "SZS status Timeout"),
+      (TimedOut, "Time limit reached"),
       (Unprovable, "Satisfiability detected"),
       (Unprovable, "Termination reason: Satisfiable"),
       (VampireTooOld, "not a valid option"),
diff -r 6354e21e61fa -r 61176a1f9cd3 src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Sat Nov 06 10:01:00 2010 -0700
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Mon Nov 08 05:07:18 2010 -0800
@@ -160,7 +160,6 @@
     KodkodiNotInstalled |
     Normal of (int * raw_bound list) list * int list * string |
     TimedOut of int list |
-    Interrupted of int list option |
     Error of string * int list
 
   exception SYNTAX of string * string
@@ -308,7 +307,6 @@
   KodkodiNotInstalled |
   Normal of (int * raw_bound list) list * int list * string |
   TimedOut of int list |
-  Interrupted of int list option |
   Error of string * int list
 
 exception SYNTAX of string * string
@@ -1085,17 +1083,6 @@
                 Normal (ps, js, first_error)
             end
         in remove_temporary_files (); outcome end
-        handle Exn.Interrupt =>  (* FIXME Exn.is_interrupt *)
-               let
-                 val nontriv_js =
-                   read_output_file new_kodkodi out_path
-                   |> snd |> snd |> map reindex
-               in
-                 (remove_temporary_files ();
-                  Interrupted (SOME (triv_js @ nontriv_js)))  (* FIXME violates Isabelle/ML exception model *)
-                 handle Exn.Interrupt =>  (* FIXME violates Isabelle/ML exception model *)
-                        (remove_temporary_files (); Interrupted NONE)
-               end
       end
   end
 
diff -r 6354e21e61fa -r 61176a1f9cd3 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Nov 06 10:01:00 2010 -0700
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 08 05:07:18 2010 -0800
@@ -231,9 +231,6 @@
     fun check_deadline () =
       if debug andalso passed_deadline deadline then raise TimeLimit.TimeOut
       else ()
-    fun do_interrupted () =
-      if passed_deadline deadline then raise TimeLimit.TimeOut
-      else raise Interrupt
 
     val assm_ts = if assms orelse auto then assm_ts else []
     val _ =
@@ -818,9 +815,6 @@
             end
           | KK.TimedOut unsat_js =>
             (update_checked_problems problems unsat_js; raise TimeLimit.TimeOut)
-          | KK.Interrupted NONE => (checked_problems := NONE; do_interrupted ())
-          | KK.Interrupted (SOME unsat_js) =>
-            (update_checked_problems problems unsat_js; do_interrupted ())
           | KK.Error (s, unsat_js) =>
             (update_checked_problems problems unsat_js;
              print_v (K ("Kodkod error: " ^ s ^ "."));
@@ -971,27 +965,15 @@
 
     val batches = batch_list batch_size (!scopes)
     val outcome_code =
-      (run_batches 0 (length batches) batches
-                   (false, max_potential, max_genuine, 0)
-       handle Exn.Interrupt => do_interrupted ())  (* FIXME violates Isabelle/ML exception model *)
+      run_batches 0 (length batches) batches
+                  (false, max_potential, max_genuine, 0)
       handle TimeLimit.TimeOut =>
              (print_m (fn () => excipit "ran out of time after checking");
               if !met_potential > 0 then "potential" else "unknown")
-           | Exn.Interrupt =>
-             if auto orelse debug then raise Interrupt
-             else error (excipit "was interrupted after checking")  (* FIXME violates Isabelle/ML exception model *)
     val _ = print_v (fn () =>
                 "Total time: " ^ string_from_time (Timer.checkRealTimer timer) ^
                 ".")
   in (outcome_code, !state_ref) end
-  handle Exn.Interrupt =>  (* FIXME violates Isabelle/ML exception model *)
-         if auto orelse #debug params then
-           raise Interrupt
-         else
-           if passed_deadline deadline then
-             (Output.urgent_message "Nitpick ran out of time."; ("unknown", state))
-           else
-             error "Nitpick was interrupted."  (* FIXME violates Isabelle/ML exception model *)
 
 fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
                       step subst assm_ts orig_t =
diff -r 6354e21e61fa -r 61176a1f9cd3 src/HOL/Tools/SMT/smt_config.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/smt_config.ML	Mon Nov 08 05:07:18 2010 -0800
@@ -0,0 +1,232 @@
+(*  Title:      HOL/Tools/SMT/smt_config.ML
+    Author:     Sascha Boehme, TU Muenchen
+
+Configuration options and diagnostic tools for SMT.
+*)
+
+signature SMT_CONFIG =
+sig
+  (*solver*)
+  val add_solver: string -> Context.generic -> Context.generic
+  val set_solver_options: string * string -> Context.generic -> Context.generic
+  val select_solver: string -> Context.generic -> Context.generic
+  val solver_of: Proof.context -> string
+  val solver_options_of: Proof.context -> string list
+
+  (*options*)
+  val oracle: bool Config.T
+  val datatypes: bool Config.T
+  val timeout: real Config.T
+  val fixed: bool Config.T
+  val verbose: bool Config.T
+  val traceN: string
+  val trace: bool Config.T
+  val trace_used_facts: bool Config.T
+  val monomorph_limit: int Config.T
+  val drop_bad_facts: bool Config.T
+  val filter_only_facts: bool Config.T
+
+  (*tools*)
+  val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
+
+  (*diagnostics*)
+  val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
+  val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit
+
+  (*certificates*)
+  val select_certificates: string -> Context.generic -> Context.generic
+  val certificates_of: Proof.context -> Cache_IO.cache option
+
+  (*setup*)
+  val setup: theory -> theory
+  val print_setup: Proof.context -> unit
+end
+
+structure SMT_Config: SMT_CONFIG =
+struct
+
+(* solver *)
+
+structure Solvers = Generic_Data
+(
+  type T = string list Symtab.table * string option
+  val empty = (Symtab.empty, NONE)
+  val extend = I
+  fun merge ((ss1, s), (ss2, _)) = (Symtab.merge (K true) (ss1, ss2), s)
+)
+
+fun set_solver_options (name, options) =
+  let val opts = String.tokens (Symbol.is_ascii_blank o str) options
+  in Solvers.map (apfst (Symtab.map_entry name (K opts))) end
+
+fun add_solver name context =
+  if Symtab.defined (fst (Solvers.get context)) name then
+    error ("Solver already registered: " ^ quote name)
+  else
+    context
+    |> Solvers.map (apfst (Symtab.update (name, [])))
+    |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
+        (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
+          (Thm.declaration_attribute o K o set_solver_options o pair name))
+        ("Additional command line options for SMT solver " ^ quote name))
+
+fun select_solver name context =
+  if Symtab.defined (fst (Solvers.get context)) name then
+    Solvers.map (apsnd (K (SOME name))) context
+  else error ("Trying to select unknown solver: " ^ quote name)
+
+val lookup_solver = snd o Solvers.get o Context.Proof
+
+fun solver_of ctxt =
+  (case lookup_solver ctxt of
+    SOME name => name
+  | NONE => error "No SMT solver selected")
+
+fun solver_options_of ctxt =
+  (case lookup_solver ctxt of
+    NONE => []
+  | SOME name =>
+      Symtab.lookup_list (fst (Solvers.get (Context.Proof ctxt))) name)
+
+val setup_solver =
+  Attrib.setup @{binding smt_solver}
+    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
+      (Thm.declaration_attribute o K o select_solver))
+    "SMT solver configuration"
+
+
+(* options *)
+
+val oracleN = "smt_oracle"
+val (oracle, setup_oracle) = Attrib.config_bool oracleN (K true)
+
+val datatypesN = "smt_datatypes"
+val (datatypes, setup_datatypes) = Attrib.config_bool datatypesN (K false)
+
+val timeoutN = "smt_timeout"
+val (timeout, setup_timeout) = Attrib.config_real timeoutN (K 30.0)
+
+val fixedN = "smt_fixed"
+val (fixed, setup_fixed) = Attrib.config_bool fixedN (K false)
+
+val verboseN = "smt_verbose"
+val (verbose, setup_verbose) = Attrib.config_bool verboseN (K true)
+
+val traceN = "smt_trace"
+val (trace, setup_trace) = Attrib.config_bool traceN (K false)
+
+val trace_used_factsN = "smt_trace_used_facts"
+val (trace_used_facts, setup_trace_used_facts) =
+  Attrib.config_bool trace_used_factsN (K false)
+
+val monomorph_limitN = "smt_monomorph_limit"
+val (monomorph_limit, setup_monomorph_limit) =
+  Attrib.config_int monomorph_limitN (K 10)
+
+val drop_bad_factsN = "smt_drop_bad_facts"
+val (drop_bad_facts, setup_drop_bad_facts) =
+  Attrib.config_bool drop_bad_factsN (K false)
+
+val filter_only_factsN = "smt_filter_only_facts"
+val (filter_only_facts, setup_filter_only_facts) =
+  Attrib.config_bool filter_only_factsN (K false)
+
+val setup_options =
+  setup_oracle #>
+  setup_datatypes #>
+  setup_timeout #>
+  setup_fixed #>
+  setup_trace #>
+  setup_verbose #>
+  setup_monomorph_limit #>
+  setup_drop_bad_facts #>
+  setup_filter_only_facts #>
+  setup_trace_used_facts
+
+
+(* diagnostics *)
+
+fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else ()
+
+fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose)
+
+fun trace_msg ctxt = cond_trace (Config.get ctxt trace)
+
+
+(* tools *)
+
+fun with_timeout ctxt f x =
+  TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f x
+  handle TimeLimit.TimeOut => raise SMT_Failure.SMT SMT_Failure.Time_Out
+
+
+(* certificates *)
+
+structure Certificates = Generic_Data
+(
+  type T = Cache_IO.cache option
+  val empty = NONE
+  val extend = I
+  fun merge (s, _) = s
+)
+
+val get_certificates_path =
+  Option.map (Cache_IO.cache_path_of) o Certificates.get o Context.Proof
+
+fun select_certificates name = Certificates.put (
+  if name = "" then NONE
+  else SOME (Cache_IO.make (Path.explode name)))
+
+val certificates_of = Certificates.get o Context.Proof
+
+val setup_certificates =
+  Attrib.setup @{binding smt_certificates}
+    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
+      (Thm.declaration_attribute o K o select_certificates))
+    "SMT certificates configuration"
+
+
+(* setup *)
+
+val setup =
+  setup_solver #>
+  setup_options #>
+  setup_certificates
+
+fun print_setup ctxt =
+  let
+    fun string_of_bool b = if b then "true" else "false"
+
+    val (names, sel) = Solvers.get (Context.Proof ctxt) |> apfst Symtab.keys
+    val ns = if null names then ["(none)"] else sort_strings names
+    val n = the_default "(none)" sel
+    val opts = solver_options_of ctxt
+    
+    val t = string_of_real (Config.get ctxt timeout)
+
+    val certs_filename =
+      (case get_certificates_path ctxt of
+        SOME path => Path.implode path
+      | NONE => "(disabled)")
+  in
+    Pretty.writeln (Pretty.big_list "SMT setup:" [
+      Pretty.str ("Current SMT solver: " ^ n),
+      Pretty.str ("Current SMT solver options: " ^ space_implode " " opts),
+      Pretty.str_list "Available SMT solvers: "  "" ns,
+      Pretty.str ("Current timeout: " ^ t ^ " seconds"),
+      Pretty.str ("With proofs: " ^
+        string_of_bool (not (Config.get ctxt oracle))),
+      Pretty.str ("Certificates cache: " ^ certs_filename),
+      Pretty.str ("Fixed certificates: " ^
+        string_of_bool (Config.get ctxt fixed))])
+  end
+
+val _ =
+  Outer_Syntax.improper_command "smt_status"
+    ("show the available SMT solvers, the currently selected SMT solver, " ^
+      "and the values of SMT configuration options")
+    Keyword.diag
+    (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
+      print_setup (Toplevel.context_of state))))
+
+end
diff -r 6354e21e61fa -r 61176a1f9cd3 src/HOL/Tools/SMT/smt_failure.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/smt_failure.ML	Mon Nov 08 05:07:18 2010 -0800
@@ -0,0 +1,41 @@
+(*  Title:      HOL/Tools/SMT/smt_failure.ML
+    Author:     Sascha Boehme, TU Muenchen
+
+Failures and exception of SMT.
+*)
+
+signature SMT_FAILURE =
+sig
+  datatype failure =
+    Counterexample of bool * term list |
+    Time_Out |
+    Out_Of_Memory |
+    Other_Failure of string
+  val string_of_failure: Proof.context -> failure -> string
+  exception SMT of failure
+end
+
+structure SMT_Failure: SMT_FAILURE =
+struct
+
+datatype failure =
+  Counterexample of bool * term list |
+  Time_Out |
+  Out_Of_Memory |
+  Other_Failure of string
+
+fun string_of_failure ctxt (Counterexample (real, ex)) =
+      let
+        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 ^ ":")
+          (map (Syntax.pretty_term ctxt) ex))
+      end
+  | string_of_failure _ Time_Out = "Timed out"
+  | string_of_failure _ Out_Of_Memory = "Ran out of memory"
+  | string_of_failure _ (Other_Failure msg) = msg
+
+exception SMT of failure
+
+end
diff -r 6354e21e61fa -r 61176a1f9cd3 src/HOL/Tools/SMT/smt_monomorph.ML
--- a/src/HOL/Tools/SMT/smt_monomorph.ML	Sat Nov 06 10:01:00 2010 -0700
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Mon Nov 08 05:07:18 2010 -0800
@@ -92,16 +92,19 @@
    computation uses only the constants occurring with schematic type
    variables in the propositions. To ease comparisons, such sets of
    costants are always kept in their initial order. *)
-fun incremental_monomorph thy limit all_grounds new_grounds irules =
+fun incremental_monomorph ctxt limit all_grounds new_grounds irules =
   let
+    val thy = ProofContext.theory_of ctxt
     val all_grounds' = Symtab.merge_list (op =) (all_grounds, new_grounds)
     val spec = specialize thy all_grounds' new_grounds
     val (irs, new_grounds') = fold_map spec irules Symtab.empty
   in
     if Symtab.is_empty new_grounds' then irs
     else if limit > 0
-    then incremental_monomorph thy (limit-1) all_grounds' new_grounds' irs
-    else (warning "SMT: monomorphization limit reached"; irs)
+    then incremental_monomorph ctxt (limit-1) all_grounds' new_grounds' irs
+    else
+     (SMT_Config.verbose_msg ctxt (K "Warning: Monomorphization limit reached")
+      (); irs)
   end
 
 
@@ -175,7 +178,7 @@
       in
         polys
         |> map (fn (i, thm) => ((i, thm), [(Vartab.empty, tvar_consts_of thm)]))
-        |> incremental_monomorph thy limit Symtab.empty grounds
+        |> incremental_monomorph ctxt' limit Symtab.empty grounds
         |> map (apsnd (filter_most_specific thy))
         |> flat o map2 (instantiate thy) Tenvs
         |> append monos
@@ -183,9 +186,6 @@
       end
 
 
-val monomorph_limit = 10
-
-
 (* Instantiate all polymorphic constants (i.e., constants occurring
    both with ground types and type variables) with all (necessary)
    ground types; thereby create copies of theorems containing those
@@ -199,6 +199,6 @@
   irules
   |> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of o snd)
   |>> incr_indexes
-  |-> mono_all ctxt monomorph_limit
+  |-> mono_all ctxt (Config.get ctxt SMT_Config.monomorph_limit)
 
 end
diff -r 6354e21e61fa -r 61176a1f9cd3 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Sat Nov 06 10:01:00 2010 -0700
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Mon Nov 08 05:07:18 2010 -0800
@@ -19,8 +19,7 @@
 sig
   type extra_norm = bool -> (int * thm) list -> Proof.context ->
     (int * thm) list * Proof.context
-  val normalize: (Proof.context -> (thm -> string) -> thm -> unit) -> bool ->
-    extra_norm -> bool -> (int * thm) list -> Proof.context ->
+  val normalize: extra_norm -> bool -> (int * thm) list -> Proof.context ->
     (int * thm) list * Proof.context
   val atomize_conv: Proof.context -> conv
   val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv
@@ -247,7 +246,7 @@
             then eta_args_conv norm_conv
               (length (Term.binder_types T) - length ts)
             else args_conv o norm_conv
-        | (_, ts) => args_conv o norm_conv)) ctxt ct
+        | _ => args_conv o norm_conv)) ctxt ct
 
   fun is_normed ctxt t =
     (case t of
@@ -516,15 +515,15 @@
 
 fun with_context f irules ctxt = (f ctxt irules, ctxt)
 
-fun normalize trace keep_assms extra_norm with_datatypes irules ctxt =
+fun normalize extra_norm with_datatypes irules ctxt =
   let
     fun norm f ctxt' (i, thm) =
-      if keep_assms then SOME (i, f ctxt' thm)
-      else
+      if Config.get ctxt' SMT_Config.drop_bad_facts then
         (case try (f ctxt') thm of
           SOME thm' => SOME (i, thm')
-        | NONE => (trace ctxt' (prefix ("SMT warning: " ^
+        | NONE => (SMT_Config.verbose_msg ctxt' (prefix ("Warning: " ^
             "dropping assumption: ") o Display.string_of_thm ctxt') thm; NONE))
+      else SOME (i, f ctxt' thm)
   in
     irules
     |> trivial_distinct ctxt
diff -r 6354e21e61fa -r 61176a1f9cd3 src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Sat Nov 06 10:01:00 2010 -0700
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Mon Nov 08 05:07:18 2010 -0800
@@ -16,9 +16,9 @@
   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 raise SMT_Solver.SMT (SMT_Solver.Other_Failure ("Solver " ^
+  else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^
     quote solver_name ^ " failed. Enable SMT tracing by setting the " ^
-    "configuration option " ^ quote SMT_Solver.traceN ^ " and " ^
+    "configuration option " ^ quote SMT_Config.traceN ^ " and " ^
     " see the trace for details."))
 
 fun on_first_line test_outcome solver_name lines =
@@ -60,14 +60,14 @@
 
 fun z3_options ctxt =
   ["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false", "-smt"]
-  |> not (Config.get ctxt SMT_Solver.oracle) ?
+  |> not (Config.get ctxt SMT_Config.oracle) ?
        append ["DISPLAY_PROOF=true","PROOF_MODE=2"]
 
 fun z3_on_last_line solver_name lines =
   let
     fun junk l =
       if String.isPrefix "WARNING: Out of allocated virtual memory" l
-      then raise SMT_Solver.SMT SMT_Solver.Out_Of_Memory
+      then raise SMT_Failure.SMT SMT_Failure.Out_Of_Memory
       else
         String.isPrefix "WARNING" l orelse
         String.isPrefix "ERROR" l orelse
diff -r 6354e21e61fa -r 61176a1f9cd3 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Sat Nov 06 10:01:00 2010 -0700
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon Nov 08 05:07:18 2010 -0800
@@ -6,14 +6,7 @@
 
 signature SMT_SOLVER =
 sig
-  datatype failure =
-    Counterexample of bool * term list |
-    Time_Out |
-    Out_Of_Memory |
-    Other_Failure of string
-  val string_of_failure: Proof.context -> string -> failure -> string
-  exception SMT of failure
-
+  (*configuration*)
   type interface = {
     extra_norm: SMT_Normalize.extra_norm,
     translate: SMT_Translate.config }
@@ -30,37 +23,16 @@
     reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
       (int list * thm) * Proof.context) option }
 
-  (*options*)
-  val oracle: bool Config.T
-  val filter_only: bool Config.T
-  val datatypes: bool Config.T
-  val keep_assms: bool Config.T
-  val timeout: real Config.T
-  val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
-  val traceN: string
-  val trace: bool Config.T
-  val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
-  val trace_used_facts: bool Config.T
-
-  (*certificates*)
-  val fixed_certificates: bool Config.T
-  val select_certificates: string -> Context.generic -> Context.generic
-
-  (*solvers*)
+  (*registry*)
   type solver = bool option -> Proof.context -> (int * thm) list ->
     int list * thm
   val add_solver: solver_config -> theory -> theory
-  val set_solver_options: string -> string -> Context.generic ->
-    Context.generic
-  val all_solver_names_of: Context.generic -> string list
-  val solver_name_of: Context.generic -> string
-  val select_solver: string -> Context.generic -> Context.generic
-  val solver_of: Context.generic -> solver
+  val solver_of: Proof.context -> solver
   val is_locally_installed: Proof.context -> bool
 
   (*filter*)
   val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int ->
-    {outcome: failure option, used_facts: 'a list,
+    {outcome: SMT_Failure.failure option, used_facts: 'a list,
     run_time_in_msecs: int option}
 
   (*tactic*)
@@ -69,31 +41,15 @@
 
   (*setup*)
   val setup: theory -> theory
-  val print_setup: Context.generic -> unit
 end
 
 structure SMT_Solver: SMT_SOLVER =
 struct
 
-datatype failure =
-  Counterexample of bool * term list |
-  Time_Out |
-  Out_Of_Memory |
-  Other_Failure of string
+structure C = SMT_Config
 
-fun string_of_failure ctxt _ (Counterexample (real, ex)) =
-      let
-        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 ^ ":")
-          (map (Syntax.pretty_term ctxt) ex))
-      end
-  | string_of_failure _ name Time_Out = name ^ " timed out."
-  | string_of_failure _ name Out_Of_Memory = name ^ " ran out of memory."
-  | string_of_failure _ _ (Other_Failure msg) = msg
 
-exception SMT of failure
+(* configuration *)
 
 type interface = {
   extra_norm: SMT_Normalize.extra_norm,
@@ -114,57 +70,6 @@
     (int list * thm) * Proof.context) option }
 
 
-
-(* SMT options *)
-
-val (oracle, setup_oracle) = Attrib.config_bool "smt_oracle" (K true)
-
-val (filter_only, setup_filter_only) =
-  Attrib.config_bool "smt_filter_only" (K false)
-
-val (datatypes, setup_datatypes) = Attrib.config_bool "smt_datatypes" (K false)
-
-val (keep_assms, setup_keep_assms) =
-  Attrib.config_bool "smt_keep_assms" (K true)
-
-val (timeout, setup_timeout) = Attrib.config_real "smt_timeout" (K 30.0)
-
-fun with_timeout ctxt f x =
-  TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f x
-  handle TimeLimit.TimeOut => raise SMT Time_Out
-
-val traceN = "smt_trace"
-val (trace, setup_trace) = Attrib.config_bool traceN (K false)
-
-fun trace_msg ctxt f x =
-  if Config.get ctxt trace then tracing (f x) else ()
-
-val (trace_used_facts, setup_trace_used_facts) =
-  Attrib.config_bool "smt_trace_used_facts" (K false)
-
-
-(* SMT certificates *)
-
-val (fixed_certificates, setup_fixed_certificates) =
-  Attrib.config_bool "smt_fixed" (K false)
-
-structure Certificates = Generic_Data
-(
-  type T = Cache_IO.cache option
-  val empty = NONE
-  val extend = I
-  fun merge (s, _) = s
-)
-
-val get_certificates_path =
-  Option.map (Cache_IO.cache_path_of) o Certificates.get
-
-fun select_certificates name = Certificates.put (
-  if name = "" then NONE
-  else SOME (Cache_IO.make (Path.explode name)))
-
-
-
 (* interface to external solvers *)
 
 fun get_local_solver env_var =
@@ -202,12 +107,16 @@
   [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
 
 fun run ctxt cmd args input =
-  (case Certificates.get (Context.Proof ctxt) of
-    NONE => Cache_IO.run (make_cmd (choose cmd) args) input
+  (case C.certificates_of ctxt of
+    NONE =>
+      let
+        val {output, redirected_output, ...} =
+          Cache_IO.run (make_cmd (choose cmd) args) input
+      in (redirected_output, output) end 
   | SOME certs =>
       (case Cache_IO.lookup certs input of
         (NONE, key) =>
-          if Config.get ctxt fixed_certificates
+          if Config.get ctxt C.fixed
           then error ("Bad certificates cache: missing certificate")
           else Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args)
             input
@@ -223,36 +132,37 @@
     fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
       (map Pretty.str ls))
 
-    val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines) input
+    val _ = C.trace_msg ctxt (pretty "Problem:" o split_lines) input
 
-    val (res, err) = with_timeout ctxt (run ctxt cmd args) input
-    val _ = trace_msg ctxt (pretty "SMT solver:") err
+    val (res, err) = C.with_timeout ctxt (run ctxt cmd args) input
+    val _ = C.trace_msg ctxt (pretty "Solver:") err
 
     val ls = rev (snd (chop_while (equal "") (rev res)))
-    val _ = trace_msg ctxt (pretty "SMT result:") ls
+    val _ = C.trace_msg ctxt (pretty "Result:") ls
   in ls end
 
 end
 
-fun trace_assms ctxt = trace_msg ctxt (Pretty.string_of o
-  Pretty.big_list "SMT assertions:" o map (Display.pretty_thm ctxt o snd))
+fun trace_assms ctxt = C.trace_msg ctxt (Pretty.string_of o
+  Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))
 
 fun trace_recon_data ctxt ({typs, terms, ...} : SMT_Translate.recon) =
   let
     fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p]
-    fun pretty_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
-    fun pretty_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t)
+    fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
+    fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t)
   in
-    trace_msg ctxt (fn () => Pretty.string_of (Pretty.big_list "SMT names:" [
-      Pretty.big_list "sorts:" (map pretty_typ (Symtab.dest typs)),
-      Pretty.big_list "functions:" (map pretty_term (Symtab.dest terms))])) ()
+    C.trace_msg ctxt (fn () =>
+      Pretty.string_of (Pretty.big_list "Names:" [
+        Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)),
+        Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) ()
   end
 
-fun invoke translate_config name cmd more_opts options irules ctxt =
+fun invoke translate_config name cmd options irules ctxt =
   let
-    val args = more_opts @ options ctxt
+    val args = C.solver_options_of ctxt @ options ctxt
     val comments = ("solver: " ^ name) ::
-      ("timeout: " ^ Time.toString (seconds (Config.get ctxt timeout))) ::
+      ("timeout: " ^ Time.toString (seconds (Config.get ctxt C.timeout))) ::
       "arguments:" :: args
   in
     irules
@@ -283,7 +193,7 @@
     val thms = filter (fn i => i >= 0) idxs
       |> map_filter (AList.lookup (op =) irules)
   in
-    if Config.get ctxt trace_used_facts andalso length thms > 0
+    if Config.get ctxt C.trace_used_facts andalso length thms > 0
     then
       tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
         (map (Display.pretty_thm ctxt) thms)))
@@ -292,17 +202,15 @@
 
 fun gen_solver name info rm ctxt irules =
   let
-    val {env_var, is_remote, options, more_options, interface, reconstruct} =
-      info
+    val {env_var, is_remote, options, interface, reconstruct} = info
     val {extra_norm, translate} = interface
     val (with_datatypes, translate') =
-      set_has_datatypes (Config.get ctxt datatypes) translate
+      set_has_datatypes (Config.get ctxt C.datatypes) translate
     val cmd = (rm, env_var, is_remote, name)
-    val keep = Config.get ctxt keep_assms
   in
     (irules, ctxt)
-    |-> SMT_Normalize.normalize trace_msg keep extra_norm with_datatypes
-    |-> invoke translate' name cmd more_options options
+    |-> SMT_Normalize.normalize extra_norm with_datatypes
+    |-> invoke translate' name cmd options
     |-> reconstruct
     |-> (fn (idxs, thm) => fn ctxt' => thm
     |> singleton (ProofContext.export ctxt' ctxt)
@@ -313,7 +221,7 @@
 
 
 
-(* solver store *)
+(* registry *)
 
 type solver = bool option -> Proof.context -> (int * thm) list -> int list * thm
 
@@ -321,7 +229,6 @@
   env_var: string,
   is_remote: bool,
   options: Proof.context -> string list,
-  more_options: string list,
   interface: interface,
   reconstruct: string list * SMT_Translate.recon -> Proof.context ->
     (int list * thm) * Proof.context }
@@ -335,24 +242,18 @@
     handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name)
 )
 
-val no_solver = "(none)"
-
-fun set_solver_options name opts = Solvers.map (Symtab.map_entry name (fn
-  {env_var, is_remote, options, interface, reconstruct, ...} =>
-  {env_var=env_var, is_remote=is_remote, options=options,
-   more_options=String.tokens (Symbol.is_ascii_blank o str) opts,
-   interface=interface, reconstruct=reconstruct}))
-
 local
   fun finish outcome cex_parser reconstruct ocl (output, recon) ctxt =
     (case outcome output of
       (Unsat, ls) =>
-        if not (Config.get ctxt oracle) andalso is_some reconstruct
+        if not (Config.get ctxt C.oracle) andalso is_some reconstruct
         then the reconstruct ctxt recon ls
         else (([], ocl ()), ctxt)
     | (result, ls) =>
         let val ts = (case cex_parser of SOME f => f ctxt recon ls | _ => [])
-        in raise SMT (Counterexample (result = Sat, ts)) end)
+        in
+          raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat, ts))
+        end)
 in
 
 fun add_solver cfg =
@@ -363,59 +264,31 @@
     fun core_oracle () = @{cprop False}
 
     fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options,
-      more_options=[], interface=interface,
+      interface=interface,
       reconstruct=finish (outcome name) cex_parser reconstruct ocl }
   in
     Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) =>
     Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
-    Attrib.setup (Binding.name (name ^ "_options"))
-      (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
-        (Thm.declaration_attribute o K o set_solver_options name))
-      ("Additional command line options for SMT solver " ^ quote name)
+    Context.theory_map (C.add_solver name)
   end
 
 end
 
-val all_solver_names_of = Symtab.keys o Solvers.get
-val lookup_solver = Symtab.lookup o Solvers.get
-
-
-
-(* selected solver *)
-
-structure Selected_Solver = Generic_Data
-(
-  type T = string
-  val empty = no_solver
-  val extend = I
-  fun merge (s, _) = s
-)
+fun name_and_solver_of ctxt =
+  let val name = C.solver_of ctxt
+  in (name, the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)) end
 
-val solver_name_of = Selected_Solver.get
-
-fun select_solver name context =
-  if is_none (lookup_solver context name)
-  then error ("SMT solver not registered: " ^ quote name)
-  else Selected_Solver.map (K name) context
-
-fun raw_solver_of context name =
-  (case lookup_solver context name of
-    NONE => error "No SMT solver selected"
-  | SOME s => s)
-
-fun solver_of context =
-  let val name = solver_name_of context
-  in gen_solver name (raw_solver_of context name) end
+fun solver_of ctxt =
+  let val (name, raw_solver) = name_and_solver_of ctxt
+  in gen_solver name raw_solver end
 
 fun is_locally_installed ctxt =
-  let
-    val name = solver_name_of (Context.Proof ctxt)
-    val {env_var, ...} = raw_solver_of (Context.Proof ctxt) name
+  let val (_, {env_var, ...}) = name_and_solver_of ctxt
   in is_some (get_local_solver env_var) end
 
 
 
-(* SMT filter *)
+(* filter *)
 
 val has_topsort = Term.exists_type (Term.exists_subtype (fn
     TFree (_, []) => true
@@ -424,19 +297,20 @@
 
 fun smt_solver rm ctxt irules =
   (* without this test, we would run into problems when atomizing the rules: *)
-  if exists (has_topsort o Thm.prop_of o snd) irules
-  then raise SMT (Other_Failure "proof state contains the universal sort {}")
-  else solver_of (Context.Proof ctxt) rm ctxt irules
+  if exists (has_topsort o Thm.prop_of o snd) irules then
+    raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("proof state " ^
+      "contains the universal sort {}"))
+  else solver_of ctxt rm ctxt irules
 
 fun smt_filter run_remote time_limit st xrules i =
   let
     val {facts, goal, ...} = Proof.goal st
     val ctxt =
       Proof.context_of st
-      |> Config.put timeout (Real.fromInt (Time.toSeconds time_limit))
-      |> Config.put oracle false
-      |> Config.put filter_only true
-      |> Config.put keep_assms false
+      |> Config.put C.oracle false
+      |> Config.put C.timeout (Real.fromInt (Time.toSeconds time_limit))
+      |> Config.put C.drop_bad_facts true
+      |> Config.put C.filter_only_facts true
     val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
     val cprop =
       concl
@@ -450,7 +324,8 @@
     |-> map_filter o try o nth
     |> (fn xs => {outcome=NONE, used_facts=xs, run_time_in_msecs=NONE})
   end
-  handle SMT fail => {outcome=SOME fail, used_facts=[], run_time_in_msecs=NONE}
+  handle SMT_Failure.SMT fail => {outcome=SOME fail, used_facts=[],
+    run_time_in_msecs=NONE}
   (* FIXME: measure runtime *)
 
 
@@ -460,14 +335,17 @@
 fun smt_tac' pass_exns ctxt rules =
   CONVERSION (SMT_Normalize.atomize_conv ctxt)
   THEN' Tactic.rtac @{thm ccontr}
-  THEN' SUBPROOF (fn {context=cx, prems, ...} =>
+  THEN' SUBPROOF (fn {context=ctxt', prems, ...} =>
     let
-      fun solve () = snd (smt_solver NONE cx (map (pair ~1) (rules @ prems)))
-      val name = solver_name_of (Context.Proof cx)
-      val trace = trace_msg cx (prefix "SMT: " o string_of_failure cx name)
+      fun solve irules = snd (smt_solver NONE ctxt' irules)
+      val tag = "Solver " ^ C.solver_of ctxt' ^ ": "
+      val str_of = SMT_Failure.string_of_failure ctxt'
+      fun safe_solve irules =
+        if pass_exns then SOME (solve irules)
+        else (SOME (solve irules) handle SMT_Failure.SMT fail =>
+          (C.trace_msg ctxt' (prefix tag o str_of) fail; NONE))
     in
-      (if pass_exns then SOME (solve ())
-       else (SOME (solve ()) handle SMT fail => (trace fail; NONE)))
+      safe_solve (map (pair ~1) (rules @ prems))
       |> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac)
     end) ctxt
 
@@ -483,60 +361,7 @@
 (* setup *)
 
 val setup =
-  Attrib.setup @{binding smt_solver}
-    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
-      (Thm.declaration_attribute o K o select_solver))
-    "SMT solver configuration" #>
-  setup_oracle #>
-  setup_filter_only #>
-  setup_datatypes #>
-  setup_keep_assms #>
-  setup_timeout #>
-  setup_trace #>
-  setup_trace_used_facts #>
-  setup_fixed_certificates #>
-  Attrib.setup @{binding smt_certificates}
-    (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
-      (Thm.declaration_attribute o K o select_certificates))
-    "SMT certificates" #>
   Method.setup @{binding smt} smt_method
     "Applies an SMT solver to the current goal."
 
-
-fun print_setup context =
-  let
-    val t = Time.toString (seconds (Config.get_generic context timeout))
-    val names = sort_strings (all_solver_names_of context)
-    val ns = if null names then [no_solver] else names
-    val n = solver_name_of context
-    val opts =
-      (case Symtab.lookup (Solvers.get context) n of
-        NONE => []
-      | SOME {more_options, options, ...} =>
-          more_options @ options (Context.proof_of context))
-    val certs_filename =
-      (case get_certificates_path context of
-        SOME path => Path.implode path
-      | NONE => "(disabled)")
-    val fixed = if Config.get_generic context fixed_certificates then "true"
-      else "false"
-  in
-    Pretty.writeln (Pretty.big_list "SMT setup:" [
-      Pretty.str ("Current SMT solver: " ^ n),
-      Pretty.str ("Current SMT solver options: " ^ space_implode " " opts),
-      Pretty.str_list "Available SMT solvers: "  "" ns,
-      Pretty.str ("Current timeout: " ^ t ^ " seconds"),
-      Pretty.str ("With proofs: " ^
-        (if Config.get_generic context oracle then "false" else "true")),
-      Pretty.str ("Certificates cache: " ^ certs_filename),
-      Pretty.str ("Fixed certificates: " ^ fixed)])
-  end
-
-val _ =
-  Outer_Syntax.improper_command "smt_status"
-    "show the available SMT solvers and the currently selected solver"
-    Keyword.diag
-    (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
-      print_setup (Context.Proof (Toplevel.context_of state)))))
-
 end
diff -r 6354e21e61fa -r 61176a1f9cd3 src/HOL/Tools/SMT/z3_proof_parser.ML
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Sat Nov 06 10:01:00 2010 -0700
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Mon Nov 08 05:07:18 2010 -0800
@@ -240,7 +240,7 @@
 
 (* core parser *)
 
-fun parse_exn line_no msg = raise SMT_Solver.SMT (SMT_Solver.Other_Failure
+fun parse_exn line_no msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure
   ("Z3 proof parser (line " ^ string_of_int line_no ^ "): " ^ msg))
 
 fun scan_exn msg ((line_no, _), _) = parse_exn line_no msg
diff -r 6354e21e61fa -r 61176a1f9cd3 src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Sat Nov 06 10:01:00 2010 -0700
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Nov 08 05:07:18 2010 -0800
@@ -19,7 +19,7 @@
 structure T = Z3_Proof_Tools
 structure L = Z3_Proof_Literals
 
-fun z3_exn msg = raise SMT_Solver.SMT (SMT_Solver.Other_Failure
+fun z3_exn msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure
   ("Z3 proof reconstruction: " ^ msg))
 
 
@@ -66,11 +66,11 @@
 (** proof tools **)
 
 fun named ctxt name prover ct =
-  let val _ = SMT_Solver.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
+  let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
   in prover ct end
 
 fun NAMED ctxt name tac i st =
-  let val _ = SMT_Solver.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
+  let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
   in tac i st end
 
 fun pretty_goal ctxt thms t =
@@ -90,7 +90,7 @@
     fun apply [] ct = error (try_apply_err ct)
       | apply (prover :: provers) ct =
           (case try prover ct of
-            SOME thm => (SMT_Solver.trace_msg ctxt I "Z3: succeeded"; thm)
+            SOME thm => (SMT_Config.trace_msg ctxt I "Z3: succeeded"; thm)
           | NONE => apply provers ct)
 
   in apply o cons (named ctxt "schematic rules" (by_schematic_rule ctxt)) end
@@ -732,9 +732,9 @@
 in
 fun trace_rule idx prove r ps ct (cxp as (ctxt, ptab)) =
   let
-    val _ = SMT_Solver.trace_msg ctxt (header idx r o count_rules) ptab
+    val _ = SMT_Config.trace_msg ctxt (header idx r o count_rules) ptab
     val result as (p, (ctxt', _)) = prove r ps ct cxp
-    val _ = if not (Config.get ctxt' SMT_Solver.trace) then ()
+    val _ = if not (Config.get ctxt' SMT_Config.trace) then ()
       else check ctxt' idx r ps ct p
   in result end
 end
@@ -844,7 +844,7 @@
     val (idx, (ptab, vars, cx)) = P.parse ctxt typs terms output
     val assms' = prepare_assms cx unfolds assms
   in
-    if Config.get cx SMT_Solver.filter_only
+    if Config.get cx SMT_Config.filter_only_facts
     then ((filter_assms cx assms' ptab idx [], @{thm TrueI}), cx)
     else apfst (pair []) (prove cx assms' vars idx ptab)
   end
diff -r 6354e21e61fa -r 61176a1f9cd3 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sat Nov 06 10:01:00 2010 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 08 05:07:18 2010 -0800
@@ -104,7 +104,7 @@
     else is_atp_installed thy name
   end
 
-val smt_default_max_relevant = 300 (* FUDGE (FIXME) *)
+val smt_default_max_relevant = 200 (* FUDGE *)
 val auto_max_relevant_divisor = 2 (* FUDGE *)
 
 fun default_max_relevant_for_prover thy name =
@@ -409,38 +409,53 @@
      run_time_in_msecs = msecs}
   end
 
-fun failure_from_smt_failure (SMT_Solver.Counterexample _) = Unprovable
-  | failure_from_smt_failure SMT_Solver.Time_Out = TimedOut
-  | failure_from_smt_failure SMT_Solver.Out_Of_Memory = OutOfResources
+fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable
+  | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
+  | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
   | failure_from_smt_failure _ = UnknownError
 
-val smt_filter_max_iter = 5
-val smt_filter_fact_divisor = 2
+val smt_max_iter = 5
+val smt_iter_fact_divisor = 2
+val smt_iter_min_msecs = 5000
+val smt_iter_timeout_divisor = 2
 
-fun smt_filter_loop iter msecs_so_far remote timeout state facts i =
+fun smt_filter_loop iter outcome0 msecs_so_far remote timeout state facts i =
   let
     val timer = Timer.startRealTimer ()
+    val ms = timeout |> Time.toMilliseconds
+    val iter_timeout =
+      if iter < smt_max_iter then
+        Int.min (ms, Int.max (smt_iter_min_msecs,
+                              ms div smt_iter_timeout_divisor))
+        |> Time.fromMilliseconds
+      else
+        timeout
     val {outcome, used_facts, run_time_in_msecs} =
-      SMT_Solver.smt_filter remote timeout state facts i
+      TimeLimit.timeLimit iter_timeout
+          (SMT_Solver.smt_filter remote iter_timeout state facts) i
+      handle TimeLimit.TimeOut =>
+             {outcome = SOME SMT_Failure.Time_Out, used_facts = [],
+              run_time_in_msecs = NONE}
+    val outcome0 = if is_none outcome0 then SOME outcome else outcome0
     val msecs_so_far = int_opt_add run_time_in_msecs msecs_so_far
     val too_many_facts_perhaps =
       case outcome of
         NONE => false
-      | SOME (SMT_Solver.Counterexample _) => false
-      | SOME SMT_Solver.Time_Out => false
-      | SOME SMT_Solver.Out_Of_Memory => true
+      | SOME (SMT_Failure.Counterexample _) => false
+      | SOME SMT_Failure.Time_Out => iter_timeout <> timeout
+      | SOME SMT_Failure.Out_Of_Memory => true
       | SOME _ => true
+    val timeout = Time.- (timeout, Timer.checkRealTimer timer)
   in
-    if too_many_facts_perhaps andalso iter < smt_filter_max_iter andalso
-       not (null facts) then
-      let val facts = take (length facts div smt_filter_fact_divisor) facts in
-        smt_filter_loop (iter + 1) msecs_so_far remote
-                        (Time.- (timeout, Timer.checkRealTimer timer)) state
+    if too_many_facts_perhaps andalso iter < smt_max_iter andalso
+       not (null facts) andalso timeout > Time.zeroTime then
+      let val facts = take (length facts div smt_iter_fact_divisor) facts in
+        smt_filter_loop (iter + 1) outcome0 msecs_so_far remote timeout state
                         facts i
       end
     else
-      {outcome = outcome, used_facts = used_facts,
-       run_time_in_msecs = msecs_so_far}
+      {outcome = if is_none outcome then NONE else the outcome0,
+       used_facts = used_facts, run_time_in_msecs = msecs_so_far}
   end
 
 fun run_smt_solver auto remote ({timeout, ...} : params) minimize_command
@@ -449,7 +464,7 @@
   let
     val ctxt = Proof.context_of state
     val {outcome, used_facts, run_time_in_msecs} =
-      smt_filter_loop 1 (SOME 0) remote timeout state
+      smt_filter_loop 1 NONE (SOME 0) remote timeout state
                       (map_filter (try dest_Untranslated) facts) subgoal
     val message =
       case outcome of
@@ -458,10 +473,10 @@
                          (apply_on_subgoal subgoal subgoal_count ^
                           command_call smtN (map fst used_facts)) ^
         minimize_line minimize_command (map fst used_facts)
-      | SOME SMT_Solver.Time_Out => "Timed out."
-      | SOME (SMT_Solver.Counterexample _) => "The SMT problem is unprovable."
+      | SOME SMT_Failure.Time_Out => "Timed out."
+      | SOME (SMT_Failure.Counterexample _) => "The SMT problem is unprovable."
       | SOME failure =>
-        SMT_Solver.string_of_failure ctxt "The SMT solver" failure
+        SMT_Failure.string_of_failure ctxt failure
     val outcome = outcome |> Option.map failure_from_smt_failure (* FIXME *)
   in
     {outcome = outcome, used_facts = used_facts,
diff -r 6354e21e61fa -r 61176a1f9cd3 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat Nov 06 10:01:00 2010 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Nov 08 05:07:18 2010 -0800
@@ -369,13 +369,16 @@
   | locality_bonus {assum_bonus, ...} Assum = assum_bonus
   | locality_bonus {chained_bonus, ...} Chained = chained_bonus
 
+fun is_odd_const_name s =
+  s = abs_name orelse String.isPrefix skolem_prefix s orelse
+  String.isSuffix theory_const_suffix s
+
 fun fact_weight fudge loc const_tab relevant_consts fact_consts =
   case fact_consts |> List.partition (pconst_hyper_mem I relevant_consts)
                    ||> filter_out (pconst_hyper_mem swap relevant_consts) of
     ([], _) => 0.0
   | (rel, irrel) =>
-    if forall (forall (String.isSuffix theory_const_suffix o fst))
-              [rel, irrel] then
+    if forall (forall (is_odd_const_name o fst)) [rel, irrel] then
       0.0
     else
       let
diff -r 6354e21e61fa -r 61176a1f9cd3 src/HOL/Tools/smallvalue_generators.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/smallvalue_generators.ML	Mon Nov 08 05:07:18 2010 -0800
@@ -0,0 +1,249 @@
+(*  Title:      HOL/Tools/smallvalue_generators.ML
+    Author:     Lukas Bulwahn, TU Muenchen
+
+Generators for small values for various types.
+*)
+
+signature SMALLVALUE_GENERATORS =
+sig
+  val ensure_smallvalue_datatype: Datatype.config -> string list -> theory -> theory
+  val compile_generator_expr:
+    Proof.context -> term -> int -> term list option * (bool list * bool)
+  val put_counterexample: (unit -> int -> term list option)
+    -> Proof.context -> Proof.context
+  val setup: theory -> theory
+end;
+
+structure Smallvalue_Generators : SMALLVALUE_GENERATORS =
+struct
+
+(** general term functions **)
+
+fun dest_funT (Type ("fun",[S, T])) = (S, T)
+  | dest_funT T = raise TYPE ("dest_funT", [T], [])
+ 
+fun mk_fun_comp (t, u) =
+  let
+    val (_, B) = dest_funT (fastype_of t)
+    val (C, A) = dest_funT (fastype_of u)
+  in
+    Const(@{const_name "Fun.comp"}, (A --> B) --> (C --> A) --> C --> B) $ t $ u
+  end;
+
+fun mk_measure f =
+  let
+    val Type ("fun", [T, @{typ nat}]) = fastype_of f 
+  in
+    Const (@{const_name Wellfounded.measure},
+      (T --> @{typ nat}) --> HOLogic.mk_prodT (T, T) --> @{typ bool})
+    $ f
+  end
+
+fun mk_sumcases rT f (Type (@{type_name Sum_Type.sum}, [TL, TR])) =
+  let
+    val lt = mk_sumcases rT f TL
+    val rt = mk_sumcases rT f TR
+  in
+    SumTree.mk_sumcase TL TR rT lt rt
+  end
+  | mk_sumcases _ f T = f T
+
+
+(** abstract syntax **)
+
+val size = @{term "i :: code_numeral"}
+val size_pred = @{term "(i :: code_numeral) - 1"}
+val size_ge_zero = @{term "(i :: code_numeral) > 0"}
+fun test_function T = Free ("f", T --> @{typ "term list option"})
+
+fun mk_none_continuation (x, y) =
+  let
+    val (T as Type(@{type_name "option"}, [T'])) = fastype_of x
+  in
+    Const (@{const_name Option.option_case}, T --> (T' --> T) --> T --> T)
+      $ y $ Const (@{const_name Some}, T' --> T) $ x
+  end
+
+(** datatypes **)
+
+(* constructing smallvalue generator instances on datatypes *)
+
+exception FUNCTION_TYPE;
+
+val smallN = "small";
+
+fun smallT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ code_numeral}
+  --> @{typ "Code_Evaluation.term list option"}
+
+fun mk_equations thy descr vs tycos (names, auxnames) (Ts, Us) =
+  let
+    val smallsN = map (prefix (smallN ^ "_")) (names @ auxnames);
+    val smalls = map2 (fn name => fn T => Free (name, smallT T))
+      smallsN (Ts @ Us)
+    fun mk_small_call T =
+      let
+        val small = Const (@{const_name "Smallcheck.small_class.small"}, smallT T)        
+      in
+        (T, (fn t => small $ absdummy (T, t) $ size_pred))
+      end
+    fun mk_small_aux_call fTs (k, _) (tyco, Ts) =
+      let
+        val T = Type (tyco, Ts)
+        val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
+        val small = nth smalls k
+      in
+        (T, (fn t => small $ absdummy (T, t) $ size_pred))
+      end
+    fun mk_consexpr simpleT (c, xs) =
+      let
+        val (Ts, fns) = split_list xs
+        val constr = Const (c, Ts ---> simpleT)
+        val bounds = map Bound (((length xs) - 1) downto 0)
+        val start_term = test_function simpleT $ (list_comb (constr, bounds))
+      in fold_rev (fn f => fn t => f t) fns start_term end
+    fun mk_rhs exprs =
+        @{term "If :: bool => term list option => term list option => term list option"}
+            $ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"}
+    val rhss =
+      Datatype_Aux.interpret_construction descr vs
+        { atyp = mk_small_call, dtyp = mk_small_aux_call }
+      |> (map o apfst) Type
+      |> map (fn (T, cs) => map (mk_consexpr T) cs)
+      |> map mk_rhs
+    val lhss = map2 (fn t => fn T => t $ test_function T $ size) smalls (Ts @ Us);
+    val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
+  in
+    (Ts @ Us ~~ (smallsN ~~ eqs))
+  end
+    
+val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
+
+fun gen_inst_state_tac ctxt rel st =
+  case Term.add_vars (prop_of st) [] of
+    [v as (_, T)] =>
+      let
+        val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
+        val rel' = cert rel
+        val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st (*FIXME??*)
+      in        
+        PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st'
+      end
+  | _ => Seq.empty;
+
+fun instantiate_smallvalue_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
+  let
+    val _ = Datatype_Aux.message config "Creating smallvalue generators ...";
+    val eqs = mk_equations thy descr vs tycos (names, auxnames) (Ts, Us)
+    fun my_relation_tac ctxt st =
+      let
+        val ((_ $ (_ $ rel)) :: tl) = prems_of st
+        val domT = (HOLogic.dest_setT (fastype_of rel))
+        fun mk_single_measure T = mk_fun_comp (@{term "Code_Numeral.nat_of"},
+            Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
+        val measure = mk_measure (mk_sumcases @{typ nat} mk_single_measure domT)
+      in
+        (Function_Common.apply_termination_rule ctxt 1
+        THEN gen_inst_state_tac ctxt measure) st
+      end
+    fun termination_tac ctxt = 
+      my_relation_tac ctxt
+      THEN rtac @{thm wf_measure} 1
+      THEN (REPEAT_DETERM (Simplifier.asm_full_simp_tac 
+        (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
+         @{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
+    fun pat_completeness_auto ctxt =
+      Pat_Completeness.pat_completeness_tac ctxt 1
+      THEN auto_tac (clasimpset_of ctxt)
+  in
+    thy
+    |> Class.instantiation (tycos, vs, @{sort small})
+    |> Function.add_function
+      (map (fn (T, (name, _)) =>
+          Syntax.no_syn (Binding.conceal (Binding.name name), SOME (smallT T))) eqs)
+        (map (pair (apfst Binding.conceal Attrib.empty_binding) o snd o snd) eqs)
+        Function_Common.default_config pat_completeness_auto
+    |> snd
+    |> Local_Theory.restore
+    |> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
+    |> snd
+    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
+  end;
+
+fun ensure_smallvalue_datatype config raw_tycos thy =
+  let
+    val algebra = Sign.classes_of thy;
+    val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =
+      Datatype.the_descr thy raw_tycos;
+    val typerep_vs = (map o apsnd)
+      (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
+    val smallvalue_insts = (map (rpair @{sort small}) o flat o maps snd o maps snd)
+      (Datatype_Aux.interpret_construction descr typerep_vs
+        { atyp = single, dtyp = (K o K o K) [] });
+    (*val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd)
+      (Datatype_Aux.interpret_construction descr typerep_vs
+        { atyp = K [], dtyp = K o K });*)
+    val has_inst = exists (fn tyco =>
+      can (Sorts.mg_domain algebra tyco) @{sort small}) tycos;
+  in if has_inst then thy
+    else case Quickcheck_Generators.perhaps_constrain thy smallvalue_insts typerep_vs
+     of SOME constrain => (instantiate_smallvalue_datatype config descr
+          (map constrain typerep_vs) tycos prfx (names, auxnames)
+            ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
+            handle FUNCTION_TYPE =>
+              (Datatype_Aux.message config
+                "Creation of smallvalue generators failed because the datatype contains a function type";
+              thy))
+      | NONE => thy
+  end;
+
+(** building and compiling generator expressions **)
+
+structure Counterexample = Proof_Data (
+  type T = unit -> int -> term list option
+  fun init _ () = error "Counterexample"
+);
+val put_counterexample = Counterexample.put;
+
+val target = "Quickcheck";
+
+fun mk_generator_expr thy prop Ts =
+  let
+    val bound_max = length Ts - 1;
+    val bounds = map Bound (bound_max downto 0)
+    val result = list_comb (prop, bounds);
+    val terms = HOLogic.mk_list @{typ term} (map2 HOLogic.mk_term_of Ts bounds);
+    val check =
+      @{term "Smallcheck.catch_match :: term list option => term list option => term list option"} $
+        (@{term "If :: bool => term list option => term list option => term list option"}
+        $ result $ @{term "None :: term list option"}
+        $ (@{term "Some :: term list => term list option"} $ terms))
+      $ @{term "None :: term list option"};
+    fun mk_small_closure (depth, T) t =
+      Const (@{const_name "Smallcheck.small_class.small"}, smallT T)
+        $ absdummy (T, t) $ depth
+  in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure (rev bounds ~~ Ts) check) end
+
+fun compile_generator_expr ctxt t =
+  let
+    val Ts = (map snd o fst o strip_abs) t;
+    val thy = ProofContext.theory_of ctxt
+  in if Quickcheck.report ctxt then
+    error "Compilation with reporting facility is not supported"
+  else
+    let
+      val t' = mk_generator_expr thy t Ts;
+      val compile = Code_Runtime.dynamic_value_strict
+        (Counterexample.get, put_counterexample, "Smallvalue_Generators.put_counterexample")
+        thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
+      val dummy_report = ([], false)
+    in compile #> rpair dummy_report end
+  end;
+
+(** setup **)
+
+val setup =
+  Datatype.interpretation ensure_smallvalue_datatype
+  #> Context.theory_map
+    (Quickcheck.add_generator ("small", compile_generator_expr));
+
+end;
diff -r 6354e21e61fa -r 61176a1f9cd3 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Sat Nov 06 10:01:00 2010 -0700
+++ b/src/Tools/Code/code_runtime.ML	Mon Nov 08 05:07:18 2010 -0800
@@ -25,8 +25,8 @@
     -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a Exn.result
   val dynamic_holds_conv: conv
   val static_holds_conv: theory -> string list -> conv
-  val code_reflect: (string * string list) list -> string list -> string -> string option
-    -> theory -> theory
+  val code_reflect: (string * string list option) list -> string list -> string
+    -> string option -> theory -> theory
   datatype truth = Holds
   val put_truth: (unit -> truth) -> Proof.context -> Proof.context
   val trace: bool Unsynchronized.ref
@@ -213,8 +213,8 @@
 structure Code_Antiq_Data = Proof_Data
 (
   type T = (string list * string list) * (bool
-    * (string * ((string * string) list * (string * string) list)) lazy);
-  fun init _ = (([], []), (true, (Lazy.value ("", ([], [])))));
+    * (string * (string * string) list) lazy);
+  fun init _ = (([], []), (true, (Lazy.value ("", []))));
 );
 
 val is_first_occ = fst o snd o Code_Antiq_Data.get;
@@ -225,24 +225,22 @@
     val tycos' = fold (insert (op =)) new_tycos tycos;
     val consts' = fold (insert (op =)) new_consts consts;
     val acc_code = Lazy.lazy (fn () =>
-      evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts');
+      evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts'
+      |> apsnd snd);
   in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end;
 
 fun register_const const = register_code [] [const];
 
-fun register_datatype tyco constrs = register_code [tyco] constrs;
-
-fun print_const const all_struct_name tycos_map consts_map =
+fun print_const const all_struct_name consts_map =
   (Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const;
 
-fun print_code is_first print_it ctxt =
+fun print_code is_first const ctxt =
   let
     val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt;
-    val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
-    val ml_code = if is_first then ml_code
-      else "";
+    val (ml_code, consts_map) = Lazy.force acc_code;
+    val ml_code = if is_first then ml_code else "";
     val all_struct_name = "Isabelle";
-  in (ml_code, print_it all_struct_name tycos_map consts_map) end;
+  in (ml_code, print_const const all_struct_name consts_map) end;
 
 in
 
@@ -251,33 +249,38 @@
     val const = Code.check_const (ProofContext.theory_of background) raw_const;
     val is_first = is_first_occ background;
     val background' = register_const const background;
-  in (print_code is_first (print_const const), background') end;
+  in (print_code is_first const, background') end;
 
 end; (*local*)
 
 
 (* reflection support *)
 
-fun check_datatype thy tyco consts =
+fun check_datatype thy tyco some_consts =
   let
     val constrs = (map (fst o fst) o snd o Code.get_type thy) tyco;
-    val missing_constrs = subtract (op =) consts constrs;
-    val _ = if null missing_constrs then []
-      else error ("Missing constructor(s) " ^ commas (map quote missing_constrs)
-        ^ " for datatype " ^ quote tyco);
-    val false_constrs = subtract (op =) constrs consts;
-    val _ = if null false_constrs then []
-      else error ("Non-constructor(s) " ^ commas (map quote false_constrs)
-        ^ " for datatype " ^ quote tyco);
-  in () end;
+    val _ = case some_consts
+     of SOME consts =>
+          let
+            val missing_constrs = subtract (op =) consts constrs;
+            val _ = if null missing_constrs then []
+              else error ("Missing constructor(s) " ^ commas (map quote missing_constrs)
+                ^ " for datatype " ^ quote tyco);
+            val false_constrs = subtract (op =) constrs consts;
+            val _ = if null false_constrs then []
+              else error ("Non-constructor(s) " ^ commas (map quote false_constrs)
+                ^ " for datatype " ^ quote tyco)
+          in () end
+      | NONE => ();
+  in (tyco, constrs) end;
 
 fun add_eval_tyco (tyco, tyco') thy =
   let
     val k = Sign.arity_number thy tyco;
-    fun pr pr' fxy [] = tyco'
-      | pr pr' fxy [ty] =
+    fun pr pr' _ [] = tyco'
+      | pr pr' _ [ty] =
           Code_Printer.concat [pr' Code_Printer.BR ty, tyco']
-      | pr pr' fxy tys =
+      | pr pr' _ tys =
           Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
   in
     thy
@@ -317,10 +320,9 @@
 fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy  =
   let
     val datatypes = map (fn (raw_tyco, raw_cos) =>
-      (prep_type thy raw_tyco, map (prep_const thy) raw_cos)) raw_datatypes;
-    val _ = map (uncurry (check_datatype thy)) datatypes;
-    val tycos = map fst datatypes;
-    val constrs = maps snd datatypes;
+      (prep_type thy raw_tyco, (Option.map o map) (prep_const thy) raw_cos)) raw_datatypes;
+    val (tycos, constrs) = map_split (uncurry (check_datatype thy)) datatypes
+      |> apsnd flat;
     val functions = map (prep_const thy) raw_functions;
     val result = evaluation_code thy module_name tycos (constrs @ functions)
       |> (apsnd o apsnd) (chop (length constrs));
@@ -347,7 +349,8 @@
 val _ = List.app Keyword.keyword [datatypesK, functionsK];
 
 val parse_datatype =
-  Parse.name --| Parse.$$$ "=" -- (Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term)));
+  Parse.name --| Parse.$$$ "=" -- ((Parse.string >> (fn "*" => NONE | _ => Scan.fail ()))
+    || ((Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term))) >> SOME));
 
 in
 
diff -r 6354e21e61fa -r 61176a1f9cd3 src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Sat Nov 06 10:01:00 2010 -0700
+++ b/src/Tools/cache_io.ML	Mon Nov 08 05:07:18 2010 -0800
@@ -6,10 +6,13 @@
 
 signature CACHE_IO =
 sig
+  (*IO wrapper*)
   val with_tmp_file: string -> (Path.T -> 'a) -> 'a
   val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
-  val run: (Path.T -> Path.T -> string) -> string -> string list * string list
+  val run: (Path.T -> Path.T -> string) -> string ->
+    {output: string list, redirected_output: string list, return_code: int}
 
+  (*cache*)
   type cache
   val make: Path.T -> cache
   val cache_path_of: cache -> Path.T
@@ -23,6 +26,8 @@
 structure Cache_IO : CACHE_IO =
 struct
 
+(* IO wrapper *)
+
 val cache_io_prefix = "cache-io-"
 
 fun with_tmp_file name f =
@@ -45,21 +50,20 @@
   with_tmp_file cache_io_prefix (fn out_path =>
     let
       val _ = File.write in_path str
-      val (out2, _) = bash_output (make_cmd in_path out_path)
+      val (out2, rc) = bash_output (make_cmd in_path out_path)
       val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
-    in (out1, split_lines out2) end))
+    in {output=split_lines out2, redirected_output=out1, return_code=rc} end))
 
 
+(* cache *)
 
 abstype cache = Cache of {
   path: Path.T,
   table: (int * (int * int * int) Symtab.table) Synchronized.var }
 with
 
-
 fun cache_path_of (Cache {path, ...}) = path
 
-
 fun load cache_path =
   let
     fun err () = error ("Cache IO: corrupted cache file: " ^
@@ -87,7 +91,6 @@
   let val table = if File.exists path then load path else (1, Symtab.empty)
   in Cache {path=path, table=Synchronized.var (Path.implode path) table} end
 
-
 fun load_cached_result cache_path (p, len1, len2) =
   let
     fun load line (i, xsp) =
@@ -97,7 +100,6 @@
       else (i, xsp)
   in pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) end
 
-
 fun lookup (Cache {path=cache_path, table}) str =
   let val key = SHA1.digest str
   in
@@ -106,10 +108,10 @@
     | SOME pos => (SOME (load_cached_result cache_path pos), key))
   end
 
-
 fun run_and_cache (Cache {path=cache_path, table}) key make_cmd str =
   let
-    val res as (out, err) = run make_cmd str
+    val {output=err, redirected_output=out, ...} = run make_cmd str
+    val res = (out, err)
     val (l1, l2) = pairself length res
     val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
     val lines = map (suffix "\n") (header :: out @ err)
@@ -121,11 +123,11 @@
         in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
   in res end
 
-
 fun run_cached cache make_cmd str =
   (case lookup cache str of
     (NONE, key) => run_and_cache cache key make_cmd str
   | (SOME output, _) => output)
 
 end
+
 end