# HG changeset patch
# User blanchet
# Date 1291631121 -3600
# Node ID 67f436af06389d77df61e1553bf46a4905718251
# Parent  3ea3124b0a2b590f6a79f5e5bcd414b1fe5368c3
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?

diff -r 3ea3124b0a2b -r 67f436af0638 src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Mon Dec 06 10:32:39 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Mon Dec 06 11:25:21 2010 +0100
@@ -19,7 +19,7 @@
   else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^
     quote solver_name ^ " failed. Enable SMT tracing by setting the " ^
     "configuration option " ^ quote SMT_Config.traceN ^ " and " ^
-    " see the trace for details."))
+    "see the trace for details."))
 
 fun on_first_line test_outcome solver_name lines =
   let
@@ -40,7 +40,8 @@
   outcome =
     on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
   cex_parser = NONE,
-  reconstruct = NONE }
+  reconstruct = NONE,
+  default_max_relevant = 250 }
 
 
 (* Yices *)
@@ -53,7 +54,8 @@
   interface = SMTLIB_Interface.interface,
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
   cex_parser = NONE,
-  reconstruct = NONE }
+  reconstruct = NONE,
+  default_max_relevant = 275 }
 
 
 (* Z3 *)
@@ -85,7 +87,8 @@
   interface = Z3_Interface.interface,
   outcome = z3_on_last_line,
   cex_parser = SOME Z3_Model.parse_counterex,
-  reconstruct = SOME Z3_Proof_Reconstruction.reconstruct }
+  reconstruct = SOME Z3_Proof_Reconstruction.reconstruct,
+  default_max_relevant = 225 }
 
 
 (* overall setup *)
diff -r 3ea3124b0a2b -r 67f436af0638 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Mon Dec 06 10:32:39 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon Dec 06 11:25:21 2010 +0100
@@ -21,7 +21,8 @@
     cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
       term list * term list) option,
     reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
-      (int list * thm) * Proof.context) option }
+      (int list * thm) * Proof.context) option,
+    default_max_relevant: int }
 
   (*registry*)
   type solver = bool option -> Proof.context -> (int * thm) list ->
@@ -32,6 +33,7 @@
   val available_solvers_of: Proof.context -> string list
   val is_locally_installed: Proof.context -> string -> bool
   val is_remotely_available: Proof.context -> string -> bool
+  val default_max_relevant: Proof.context -> string -> int
 
   (*filter*)
   val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int ->
@@ -70,7 +72,8 @@
   cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
     term list * term list) option,
   reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
-    (int list * thm) * Proof.context) option }
+    (int list * thm) * Proof.context) option,
+  default_max_relevant: int }
 
 
 (* interface to external solvers *)
@@ -215,7 +218,7 @@
 
 fun gen_solver name info rm ctxt irules =
   let
-    val {env_var, is_remote, 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 C.datatypes) translate
@@ -244,7 +247,8 @@
   options: Proof.context -> string list,
   interface: interface,
   reconstruct: string list * SMT_Translate.recon -> Proof.context ->
-    (int list * thm) * Proof.context }
+    (int list * thm) * Proof.context,
+  default_max_relevant: int }
 
 structure Solvers = Generic_Data
 (
@@ -279,13 +283,14 @@
 fun add_solver cfg =
   let
     val {name, env_var, is_remote, options, interface, outcome, cex_parser,
-      reconstruct} = cfg
+      reconstruct, default_max_relevant} = cfg
 
     fun core_oracle () = cfalse
 
     fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options,
       interface=interface,
-      reconstruct=finish (outcome name) cex_parser reconstruct ocl }
+      reconstruct=finish (outcome name) cex_parser reconstruct ocl,
+      default_max_relevant=default_max_relevant }
   in
     Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) =>
     Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
@@ -294,9 +299,12 @@
 
 end
 
+fun get_info ctxt name =
+  the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)
+
 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
+  in (name, get_info ctxt name) end
 
 val solver_name_of = fst o name_and_solver_of
 fun solver_of ctxt =
@@ -306,11 +314,12 @@
 val available_solvers_of = Symtab.keys o Solvers.get o Context.Proof
 
 fun is_locally_installed ctxt name =
-  let val {env_var, ...} = the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)
+  let val {env_var, ...} = get_info ctxt name
   in is_some (get_local_solver env_var) end
 
-fun is_remotely_available ctxt name =
-  #is_remote (the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name))
+val is_remotely_available = #is_remote oo get_info
+
+val default_max_relevant = #default_max_relevant oo get_info
 
 
 (* filter *)